Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A unitary interaction coupling two parties enables quantum communication in both the forward and backward directions. Each communication capacity can be thought of as a tradeoff between the achievable rates of specific types of forward and backward communication. Our first result shows that for any bipartite unitary gate, coherent classical communication is no more difficult than classical communication -- they have the same achievable rate regions. Previously this result was known only for the unidirectional capacities (i.e., the boundaries of the tradeoff). We then relate the tradeoff curve for two-way coherent communication to the tradeoff for two-way quantum communication and the tradeoff for coherent communiation in one direction and quantum communication in the other.
This mission is the statement-level formalization of Bidirectional coherent classical communication (arXiv:quant-ph/0412126v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Bidirectional coherification with arbitrary signed entanglement (Theorem 1, Eqs. (2)–(3), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
A general method for proving continuity of the von Neumann entropy on subsets of positive trace-class operators is considered. This makes it possible to re-derive the known conditions for continuity of the entropy in more general forms and to obtain several new conditions. The method is based on a particular approximation of the von Neumann entropy by an increasing sequence of concave continuous unitary invariant functions defined using decompositions into finite rank operators. The existence of this approximation is a corollary of a general property of the set of quantum states as a convex topological space called the strong stability property. This is considered in the first part of the paper.
This mission is the statement-level formalization of Continuity of the von Neumann entropy (arXiv:0904.1963v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1: barycentric representation of the closed convex hull (Lemma 1: barycentric representation of the closed convex hull, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
19 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper we study the problem of calculating the convex hull of certain affine algebraic varieties. As we explain, the motivation for considering this problem is that certain pure-state measures of quantum entanglement, which we call polynomial entanglement measures, can be represented as affine algebraic varieties. We consider the evaluation of certain mixed-state extensions of these polynomial entanglement measures, namely convex and concave roofs. We show that the evaluation of a roof-based mixed-state extension is equivalent to calculating a hyperplane which is multiply tangent to the variety in a number of places equal to the number of terms in an optimal decomposition for the measure. In this way we provide an implicit representation of optimal decompositions for mixed-state entanglement measures based on the roof construction.
This mission is the statement-level formalization of Convex Hulls of Varieties and Entanglement Measures Based on the Roof Construction (arXiv:quant-ph/0402055v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Both roofs are graph-hull fiber extrema (Lemma 2.2: roofs are graph-hull fiber extrema, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
7 results of the paper are not stated yet, because the library lacks an interface they need:
A class of problems in quantum information theory, having an elementary formulation but still resisting solution, concerns the additivity properties of various quantities characterizing quantum channels, notably the "classical capacity", and the "maximal output purity". All known results, including extensive numerical work, are consistent with the conjecture that these quantities are indeed additive (resp. multiplicative) with respect to tensor products of channels. A proof of this conjecture would have important consequences in quantum information theory. In particular, according to this conjecture, the classical capacity or the maximal purity of outputs cannot be increased by using entangled inputs of the channel. In this paper we state the additivity/multiplicativity problems, give some relations between them, and prove some new partial results, which also support the conjecture.
This mission is the statement-level formalization of On some additivity problems in quantum information theory (arXiv:math-ph/0003002v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Depolarizing products: multiplicativity and explicit purities (§5, Theorem (i)-(iii): multiplicativity and explicit depolarizing purities, PDF p. 11). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Despite the great promise of quantum machine learning models, there are several challenges one must overcome before unlocking their full potential. For instance, models based on quantum neural networks (QNNs) can suffer from excessive local minima and barren plateaus in their training landscapes. Recently, the nascent field of geometric quantum machine learning (GQML) has emerged as a potential solution to some of those issues. The key insight of GQML is that one should design architectures, such as equivariant QNNs, encoding the symmetries of the problem at hand. Here, we focus on problems with permutation symmetry (i.e., the group of symmetry ), and show how to build -equivariant QNNs. We provide an analytical study of their performance, proving that they do not suffer from barren plateaus, quickly reach overparametrization, and generalize well from small amounts of data. To verify our results, we perform numerical simulations for a graph state classification task. Our work provides the first theoretical guarantees for equivariant QNNs, thus indicating the extreme power and potential of GQML.
This mission is the statement-level formalization of Theoretical Guarantees for Permutation-Equivariant Quantum Neural Networks (arXiv:2210.09974v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (Variance of partial derivatives) (Theorem 1 (Variance of partial derivatives); seed paper result, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
9 results of the paper are not stated yet, because the library lacks an interface they need:
We address the question of the multiplicativity of the maximal p-norm output purities of bosonic Gaussian channels under Gaussian inputs. We focus on general Gaussian channels resulting from the reduction of unitary dynamics in larger Hilbert spaces. It is shown that the maximal output purity of tensor products of single-mode channels under Gaussian inputs is multiplicative for any p>1 for products of arbitrary identical channels as well as for a large class of products of different channels. In the case of p=2 multiplicativity is shown to be true for arbitrary products of generic channels acting on any number of modes.
This mission is the statement-level formalization of Multiplicativity of maximal output purities of Gaussian channels under Gaussian inputs (arXiv:quant-ph/0406065v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract/main result: Gaussian maximal-output-purity multiplicativity (Abstract/main result: Gaussian maximal-output-purity multiplicativity, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum information characteristics, such as quantum mutual information, loss, noise and coherent information are explicitly calculated for Bosonic attenuation/amplification channel with input Gaussian state. The coherent information is shown to be negative for the values of the attenuation coefficient .
This mission is the statement-level formalization of Sending Quantum Information with Gaussian States (arXiv:quant-ph/9809022v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal output and the three entropies (§4, unnumbered main result: thermal output and all three entropies, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
The existing unconditional security definitions of quantum key distribution (QKD) do not apply to joint attacks over QKD and the subsequent use of the resulting key. In this paper, we close this potential security gap by using a universal composability theorem for the quantum setting. We first derive a composable security definition for QKD. We then prove that the usual security definition of QKD still implies the composable security definition. Thus, a key produced in any QKD protocol that is unconditionally secure in the usual definition can indeed be safely used, a property of QKD that is hitherto unproven. We propose two other useful sufficient conditions for composability. As a simple application of our result, we show that keys generated by repeated runs of QKD degrade slowly.
This mission is the statement-level formalization of The Universal Composable Security of Quantum Key Distribution (arXiv:quant-ph/0409078v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §4.2: ideal KD has perfect equality, uniformity and privacy (§4.2: ideal KD has perfect equality, uniformity and privacy, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
8 results of the paper are not stated yet, because the library lacks an interface they need:
The classical asymptotic equipartition property is the statement that, in the limit of a large number of identical repetitions of a random experiment, the output sequence is virtually certain to come from the typical set, each member of which is almost equally likely. In this paper, we prove a fully quantum generalization of this property, where both the output of the experiment and side information are quantum. We give an explicit bound on the convergence, which is independent of the dimensionality of the side information. This naturally leads to a family of Renyi-like quantum conditional entropies, for which the von Neumann entropy emerges as a special case.
This mission is the statement-level formalization of A Fully Quantum Asymptotic Equipartition Property (arXiv:0811.1221v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Fully quantum asymptotic equipartition property (Theorem 1 (AEP), equations (6)-(7); original paper-level seed, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We present two approaches for transmitting classical information over quantum broadcast channels. The first technique is a quantum generalization of the superposition coding scheme for the classical broadcast channel. We use a quantum simultaneous nonunique decoder and obtain a proof of the rate region stated in [Yard et al., IEEE Trans. Inf. Theory 57 (10), 2011]. Our second result is a quantum generalization of the Marton coding scheme. The error analysis for the quantum Marton region makes use of ideas in our earlier work and an idea recently presented by Radhakrishnan et al. in arXiv:1410.3248. Both results exploit recent advances in quantum simultaneous decoding developed in the context of quantum interference channels.
This mission is the statement-level formalization of Classical codes for quantum broadcast channels (arXiv:1111.3645v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: superposition coding inner bound (Theorem 1: superposition coding inner bound (paper seed), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
We report a deterministic and exact protocol to reverse any unknown qubit-unitary operation, which simulates the time inversion of a closed qubit system. To avoid known no-go results on universal deterministic exact unitary inversion, we consider the most general class of protocols transforming unknown unitary operations within the quantum circuit model, where the input unitary operation is called multiple times in sequence and fixed quantum circuits are inserted between the calls. In the proposed protocol, the input qubit-unitary operation is called 4 times to achieve the inverse operation, and the output state in an auxiliary system can be reused as a catalyst state in another run of the unitary inversion. We also present the simplification of the semidefinite programming for searching the optimal deterministic unitary inversion protocol for an arbitrary dimension presented by M. T. Quintino and D. Ebler [Quantum , 679 (2022)]. We show a method to reduce the large search space representing all possible protocols, which provides a useful tool for analyzing higher-order quantum transformations for unitary operations.
This mission is the statement-level formalization of Reversing Unknown Qubit-Unitary Operation, Deterministically and Exactly (arXiv:2209.02907v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: deterministic exact four-call inversion (Theorem 1: deterministic exact four-call qubit-unitary inversion, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
5 results of the paper are not stated yet, because the library lacks an interface they need:
Two new relative entropy quantities, called the min- and max-relative entropies, are introduced and their properties are investigated. The well-known min- and max- entropies, introduced by Renner, are obtained from these. We define a new entanglement monotone, which we refer to as the max-relative entropy of entanglement, and which is an upper bound to the relative entropy of entanglement. We also generalize the min- and max-relative entropies to obtain smooth min- and max- relative entropies. These act as parent quantities for the smooth Renyi entropies, and allow us to define the analogues of the mutual information, in the Smooth Renyi Entropy framework. Further, the spectral divergence rates of the Information Spectrum approach are shown to be obtained from the smooth min- and max-relative entropies in the asymptotic limit.
This mission is the statement-level formalization of Min-and Max-Relative Entropies and a New Entanglement Monotone (arXiv:0803.2770v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
22 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (§V): max-relative entropy of entanglement is an entanglement monotone (Theorem 1 (§V): max-relative entropy of entanglement is an entanglement monotone, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
We propose a general method for studying properties of quantum channels acting on an n-partite system, whose action is invariant under permutations of the subsystems. Our main result is that, in order to prove that a certain property holds for any arbitrary input, it is sufficient to consider the special case where the input is a particular de Finetti-type state, i.e., a state which consists of n identical and independent copies of an (unknown) state on a single subsystem. A similar statement holds for more general channels which are covariant with respect to the action of an arbitrary finite or locally compact group. Our technique can be applied to the analysis of information-theoretic problems. For example, in quantum cryptography, we get a simple proof for the fact that security of a discrete-variable quantum key distribution protocol against collective attacks implies security of the protocol against the most general attacks. The resulting security bounds are tighter than previously known bounds obtained by proofs relying on the exponential de Finetti theorem [Renner, Nature Physics 3,645(2007)].
This mission is the statement-level formalization of Post-selection technique for quantum channels with applications to quantum cryptography (arXiv:0809.3019v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: postselection bound (Theorem 1: Post-Selection Theorem (seed paper result), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
A strong converse theorem for the classical capacity of a quantum channel states that the probability of correctly decoding a classical message converges exponentially fast to zero in the limit of many channel uses if the rate of communication exceeds the classical capacity of the channel. Along with a corresponding achievability statement for rates below the capacity, such a strong converse theorem enhances our understanding of the capacity as a very sharp dividing line between achievable and unachievable rates of communication. Here, we show that such a strong converse theorem holds for the classical capacity of all entanglement-breaking channels and all Hadamard channels (the complementary channels of the former). These results follow by bounding the success probability in terms of a "sandwiched" Renyi relative entropy, by showing that this quantity is subadditive for all entanglement-breaking and Hadamard channels, and by relating this quantity to the Holevo capacity. Prior results regarding strong converse theorems for particular covariant channels emerge as a special case of our results.
This mission is the statement-level formalization of Strong converse for the classical capacity of entanglement-breaking and Hadamard channels via a sandwiched Renyi relative entropy (arXiv:1306.1586v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exponential strong converse for entanglement-breaking and Hadamard channels (seed, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
The one-shot classical capacity of a quantum channel quantifies the amount of classical information that can be transmitted through a single use of the channel such that the error probability is below a certain threshold. In this work, we show that this capacity is well approximated by a relative-entropy-type measure defined via hypothesis testing. Combined with a quantum version of Stein's lemma, our results give a conceptually simple proof of the well-known Holevo-Schumacher-Westmoreland theorem for the capacity of memoryless channels. More generally, we obtain tight capacity formulas for arbitrary (not necessarily memoryless) channels.
This mission is the statement-level formalization of One-Shot Classical-Quantum Capacity and Hypothesis Testing (arXiv:1007.5456v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-sided one-shot classical-quantum capacity bounds (Theorem 1, (3): two-sided epsilon-one-shot classical-quantum capacity bounds, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
We describe a modification of the Alicki-Fannes-Winter method which allows to prove uniform continuity on the set of quantum states with bounded energy of any locally almost affine function having limited growth with increasing energy. Some applications in quantum information theory are considered. The asymptotic continuity of the relative entropy of entanglement and of its regularization under the energy constraint on one subsystem is proved. Channel-independent continuity bounds for the quantum mutual information at the output of a local channel and for the output Holevo quantity under the input energy constraint are obtained.
This mission is the statement-level formalization of Adaptation of the Alicki-Fannes-Winter method for the set of states with bounded energy and its use (arXiv:1609.07044v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 2: logarithmic-power spectral threshold (Lemma 2, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
15 results of the paper are not stated yet, because the library lacks an interface they need:
We are interested in the properties and relations of entanglement measures. Especially, we focus on the squashed entanglement and relative entropy of entanglement, as well as their analogues and variants. Our first result is a monogamy-like inequality involving the relative entropy of entanglement and its one-way LOCC variant. The proof is accomplished by exploring the properties of relative entropy in the context of hypothesis testing via one-way LOCC operations, and by making use of an argument resembling that by Piani on the faithfulness of regularized relative entropy of entanglement. Following this, we obtain a commensurate and faithful lower bound for squashed entanglement, in the form of one-way LOCC relative entropy of entanglement. This gives a strengthening to the strong subadditivity of von Neumann entropy. Our result improves the trace-distance-type bound derived in [Comm. Math. Phys., 306:805-830, 2011], where faithfulness of squashed entanglement was first proved. Applying Pinsker's inequality, we are able to recover the trace-distance-type bound, even with slightly better constant factor. However, the main improvement is that our new lower bound can be much larger than the old one and it is almost a genuine entanglement measure. We evaluate exactly the various relative entropy of entanglement under restricted measurement classes, for maximally entangled states. Then, by proving asymptotic continuity, we extend the exact evaluation to their regularized versions for all pure states. Finally, we consider comparisons and separations between some important entanglement measures and obtain several new results on these, too.
This mission is the statement-level formalization of Relative entropy and squashed entanglement (arXiv:1210.3181v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2, Eq. (8): commensurate lower bound for squashed entanglement (Theorem 2, Eq. (8): commensurate lower bound for squashed entanglement, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
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)). The present paper is a follow-up on this, and provides sharp upper bounds on the relative entropy in terms of the trace norm distance and of the smallest eigenvalues of both states concerned. The results obtained here are more general than the corresponding one from our previous work, and also corrects a mistake in one of its proofs. As a by-product, we obtain a sharp upper bound on the regularised relative entropy introduced by Lendi, Farhadmotamed and van Wonderen.
This mission is the statement-level formalization of Continuity bounds on the quantum relative entropy - II (arXiv:1105.2656v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Relative entropy bound using both smallest eigenvalues (Theorem 1: upper bound with both minimum eigenvalues (17)–(18), PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum f-divergences are a quantum generalization of the classical notion of f-divergences, and are a special case of Petz' quasi-entropies. Many well known distinguishability measures of quantum states are given by, or derived from, f-divergences; special examples include the quantum relative entropy, the Renyi relative entropies, and the Chernoff and Hoeffding measures. Here we show that the quantum f-divergences are monotonic under the dual of Schwarz maps whenever the defining function is operator convex. This extends and unifies all previously known monotonicity results. We also analyze the case where the monotonicity inequality holds with equality, and extend Petz' reversibility theorem for a large class of f-divergences and other distinguishability measures. We apply our findings to the problem of quantum error correction, and show that if a stochastic map preserves the pairwise distinguishability on a set of states, as measured by a suitable f-divergence, then its action can be reversed on that set by another stochastic map that can be constructed from the original one in a canonical way. We also provide an integral representation for operator convex functions on the positive half-line, which is the main ingredient in extending previously known results on the monotonicity inequality and the case of equality. We also consider some special cases where the convexity of f is sufficient for the monotonicity, and obtain the inverse Holder inequality for operators as an application. The presentation is completely self-contained and requires only standard knowledge of matrix analysis.
This mission is the statement-level formalization of Quantum f-divergences and error correction (arXiv:1008.2529v6). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
53 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract main result (p.1), pinned to Theorem 7.1 (Theorem 7.1 (abstract main result), PDF p. 33). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
9 results of the paper are not stated yet, because the library lacks an interface they need:
We prove a lower bound on the relative entropy between two finite-dimensional states in terms of their entropy difference and the dimension of the underlying space. The inequality is tight in the sense that equality can be attained for any prescribed value of the entropy difference, both for quantum and classical systems. We outline implications for information theory and thermodynamics, such as a necessary condition for a process to be close to thermodynamic reversibility, or an easily computable lower bound on the classical channel capacity. Furthermore, we derive a tight upper bound, uniform for all states of a given dimension, on the variance of the surprisal, whose thermodynamic meaning is that of heat capacity.
This mission is the statement-level formalization of Tight bound on relative entropy by entropy difference (arXiv:1304.0036v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
25 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Tight relative entropy bound and explicit equality witnesses (theorem1, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
We investigate Gaussian quantum states in view of their exceptional role within the space of all continuous variables states. A general method for deriving extremality results is provided and applied to entanglement measures, secret key distillation and the classical capacity of Bosonic quantum channels. We prove that for every given covariance matrix the distillable secret key rate and the entanglement, if measured appropriately, are minimized by Gaussian states. This result leads to a clearer picture of the validity of frequently made Gaussian approximations. Moreover, it implies that Gaussian encodings are optimal for the transmission of classical information through Bosonic channels, if the capacity is additive.
This mission is the statement-level formalization of Extremality of Gaussian quantum states (arXiv:quant-ph/0509154v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1, (2): general Gaussian extremality (original seed) (Lemma 1, (2): general Gaussian extremality (original seed), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
7 results of the paper are not stated yet, because the library lacks an interface they need:
Additivity of the Holevo capacity is proved for product channels, under the condition that one of the channels is in a certain class of unital qubit channels, with the other completely arbitrary. This qubit class includes the depolarizing channel. As a byproduct this proves that the Holevo bound is the ultimate information capacity of such qubit channels (assuming no prior entanglement between sender and receiver). Additivity of minimal entropy and multiplicativity of p-norms are also proved under the same assumptions.
This mission is the statement-level formalization of Additivity for a class of unital qubit channels (arXiv:quant-ph/0103156v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Unital qubit channels: norm multiplicativity and entropy and Holevo additivity (Theorem 1, equations (5)–(7), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
We derive one-shot upper bounds for quantum noisy channel codes. We do so by regarding a channel code as a bipartite operation with an encoder belonging to the sender and a decoder belonging to the receiver, and imposing constraints on the bipartite operation. We investigate the power of codes whose bipartite operation is non-signalling from Alice to Bob, positive-partial transpose (PPT) preserving, or both, and derive a simple semidefinite program for the achievable entanglement fidelity. Using the semidefinite program, we show that the non-signalling assisted quantum capacity for memoryless channels is equal to the entanglement-assisted capacity. We also relate our PPT-preserving codes and the PPT-preserving entanglement distillation protocols studied by Rains. Applying these results to a concrete example, the 3-dimensional Werner-Holevo channel, we find that codes that are non-signalling and PPT-preserving can be strictly less powerful than codes satisfying either one of the constraints, and therefore provide a tighter bound for unassisted codes. Furthermore, PPT-preserving non-signalling codes can send one qubit perfectly over two uses of the channel, which has no quantum capacity. We discuss whether this can be interpreted as a form of superactivation of quantum capacity.
This mission is the statement-level formalization of On the power of PPT-preserving and non-signalling codes (arXiv:1406.7142v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract main result; §V (49): non-signalling and entanglement-assisted quantum capacities coincide (Abstract main result; §V (49): non-signalling and entanglement-assisted quantum capacities coincide, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
4 results of the paper are not stated yet, because the library lacks an interface they need:
We study a protocol in which many parties use quantum communication to transfer a shared state to a receiver without communicating with each other. This protocol is a multiparty version of the fully quantum Slepian-Wolf protocol for two senders and arises through the repeated application of the two-sender protocol. We describe bounds on the achievable rate region for the distributed compression problem. The inner bound arises by expressing the achievable rate region for our protocol in terms of its vertices and extreme rays and, equivalently, in terms of facet inequalities. We also prove an outer bound on all possible rates for distributed compression based on the multiparty squashed entanglement, a measure of multiparty entanglement.
This mission is the statement-level formalization of Distributed Compression and Multiparty Squashed Entanglement (arXiv:0707.2792v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem II.1: multiparty distributed compression inner bound (seed paper result) (Theorem II.1: multiparty distributed compression inner bound (seed paper result), PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
We study the symmetric-side-channel-assisted private capacity of a quantum channel, for which we provide a single-letter formula. This capacity is additive, convex, and, for degradable channels, equal to the unassisted private capacity. While a channel's (unassisted) capacity for for private classical communication may be strictly larger than its quantum capacity, we will show that these capacities are equal for degradable channels, thus demonstrating the equivalence of privacy and quantum coherence in this context. We use these ideas to find new bounds on the key rate of quantum key distribution protocols with one-way classical post-processing. For the Bennett-Brassard-84 (BB84) protocol, our results demonstrate that collective attacks are strictly stronger than individual attacks.
This mission is the statement-level formalization of The private classical capacity with a symmetric side channel and its application to quantum cryptography (arXiv:0705.3838v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 (seed paper result): single-letter ss-private capacity (Theorem 5 (seed paper result): single-letter ss-private capacity, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need: