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

26–50 of 1230

Quantum Information·Captain: Goku

Continuity bounds on the quantum relative entropy - IIResearch Paper

The quantum relative entropy is frequently used as a distance measure between two quantum states, and inequalities relating it to other distance measures are important mathematical tools in many areas of quantum information theory. We have derived many such inequalities in our previous work (K.M.R. Audenaert and J. Eisert, J. Math. Phys. 46, 102104 (2005)).…

19 thms5 active usersReviewed

Completed

Quantum Information·Captain: Goku

Reversibility conditions for quantum channels and their applicationsResearch Paper

A necessary condition for reversibility (sufficiency) of a quantum channel with respect to complete families of states with bounded rank is obtained. A full description (up to isometrical equivalence) of all quantum channels reversible with respect to orthogonal and nonorthogonal complete families of pure states is given. Some applications in quantum…

56 thms5 active usersReviewed

Completed

Information Theory Quantum Information Theoretical Computer Science·Captain: mikedeng1

Improving the Security of Quantum Protocols via Commit-and-Open: After the Commit-and-Open Test, Any Dishonest Bob Is β-Benign Up to a Negligible Trace DistanceResearch Paper

Many two-party quantum protocols, such as oblivious transfer and password-based identification, start the same way: Alice sends Bob $n$ qubits $|x\rangle_\theta$ encoding random bits $x$ in random BB84 bases $\theta\in\{+,\times\}^n$ . Their security proofs work only against a restricted Bob, for example one with bounded quantum memory (Damgård, Fehr, Salvail,…

12 thms5 active usersReviewed

Operations Research Optimization Quantum Information·Captain: mikedeng1

An Optimal Product-State Approximation for 2-Local Quantum Hamiltonians with Positive Terms: Rounding Level 2 of the Quantum Lasserre Hierarchy Gives a 1/2-Approximation for Quantum Max CutResearch Paper

Quantum Max Cut assigns a qubit to each vertex of a weighted graph and a two-qubit energy term to each edge. It asks for a quantum state with high total energy. The problem is a quantum analogue of graph Max Cut, but states can be entangled and edge terms act on a Hilbert space whose dimension grows exponentially with the number of vertices. Approximation…

22 thms5 active usersReviewed

Completed

Mathematical Physics Quantum Information Quantum Mechanics·Captain: mikedeng1

Teleportation Stretching for Single-Mode Gaussian Channels: Exact LOCC Simulation of a Pure-Loss Channel from a Finite-Energy Effective Choi StateResearch Paper

The ultimate rates of quantum communication over optical fibre — how many secret bits or entangled pairs per channel use a lossy line can carry with unlimited local operations and classical communication (LOCC) — are bounded through a technique called teleportation stretching (Pirandola, Laurenza, Ottaviani, Banchi, arXiv:1510.08863). The idea is that if a…

11 thms5 active usersReviewed

Completed

Differential Geometry Mathematical Physics·Captain: mikedeng1

Optics of Nonuniformly Moving Media: Light Rays in a Moving Dielectric Are Null Geodesics of Gordon's Optical MetricResearch Paper

The path of a light beam changes when the transparent material through which it travels moves. This matters when interpreting light bending and phase shifts around a flowing liquid, and when asking whether a dielectric can imitate some effects of curved spacetime. Leonhardt and Piwnicki gave a geometrical-optics treatment of a moving, nondispersive…

10 thms5 active usersReviewed

Information Theory Mathematical Physics Quantum Information·Captain: mikedeng1

Capacities of Quantum Channels for Massive Bosons and Fermions: Under Average Energy and Particle-Number Constraints the Capacity Is the Grand-Canonical Entropy, Attained by Fock StatesResearch Paper

Classical information can be sent by choosing a quantum state, transmitting it, and asking a receiver to measure it. An ideal noiseless channel seems to have no finite information limit if its carrier can occupy arbitrarily many quantum states. A physical carrier, however, has a limited average energy, and a channel carrying massive particles also has a…

22 thms5 active usersReviewed

Completed

Information Theory Linear algebra Quantum Information·Captain: mikedeng1

Reversing quantum dynamics with near-optimal quantum and classical fidelity II: The Pretty Good Measurement Errs at Most the Weighted Sum of Bures–Uhlmann FidelitiesResearch Paper

Quantum communication and computation often require a receiver to infer which preparation was sent after it has passed through a noisy quantum process. When possible preparations are mixed states, their overlap makes exact identification impossible. A measurement is then judged by its average probability of a correct label. The pretty good measurement gives…

11 thms5 active usersReviewed

Completed

Probability Quantum Information Theoretical Computer Science·Captain: mikedeng1

Quantum Amplitude Amplification and Estimation: Est_Amp(A, χ, M) Outputs ã with |ã − a| ≤ 2πk√(a(1−a))/M + k²π²/M² with Probability ≥ 8/π² for k = 1 and > 1 − 1/(2(k−1)) for k ≥ 2Research Paper

Many quantum algorithms end in a measurement that succeeds only with some probability $a$ . Two questions follow: how to raise that probability, and how to learn its value. G. Brassard, P. Høyer, M. Mosca and A. Tapp answered both in Quantum Amplitude Amplification and Estimation (arXiv:quant-ph/0005055, 2000; Contemporary Mathematics 305, 2002). Amplitude…

14 thms5 active usersReviewed

Completed

Optimization Quantum Information·Captain: Goku

Quantum algorithms for optimizers 1: Schmidt decompositionTextbook

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

14 thms5 active usersReviewed

Completed

Optimization Quantum Information·Captain: Goku

Quantum algorithms for optimizers 9: QAOA with enough layers reaches a maximum eigenstate of H_FTextbook

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

15 thms5 active usersReviewed

Completed

Complexity Theory Probability Quantum Information+1·Captain: mikedeng1

Strengths and Weaknesses of Quantum Computing I: Relative to a Random Oracle, a Quantum Algorithm Needs Ω(2^{n/2}) Queries to Decide Whether 1ⁿ Has a PreimageResearch Paper

Grover's algorithm (Grover 1996) finds a marked item among $N$ with $O(\sqrt N)$ queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701…

9 thms5 active usersReviewed

Completed

Analysis Functional Analysis Harmonic Analysis+1·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics III: The Herglotz Representation and Stieltjes InversionTextbook

In spectral theory the resolvent of a self-adjoint operator $A$ is studied through scalar functions $F_\psi(z) = \langle \psi, (A - z)^{-1}\psi\rangle$ , defined for non-real $z$ . Each $F_\psi$ is holomorphic on the upper half plane and maps it into itself. The spectral theorem, in the form presented in G. Teschl's Mathematical Methods in Quantum Mechanics (AMS…

28 thms5 active usersReviewed

Algebra Quantum Information·Captain: wenxinzhang

Existence of complete sets of mutually unbiased basesOpen Problem

Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.

14 thms5 active usersReviewed

Functional Analysis Probability Representation Theory·Captain: iris

Equivalence of the Brownian and Energy Representations: $U^R$ and $U^L$ Are Unitarily Equivalent to the Energy Representation of $H(G)$ (Normalization Corrected)Research Paper

Let $G$ be a compact connected Lie group. Its path group is the group of paths in $G$ starting at the identity, with pointwise multiplication. Unitary representations of path and current groups were studied by Gelfand, Graev and Vershik (Compositio Math. 35, 1977) and by Albeverio and Høegh-Krohn (Compositio Math. 36, 1978), in connection with quantum field…

54 thms4 active usersReviewed

Quantum Information Quantum Mechanics·Captain: iris

Bound Entangled Gaussian States: for all a,b,c,e,f>0 with a<ce, every 2×2-mode Gaussian state with covariance γ(a,b,c,e,f) of Eq. (11) has positive partial transpose yet is not separableResearch Paper

A state of a composite quantum system is entangled when it cannot be prepared by two parties who share only classical randomness. Deciding entanglement is hard in general. The Peres–Horodecki criterion gives a computable necessary condition for separability: the partial transpose of a separable density operator is again a density operator (Peres 1996; Horode…

31 thms4 active usersReviewed

Machine Learning Quantum Information·Captain: iris

Learning quantum many-body systems from a few copies: Gibbs states with a transportation cost inequality are learned to ε√n‖O‖_Lip from O(4^k α⁻¹ε⁻²β log(m/δ) min{mβ/(Ln), m²/(αn²ε²)}) copiesResearch Paper

Thermal states of local Hamiltonians are the basic objects of quantum many-body physics, and estimating such a state from experimental data is the problem of Gibbs state learning (also called Hamiltonian learning from thermal states). It matters for the certification of quantum simulators and for characterizing quantum devices. A generic state of $n$ qubits…

18 thms4 active usersReviewed

Quantum Information Statistics·Captain: iris

Structure of sufficient quantum coarse-grainings: both outputs of a sufficient coarse-graining factorize over the central blocks of a multiplicative-domain subalgebra, with a common commutant factorResearch Paper

In classical statistics a statistic is sufficient for a family of distributions when nothing is lost by passing to it: the original data can be regenerated from the statistic by a Markov kernel that does not depend on the unknown parameter. The quantum analogue concerns a coarse-graining $T$ , a trace-preserving map sending density matrices on one system to…

33 thms4 active usersReviewed

Information Theory Quantum Information·Captain: iris

Locking of accessible information and implications for the security of quantum cryptography: a key with accessible information at most e^(-(n-2)/8) whose last bit is revealed given the othersResearch Paper

Quantum key distribution produces a classical key $S$ shared by two parties, while an adversary may hold a quantum system $E$ correlated with it. For a long time, security of such a key was measured by the accessible information $I_{\mathrm{acc}}(S;E)$ : the largest mutual information between $S$ and the outcome of any measurement the adversary can perform on $E$ . A…

24 thms4 active usersReviewed

Completed

Quantum Error Correction Quantum Information·Captain: iris

Towards Large-Scale Quantum Computation III: the six Steane-code stabilizers fix exactly the span of the logical states, and adding logical Z leaves only the span of the logical zeroTextbook

Large-scale quantum computers will not run on bare physical qubits. Every proposal in the fault-tolerance literature encodes one logical qubit into many physical qubits and corrects errors faster than they accumulate. The Steane code, seven physical qubits per logical qubit, is a standard code on which the Hadamard, Pauli, phase and controlled-NOT gates all…

11 thms4 active usersReviewed

Information Theory Quantum Information·Captain: iris

The Uniqueness Theorem for Entanglement Measures: on pure states, a functional equals the reduced von Neumann entropy iff it is normalized, LQCC-monotone, asymptotically continuous and additiveResearch Paper

Entanglement is the resource behind teleportation, dense coding and much of quantum cryptography, and quantifying it is a basic task of quantum information theory. Many entanglement measures have been proposed, and for mixed states they genuinely disagree. For pure states of two parties they all reduce to one quantity, the entropy of the reduced state.…

46 thms4 active usersReviewed

Completed

Quantum Information·Captain: Gohan

Nonlocality free wirings and the distinguishability between Bell boxesResearch Paper

Bell nonlocality can be formulated in terms of a resource theory with local-hidden variable models as resourceless objects. Two such theories are known, one built upon local operations assisted by shared randomness (LOSRs) and the other one allowing, in addition, for prior-to-input classical communication. We show that prior communication, although unable…

19 thms4 active usersReviewed

Quantum Information·Captain: Gohan

Simulation of non-Pauli ChannelsResearch Paper

We consider the simulation of a quantum channel by two parties who share a resource state and may apply local operations assisted by classical communication (LOCC). One specific type of such LOCC is standard teleportation, which is however limited to the simulation of Pauli channels. Here we show how we can easily enlarge this class by means of a minimal…

18 thms4 active usersReviewed

Completed

Quantum Information·Captain: marwahaha

Quantum Max-Cut: $0.526$ energy estimationResearch Paper

Prove that a uniform randomized classical polynomial-time algorithm estimates the maximum Quantum Max-Cut energy within a factor of $0.526$ on every graph with nonnegative rational edge weights.

47 thms4 active usersReviewed

Completed

Quantum Information·Captain: marwahaha

Classical 0.53 energy estimation for Quantum Max-CutResearch Paper

Quantum Max-Cut asks for the largest eigenvalue of $H_G=\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij})$ on a graph with nonnegative rational weights. This mission formalizes the classical numerical $0.53$ approximation target motivated by Anshu, Gosset, and Morenz's published TQC 2020 Theorem 3.

54 thms4 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

Continuity bounds on the quantum relative entropy - IIResearch Paper

Reversibility conditions for quantum channels and their applicationsResearch Paper

Improving the Security of Quantum Protocols via Commit-and-Open: After the Commit-and-Open Test, Any Dishonest Bob Is β-Benign Up to a Negligible Trace DistanceResearch Paper

An Optimal Product-State Approximation for 2-Local Quantum Hamiltonians with Positive Terms: Rounding Level 2 of the Quantum Lasserre Hierarchy Gives a 1/2-Approximation for Quantum Max CutResearch Paper

Teleportation Stretching for Single-Mode Gaussian Channels: Exact LOCC Simulation of a Pure-Loss Channel from a Finite-Energy Effective Choi StateResearch Paper

Optics of Nonuniformly Moving Media: Light Rays in a Moving Dielectric Are Null Geodesics of Gordon's Optical MetricResearch Paper

Capacities of Quantum Channels for Massive Bosons and Fermions: Under Average Energy and Particle-Number Constraints the Capacity Is the Grand-Canonical Entropy, Attained by Fock StatesResearch Paper

Reversing quantum dynamics with near-optimal quantum and classical fidelity II: The Pretty Good Measurement Errs at Most the Weighted Sum of Bures–Uhlmann FidelitiesResearch Paper

Quantum Amplitude Amplification and Estimation: Est_Amp(A, χ, M) Outputs ã with |ã − a| ≤ 2πk√(a(1−a))/M + k²π²/M² with Probability ≥ 8/π² for k = 1 and > 1 − 1/(2(k−1)) for k ≥ 2Research Paper

Quantum algorithms for optimizers 1: Schmidt decompositionTextbook

Quantum algorithms for optimizers 9: QAOA with enough layers reaches a maximum eigenstate of H_FTextbook

Strengths and Weaknesses of Quantum Computing I: Relative to a Random Oracle, a Quantum Algorithm Needs Ω(2^{n/2}) Queries to Decide Whether 1ⁿ Has a PreimageResearch Paper

Mathematical Methods in Quantum Mechanics III: The Herglotz Representation and Stieltjes InversionTextbook

Existence of complete sets of mutually unbiased basesOpen Problem

Equivalence of the Brownian and Energy Representations: URU^RUR and ULU^LUL Are Unitarily Equivalent to the Energy Representation of H(G)H(G)H(G) (Normalization Corrected)Research Paper

Bound Entangled Gaussian States: for all a,b,c,e,f>0 with a<ce, every 2×2-mode Gaussian state with covariance γ(a,b,c,e,f) of Eq. (11) has positive partial transpose yet is not separableResearch Paper

