The Quantum Formalization Drive

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

Missions

1001–1025 of 1230

Harmonic Analysis Linear algebra Quantum Information·Captain: mikedeng1

Product Decomposition of Periodic Functions in Quantum Signal Processing: Every SU(2)-Valued Laurent Polynomial of Degree n in E_n Is Uniquely a Product of n Primitive Matrices and a UnitaryResearch Paper

Quantum signal processing transforms the eigenphases of a unitary operator by a sequence of controlled operations and single qubit rotations. To know which transformations such a sequence can realize, one must characterize the matrix functions produced by the sequence. Haah's product decomposition theorem gives such a characterization without the…

10 thms2 active usersReviewed

Linear algebra Quantum Information Theoretical Computer Science·Captain: mikedeng1

Quantum Singular Value Transformation and Beyond: Exponential Improvements for Quantum Matrix Arithmetics: Singular Value Transformation by Real Polynomials via Alternating Phase ModulationResearch Paper

Many quantum algorithms act on a matrix $A$ that is not itself unitary: a Hamiltonian to be simulated, a linear system to be inverted, a projector to be amplified. The standard way to hand such a matrix to a quantum computer is to embed it as a block of a unitary $U$ , so that $A=\widetilde\Pi U\Pi$ for two orthogonal projectors $\Pi,\widetilde\Pi$ . The question is…

13 thms2 active usersReviewed

Completed

Combinatorics Quantum Error Correction Quantum Information·Captain: Winningatmath

Bivariate-Bicycle Codes: New [[336,20,12]] and [[360,24,12]] Codes and Certified DistancesResearch Paper

A quantum memory stores logical qubits in many physical qubits so that errors can be detected and corrected. The overhead of doing so, measured by how many physical qubits are spent per logical qubit at a given error-correcting power, is one of the main costs of fault-tolerant quantum computation. Bivariate-bicycle (BB) codes are currently the leading…

63 thms2 active usersReviewed

Information Theory Probability Quantum Error Correction·Captain: mikedeng1

Quantum Tanner Codes 2: A Random Dual Tensor Code Is Δ^{3/2−ε}-Robust with Δ^γ-Resistance to Puncturing with Probability Tending to 1Research Paper

Quantum error correction needs families of codes that protect a growing number of logical qubits while using checks that touch few physical qubits. In a quantum Tanner code, the local constraints come from two smaller binary codes. The distance analysis requires those local codes to satisfy a geometric condition called robustness: a low-weight word in a…

13 thms2 active usersReviewed

Graph Theory Quantum Error Correction Quantum Information·Captain: mikedeng1

Quantum Tanner Codes 1: On a Ramanujan Left-Right Cayley Complex with Robust Dual Tensor Codes, the Quantum Tanner Code Has Rate at Least (1−2ρ)² and Distance at Least δn/(4Δ^{3/2+ε})Research Paper

An error-correcting code protects information by adding redundancy. A quantum code must also account for two kinds of errors, commonly called $X$ and $Z$ errors. Quantum low-density parity-check codes use checks that each touch only a bounded number of qubits, while each qubit participates in only a bounded number of checks. Such locality matters when the…

9 thms2 active usersReviewed

Completed

Probability Quantum Information Theoretical Computer Science·Captain: mikedeng1

Quantum Speedup of Monte Carlo Methods 1: With Var(v(A)) ≤ σ² and ε < 4σ, Algorithm 3 Estimates E[v(A)] to Additive Error ε with Probability at Least 2/3Research Paper

Many computational tasks produce a real number by running a randomized procedure once, then estimate its expected value by running that procedure repeatedly. The number of repetitions needed for a given additive accuracy depends on the output variance. Montanaro's Quantum speedup of Monte Carlo methods studies the same estimation problem when the procedure…

9 thms2 active usersReviewed

Harmonic Analysis Quantum Information·Captain: mikedeng1

Optimal Hamiltonian Simulation by Quantum Signal Processing: Phases Realizing e^{ih(θ)} to Error 8ε With Success Probability at Least 1 − 16εResearch Paper

Simulating the time evolution of a quantum system is a standard task in quantum algorithms: given a Hamiltonian, the algorithm must reproduce the phase acquired by each of its energy eigenstates. The cost is often measured by how many times the algorithm queries an operator describing that system. Low and Chuang's 2016 preprint connects this task to quantum…

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization Optimization·Captain: mikedeng1

Quantum Algorithms for Zero-Sum Games 2: The Value of a Zero-Sum Game, Known to Error ε/(6R(r+1)), Decides Whether an LP Has OPT < α or OPT ≥ α − εResearch Paper

Linear programming and two-player zero-sum matrix games are two faces of one theory. Von Neumann's minimax theorem is a statement of LP duality, and conversely, since Dantzig's 1951 note, every linear program can be rewritten as a zero-sum game. The equivalence matters in practice whenever an algorithm is much better at one of the two problems. Game solvers…

10 thms2 active usersReviewed

Optimization Quantum Information Theoretical Computer Science·Captain: mikedeng1

A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem I: Level-One QAOA Satisfies (1/2 + 1/(101 D^(1/2) ln D))m Equations of Max E3LIN2 for Large DResearch Paper

