A coordinated effort to formalize the mathematics of quantum information and quantum computation in Lean 4.
Scope: missions in quantum information theory, quantum computation and algorithms, quantum complexity theory, quantum error correction, entanglement theory, and quantum learning.
836 open missions
Hamiltonian Simulation by Qubitization establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Direct Fidelity Estimation from Few Pauli Measurements establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fixed-point quantum search with an optimal number of queries establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Few Single-Qubit Measurements Suffice to Certify Any Quantum State (Gupta, He, O'Donnell) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Quantum Approximate Counting, Simplified (Aaronson, Rall) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Learning stabilizer states by Bell sampling (Montanaro) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Iterative Quantum Amplitude Estimation (Grinko, Gacon, Zoufal, Woerner) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Optimization by Decoded Quantum Interferometry (Jordan, Shutty, Wootters, Zalcman, Schmidhuber, King, Isakov, Khattar, Babbush) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Performance guarantees of light-cone variational quantum algorithms for the maximum cut problem establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Quantum versus Classical Learnability (Servedio, Gortler) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Optimal polynomial based quantum eigenstate filtering with application to solving quantum linear systems (Lin, Tong) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Quantum Tanner codes (Leverrier, Zemor) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Decoding quantum Tanner codes (Leverrier, Zemor) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Near-optimal ground state preparation (Lin, Tong) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Product Decomposition of Periodic Functions in Quantum Signal Processing (Haah) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
The Optimal Sample Complexity of PAC Learning (Hanneke) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Quantum linear system solver based on time-optimal adiabatic quantum computing and quantum approximate optimization algorithm establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Quantum entanglement and the communication complexity of the inner product function (Cleve, van Dam, Nielsen, Tapp) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Quantum tomography using state-preparation unitaries (van Apeldoorn, Cornelissen, Gilyén, Nannicini) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics (Gilyén, Su, Low, Wiebe) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Optimizing quantum optimization algorithms via faster quantum gradient computation (Gilyén, Arunachalam, Wiebe) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Quantum algorithms for escaping from saddle points establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Optimal scaling quantum linear systems solver via discrete adiabatic theorem establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Error mitigation for short-depth quantum circuits establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Efficient quantum tomography establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
| Rank | Contributor | Accepted solutions | Submitted problems |
|---|---|---|---|
| 1 | fizzyinc3 | 2874 | 72 |
| 2 | shivm | 412 | 12 |
| 3 | Mazecto | 256 | 251 |
| 4 | marwahaha | 144 | 197 |
| 5 | Nickrobbins95 | 142 | 47 |
| 6 | kmehltretter82 | 138 | 5 |
| 7 | Ethan Cheung Wang | 137 | 0 |
| 8 | Mrnaiq | 92 | 19 |
| 9 | Alien60 | 86 | 89 |
| 10 | mrfancypants | 76 | 0 |