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?
The information-spectrum analysis made by Han for classical hypothesis testing for simple hypotheses is extended to a unifying framework including both classical and quantum hypothesis testing as well as fixed-length source coding, whereby general formulas for several quantities concerning the asymptotic optimality of tests/codes are established in terms of classical and quantum information spectrum. Generality of theorems and simplicity of proofs are fully pursued, and as byproducts some improvements on the original classical results are also obtained.
This mission is the statement-level formalization of An Information-Spectrum Approach to Classical and Quantum Hypothesis Testing for Simple Hypotheses (arXiv:quant-ph/0206185v2). 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 Theorem 1: general operational exponents equal spectral divergence rates (24)–(27) (Theorem 1: general operational exponents equal spectral divergence rates (24)–(27), PDF p. 7). 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:
The dynamic capacity theorem characterizes the reliable communication rates of a quantum channel when combined with the noiseless resources of classical communication, quantum communication, and entanglement. In prior work, we proved the converse part of this theorem by making contact with many previous results in the quantum Shannon theory literature. In this work, we prove the theorem with an "ab initio" approach, using only the most basic tools in the quantum information theorist's toolkit: the Alicki-Fannes' inequality, the chain rule for quantum mutual information, elementary properties of quantum entropy, and the quantum data processing inequality. The result is a simplified proof of the theorem that should be more accessible to those unfamiliar with the quantum Shannon theory literature. We also demonstrate that the "quantum dynamic capacity formula" characterizes the Pareto optimal trade-off surface for the full dynamic capacity region. Additivity of this formula simplifies the computation of the trade-off surface, and we prove that its additivity holds for the quantum Hadamard channels and the quantum erasure channel. We then determine exact expressions for and plot the dynamic capacity region of the quantum dephasing channel, an example from the Hadamard class, and the quantum erasure channel.
This mission is the statement-level formalization of The quantum dynamic capacity formula of a quantum channel (arXiv:1004.0458v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
19 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (Dynamic Capacity); seed paper result advertised on p.1 (Theorem 1 (Dynamic Capacity); seed paper result advertised on p.1, 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.
In the simple quantum hypothesis testing problem, upper bounds on the error probabilities are shown based on a key operator inequality between a density operator and its pinching. Concerning the error exponents, the upper bounds lead to a noncommutative analogue of the Hoeffding bound, which is identical with the classical counter part if the hypotheses, composed of two density operators, are mutually commutative. The upper bounds also provide a simple proof of the direct part of the quantum Stein's lemma.
This mission is the statement-level formalization of On Error Exponents in Quantum Hypothesis Testing (arXiv:quant-ph/0206151v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Pinched tests achieve every rate below relative entropy (Theorem 3, equations (54)–(55), 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.
8 results of the paper are not stated yet, because the library lacks an interface they need:
text of abstract (We present a utilitarian review of the family of matrix groups , in a form suited to various applications both in optics and quantum mechanics. We contrast these groups and their geometry with the much more familiar Euclidean and unitary geometries. Both the properties of finite group elements and of the Lie algebra are studied, and special attention is paid to the so-called unitary metaplectic representation of . Global decomposition theorems, interesting subgroups and their generators are described. Turning to -mode quantum systems, we define and study their variance matrices in general states, the implications of the Heisenberg uncertainty principles, and develop a U(n)-invariant squeezing criterion. The particular properties of Wigner distributions and Gaussian pure state wavefunctions under action are delineated.)
This mission is the statement-level formalization of The Real Symplectic Groups in Quantum Mechanics and Optics (arXiv:quant-ph/9509002v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
37 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §IV (4.20): Euler decomposition (seed paper result) (§IV (4.20): Euler decomposition (seed paper result), PDF p. 16). 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.
23 results of the paper are not stated yet, because the library lacks an interface they need:
We introduce a Gaussian version of the entanglement of formation adapted to bipartite Gaussian states by considering decompositions into pure Gaussian states only. We show that this quantity is an entanglement monotone under Gaussian operations and provide a simplified computation for states of arbitrary many modes. For the case of one mode per site the remaining variational problem can be solved analytically. If the considered state is in addition symmetric with respect to interchanging the two modes, we prove additivity of the considered entanglement measure. Moreover, in this case and considering only a single copy, our entanglement measure coincides with the true entanglement of formation.
This mission is the statement-level formalization of Gaussian Entanglement of Formation (arXiv:quant-ph/0306177v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Parametrization of pure Gaussian covariance matrices (Lemma 1, Eq.(16), 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.
13 results of the paper are not stated yet, because the library lacks an interface they need:
The von Neumann entropy at the output of a bosonic channel with thermal noise is analyzed. Coherent-state inputs are conjectured to minimize this output entropy. Physical and mathematical evidence in support of the conjecture is provided. A stronger conjecture--that output states resulting from coherent-state inputs majorize the output states from other inputs--is also discussed.
This mission is the statement-level formalization of Minimum output entropy of bosonic channels: a conjecture (arXiv:quant-ph/0404005v1). 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 Coherent outputs and attained entropy upper bounds (Eqs.(7)–(9), Appendix A: coherent outputs and attained upper 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.
8 results of the paper are not stated yet, because the library lacks an interface they need:
The information capacities and ``distillability'' of a quantum channel are studied in the presence of auxiliary resources. These include prior entanglement shared between the sender and receiver and free classical bits of forward and backward communication. Inequalities and trade-off curves are derived. In particular an alternative proof is given that in the absence of feedback and shared entanglement, forward classical communication does not increase the quantum capacity of a channel.
This mission is the statement-level formalization of Inequalities for quantum channels assisted by limited resources (arXiv:quant-ph/0406111v3). 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 A dephasing side channel cannot increase unassisted quantum capacity (§II B Eq.(16): a dephasing side channel cannot increase quantum capacity, 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.
27 results of the paper are not stated yet, because the library lacks an interface they need:
We show how to compute or at least to estimate various capacity-related quantities for Bosonic Gaussian channels. Among these are the coherent information, the entanglement assisted classical capacity, the one-shot classical capacity, and a new quantity involving the transpose operation, shown to be a general upper bound on the quantum capacity, even allowing for finite errors. All bounds are explicitly evaluated for the case of a one-mode channel with attenuation/amplification and classical noise.
This mission is the statement-level formalization of Evaluating Capacities of Bosonic Gaussian Channels (arXiv:quant-ph/9912067v1). 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 II.B, Eq.(2.9): finite-error transpose capacity bound (II.B, Eq.(2.9): finite-error transpose capacity bound, 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.
22 results of the paper are not stated yet, because the library lacks an interface they need:
The applications of the general formulae of channel capacity developed in the quantum information theory to evaluation of information transmission capacity of optical channel are interesting subjects. In this review paper, we will point out that the formulation based on only classical-quantum channel mapping model may be inadequate when one takes into account a power constraint for noisy channel. To define the power constraint well, we should explicitly consider how quantum states are conveyed through a transmission channel. Basing on such consideration, we calculate a capacity formula for an attenuated noisy optical channel with genreral Gaussian state input; this gives certain progress beyond the example in our former paper.
This mission is the statement-level formalization of Information capacity formula of quantum optical channels (arXiv:quant-ph/0105042v1). 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 Lossless number-state entropy maximum and capacity (Eqs.(58)-(59), PDF p. 15). 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 present a simplified framework for proving sequential composability in the quantum setting. In particular, we give a new, simulation-based, definition for security in the bounded-quantum-storage model, and show that this definition allows for sequential composition of protocols. Damgard et al. (FOCS '05, CRYPTO '07) showed how to securely implement bit commitment and oblivious transfer in the bounded-quantum-storage model, where the adversary is only allowed to store a limited number of qubits. However, their security definitions did only apply to the standalone setting, and it was not clear if their protocols could be composed. Indeed, we first give a simple attack that shows that these protocols are not composable without a small refinement of the model. Finally, we prove the security of their randomized oblivious transfer protocol in our refined model. Secure implementations of oblivious transfer and bit commitment then follow easily by a (classical) reduction to randomized oblivious transfer.
This mission is the statement-level formalization of Composable Security in the Bounded-Quantum-Storage Model (arXiv:0709.0492v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Measured BB84 uncertainty with explicit smoothing and positivity (Lemma 2.3, 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.
14 results of the paper are not stated yet, because the library lacks an interface they need:
By combining the Minkowski inequality and the quantum Chernoff bound, we derive easy-to-compute upper bounds for the error probability affecting the optimal discrimination of Gaussian states. In particular, these bounds are useful when the Gaussian states are unitarily inequivalent, i.e., they differ in their symplectic invariants.
This mission is the statement-level formalization of Computable bounds for the discrimination of Gaussian states (arXiv:0806.1625v2). 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 Minkowski spectral bound for Gaussian-state discrimination (Theorem 4, Eqs. (60)–(62), 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.
After proving a general no-cloning theorem for black boxes, we derive the optimal universal cloning of unitary transformations, from one to two copies. The optimal cloner is realized by quantum channels with memory, and greately outperforms the optimal measure-and-reprepare cloning strategy. Applications are outlined, including two-way quantum cryptographic protocols.
This mission is the statement-level formalization of Optimal cloning of unitary transformations (arXiv:0804.0129v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal universal one-to-two unitary cloning, with attaining channels (Theorem 1; Eqs. (8)–(10), 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:
In this paper we develop two types of tools to deal with differentiability properties of vectors in continuous representations of an infinite dimensional Lie group on a locally convex space . The first class of results concerns the space of smooth vectors. If is a Banach--Lie group, we define a topology on the space of smooth vectors for which the action of on this space is smooth. If is a Banach space, then is a Fr'echet space. This applies in particular to -dynamical systems , where is a Banach--Lie group. For unitary representations we show that a vector is smooth if the corresponding positive definite function is smooth. The second class of results concerns criteria for -vectors in terms of operators of the derived representation for a Banach--Lie group acting on a Banach space . In particular, we provide for each examples of continuous unitary representations for which the space of -vectors is trivial and the space of -vectors is dense.
This mission is the statement-level formalization of On Differentiable Vectors for Representations of Infinite Dimensional Lie Groups (arXiv:1002.1602v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Hilbert-valued smoothness and the inner-product kernel (Theorem 7.1, PDF p. 21). 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.
42 results of the paper are not stated yet, because the library lacks an interface they need:
We give two integrability criteria for representations of Banach--Lie algebras as skew-symmetric unbounded operators on a dense domain of a Hilbert space.
This mission is the statement-level formalization of Integrating representations of Banach--Lie algebras (arXiv:1003.0999v3). 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 Product rule for a strongly continuous operator path (Lemma 4, 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.
8 results of the paper are not stated yet, because the library lacks an interface they need:
We address the problem of the information-disturbance trade-off associated to the estimation of a quantum transformation, and show how the extraction of information about the a black box causes a perturbation of the corresponding input-output evolution. In the case of a black box performing a unitary transformation, randomly distributed according to the invariant measure, we give a complete solution of the problem, deriving the optimal trade-off curve and presenting an explicit construction of the optimal quantum network.
This mission is the statement-level formalization of Information - Disturbance Tradeoff in the Estimation of a Unitary Transformation (arXiv:1006.5665v2). 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 Attained optimal information–disturbance frontier (§IV C, Eqs.(30)–(34); abstract on PDF p.1, PDF p. 7). 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 analyze quantum algorithms for cloning of a quantum measurement. Our aim is to mimic two uses of a device performing an unknown von Neumann measurement with a single use of the device. When the unknown device has to be used before the bipartite state to be measured is available we talk about 1 -> 2 learning of the measurement, otherwise the task is called 1 -> 2 cloning of a measurement. We perform the optimization for both learning and cloning for arbitrary dimension of the Hilbert space. For 1 -> 2 cloning we also propose a simple quantum network that realizes the optimal strategy.
This mission is the statement-level formalization of Cloning of a quantum measurement (arXiv:1103.5709v2). 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 Optimal one-to-two measurement cloning fidelity (§V, Eq.(61): optimal one-to-two cloning fidelity (seed announced in abstract), PDF p. 7). 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:
A definition of the Schmidt number of a state of an infinite dimensional bipartite quantum system is given and properties of the corresponding family of Schmidt classes are considered. The existence of states with a given Schmidt number such that any their countable convex decomposition does not contain pure states with finite Schmidt rank is established. Partially entanglement breaking channels in infinite dimensions are studied. Several properties of these channels well known in finite dimensions are generalized to the infinite dimensional case. At the same time, the existence of partially entanglement breaking channels (in particular, entanglement breaking channels) such that all operators in any their Kraus representations have infinite rank is proved.
This mission is the statement-level formalization of The Schmidt number and partially entanglement breaking channels in infinite dimensions (arXiv:1110.4363v3). 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 Proposition 9B: exact k-PEB channels with only infinite-rank nonzero Kraus operators (Proposition 9B: exact k-PEB channels with only infinite-rank nonzero Kraus operators, PDF p. 12). 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 extend the mathematical theory of quantum hypothesis testing to the general -algebraic setting and explore its relation with recent developments in non-equilibrium quantum statistical mechanics. In particular, we relate the large deviation principle for the full counting statistics of entropy flow to quantum hypothesis testing of the arrow of time.
This mission is the statement-level formalization of Quantum Hypothesis Testing and Non-Equilibrium Statistical Mechanics (arXiv:1109.3804v2). 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 Proposition 1.1 (Proposition 1.1, 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.
40 results of the paper are not stated yet, because the library lacks an interface they need:
We study quantum learning algorithms for quantum measurements. The optimal learning algorithm is derived for arbitrary von Neumann measurements in the case of training with one or two examples. The analysis of the case of three examples reveals that, differently from the learning of unitary gates, the optimal algorithm for learning of quantum measurements cannot be parallelized, and requires quantum memories for the storage of information.
This mission is the statement-level formalization of Quantum learning algorithms for quantum measurements (arXiv:1103.0480v2). 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 Three-example qubit learning requires adaptation (Abstract; §V.C and Remark 1: optimal three-example qubit learning requires adaptation, 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:
In most communication schemes information is transmitted via travelling modes of electromagnetic radiation. These modes are unavoidably subject to environmental noise along any physical transmission medium and the quality of the communication channel strongly depends on the minimum noise achievable at the output. For classical signals such noise can be rigorously quantified in terms of the associated Shannon entropy and it is subject to a fundamental lower bound called entropy power inequality. Electromagnetic fields are however quantum mechanical systems and then, especially in low intensity signals, the quantum nature of the information carrier cannot be neglected and many important results derived within classical information theory require non-trivial extensions to the quantum regime. Here we prove one possible generalization of the Entropy Power Inequality to quantum bosonic systems. The impact of this inequality in quantum information theory is potentially large and some relevant implications are considered in this work.
This mission is the statement-level formalization of A generalization of the Entropy Power Inequality to Bosonic Quantum Systems (arXiv:1402.0404v2). 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 Three scalar thermal-entropy asymptotics (§IV.B Eq. (86); §VI.B Eqs. (103), (104), PDF p. 17). 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:
A consistent functional calculus approach to the spectral theorem for strongly commuting normal operators on Hilbert spaces is presented. In contrast to the common approaches using projection-valued measures or multiplication operators, here the functional calculus is not treated as a subordinate but as the central concept. Based on five simple axioms for a "measurable functional calculus", the theory of such calculi is developed in detail, including spectral theory, uniqueness results and construction principles. Finally, the functional calculus form of the spectral theorem is stated and proved, with some proof variants being discussed.
This mission is the statement-level formalization of The Functional Calculus Approach to the Spectral Theorem (arXiv:2003.06130v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
49 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 7.6 (Spectral Theorem: General Case) (Theorem 7.6 (Spectral Theorem: General Case), PDF p. 35). 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 show that the cross Wigner function can be written in the form where is the Fourier transform of and is a metaplectic operator that projects onto a linear symplectomorphism consisting of a rotation along an ellipse in phase space (or in the time-frequency space). This formulation can be extended to generic Weyl symbols and yields an interesting fractional generalization of the Weyl-Wigner formalism. It also provides a suitable approach to study the Bopp phase space representation of quantum mechanics, familiar from deformation quantization. Using the "metaplectic formulation" of the Wigner transform we construct a complete set of intertwiners relating the Weyl and the Bopp pseudo-differential operators. This is an important result that allows us to prove the spectral and dynamical equivalence of the Schr"odinger and the Bopp representations of quantum mechanics.
This mission is the statement-level formalization of Metaplectic formulation of the Wigner transform and applications (arXiv:1401.3388v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Periodicity, two elliptic invariants, and coordinate-pair rotations (Remark 5: periodicity and elliptic invariants, 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.
23 results of the paper are not stated yet, because the library lacks an interface they need:
We consider a quantum generalization of the classical heat equation, and study contractivity properties of its associated semigroup. We prove a Nash inequality and a logarithmic Sobolev inequality. The former leads to an ultracontractivity result. This in turn implies that the largest eigenvalue and the purity of a state with positive Wigner function, evolving under the action of the semigroup, decrease at least inverse polynomially in time, while its entropy increases at least logarithmically in time.
This mission is the statement-level formalization of Contractivity properties of a quantum diffusion semigroup (arXiv:1607.04242v6). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Order comparison of second derivatives at a common zero minimum (Lemma 3 (Appendix C), PDF p. 29). 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.
13 results of the paper are not stated yet, because the library lacks an interface they need:
We consider three different communication tasks for quantum broadcast channels, and we determine the capacity region of a Hadamard broadcast channel for these various tasks. We define a Hadamard broadcast channel to be such that the channel from the sender to one of the receivers is entanglement-breaking and the channel from the sender to the other receiver is complementary to this one. As such, this channel is a quantum generalization of a degraded broadcast channel, which is well known in classical information theory. The first communication task we consider is classical communication to both receivers, the second is quantum communication to the stronger receiver and classical communication to other, and the third is entanglement-assisted classical communication to the stronger receiver and unassisted classical communication to the other. The structure of a Hadamard broadcast channel plays a critical role in our analysis: the channel to the weaker receiver can be simulated by performing a measurement channel on the stronger receiver's system, followed by a preparation channel. As such, we can incorporate the classical output of the measurement channel as an auxiliary variable and solve all three of the above capacities for Hadamard broadcast channels, in this way avoiding known difficulties associated with quantum auxiliary variables.
This mission is the statement-level formalization of Hadamard quantum broadcast channels (arXiv:1611.07651v3). 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 2: exact classical capacity of a Hadamard broadcast channel (Theorem 2, §3.3: classical capacity of a Hadamard broadcast channel (seed paper result), 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 consider energy-constrained infinite-dimensional quantum channels from a given system (satisfying a certain condition) to any other systems. We show that dealing with basic capacities of these channels we may assume (accepting arbitrarily small error ) that all channels have the same finite-dimensional input space -- the subspace corresponding to the minimal eigenvalues of the input Hamiltonian. We also show that for the class of energy-limited channels (mapping energy-bounded states to energy-bounded states) the above result is valid with substantially smaller dimension . The uniform finite-dimensional approximation allows to prove the uniform continuity of the basic capacities on the set of all quantum channels with respect to the strong (pointwise) convergence topology. For all the capacities we obtain continuity bounds depending only on the input energy bound and the energy-constrained-diamond-norm distance between quantum channels (generating the strong convergence on the set of quantum channels).
This mission is the statement-level formalization of Uniform finite-dimensional approximation of basic capacities of energy-constrained channels (arXiv:1707.05641v2). 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 Monotonicity of the perspective of a nonnegative concave function (Lemma 1, 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.
8 results of the paper are not stated yet, because the library lacks an interface they need: