QCLib

The aim of this library is to provide a framework for reasoning about quantum gates and quantum circuits.

It is very much in an "alpha" stage of development.

Quick tour

• QCLib/Mathlib

This directory contains results that are of sufficient generality that they might be of interest to Mathlib. (There is no implication that the results are already sufficiently polished to be upstreamed).

• QCLib/Mathlib/PiOuterProduct.lean QCLib/Mathlib/UnitaryGroup/PiKronecker.lean

The files define tensor products of indexed families of concrete vectors (i.e. functions into a CommMonoid) and of (unitary) matrices. Most of the rest of the library builds on these definitions. This is the most mature part of the library at the moment.

• QCLib/Mathlib/UnitaryGroup/Lemmas.lean QCLib/Matrix/UnitaryGroup

In QCLib, quantum gates are modelled as unitary matrices. These files contain general lemmas on unitaries.

There's also a messy file QCLib/UnitaryGroup/RootsOfUnity.lean with results on complex numbers on the unit circle as objects of type unitary ℂ. It may or may not be a good idea to re-write these files in terms of e.g. stdAddChar.

• QCLib/Circuit/Gate/Qubit.lean

Chaotic file with lots of minor results on single qubit gates. It incorporates significant material from "Lean-QuantumInfo".

• QCLib/Circuit/Gate/Qubit/Bipartite.lean

Permutations and controlled gates. Not restricted to qubits.

• QCLib/Circuit/Gate/Qubit/Embed.lean

The embedding of single-party and bipartite unitaries into the unitary group on a tensor product. Most results are dependently-typed (i.e. they work for tensor products with inhomogeneous factors).

• QCLib/Circuit/Gate/Qubit/PauliGroup

Some basic results on the n-qubit Pauli group.

• QCLib/Circuit/Gate/Qubit/QFT.lean

A first implementation of a QFT circuit. [Cleanup is ongoing.]

• QCLib/Circuit/Gate/Qubit/CZ.lean

Work towards the "diagonal real Clifford group", i.e. the group generated by Z and controlled-Z gates. Goal is to reason about graph states. Incomplete.

• QCLib/Circuit/Gate/Qubit/Complexity.lean

Experiment for defining the gate complexity of a unitary. (Other projects seem to have much more sophisticated frameworks for talking about the syntax of quantum circuits / algorithms. So this file might be a dead end).

• QCLib/Tactic/MatrixExpand.lean

The matrix_expand tactic is a slight variation of the one found in "Lean-QuantumInfo". The file also contains logic for producing simpler goals when using the fin_cases tactic on tuples (with contributions by Andrés Goens).

• QCLib/Tactic/AssocRw.lean

A port of Lean3's AssocRw tactic. It's working, but an improved version better adapted to Lean4 is being developed. Written by Georgios Afentakis.

• ExperimentsAndDeadEnds

Material that isn't working yet or not anymore. Experiments that didn't pan out.

• ExperimentsAndDeadEnds/MatrixLike.lean

Experiments for a MatrixLike typeclass to avoid code duplication when working with types that bundle a matrix with additional information (unitarity / hermiticity / invertibility). Incomplete, but should be discussed.

• ExperimentsAndDeadEnds/Braket

Braket formalism based on interpreting a ket ∣ψ⟩ as a linear map that sends s : ℂ to s • ψ. Including a version for continuous linear maps. Incomplete.

• ExperimentsAndDeadEnds/PiTensorProduct

Hilbert space instances on the PiTensorProduct of Hilbert spaces. Approach abandoned in favor of concrete vectors / matrices.

• UnitTests

Some tests.

Not yet included

Results that are mainly done, but not yet included in the public repository:

• A first formalization of Grover search by Georgios Afentakis.
• More general theory of digits of numbers modulo d ^ n, and a simpler proof for the QFT circuit

Contributors

Main authors:

• Davood Haji Taghi Tehrani Paradoxy (Zulipchat)
• David Gross david.gross@thp.uni-koeln.de

Contributors:

• Georgios Afentakis gafentak@smail.uni-koeln.de
• Andrés Goens andres.goens@tu-darmstadt.de

License

Copyright (c) 2026 David Gross, Davood Tehrani. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE.

Attributions

The files QCLib/Circuit/Gate/Qubit.lean and QCLib/Tactic/MatrixExpand.lean contain material from the Lean QuantumInfo repository https://github.com/Timeroot/Lean-QuantumInfo.

Copyright (c) 2025 Alex Meiburg.

These parts are licensed under the MIT License:

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the “Software”), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.