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
This mission develops Chapter 2 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 8 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 5 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 21 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 27 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 9 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 33 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 6 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 7 of Stabilizer Codes and Quantum Error Correction by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 29 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 3 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 8 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 26 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 18 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 30 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 22 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 12 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
This mission develops Chapter 5 of An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.
The AdS/CFT correspondence relates a theory of quantum gravity in anti-de Sitter space (the bulk) to a quantum field theory without gravity on its boundary (the CFT). A central question is how a local field operator deep in the bulk is represented by boundary operators. Almheiri, Dong and Harlow (JHEP 04 (2015) 163) pointed out a puzzle.
Quantum information often describes a system through a state shared among many small registers. One would like to replace the state on a few registers by a product of their individual states, because product states are easier to estimate and optimize over. The usual finite quantum de Finetti theorems obtain such approximations from permutation symmetry. A…
Many problems in quantum information theory ask for the maximum of a linear functional over pairs of quantum states, one on each of two systems, subject to linear constraints on each state. The best success probability of an approximate quantum error-correcting code of given size is of this form: the encoder and the decoder are quantum channels, their Choi…
Projective measurement is usually taught together with state update: an observable is measured, a value is obtained, and the conditional state is assigned. These are two different questions. The first is the prediction of the outgoing ensemble from the incoming ensemble and the measured observable alone, before the outcome is known; the second is the…
The parity function tests whether a shallow quantum circuit can combine information from all input bits. Polynomially many ancillary qubits make the measured-output formulation substantially stronger than a restriction to clean final registers. The pinned manuscript supplies the research context.
A quantum channel models how a physical system, used to carry information, is corrupted by its environment. The classical capacity of a channel is the largest rate, in bits per use, at which classical messages can be sent with vanishing error when the sender may encode into arbitrary — possibly entangled — states of many uses and the receiver may measure…
Computing the ground-state energy of electrons in the Coulomb field of fixed nuclei is the basic problem of quantum chemistry. In quantum complexity theory, a problem is QMA-hard if every problem with polynomial-time quantum verification of a quantum witness (the quantum analogue of NP) reduces to it. Hardness was previously known for lattice models with…
| 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 |