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?
We prove an exponential strong converse for the unassisted private capacity of every finite-dimensional degradable quantum channel. We use a single error criterion: the infidelity between the actual message-estimate-environment state and an ideal state consisting of uniformly distributed, perfectly correlated messages that are independent of the environment. At every rate strictly above the channel's maximum coherent information, the optimized fidelity to this ideal state decays exponentially in the number of channel uses. The same bound holds when the ideal environment state is fixed to the actual environment marginal. The proof applies to arbitrary mixed-state encoders and arbitrary collective decoders. Its main operator ingredient is an overlap bound for privacy tests: two receiver placements with a common subsystem of dimension have overlap at most , where is the key size, independently of both shield dimensions. We combine this bound with the signed averaging construction presented in arXiv:2608.01308 and a single-filter reduction to symmetric states. A Gaussian filter replaces the common receiver subsystem by a system of controlled dimension from which the original correlations can be approximately recovered using quantum side information. The filter preserves exact exchange symmetry, and a uniform smooth-entropy estimate bounds its output dimension for arbitrary correlated channel inputs. We also obtain an exponential strong converse at zero for antidegradable channels under the same joint criterion and, consequently, for the private capacity of the quantum erasure channel throughout its parameter range. △ Less
This mission is the statement-level formalization of An exponential strong converse for private communication over degradable quantum channels (arXiv:2609.32515v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
23 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2.1 (Exponential strong converse) (Theorem 2.1 (Exponential strong converse), 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.
Two irreducible representations of whose Young diagrams differ by a single box are connected by four covariant quantum channels: the box can be removed or added, and one keeps either the new diagram or the box ( or its dual). We prove that for each of these channels the output of a coherent state majorizes every other output, so that coherent states minimize the output entropy, and we compute the optimal output explicitly in terms of hook lengths. For the two channels that keep the box we also determine all minimizers; these need not be coherent, even when they are pure. As an application we consider particles with a given permutation symmetry and find sharp bounds on the spectrum of the reduced density matrix of a single particle, as well as the exact set of spectra that mixed states can reach (for fermions these are the Pauli principle and Coleman's theorem). △ Less
This mission is the statement-level formalization of Minimal output entropy for the channels that add or remove a box of a Young diagram, and a Pauli principle for every permutation symmetry (arXiv:2609.33498v1). 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 Lemma 3.2: Tail-weight saturation (Lemma 3.2: Tail-weight saturation, PDF p. 14). 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.
36 results of the paper are not stated yet, because the library lacks an interface they need:
Given multiple uses of an unknown quantum channel, we determine whether it is a specified non-mixed-unitary channel or belongs to the set of mixed-unitary channels. Formulating this as a composite channel hypothesis testing problem, we characterize the Stein exponents achievable by parallel strategies under progressively weaker restrictions on probe states and auxiliary memory. In particular, we consider block-i.i.d. probes, which allow arbitrary correlations within blocks of fixed size while remaining i.i.d. across different blocks, and derive finite-letter expressions of the corresponding Stein exponents. Varying the block size, which interpolates between fully i.i.d. and arbitrary probes, together with further restrictions on intra-block correlations and access to auxiliary memory, results in a multifaceted hierarchy. We establish several strict separations within this hierarchy. Without auxiliary memory, we prove that fully i.i.d. probes yield a vanishing Stein exponent for every unital non-mixed-unitary channel, while blocks of three product probes suffice to obtain a strictly positive exponent for the qutrit Werner-Holevo channel. For block size two, although product probes seem to be insufficient for -covariant channels, an entangled probe achieves a strictly positive exponent for the qutrit Werner-Holevo channel, even though every maximally entangled probe fails. In contrast, access to auxiliary memory makes fully i.i.d. probes sufficient by yielding a strictly positive exponent for every non-mixed-unitary channel, even without requiring input-reference entanglement, and this exponent admits a lower bound determined by the diamond-norm distance from the mixed-unitary set. Moreover, for odd-dimensional Werner-Holevo channels, we find that this exponent is infinite, with every full-Schmidt-rank pure state being optimal. △ Less
This mission is the statement-level formalization of Quantum hypothesis testing of non-mixed-unitarity: A multifaceted hierarchy of quantum channel discrimination (arXiv:2609.40355v1). 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 (seed paper result): finite-letter BIID_k Stein exponents (Theorem 1 (seed paper result): finite-letter BIID_k Stein exponents, 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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
A central challenge in quantum information theory is to determine whether entanglement provides an advantage for information processing when coherent operations across multiple channel uses are allowed. For depolarizing channels, King's proof of the additivity of the minimum output entropy rules out such an advantage for classical communication at leading asymptotic order, while leaving open the possibility of an advantage for higher orders. In this work, we conjecture a majorization relation for the outputs of depolarizing channels and prove an approximate version of this conjecture. Our proof combines an exact ordering of shifted log-determinants with an anti-concentration bound for the spectrum of the product-state output, refining King's analysis based on Schatten norms. As a direct application, we obtain a tight third-order expansion for the classical capacity of quantum depolarizing channels. Consequently, entangled codewords and collective decoding can improve the message size over the product-coding strategy by at most bits, sharpening our understanding of the role of entanglement in the finite-blocklength regime. △ Less
This mission is the statement-level formalization of Approximate majorization and high-order capacity of quantum depolarizing channels (arXiv:2609.37240v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Third-order classical capacity of the depolarizing channel (Theorem 2, Eq. (5), 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.
For classical--quantum wiretap channels with a transitive covariant input action, both output ensembles admit a description as unitary group orbits of fixed seed states. We use this structure to construct finite-block preprocessing schemes whose private information is an entropy difference evaluated at two distributions related by group convolution. Applying the construction to product groups allows correlations across any fixed number of channel uses. We give a sufficient condition for the associated uniform-input bound to equal the single-use private information. Constant-composition channel codes and universal hashing achieve the resulting rates, with trace-distance leakage controlled by sandwiched Rényi information. For uniform outer randomization, the representation structure reduces the comparison-state optimization to Eve's invariant states. For the hybrid binary channel considered by Tikku, Berta and Renes, numerical optimization at three and four uses gives rates above our numerical estimate of the optimized noisy-repetition benchmark wherever that estimate is positive on the tested grid. The improvement comes from noise distributions beyond the family of independent physical flips and a symmetric logical flip. We also prove nonadditivity at an explicit channel parameter using a two-use encoder, an analytic single-use converse, and certified entropy bounds. Finally, we relate the hybrid model to binary phase-shift keying with a fixed receiver measurement. △ Less
This mission is the statement-level formalization of From Symmetry to Secrecy: Covariant Classical--Quantum Wiretap Channels (arXiv:2610.03580v1). 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 Theorem IV.1: covariant preprocessing identity and bounds (Theorem IV.1: covariant preprocessing identity and bounds, 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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
We determine the optimal success probability for transmitting a fixed number of classical messages through a finite number of uses of the quantum erasure channel, assisted by noiseless classical feedback and without initial shared entanglement. For an input dimension , an erasure probability , a blocklength , and equiprobable messages, the optimal success probability is equal to , where is binomial with parameters and . The converse allows arbitrary adaptive quantum encoders, quantum memories, and receiver instruments. Its main ingredient is an elementary dimension bound for noiseless quantum communication with classical feedback, proved by fixing the classical controls without conditioning the sender's state on the observed transcript. A classical protocol that transmits the base- digits of an integer representing the message, repeating each digit until the receiver acknowledges its reception or the prescribed blocklength is reached, attains the bound for every integer . We also establish a relative-majorization property of erasure-channel outputs and exactly evaluate a hypothesis-testing converse, recovering the same numerical bound without feedback. That converse need not be achievable without feedback: four uses of the qubit erasure channel and four messages give a strict gap. A product-state code employing tetrahedral qubit states nevertheless outperforms every classical binary erasure code with these parameters. We give an explicit message-size formula and show that the bounded-remainder normal approximation and the average-success strong-converse exponent are unchanged without feedback. We also determine the feedback-assisted error exponent below capacity, prove that it agrees with the no-feedback exponent above a critical rate, and give no-feedback bounds at lower rates. △ Less
This mission is the statement-level formalization of Finite-blocklength classical communication over the quantum erasure channel with and without classical feedback (arXiv:2610.00440v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Simultaneous relative majorization of erasure outputs (Theorem 5.1, PDF p. 19). 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.
10 results of the paper are not stated yet, because the library lacks an interface they need:
We show that completely positive maps can be decomposed into sums of submaps which are close in completely bounded trace norm but as far apart as possible in terms of geometric channel fidelity. We then show that this kind of behavior extends to a large class of quantum channel divergences. We construct quantitative norm estimates for quantum channel divergences in terms of the Arveson-Radon-Nikodym theorem. △ Less
This mission is the statement-level formalization of Quantitative upper bounds for certain quantum channel divergences (arXiv:2610.16270v1). 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 Theorem 4.6: geometric fidelity under a common ARN frame (Theorem 4.6, PDF p. 14). 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 investigate converse bounds on the average decoding error probability in finite-blocklength classical-quantum channel coding. We first present a lower bound for multiple quantum hypothesis testing in terms of pairwise trace distances and derive a corresponding fidelity bound. We then obtain a spectrum-based converse that depends only on the a priori probabilities and spectra of the states. We show that the converse bound remains tight for the quantum depolarizing channel under suitable conditions. For codes with product-state outputs, this converse takes an explicit form involving products of output-state eigenvalues. We apply it to binary codes over the quantum amplitude damping channel using the input states and . For this setting, we also discuss a normal approximation to the spectrum-based converse in the large blocklength regime. In all numerical examples considered, the spectrum-based converse is tighter than the other converse bounds at low noise levels. △ Less
This mission is the statement-level formalization of A Spectrum-Based Converse for Quantum State Discrimination and Its Applications to Classical-Quantum Channel Coding (arXiv:2610.06840v1). 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 Theorem 4 (Spectral converse); seed paper result (Theorem 4 (Spectral converse); 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.
6 results of the paper are not stated yet, because the library lacks an interface they need:
We prove that four capacities of single-mode bosonic dephasing channels coincide under an average photon-number constraint: the unassisted quantum capacity, the unassisted private capacity, the two-way classically assisted quantum capacity, and the two-way public-classically assisted private capacity. The assistance may be interactive: the parties can exchange classical messages between channel uses and choose subsequent inputs based on earlier outcomes. For every finite value of the constraint, their common value is the coherent information optimized over Fock-diagonal input states satisfying the constraint. The proof uses a relative entropy comparison with the completely dephasing channel to derive chain rules for the Rains relative entropy and the relative entropy of entanglement. These chain rules give an upper bound on the rates achievable by adaptive protocols whose mean input photon number is constrained on average over all channel uses. We also show that both chain rules are attained by canonical purifications of finite-energy Fock-diagonal states. △ Less
This mission is the statement-level formalization of No advantage from classical assistance for energy-constrained bosonic dephasing channels (arXiv:2610.13854v1). 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 Fock dephasing absorbs bosonic dephasing on either side (Lemma 2.2, Eq. (23), 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.
13 results of the paper are not stated yet, because the library lacks an interface they need:
Coherences between different energy levels are strongly constrained by thermodynamics. Here we ask a related question: if several coherence transfers can be optimized separately, can they also be optimized simultaneously by the same thermodynamic process? We show that this is in general a compatibility problem. Using an energy-resolved Stinespring representation of thermal operations, we express elementary coherence-transfer amplitudes as inner products of bath-weighted vectors associated with total-energy shells. Saturation of the corresponding Cauchy--Schwarz bounds requires these vectors to be collinear. Since all transfers have to arise from the same energy-preserving system--bath unitary, such saturation conditions cannot in general be imposed independently. Trace and Gibbs preservation lead to additional phase-closure conditions and to polygon inequalities that can rule out simultaneous saturation for fixed population-transfer data. We complement these analytic results with a rigorous computer-assisted semidefinite-program analysis. For the mixed-degenerate Hamiltonian , machine-certified primal and dual bounds show that no covariant Gibbs-preserving channel can simultaneously attain three individually optimal directional coherence transfers. Since every thermal operation is covariant and Gibbs preserving, the same triple of -optimal values cannot be attained by a thermal operation. We also analyze auxiliary Choi-sector Gram matrices for mixed-degenerate ladders. Under specified directional rank assumptions, positivity imposes range-inclusion conditions, from which we obtain conditional non-genericity statements for physical joint saturation. △ Less
This mission is the statement-level formalization of Limitations on Joint Coherence Transfer in Quantum Thermodynamics (arXiv:2608.11872v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
31 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Paper seed / Theorem 5: certified incompatibility of three CGP-optimal directional transfers (Paper seed / Theorem 5: certified incompatibility of three CGP-optimal directional transfers, PDF p. 18). 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:
The temporal Clauser-Horne-Shimony-Holt (CHSH) inequality witnesses the nonclassicality of temporal correlations, but its violation is generally degraded by environmental noise. Here, we show that violation of the temporal CHSH inequality can be revived through coherent control of noisy quantum evolutions. We compare two physically distinct implementations: coherent control of noisy evolutions induced by interaction of the system with independent environments, and coherent control of two physically distinct, unitarily equivalent Stinespring dilations of the same noisy channel. Although these constructions generate identical deterministic system dynamics, they induce distinctly different post-selected evolutions. With a focus on the amplitude damping channel (ADC), we show that coherent control of equivalent dilations extend the range of temporal CHSH inequality violation well beyond both the incoherently controlled, or deterministic, scenario and what is achievable with independent environments. Under setting-independent post-selection of the coherent control implementation, the resulting violation further certifies that the channel is not strongly CHSH nonlocality-breaking. Our results identify the choice of Stinespring dilation as an operationally relevant resource in coherently controlled tests of temporal quantum correlations. △ Less
This mission is the statement-level formalization of Coherent Control of Channel Dilations Activate Temporal Bell Nonclassicality (arXiv:2607.05643v1). 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 Dilation choice strictly enlarges equatorial temporal-CHSH activation (Abstract / §§IV–V: dilation choice strictly enlarges equatorial temporal-CHSH activation, 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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
A resource theory of quantum measurement can be addressed in terms of quantum coherence and measurement sharpness, respectively. The former analyzes the off-diagonal structure of POVM elements in a predetermined basis while the latter analyzes the deviation from trivial, state-independent, measurements. We establish a direct connection between the two resource theories by identifying measurement sharpness as the maximal coherence that is achievable under all possible unitary changes of the reference basis. For a broad class of POVMs whose elements share a common eigenbasis, we show that the maximal distance-based coherence of measurement coincides exactly with the corresponding distance-based sharpness monotone. We further extend this equivalence, with element-additive distances, to POVMs whose elements admit a common mutually unbiased basis structure. These results provide a measurement-theoretic analogue of the maximal-coherence & purity correspondence for quantum states. We also show that the maximal coherence of measurement is faithful with respect to trivial measurements and is monotonic under fuzzifying operations for dichotomic measurements, as well as under mixed-unitary and unitarily covariant preprocessing channels. Finally, we illustrate the operational meaning and limitations of the equivalence through qubit POVMs, single-photon phase sensing, and noisy photon-number resolving detection. In particular, the maximal Fisher information in a Mach-Zehnder interferometer is shown to be determined by the squared maximal coherence of the measurement, while in an imperfect photon-number resolving detector the maximal coherence behaves as a proper sharpness monotone, unlike conventional PVM-based unsharpness measures. △ Less
This mission is the statement-level formalization of Maximal coherence of quantum measurement and the resource theory of sharpness (arXiv:2607.05847v1). 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 Common-MUB equivalence for spectral distance (§III B, Eq. (32), 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.
11 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum coherence is a central resource in quantum information science, yet general frameworks and constraints governing its dynamics remain limited. Although quantum coherence lacks a general monotonicity law, we establish an exact integral fluctuation theorem (FT) for coherence dynamics, formulated in terms of Kirkwood-Dirac (KD) quasiprobability trajectories and valid for arbitrary initial states and dynamics. This integral FT deviates from the standard unit-valued form, and the complex deviation, termed the anomaly, quantifies a weighted overlap between the residual final-state coherence and the coherence generated from the dephased input. The real part of the anomaly yields bounds on coherence change, while its imaginary part constrains the second-order moment of the stochastic coherence change weighted by the imaginary parts of the KD quasiprobabilities. Our results establish general statistical constraints on coherence dynamics, demonstrating the utility and broad applicability of FTs for studying quantum-resource dynamics. △ Less
This mission is the statement-level formalization of Anomaly fluctuation theorem for quantum coherence dynamics (arXiv:2609.06632v1). 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 Anomaly bounded by output coherence and cohering power (Eq.(5), 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:
Rényi coherent information, a computable proxy for the von Neumann coherent information, is widely used to study mixed-state phases of matter and decodability transitions in noisy quantum error-correcting codes. However, being a difference of two Rényi entropies, it need not be monotonic in the Rényi index, and lacks the operational meaning of its von Neumann counterpart. Here we address both issues for stabilizer codes. First, for Pauli noise generated by independent Bernoulli events, we prove that the Rényi- coherent information is nondecreasing in . This follows from a general theorem: if independent random bits are mapped linearly to a fine label and a coarse label , then the Rényi entropy difference is nondecreasing in . For stabilizer codes, is the joint syndrome--logical class and is the syndrome, and the difference is the Rényi- coherent information up to a constant. The same theorem covers classical linear codes and independent detector error models. Second, for arbitrary stochastic Pauli noise, we give the Rényi- coherent information an operational meaning via postselection on matching syndromes between one data block and auxiliary blocks. We determine when this defines a quantum channel and show that saturation of the Rényi- coherent information is equivalent to asymptotically perfect recovery of the postselected channel. Moreover, the Rényi- coherent information also upper-bounds the ordinary coherent information achievable after any syndrome-conditioned recovery. △ Less
This mission is the statement-level formalization of Hierarchy of Rényi Coherent Information in Stabilizer Codes (arXiv:2609.11930v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Corollary 1.1 / abstract: stabilizer-code Rényi hierarchy (Corollary 1.1 / abstract: stabilizer-code Rényi hierarchy, 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.
18 results of the paper are not stated yet, because the library lacks an interface they need:
Coherence-generating power (CGP) tells how much coherence a quantum process produces on average from incoherent inputs, but an average can hide where that coherence comes from. We introduce the coherence-generating power deviation (CGPD), the standard deviation of the generated Hilbert--Schmidt coherence over the uniform simplex of incoherent states. CGPD turns coherence generation into a landscape: a small value signals robust production across input populations, whereas a large value reveals selective conversion of particular population imbalances. By representing unitary coherence generation as a quadratic response on population space, we obtain exact first and second moments in arbitrary finite dimension. We prove that every nontrivial unitary generator must fluctuate, and we separate this unavoidable isotropic fluctuation from excess anisotropy. The resulting distinction between average strength and input selectivity has direct consequences for benchmarking, reliability guarantees, input-ensemble susceptibility, and four-copy measurement protocols; it also extends naturally to unital quantum channels. Matched quantum-walk and quasiperiodic-transport examples show that topology and localization can leave CGP unchanged while substantially changing CGPD, revealing structure invisible to the mean alone. △ Less
This mission is the statement-level formalization of Coherence-generating power deviation: Fluctuations and input selectivity beyond average coherence generation (arXiv:2609.19046v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
34 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3, Exact coherence moments (original paper seed) (Theorem 3, Exact coherence moments (original paper seed), 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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We obtain a complete characterization of eventually entanglement breaking (EEB) unital channels in terms of some simple commutation properties of their eigenvectors. Specifically, the following properties are equivalent for a unital channel: (i) it is EEB; (ii) it is eventually positive partial transpose (PPT); (iii) it is eventually mixed twisted dephasing; and (iv) its eigenvectors corresponding to non-zero eigenvalues commute with all its peripheral eigenvectors. Similar results hold for one-parameter semigroups of unital quantum channels, where continuity forces such semigroups to become primitive. We employ a matrix integral technique inspired by a result of Watrous. We also characterize the extreme points of the convex set of unital EB channels and, using this characterization and the theory of equiangular tight frames (ETFs), identify several extreme points beyond the twisted dephasing channels. △ Less
This mission is the statement-level formalization of A complete characterization of eventually entanglement breaking unital quantum channels (arXiv:2609.24168v1). 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 6.11: seven equivalent eventual channel properties (Theorem 6.11, PDF p. 24). 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 develop a general framework for higher-order quantum resources that treats the resourcefulness of quantum states, channels, and supermaps (also called processes) in a unified manner. By generalizing well-established concepts from resource theories of states and channels, we introduce and study supermap resource monotones and supermap distillation and dilution. As free supermaps, we consider free networks (supermaps that can be implemented with free channels), compatible supermaps (sets of supermaps closed under arbitrary composition), and maximally free superchannels. Specializing to approximate channel-to-channel conversions, we show that under mild assumptions, the conversion error with respect to the diamond distance and the worst-case infidelity coincide. We then apply the general framework to resource theories of dynamical coherence, where we establish the existence of largest sets of compatible supermaps. By characterizing these sets with semidefinite constraints, we show that they are strictly larger than the corresponding free networks but do not contain all maximally free superchannels. We finish by investigating the operational differences of these sets in one-shot channel distillation and dilution, providing solutions for both tasks in the parallel setting and for dilution in the adaptive setting. △ Less
This mission is the statement-level formalization of The Structure of Higher-Order Quantum Resources with an Application to Coherence (arXiv:2609.40186v1). 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 Lemma 18: four explicit DIO channels used as compatibility testers (Lemma 18, PDF p. 25). 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.
20 results of the paper are not stated yet, because the library lacks an interface they need:
This work studies the placement of an entanglement source along a communication line formed by two noisy qubit channels. Recent work argued, on analytical and numerical grounds, that midpoint placement should be at least as favorable as endpoint placement. Here it is shown that, for arbitrary qubit channels, if a sequential composition can preserve entanglement, then the corresponding parallel action cannot annihilate all entanglement. The proof uses the transpose-factorization criterion introduced in that recent work. Quantum Sinkhorn scaling converts every strictly positive qubit channel into a unital representative, and the special normal form of unital qubit channels then yields the required factorization of the transposed map through the original channel. Depolarizing regularization and the closedness of the set of entanglement-breaking channels extend the result to arbitrary channels. Consequently, implies , and, by exchanging the two channels, the same holds for the opposite composition order. This proves the recent conjecture that midpoint placement is optimal for all qubit channels, in the feasibility sense in which that optimality was originally defined. △ Less
This mission is the statement-level formalization of Feasibility Ordering of Entanglement-Source Placement for Qubit Channels (arXiv:2609.18803v1). 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 Parallel EA implies sequential EB (Theorem 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.
The direct static capacity region of a bipartite quantum state describes its asymptotic conversion into classical communication, quantum communication, and entanglement, with all communication directed from Alice to Bob. This paper gives a unified entropic converse for this region. The proof treats generated and consumed resources simultaneously and derives all three information inequalities for one local instrument. Its main ingredients are no-signalling, the chain rule, strong subadditivity, and continuity of conditional entropy. A supporting-hyperplane characterization leads to the static capacity formula, which is helpful in determining single-letterization of the capacity region. For a pure state of entanglement entropy subjected to erasure with probability , the complete region is the convex hull of and , plus the unit-resource cone. This statement holds for arbitrary collective instruments by using subset-entropy inequalities related to earlier methods used for the dynamic capacity region of the erasure channel. Complete characterizations also hold for symmetrically extendible states and locally flagged pure-state mixtures. For maximally correlated states, the optimization over local instruments admits an exact matrix formulation and an additive outer bound. An explicit qubit example shows that a nonorthogonal discarded quantum memory can outperform every efficient instrument and every instrument with conditionally commuting discarded states. For states obtained by qubit dephasing of Schmidt-aligned pure states, an exact threshold characterizes when the static capacity formula vanishes, at every blocklength and after regularization. Full single-letter characterizations for general Hadamard states and for the remaining trade-offs for dephased states remain open, with sufficient additivity conditions identified. △ Less
This mission is the statement-level formalization of Static classical-quantum-entanglement trade-offs: an entropic converse and single-letter characterizations (arXiv:2609.23298v1). 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 §8.2.4: matrix score as a weighted coherence difference (§8.2.4: matrix score as a weighted coherence difference, PDF p. 36). 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.
36 results of the paper are not stated yet, because the library lacks an interface they need:
Encrypted quantum cloning distributes an unknown -qubit state among encrypted clones so that no individual clone reveals the input, yet the state can be recovered from any one clone together with a common quantum key. We ask the inverse question: for a fixed encoding architecture, which multipartite pure states can serve as exact resources for this task? For , we completely characterize the pure resources compatible with a sector-wise two-Pauli encoder, with necessity holding for arbitrary completely positive trace-preserving (CPTP) recovery maps. For even , exact recovery requires maximal entanglement across the signal--noise cut. For odd , less entanglement can suffice, provided that the surviving signal correlations have the structure selected by the encoder. We further show, without fixing the encoder, that exact recovery from every authorized subsystem already implies perfect concealment of each individual signal and requires at least ebits of signal--noise entanglement. For graph states, the resource classification reduces to an exact condition on the kernel of the signal--noise cut matrix, leading to binary certification and constructive Clifford recovery. We identify rank-deficient graph resources that attain the architecture-independent entanglement bound and prove that the entire Dicke family, including states, is excluded for every sector-wise two-Pauli encoder. Our results show that encrypted recovery depends not only on how much entanglement a resource contains, but also on how its correlations are organized relative to the encoder. △ Less
This mission is the statement-level formalization of Beyond Maximal Entanglement : Exact Resources for Multiparty Encrypted Quantum Cloning (arXiv:2609.28241v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
40 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (seed): Exact fixed-encoder pure-resource criterion (Theorem 1 (seed): Exact fixed-encoder pure-resource criterion, 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:
For a channel on written in the generalised Bloch parameterisation , we prove that entanglement breaking implies , where denotes the nuclear norm. The bound is attained in every dimension by the completely dephasing channel, and at by an explicit family with . The qubit case reads and extends to full rank a rank-two condition of Ruskai. The proof sharpens Ruskai's bound by retaining the POVM completeness relation , which her argument discards; this recentres from a second moment into a cross-covariance, and is the entire content of the improvement. △ Less
This mission is the statement-level formalization of A sharp norm inequality for entanglement-breaking channels (arXiv:2609.27906v1). 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 (§3): sharp EB nuclear-norm inequality, including its qubit specialization (Theorem 1 (§3): sharp EB nuclear-norm inequality, including its qubit specialization, 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:
Suppose Alice and Bob can transform one shared mixed state into another by local operations and classical communication, and can also recover the first state from the second. What can change in such a conversion? We give a complete classification of reversible conversions between two-qutrit states. We consider exact deterministic LOCC transformations of a single copy, allowing finite protocols and the countable protocols specified here. Local flags are known to allow a separable part to be replaced by local preparation while an entangled block is retained. We prove that such a decomposition is necessary for two mutually convertible entangled states that are not locally unitarily equivalent. The two parts are distinguishable by local measurements. The entangled blocks have the same weight and are locally unitarily equivalent after normalization. Each entangled state has a unique smallest retained block. Two entangled states are reversibly convertible if and only if these unnormalized blocks are locally unitarily equivalent. For a state with negative partial transpose, the smallest block can be found using the negative eigenspace of its partial transpose and at most three matrix zero tests. △ Less
This mission is the statement-level formalization of Complete Classification of Reversible Entanglement Transformations of Two Qutrits (arXiv:2610.05234v1). 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 Lemma E1: joint-kernel obstruction (Lemma E1: joint-kernel obstruction, 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.
16 results of the paper are not stated yet, because the library lacks an interface they need:
We study entanglement distillation under operations that remain completely positive under partial-transpose conjugation, a.k.a. PPT channels, in the standard quantum Shannon theory regime of asymptotically vanishing but non-zero error. Our main results are: (a) a regularised formula for the PPT distillable entanglement in terms of a measured-relative-entropy-like quantity; and (b) two different single-letter converses, one based on operator quadratic forms and the other on Hirschman's strengthening of the Hadamard three-line theorem. As an immediate application of (b), we show that the PPT distillable entanglement can be strictly smaller than the regularised Rains bound, thereby resolving an open problem in the theory of entanglement manipulation [Regula et al., NJP 21:103017, 2019]. A gap appears already for Werner states: at antisymmetric weight , a certified upper bound of ebits lies below the (regularised) Rains bound, which equals ebits. On a different note, (a) implies a faithful lower bound on the PPT distillable entanglement in terms of the entanglement negativity, which provides a quantitative counterpart to the qualitatively known fact that any NPT state is PPT distillable [Eggeling et al., PRL 87:257902, 2001]. △ Less
This mission is the statement-level formalization of On PPT entanglement distillation (arXiv:2610.12454v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Regularized formula for PPT distillable entanglement (Theorem1, 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.
18 results of the paper are not stated yet, because the library lacks an interface they need:
The detection and quantification of quantum entanglement are central problems in quantum information science. Based on the realignment of density matrices and the vectorization of reduced density matrices, we construct a family of enhanced separability criteria for bipartite and multipartite quantum systems. Our criteria recover the previously proposed realignment-based criteria as special cases and detect more entanglement than the earlier ones. Moreover, we derive tighter lower bounds for the concurrence and the convex-roof extended negativity, criteria for detecting the genuine tripartite entanglement, and lower bounds on genuine-multipartite-entanglement concurrence. The advantages of our results are demonstrated with detailed examples. △ Less
This mission is the statement-level formalization of Separability criteria and lower bounds of entanglement via realignment (arXiv:2610.15664v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Arbitrary-rank bipartite separability criterion (Theorem 1, 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:
Communication using quantum channels generally requires encoding and decoding on many identical uses of a quantum channel. In practical settings, decoherence may severely limit our ability to do so, potentially rendering each channel use nonidentical. Given nonidentical channels, we present an entanglement-assisted encoding and decoding strategy that yields a channel with higher worst-case fidelity than all of the given channels. The strategy is universal, in the sense that the improvement holds regardless of what channels are given, as long as they satisfy mild assumptions on their initial entanglement fidelities. Our protocol is optimal when the given channels are depolarizing channels, and is essentially the unique one that is universal. This idea can also be extended to classical channels, where shared randomness between the sender and the receiver allows universal enhancement of the probability of correct transmission. We then consider general quantum resource theories, providing a necessary condition and a sufficient condition for the possibility of such universal improvement of quantum resources. △ Less
This mission is the statement-level formalization of Universal Improvement of Channel Fidelity via Entanglement Assistance (arXiv:2610.05669v1). 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 Unnumbered: shared-randomness protocol and identity-biased improvement (Unnumbered: shared-randomness protocol and identity-biased improvement, 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.
25 results of the paper are not stated yet, because the library lacks an interface they need: