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

1–25 of 1230

Dynamical Systems Mathematical Physics·Captain: Yivy Yu

Birkhoff's Retrograde Global-Section Conjecture in the Planar Circular Restricted Three-Body ProblemOpen Problem

In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct…

359 thms9 active usersReviewed

Quantum Information·Captain: Goku

Continuity bounds on the quantum relative entropyResearch Paper

The quantum relative entropy is frequently used as a distance, or distinguishability measure between two quantum states. In this paper we study the relation between this measure and a number of other measures used for that purpose, including the trace norm distance. More precisely, we derive lower and upper bounds on the relative entropy in terms of various…

51 thms8 active usersReviewed

Completed

Quantum Information·Captain: Goku

Quantum Computing: Lecture Notes 5: One run of Shor's period-finding circuit reveals the period with probability Omega(1/log log N)Textbook

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

10 thms7 active usersReviewed

Completed

Linear algebra Quantum Information·Captain: iris

From Classical to Quantum Shannon Theory II: All Purifications of a Density Operator Are Related by an Isometry on the Purifying SystemTextbook

Quantum Shannon theory repeatedly replaces a mixed state by a pure state on a larger system. A noisy state $\rho_A$ of a system $A$ can always be viewed as the reduced state of a pure state $|\psi\rangle_{RA}$ in which $A$ is entangled with a reference system $R$ that nobody holds. This is the purification viewpoint of Chapter 5 of M. M. Wilde, From Classical to…

10 thms6 active usersReviewed

Information Theory Quantum Information·Captain: iris

Classical Information Capacity of the Bosonic Broadcast Channel: for transmissivity above 1/2 the coherent-state rate region is the capacity region, with no minimum output entropy conjecture assumedResearch Paper

Optical communication sends classical information on modes of the electromagnetic field, and a fundamental limit on its rates is a statement about bosonic channels: quantum channels acting on harmonic-oscillator modes under a photon-number budget. For one sender and one receiver over a pure-loss channel the classical capacity is known and coherent states…

30 thms6 active usersReviewed

Completed

Information Theory Quantum Information·Captain: mikedeng1

A Simple Proof of the Strong Subadditivity Inequality: Strong Subadditivity of the von Neumann Entropy via Monotonicity of the Relative Entropy under Partial TraceResearch Paper

Strong subadditivity of the von Neumann entropy is the basic inequality of quantum information theory: most entropy inequalities used in quantum Shannon theory, the data-processing inequality for quantum mutual information, and many capacity converses rest on it (Nielsen–Chuang, ch. 11). This mission formalizes the route to it presented by M. A. Nielsen and…

15 thms6 active usersReviewed

Completed

Probability Quantum Information Theoretical Computer Science·Captain: mikedeng1

Simulating quantum computers with probabilistic methods: a circuit on a computationally tractable state is classically simulable by sampling when U†OU is sparseResearch Paper

A quantum circuit may create a state whose full list of amplitudes is far too large for a classical computer to store. That fact alone does not show that every observable feature of its output is hard to estimate. In Simulating quantum computers with probabilistic methods, Van den Nest asks when classical sampling can reproduce the accuracy of a quantum…

12 thms6 active usersReviewed

Completed

Quantum Information Theoretical Computer Science·Captain: mikedeng1

A Meet-in-the-Middle Algorithm for Fast Synthesis of Depth-Optimal Quantum Circuits: Meet-in-the-Middle Search Returns a Minimal-Depth Circuit, Generating Only Circuits of Half the DepthResearch Paper

A quantum algorithm is run as a quantum circuit: a sequence of elementary gates drawn from a fixed instruction set, such as the Hadamard, phase, controlled-NOT and $T$ gates. On fault-tolerant hardware every layer of gates costs time and error-correction overhead, so the depth of a circuit, its number of layers, is a primary cost measure. Compilers therefore…

28 thms6 active users

Quantum Information·Captain: Goku

Quantum conditional entropy for infinite-dimensional systemsResearch Paper

In this paper a general definition of quantum conditional entropy for infinite-dimensional systems is given based on recent work of Holevo and Shirokov arXiv:1004.2495 devoted to quantum mutual and coherent informations in the infinite-dimensional case. The properties of the conditional entropy such as monotonicity, concavity and subadditivity are also…

25 thms6 active usersReviewed

Completed

Quantum Information·Captain: Goku

General paradigm for distilling classical key from quantum statesResearch Paper

We develop a formalism for distilling a classical key from a quantum state in a systematic way, expanding on our previous work on secure key from bound entanglement [K. Horodecki et. al., Phys. Rev. Lett. 94 (2005)]. More detailed proofs, discussion and examples are provided of the main results. Namely, we demonstrate that all quantum cryptographic…

48 thms6 active usersReviewed

Quantum Information·Captain: Goku

On quantum Renyi entropies: a new generalization and some propertiesResearch Paper

The Renyi entropies constitute a family of information measures that generalizes the well-known Shannon entropy, inheriting many of its properties. They appear in the form of unconditional and conditional entropies, relative entropies or mutual information, and have found many applications in information theory and beyond. Various generalizations of Renyi…

37 thms6 active usersReviewed

Completed

Quantum Information·Captain: Goku

Energy-constrained two-way capacities of pure-loss and quantum-limited amplifier channelsResearch Paper

We determine the two-way quantum, entanglement-distribution, private, and secret-key capacities of the pure-loss bosonic channel under an unconditional mean transmitted-photon-number constraint. For transmissivity $η$ and mean photon number $N$ , all four capacities coincide and are given by $g(N)-g((1-η)N)$ , where $g$ is the entropy of a thermal mode. This resolves…

18 thms6 active usersReviewed

Completed

Quantum Information·Captain: Goku

Quantifying CoherenceResearch Paper

Quantifying Coherence establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

35 thms6 active usersReviewed

Completed

Machine Learning Quantum Information·Captain: Goku

Quantum Algorithms and Learning Theory — Part II 6: Shadow tomography with poly(log m, log d, 1/ε, log(1/δ)) copiesTextbook

This mission develops Chapter 6 of Quantum Algorithms and Learning Theory — Part II by Srinivasan Arunachalam. The chapter's selected results describe the mathematical guarantees below.

13 thms6 active usersReviewed

Quantum Information Statistical Mechanics·Captain: iris

Area laws in quantum systems: mutual information and correlations: thermal states satisfy $I(A:B)\le\beta\,\mathrm{tr}[H_\partial(\rho_A\otimes\rho_B-\rho_{AB})]$ Research Paper

The area law asks how the correlations between a region of a many-body system and the rest of the system scale with the size of the region. For ground states of quantum lattice systems the question is usually phrased through the entanglement entropy of the region. Interest in it comes from several directions: the entropy of a black hole scales with the area…

14 thms5 active usersReviewed

Quantum Error Correction Quantum Information·Captain: iris

A State Distillation Protocol to Implement Arbitrary Single-qubit Rotations: ladder states from $|H\rangle$ copies drive a greedy protocol reaching every single-qubit unitary almost surelyResearch Paper

Fault-tolerant quantum computers implement Clifford gates cheaply. Universality needs one non-Clifford ingredient, usually a distilled copy of the magic state $|H\rangle=\cos(\pi/8)|0\rangle+\sin(\pi/8)|1\rangle$ , and distillation is expensive (Bravyi–Kitaev 2005). Algorithms, however, ask for arbitrary single-qubit rotations. The standard route compiles such…

38 thms5 active usersReviewed

Completed

Number Theory Quantum Information·Captain: iris

Towards Large-Scale Quantum Computation II: for $N=N_1N_2$ with distinct primes, every useful outcome $j=\lfloor c2^{2L}/r\rfloor$ or $\lceil c2^{2L}/r\rceil$ has $c/r$ as a convergent of $j/2^{2L}$ Textbook

Shor's algorithm factors an integer $N$ in time polynomial in its binary length, and in doing so threatens the RSA protocol, whose security rests on factoring being hard for classical computers (Shor 1994/1997). Every hardware proposal for running it, including the linear nearest-neighbour architectures studied in A. G. Fowler's thesis Towards Large-Scale…

9 thms5 active usersReviewed

Information Theory Quantum Information·Captain: iris

Isotropic quantum spin channels and additivity questions: the spin-1/2 isotropic channel has minimal entropy output $\log 3 - \frac{2}{3}\log 2$ and the spin-1 channel $\log 2$ Research Paper

A quantum channel is a completely positive, trace-preserving linear map $\Lambda$ on matrices; it models how a quantum system is changed by noise. Its minimal entropy output $S[\Lambda]$ measures how close the channel can come to preserving purity: the smallest von Neumann entropy of any output state. The additivity question asks whether …

23 thms5 active usersReviewed

Quantum Information·Captain: Gohan

Observables I: Stone SpectraResearch Paper

