Generators and relations for n-qubit Clifford operators, in Lean

A formalization of the main result of P. Selinger, "Generators and relations for n-qubit Clifford operators", Logical Methods in Computer Science 11(2:10), 2015 (doi:10.2168/LMCS-11(2:10)2015, arXiv:1310.6813): the relations C1–C15 of Figure 8 are sound and complete for n-qubit Clifford circuits (Proposition 7.1).

The files are listed in order of dependency: each file only imports earlier ones (Clifford.lean imports all of them).

(a) Background

File Contents
PRO/Basic.lean PROs (strict monoidal categories whose objects are the natural numbers) and their laws, including the spatial law for scalars.
PRO/Free.lean The free PRO on a signature, presentations by relations (Γ ⊢ t = u), interpretations of terms (⟦t⟧ρ), and soundness of interpretations.
PRO/Matrix.lean The PRO of matrices indexed by bit vectors, with the Kronecker product as tensor.
PRO/Subst.lean Substituting terms for generators; it preserves provable equations.

(b) Statement of the result

File Contents
Statement.lean Generators ω, H, S, CZ, the relations C1–C15, the interpretation as complex matrices (ω = e^{iπ/4}), and MainTheorem (soundness and completeness).

This file depends only on the background in (a).

(c) Proofs

File Contents Paper
Soundness.lean Soundness: C1–C15 hold as matrix equations, decided over the Gaussian integers.
Word.lean Circuits as words of gates on adjacent wires; every circuit is equal to the circuit of its word; gates on disjoint wires commute.
Rule.lean Rules (provable equations between words), applied at an offset and up to commuting gates; inverse words.
AxiomRules.lean C1–C15 as rules, and the properties of the supplement that are relations; every gate is invertible.
Reduce.lean Sorting commuting gates and deleting full powers HH, SSSS, CZ CZ, ω⁸; applying a rule up to these reductions.
Derivations/Lemmas.lean The properties (1)–(21), with the proofs of the supplement, step by step; some of them followed by their upside-down versions (names ending in m). Supplement, Secs. 1, 2
Derivations/Equations1.lean … Equations10.lean The equations 3.1–3.101 (3.1–3.10, 3.11–3.20, …, 3.91–3.101), with the proofs of the supplement, step by step. They use only the properties (1)–(21), not each other. Supplement, Sec. 3
NormalForm/Basic.lean Derived generators, dirty gates, labelled wires (Bundle), normal forms as circuits of clean gates between labelled wires. Defs. 4.2, 4.3, 6.1
NormalForm/Lemmas.lean, NormalForm/Step.lean Absorbing one dirty gate: by a rewrite rule, or by moving it past a clean gate on other wires. Lemma 6.2
NormalForm/Cases.lean Every admissible dirty gate is absorbed: the case distinction over the rewrite rules 3.3–3.101. Lemma 6.2, Figs. 3–7
NormalForm/Exists.lean The normal form of the identity; every circuit is equal to a normal form. Prop. 6.3
Uniqueness/Pauli.lean Pauli operators and the action of gates on them by conjugation. Sec. 3
Uniqueness/Local.lean, Uniqueness/Facts.lean The action of the derived generators on the Pauli operators on their wires. Fig. 2
Uniqueness/ZX.lean Uniqueness of Z-normal and X-normal circuits; X-normal circuits take Z ⊗ I ⊗ ⋯ to I ⊗ ⋯ ⊗ Z. Lemmas 5.1, 5.2, 5.4
Uniqueness/Unique.lean Normal forms with the same action on Pauli operators are equal. Prop. 5.5
Uniqueness/Conj.lean, Uniqueness/Matrix.lean Circuits with equal matrices act equally on Pauli operators. Sec. 3
Completeness.lean Completeness of C1–C15. Prop. 7.1

(d) The final witness

File Contents
Main.lean theorem mainTheorem : MainTheorem.

It depends only on the standard axioms propext, Classical.choice, and Quot.sound; Main.lean prints them (#print axioms) when it is checked.

Generated files

Derivations/Lemmas.lean, Equations1.lean … Equations10.lean (by scripts/emit.py) and NormalForm/Cases.lean (by scripts/nfcases.py) are generated by Python scripts. They read the relations and the derivations of the supplement from the data file data/clifford.json, which contains all circuits of the paper and its supplement in machine-readable form (its conventions are described in the file).

Checking the proofs

You need an internet connection, about 8 GB of disk space (mostly for Mathlib), and the programs git and curl. The versions of Lean and Mathlib are fixed by the files lean-toolchain and lake-manifest.json; the commands below install exactly these versions.

  1. Install elan, the installer of Lean (Linux and macOS; for Windows, see https://lean-lang.org/install/):

    curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

    Answer the question with 1 (proceed with the default installation), then make the commands lean and lake available in the current shell:

    source $HOME/.elan/env

  2. Go to the directory containing this file, and download Mathlib, already compiled (this takes a few minutes):

    lake exe cache get

  3. Check all proofs (this takes about 5 to 20 minutes, depending on the computer):

    lake build

    The output ends with

    info: Clifford/Main.lean:17:0: 'Clifford.mainTheorem' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [2231/2232] Built Clifford (2.1s)
Build completed successfully (2232 jobs).

    This certifies that the theorem is proved, using only the standard axioms.

The Python scripts

The Python scripts in scripts/ are included for reference only. They are not needed for checking the proofs, and they need not be trusted: Lean checks every proof, whichever program wrote it. What a reader has to check is only that the statement in (b) says what the paper says. To regenerate the generated files, run python3 scripts/emit.py and python3 scripts/nfcases.py (Python 3, no other packages); they read data/clifford.json and write only the generated files listed above.

License

Copyright (c) 2026 Peter Selinger.

The files in this directory (the Lean files, the Python scripts, and the data file) are released under the MIT license; see the file LICENSE. They are provided "as is", without warranty of any kind.