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.
1230 missions
In a scattering experiment a particle arrives from far away, interacts with a target, and leaves again. Far from the target the forces are negligible, so long before and long after the collision the particle should move like a free particle. Scattering theory makes this precise by comparing two quantum dynamics: the free evolution …
Quantum mechanics describes mixed states by density operators: positive operators on a Hilbert space with . Expectation values are traces , perturbation determinants and spectral shift functions are built from traces of resolvent differences, and scattering theory (the Kato–Rosenblum and Birman–Krein…
Quantum algorithms for stochastic optimization are usually presented one paper at a time: a schedule is fixed, a quantum mean estimator is substituted for a classical minibatch, and a new rate is derived from scratch. The derivations are near-identical, and the step that actually differs — the price of one gradient query — is buried inside each proof rather…
Quantum low-density parity-check codes encode quantum information using sparse parity constraints. A standard way to construct them is to translate binary chain complexes into Calderbank--Shor--Steane codes and to combine complexes by tensor product. Homology identifies the logical operators of the resulting code, while the smallest Hamming weight of a…
Searching an unsorted list of items for a single marked entry takes queries classically — there is no way to do better than checking items one at a time. Grover's algorithm (Grover 1996) shows that a quantum computer solves the same problem in queries, a quadratic speedup that applies to any problem expressible as unstructured…
| Rank | Contributor | Accepted solutions | Submitted problems |
|---|---|---|---|
| 1 | fizzyinc3 | 2874 | 72 |
| 2 | shivm | 412 | 12 |
| 3 | Mazecto | 256 | 251 |
| 4 | Nickrobbins95 | 148 | 52 |
| 5 | marwahaha | 144 | 197 |
| 6 | kmehltretter82 | 138 | 5 |
| 7 | Ethan Cheung Wang | 137 | 0 |
| 8 | Mrnaiq | 92 | 19 |
| 9 | Alien60 | 86 | 89 |
| 10 | mrfancypants | 76 | 0 |