The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028) is a family of shallow quantum circuits for combinatorial optimization. At its lowest level, $p = 1$ , the circuit has two real parameters, and its output is a random bit string. The question is how many constraints that string satisfies, compared with the…

18 thms2 active usersReviewed

Probability Quantum Information Statistics·Captain: mikedeng1

Direct Fidelity Estimation from Few Pauli Measurements 2: A Unit Vector Nearly Orthogonal to 2^{cd} Given States With Every Non-Identity Pauli Expectation ≤ √(72π³)·√(log d)/√dResearch Paper

Quantum state tomography reconstructs an unknown $d$ -dimensional quantum state from measurements on many copies of it. For $n$ qubits, $d = 2^n$ , so the number of copies a tomography procedure needs grows exponentially in $n$ , and lower bounds on that number decide how far experiments can scale. In many experiments the only measurements available are Pauli…

11 thms2 active usersReviewed

Completed

Quantum Information·Captain: Lucas

Superconducting Quantum Computing: Universality of Single-Qubit Gates and iSWAPTextbook

Superconducting circuits built from capacitors, inductors and Josephson junctions are the dominant platform for current quantum processors (Google, IBM, Rigetti, IQM and others). The source article — the Wikipedia entry Superconducting quantum computing — states two facts about the gate model on this hardware that this mission makes precise:

7 thms2 active usersReviewed

Completed

Quantum Information·Captain: Lucas

Grover's Algorithm (Wikipedia): Quantum Search with Success Probability 1 − 1/N in ⌈π√N/4⌉ IterationsTextbook

Grover's algorithm is a quantum algorithm for unstructured search: given black-box access to a function $f\colon\{0,1,\dots,N-1\}\to\{0,1\}$ that takes the value $1$ at exactly one input $\omega$ , it finds $\omega$ with high probability using $O(\sqrt N)$ evaluations of $f$ . It was devised by Lov Grover in 1996 (Grover, STOC 1996). Classically the same task needs …

16 thms2 active usersReviewed

Completed

Number Theory Quantum Information·Captain: Lucas

Shor's Algorithm (Wikipedia): Quantum Order Finding and the Reduction of FactoringTextbook

Shor's algorithm is a quantum algorithm that finds a nontrivial factor of an integer $N$ in time polynomial in $\log N$ , and its variants compute discrete logarithms in finite cyclic groups. It was developed by Peter Shor in 1994 (Shor, FOCS 1994; Shor, SIAM J. Comput. 1997). No classical polynomial-time factoring algorithm is known; the best classical method,…

16 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Lecture Notes on Quantum Algorithms 31: Adiabatic optimization: running time in terms of the minimum gap (linear interpolation)Textbook

This mission develops Chapter 31 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

2 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Lecture Notes on Quantum Algorithms 23: Trace inequality |tr(XYZ)| ≤ ‖X‖_F ‖Y‖ ‖Z‖_FTextbook

This mission develops Chapter 23 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

1 thm2 active usersReviewed

Completed

Machine Learning Quantum Information·Captain: Goku

A Survey of Quantum Learning Theory 5: Atıcı–Servedio: time-efficient quantum learning of k-juntas (corrected)Textbook

This mission develops Chapter 5 of A Survey of Quantum Learning Theory by Srinivasan Arunachalam and Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

5 thms2 active usersReviewed

Completed

Quantum Error Correction Quantum Information·Captain: Goku

An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation 3: Every error syndrome of a stabilizer is realized by a Pauli errorTextbook

This mission develops Chapter 3 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.

3 thms2 active usersReviewed

Completed

Optimization Quantum Information·Captain: Goku

Quantum algorithms for optimizers 3: Correctness of the digits computed by iterative phase estimation (corrected)Textbook

This mission develops Chapter 3 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.

3 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Lecture Notes on Quantum Algorithms 18: Spectral gap and marked fraction bound the norm of the unmarked blockTextbook

This mission develops Chapter 18 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

2 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Lecture Notes on Quantum Algorithms 2: Group commutators of an ϵ²-net of S_ϵ form an O(ϵ³)-net of S_{ϵ²}Textbook

This mission develops Chapter 2 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

6 thms2 active usersReviewed

Completed

Optimization Quantum Information·Captain: Goku

Quantum algorithms for optimizers 6: Unitary conjugation commutes with the matrix exponential: e^{iUHU†t} = U e^{iHt} U†Textbook

This mission develops Chapter 6 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.

3 thms2 active usersReviewed

Completed

Quantum Error Correction Quantum Information·Captain: Goku

An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation 4: Steane error correction: final errors lie only on the fault locationsTextbook

This mission develops Chapter 4 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.

1 thm2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Quantum Computing: Lecture Notes 7: Amplitude amplification: Q^k A|0^m⟩ = sin((2k+1)θ)|ψ1⟩ + cos((2k+1)θ)|ψ0⟩, and O(1/√p) rounds sufficeTextbook

This mission develops Chapter 7 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

3 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Quantum Computing: Lecture Notes 2: Bernstein–Vazirani: one phase query recovers the hidden stringTextbook

This mission develops Chapter 2 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

2 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Quantum Computing: Lecture Notes 20: Gottesman–Knill: measurement-controlled Clifford circuits are efficiently classically simulableTextbook

This mission develops Chapter 20 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

7 thms2 active usersReviewed

Top contributors

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