Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Collections

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.

836 open missions

Missions

626–650 of 836
Open836Completed394All1230
Quantum Information·Captain: Goku

Unifying classical and quantum key distillationResearch Paper

Assume that two distant parties, Alice and Bob, as well as an adversary, Eve, have access to (quantum) systems prepared jointly according to a tripartite state. In addition, Alice and Bob can use local operations and authenticated public classical communication. Their goal is to establish a key which is unknown to Eve. We initiate the study of this scenario…

11 thms2 active usersReviewed
Quantum Information·Captain: Goku

Contractivity of positive and trace preserving maps under Lₚ normsResearch Paper

We provide a complete picture of contractivity of trace preserving positive maps with respect to ppp-norms. We show that for p>1p>1p>1 contractivity holds in general if and only if the map is unital. When the domain is restricted to the traceless subspace of Hermitian matrices, then contractivity is shown to hold in the case of qubits for arbitrary p≥1p\geq 1p≥1 and in…

17 thms2 active usersReviewed
Quantum Information·Captain: Goku

Entanglement Cost of Quantum ChannelsResearch Paper

The entanglement cost of a quantum channel is the minimal rate at which entanglement (between sender and receiver) is needed in order to simulate many copies of a quantum channel in the presence of free classical communication. In this paper we show how to express this quantity as a regularised optimisation of the entanglement formation over states that can…

27 thms2 active usersReviewed
Quantum Information·Captain: Goku

Semidefinite programming strong converse bounds for classical capacityResearch Paper

We investigate the classical communication over quantum channels when assisted by no-signaling (NS) and positive-partial-transpose-preserving (PPT) codes, for which both the optimal success probability of a given transmission rate and the one-shot ϵ\epsilonϵ-error capacity are formalized as semidefinite programs (SDPs). Based on this, we obtain improved SDP…

38 thms2 active usersReviewed
Quantum Information·Captain: Goku

Non-asymptotic entanglement distillationResearch Paper

Entanglement distillation, an essential quantum information processing task, refers to the conversion from multiple copies of noisy entangled states to a smaller number of highly entangled states. In this work, we study the non-asymptotic fundamental limits for entanglement distillation. We investigate the optimal tradeoff between the distillation rate, the…

27 thms2 active usersReviewed
Quantum Information·Captain: Goku

Capacities of Quantum Amplifier ChannelsResearch Paper

Quantum amplifier channels are at the core of several physical processes. Not only do they model the optical process of spontaneous parametric down-conversion, but the transformation corresponding to an amplifier channel also describes the physics of the dynamical Casimir effect in superconducting circuits, the Unruh effect, and Hawking radiation. Here we…

6 thms2 active usersReviewed
Quantum Information·Captain: Goku

On Dimension Bounds for Auxiliary Quantum SystemsResearch Paper

Expressions of several capacity regions in quantum information theory involve an optimization over auxiliary quantum registers. Evaluating such expressions requires bounds on the dimension of the Hilbert space of these auxiliary registers, for which no non-trivial technique is known; we lack a quantum analog of the Carath'{e}odory theorem. In this paper, we…

25 thms2 active usersReviewed
Quantum Information·Captain: Goku

The private classical capacity and quantum capacity of a quantum channelResearch Paper

A formula for the capacity of a quantum channel for transmitting private classical information is derived. This is shown to be equal to the capacity of the channel for generating a secret key, and neither capacity is enhanced by forward public classical communication. Motivated by the work of Schumacher and Westmoreland on quantum privacy and quantum…

20 thms2 active usersReviewed
Quantum Information·Captain: Goku

Zero-error communication under discrete-time Markovian dynamicsResearch Paper

Consider an open quantum system with (discrete-time) Markovian dynamics. Our task is to store information in the system in such a way that it can be retrieved perfectly, even after the system is left to evolve for an arbitrarily long time. We show that this is impossible for classical (resp. quantum) information precisely when the dynamics is mixing (resp.…

45 thms2 active usersReviewed
Quantum Information·Captain: Goku

One-Shot Manipulation of Dynamical Quantum ResourcesResearch Paper

We develop a unified framework to characterize one-shot transformations of dynamical quantum resources in terms of resource quantifiers, establishing universal conditions for exact and approximate transformations in general resource theories. Our framework encompasses all dynamical resources represented as quantum channels, including those with a specific…

30 thms2 active usersReviewed
Quantum Information·Captain: Goku

Lower bound on entanglement in subspaces defined by Young diagramsResearch Paper

Eigenvalues of 1-particle reduced density matrices of NNN-fermion states are upper bounded by 1/N1/N1/N, resulting in a lower bound on entanglement entropy. We generalize these bounds to all other subspaces defined by Young diagrams in the Schur-Weyl decomposition of ⊗NCd\otimes^N\mathbb{C}^d⊗NCd.

15 thms2 active usersReviewed
Quantum Information·Captain: Goku

The mother of all protocols: Restructuring quantum information's family treeResearch Paper

We give a simple, direct proof of the "mother" protocol of quantum information theory. In this new formulation, it is easy to see that the mother, or rather her generalization to the fully quantum Slepian-Wolf protocol, simultaneously accomplishes two goals: quantum communication-assisted entanglement distillation, and state transfer from the sender to the…

24 thms2 active usersReviewed
Quantum Information·Captain: Goku

Universal recovery maps and approximate sufficiency of quantum relative entropyResearch Paper

The data processing inequality states that the quantum relative entropy between two states ρ\rhoρ and σ\sigmaσ can never increase by applying the same quantum channel N\mathcal{N}N to both states. This inequality can be strengthened with a remainder term in the form of a distance between ρ\rhoρ and the closest recovered state (R∘N)(ρ)(\mathcal{R} \circ \mathcal{N})(\rho)(R∘N)(ρ),…

15 thms2 active usersReviewed
Quantum Information·Captain: Goku

Upper Bounds on the Distillable Randomness of Bipartite Quantum StatesResearch Paper

The distillable randomness of a bipartite quantum state is an information-theoretic quantity equal to the largest net rate at which shared randomness can be distilled from the state by means of local operations and classical communication. This quantity has been widely used as a measure of classical correlations, and one version of it is equal to the…

24 thms2 active usersReviewed
Quantum Information·Captain: Goku

Necessary and Sufficient Conditions on Measurements of Quantum ChannelsResearch Paper

Quantum supermaps are a higher-order generalization of quantum maps, taking quantum maps to quantum maps. It is known that any completely positive, trace non-increasing (CPTNI) map can be performed as part of a quantum measurement. By providing an explicit counterexample we show that, instead, not every quantum supermap sending a quantum channel to a CPTNI…

18 thms2 active usersReviewed
Quantum Information·Captain: Goku

Strong Converses for Quantum Channel Capacities from Blowing-Up LemmataResearch Paper

A quantum channel can transmit quantum states, classical messages, or classical messages that remain secret from its environment. We prove exponential strong converses for all three tasks over arbitrary finite-dimensional memoryless quantum channels, at their respective regularized capacities and allowing arbitrary entangled inputs across channel uses and…

9 thms2 active usersReviewed
Quantum Information·Captain: Goku

A Generalized Stein Lemma for Quantum ChannelsResearch Paper

We prove a generalized quantum Stein lemma for parallel discrimination of an arbitrary finite-dimensional channel against families of alternative channels. The alternatives are compact and convex, closed under tensor products, and contain a faithful replacer. At every fixed type-I error tolerance, the optimal type-II error exponent equals the regularized…

34 thms2 active usersReviewed
Quantum Information·Captain: Goku

An exponential strong converse for private communication over degradable quantum channelsResearch Paper

We prove an exponential strong converse for the unassisted private capacity of every finite-dimensional degradable quantum channel. We use a single error criterion: the infidelity between the actual message-estimate-environment state and an ideal state consisting of uniformly distributed, perfectly correlated messages that are independent of the…

28 thms2 active usersReviewed
Quantum Information·Captain: Goku

Minimal output entropy for the channels that add or remove a box of a Young diagram, and a Pauli principle for every permutation symmetryResearch Paper

Two irreducible representations of U(d)U(d)U(d) whose Young diagrams differ by a single box are connected by four covariant quantum channels: the box can be removed or added, and one keeps either the new diagram or the box (Cd\mathbb{C}^dCd or its dual). We prove that for each of these channels the output of a coherent state majorizes every other output, so that…

6 thms2 active usersReviewed
Quantum Information·Captain: Goku

Quantum hypothesis testing of non-mixed-unitarity: A multifaceted hierarchy of quantum channel discriminationResearch Paper

Given multiple uses of an unknown quantum channel, we determine whether it is a specified non-mixed-unitary channel or belongs to the set of mixed-unitary channels. Formulating this as a composite channel hypothesis testing problem, we characterize the Stein exponents achievable by parallel strategies under progressively weaker restrictions on probe states…

27 thms2 active usersReviewed
Quantum Information·Captain: Goku

Approximate majorization and high-order capacity of quantum depolarizing channelsResearch Paper

A central challenge in quantum information theory is to determine whether entanglement provides an advantage for information processing when coherent operations across multiple channel uses are allowed. For depolarizing channels, King's proof of the additivity of the minimum output entropy rules out such an advantage for classical communication at leading…

19 thms2 active usersReviewed
Quantum Information·Captain: Goku

From Symmetry to Secrecy: Covariant Classical--Quantum Wiretap ChannelsResearch Paper

For classical--quantum wiretap channels with a transitive covariant input action, both output ensembles admit a description as unitary group orbits of fixed seed states. We use this structure to construct finite-block preprocessing schemes whose private information is an entropy difference evaluated at two distributions related by group convolution.…

32 thms2 active usersReviewed
Quantum Information·Captain: Goku

Quantitative upper bounds for certain quantum channel divergencesResearch Paper

We show that completely positive maps can be decomposed into sums of submaps which are close in completely bounded trace norm but as far apart as possible in terms of geometric channel fidelity. We then show that this kind of behavior extends to a large class of quantum channel divergences. We construct quantitative norm estimates for quantum channel…

33 thms2 active usersReviewed
Quantum Information·Captain: Goku

Maximal coherence of quantum measurement and the resource theory of sharpnessResearch Paper

A resource theory of quantum measurement can be addressed in terms of quantum coherence and measurement sharpness, respectively. The former analyzes the off-diagonal structure of POVM elements in a predetermined basis while the latter analyzes the deviation from trivial, state-independent, measurements. We establish a direct connection between the two…

9 thms2 active usersReviewed
Quantum Information·Captain: Goku

Hierarchy of Rényi Coherent Information in Stabilizer CodesResearch Paper

Rényi coherent information, a computable proxy for the von Neumann coherent information, is widely used to study mixed-state phases of matter and decodability transitions in noisy quantum error-correcting codes. However, being a difference of two Rényi entropies, it need not be monotonic in the Rényi index, and lacks the operational meaning of its von…

15 thms2 active usersReviewed
PreviousPage 26 of 34Next

Top contributors

RankContributorAccepted solutionsSubmitted problems
1FIfizzyinc3287472
2SHshivm41212
3MAMazecto256251
4MAmarwahaha144197
5NINickrobbins9514247
6KMkmehltretter821385
7ECEthan Cheung Wang1370
8MRMrnaiq9219
9ALAlien608689
10MRmrfancypants760

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me