Quantum Computing
Toward theorem-backed quantum algorithms and verifiable quantum advantage
Quantum computing is one of the most promising and most difficult frontiers in computational science. The challenge is not only to design new quantum algorithms, but to understand them with mathematical precision: when they work, why they work, how performance scales, and where genuinely quantum behavior may emerge beyond the reach of classical methods. Our goal is to develop theorem-backed understanding of quantum algorithmic performance, building on our quantum information foundations. QAOA is our flagship case study: one of the central algorithms in near-term quantum computing, structured enough to study deeply, yet rich enough to expose some of the most important open questions in quantum algorithm theory.
A Structured Algorithm with Deep Questions
The Quantum Approximate Optimization Algorithm is a leading quantum algorithm for combinatorial optimization. It builds parameterized quantum circuits by alternating between problem-dependent and mixing operations, creating a family of algorithms whose behavior can change dramatically with depth, parameter choice, and problem structure. Basic questions about its performance quickly lead to deep mathematics: how approximation quality scales, which regimes admit provable guarantees, when classical simulation remains possible, and where one may begin to see rigorous signatures of quantum advantage.
QAOA lies at the intersection of optimization, probability, quantum many-body systems, and complexity theory. For us it is not only an algorithm of practical interest, but a model system for a broader scientific question: can we develop a rigorous theory of quantum algorithms that goes beyond heuristic exploration toward precise, trustworthy mathematics?
This project builds on the verified mathematical infrastructure developed in our Quantum Information project.
Theory, Verification, and Discovery
Rigorous Performance Theory
We aim to prove theorems about QAOA performance in important algorithmic and physical regimes — understanding how approximation quality scales, which parameter choices lead to provable guarantees, and where structured problem instances reveal tractable mathematical structure.
Classical vs. Quantum Boundary
One of the deepest questions in quantum computing is where classical simulation ends and genuinely quantum computational power begins. We study this boundary for QAOA and related algorithms, seeking rigorous characterizations of the regimes where quantum advantage may emerge.
Formal Verification
We use Lean 4 to make key results machine-checkable, building reusable mathematical infrastructure for QAOA and related quantum algorithms. Formal verification ensures that claims about performance and scaling rest on precise, auditable foundations.
What We Aim to Understand
The long-term ambition is theorem-backed understanding of quantum algorithmic performance — including questions related to quantum advantage and, in stronger regimes, the kinds of separation phenomena sometimes associated with quantum supremacy. Our emphasis is always on mathematical clarity: the goal is not to claim more, but to know more with greater confidence.