Toffoli gate from single-qubit and two-qubit gates

Proved

SuperconductingQC.toffoli_mem_closure_singleQubit_CNOT

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

quantum-computingquantum-gates

On three qubits, the Toffoli (CCNOT) gate $|a,b,c\rangle\mapsto|a,b,c\oplus ab\rangle$ lies in the subgroup of $U(8)$ generated by single-qubit gates and CNOTs:

\mathrm{Toffoli}\in\big\langle\,\mathcal S_3\cup\mathcal G_3(\mathrm{CNOT})\,\big\rangle .

That is, the three-qubit Toffoli gate is an exact finite product of single- and two-qubit gates, as used in its experimental realisation on three superconducting transmon qubits.

Preamble

import Mathlib
import Definitions.Def_SuperconductingQC_Gates

open scoped Matrix Kronecker

Formal statement

namespace SuperconductingQC

theorem toffoli_mem_closure_singleQubit_CNOT :
    ∃ W ∈ Subgroup.closure (singleQubitGates 3 ∪ twoQubitGateInstances 3 CNOT),
      (W : Matrix (Fin 3 → Fin 2) (Fin 3 → Fin 2) ℂ) = toffoli := by
  sorry

end SuperconductingQC

Source

Wikipedia, "Superconducting quantum computing" (PDF snapshot supplied by the mission author, retrieved 2026-10-13), https://en.wikipedia.org/wiki/Superconducting_quantum_computing; section 'Quantum gates', figure caption: 'A three qubit Toffoli gate (CCNOT) is implemented using a combination of single and two-qubit gates' (article ref. [23]); Nielsen & Chuang Fig. 4.9

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph