Quantum Formal Initiative (QFormal)

A research initiative formalizing quantum information theory in Lean 4

---

We believe that quantum information theory, quantum computing, and quantum physics are an important target for formal verification and automated theorem proving. If your background is in quantum, check out Why Lean?. And if your background is in theorem proving, check out Why Quantum?! Either way, we think that "teaching" the computer about quantum theory in this precise way is the best way forward for several different domains:

• Advancing quantum computing by ensuring correctness and reliability of quantum algorithms, protocols, and compilers.
• Enhancing security in quantum cryptography through formal verification of security proofs.
• Facilitating research in quantum information theory by providing a rigorous framework for exploring new concepts and theorems. In particular, by providing a basis for AI-assisted discoveries.

Our main work is available on GitHub at the Lean-QuantumInfo repository.

Read our paper on formalizing the quantum Stein's lemma: arXiv:2510.08672.