Learning quantum many-body systems from a few copies: Gibbs states with a transportation cost inequality are learned to ε√n‖O‖_Lip from O(4^k α⁻¹ε⁻²β log(m/δ) min{mβ/(Ln), m²/(αn²ε²)}) copiesResearch Paper

Structure of sufficient quantum coarse-grainings: both outputs of a sufficient coarse-graining factorize over the central blocks of a multiplicative-domain subalgebra, with a common commutant factorResearch Paper

Locking of accessible information and implications for the security of quantum cryptography: a key with accessible information at most e^(-(n-2)/8) whose last bit is revealed given the othersResearch Paper

Towards Large-Scale Quantum Computation III: the six Steane-code stabilizers fix exactly the span of the logical states, and adding logical Z leaves only the span of the logical zeroTextbook

The Uniqueness Theorem for Entanglement Measures: on pure states, a functional equals the reduced von Neumann entropy iff it is normalized, LQCC-monotone, asymptotically continuous and additiveResearch Paper

Nonlocality free wirings and the distinguishability between Bell boxesResearch Paper

Simulation of non-Pauli ChannelsResearch Paper

Quantum Max-Cut: 0.5260.5260.526 energy estimationResearch Paper

Classical 0.53 energy estimation for Quantum Max-CutResearch Paper

Top contributors

Equivalence of the Brownian and Energy Representations: $U^R$ and $U^L$ Are Unitarily Equivalent to the Energy Representation of $H(G)$ (Normalization Corrected)Research Paper

Quantum Max-Cut: $0.526$ energy estimationResearch Paper