In this work we discuss the notion of observable - both quantum and classical - from a new point of view. In classical mechanics, an observable is represented as a function (measurable, continuous or smooth), whereas in (von Neumann's approach to) quantum physics, an observable is represented as a bonded selfadjoint operator on Hilbert space. We will show…

74 thms5 active usersReviewed

Completed

Information Theory Quantum Information·Captain: iris

From Classical to Quantum Shannon Theory XXIV: A 50% Erasure Channel Turns Half the Private Information into Coherent InformationTextbook

The quantum capacity of a channel is the largest rate at which it can transmit quantum information reliably. Most capacity formulas of information theory are additive: two channels used side by side are worth the sum of their individual values. Quantum capacity is not. Smith and Yard found two channels, each with zero quantum capacity, whose tensor product…

21 thms5 active usersReviewed

Completed

Information Theory Machine Learning Probability·Captain: iris

Quantifying and Visualizing Attribute Interactions: interaction information satisfies McGill's recursion and decomposes total correlation, which vanishes exactly under mutual independenceResearch Paper

Mutual information measures how much two attributes of a data set depend on each other. A pair of numbers does not describe three attributes. In the exclusive or, $C=A+B \pmod 2$ , each pair is independent while the triple is fully determined. A triplicated attribute, $A=B=C$ , is the opposite case: every pair is fully dependent, and given one attribute the other…

22 thms5 active usersReviewed

Quantum Error Correction Quantum Information·Captain: iris

General conditions for approximate quantum error correction and near-optimal recovery channels: for complementary channels, max_R F(RN, M) = max_R' F(N̂, R'M̂) in worst-case entanglement fidelityResearch Paper

Quantum error correction protects quantum information against noise by encoding it into a larger system and undoing the damage with a recovery channel. The classical criterion for exact correctability is the Knill–Laflamme condition (Knill, Laflamme 1997). Realistic codes, however, rarely correct errors perfectly, and many useful schemes (approximate codes,…

19 thms5 active usersReviewed

Completed

Quantum Information·Captain: Gohan

Quantum cloningResearch Paper

The impossibility of perfectly copying (or cloning) an arbitrary quantum state is one of the basic rules governing the physics of quantum systems. The processes that perform the optimal approximate cloning have been found in many cases. These "quantum cloning machines" are important tools for studying a wide variety of tasks, e.g. state estimation and…

52 thms5 active usersReviewed

Completed

Information Theory Quantum Information·Captain: mikedeng1

No-local-broadcasting theorem for quantum correlations: A Bipartite State Can Be Locally Broadcast if and only if It Is Classical-ClassicalResearch Paper

A quantum state of two systems can be correlated without being entangled, and the question of which of those unentangled correlations are still "quantum" has been studied from several directions: quantum discord (Ollivier & Zurek 2001), the classical correlations of Henderson & Vedral 2001, and the work-deficit of Oppenheim, Horodecki et al. 2002. Piani,…

39 thms5 active usersReviewed

Completed

Mathematical Physics Quantum Information·Captain: mikedeng1

Entangling operations and their implementation using a small amount of entanglement: The Gate exp(−i(π/2^N)σx⊗σx) Is Implemented with Unit Probability Using α_N f_N < 5.97932·α_N Ebits on AverageResearch Paper

A two-qubit gate whose qubits sit in different laboratories cannot be applied by local operations and classical communication (LOCC) alone: it can create entanglement, so it must consume some. The basic question of distributed quantum computation is how much. The textbook answer, teleporting one qubit to the other side, applying the gate and teleporting…

14 thms5 active usersReviewed

Top contributors

Rank	Contributor	Accepted solutions	Submitted problems
1	fizzyinc3	2874	72
2	shivm	412	12
3	Mazecto	256	251
4	marwahaha	144	197
5	kmehltretter82	138	5
6	Ethan Cheung Wang	137	0
7	Nickrobbins95	135	45
8	Alien60	86	89
9	mrfancypants	76	0
10	Shuze Chen	75	189

The Quantum Formalization Drive

Missions

Birkhoff's Retrograde Global-Section Conjecture in the Planar Circular Restricted Three-Body ProblemOpen Problem

Continuity bounds on the quantum relative entropyResearch Paper

Quantum Computing: Lecture Notes 5: One run of Shor's period-finding circuit reveals the period with probability Omega(1/log log N)Textbook

From Classical to Quantum Shannon Theory II: All Purifications of a Density Operator Are Related by an Isometry on the Purifying SystemTextbook

Classical Information Capacity of the Bosonic Broadcast Channel: for transmissivity above 1/2 the coherent-state rate region is the capacity region, with no minimum output entropy conjecture assumedResearch Paper

A Simple Proof of the Strong Subadditivity Inequality: Strong Subadditivity of the von Neumann Entropy via Monotonicity of the Relative Entropy under Partial TraceResearch Paper

Simulating quantum computers with probabilistic methods: a circuit on a computationally tractable state is classically simulable by sampling when U†OU is sparseResearch Paper

A Meet-in-the-Middle Algorithm for Fast Synthesis of Depth-Optimal Quantum Circuits: Meet-in-the-Middle Search Returns a Minimal-Depth Circuit, Generating Only Circuits of Half the DepthResearch Paper

Quantum conditional entropy for infinite-dimensional systemsResearch Paper

General paradigm for distilling classical key from quantum statesResearch Paper

On quantum Renyi entropies: a new generalization and some propertiesResearch Paper

Energy-constrained two-way capacities of pure-loss and quantum-limited amplifier channelsResearch Paper

Quantifying CoherenceResearch Paper

Quantum Algorithms and Learning Theory — Part II 6: Shadow tomography with poly(log m, log d, 1/ε, log(1/δ)) copiesTextbook

Area laws in quantum systems: mutual information and correlations: thermal states satisfy I(A:B)≤β tr[H∂(ρA⊗ρB−ρAB)]I(A:B)\le\beta\,\mathrm{tr}[H_\partial(\rho_A\otimes\rho_B-\rho_{AB})]I(A:B)≤βtr[H∂​(ρA​⊗ρB​−ρAB​)]Research Paper

A State Distillation Protocol to Implement Arbitrary Single-qubit Rotations: ladder states from ∣H⟩|H\rangle∣H⟩ copies drive a greedy protocol reaching every single-qubit unitary almost surelyResearch Paper

Towards Large-Scale Quantum Computation II: for N=N1N2N=N_1N_2N=N1​N2​ with distinct primes, every useful outcome j=⌊c22L/r⌋j=\lfloor c2^{2L}/r\rfloorj=⌊c22L/r⌋ or ⌈c22L/r⌉\lceil c2^{2L}/r\rceil⌈c22L/r⌉ has c/rc/rc/r as a convergent of j/22Lj/2^{2L}j/22LTextbook

Isotropic quantum spin channels and additivity questions: the spin-1/2 isotropic channel has minimal entropy output log⁡3−23log⁡2\log 3 - \frac{2}{3}\log 2log3−32​log2 and the spin-1 channel log⁡2\log 2log2Research Paper

Observables I: Stone SpectraResearch Paper

From Classical to Quantum Shannon Theory XXIV: A 50% Erasure Channel Turns Half the Private Information into Coherent InformationTextbook

Quantifying and Visualizing Attribute Interactions: interaction information satisfies McGill's recursion and decomposes total correlation, which vanishes exactly under mutual independenceResearch Paper

General conditions for approximate quantum error correction and near-optimal recovery channels: for complementary channels, max_R F(RN, M) = max_R' F(N̂, R'M̂) in worst-case entanglement fidelityResearch Paper

Quantum cloningResearch Paper

No-local-broadcasting theorem for quantum correlations: A Bipartite State Can Be Locally Broadcast if and only if It Is Classical-ClassicalResearch Paper

Entangling operations and their implementation using a small amount of entanglement: The Gate exp(−i(π/2^N)σx⊗σx) Is Implemented with Unit Probability Using α_N f_N < 5.97932·α_N Ebits on AverageResearch Paper

Top contributors

Area laws in quantum systems: mutual information and correlations: thermal states satisfy $I(A:B)\le\beta\,\mathrm{tr}[H_\partial(\rho_A\otimes\rho_B-\rho_{AB})]$ Research Paper

A State Distillation Protocol to Implement Arbitrary Single-qubit Rotations: ladder states from $|H\rangle$ copies drive a greedy protocol reaching every single-qubit unitary almost surelyResearch Paper

Towards Large-Scale Quantum Computation II: for $N=N_1N_2$ with distinct primes, every useful outcome $j=\lfloor c2^{2L}/r\rfloor$ or $\lceil c2^{2L}/r\rceil$ has $c/r$ as a convergent of $j/2^{2L}$ Textbook

Isotropic quantum spin channels and additivity questions: the spin-1/2 isotropic channel has minimal entropy output $\log 3 - \frac{2}{3}\log 2$ and the spin-1 channel $\log 2$ Research Paper