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?
Many two-party quantum protocols, such as oblivious transfer and password-based identification, start the same way: Alice sends Bob qubits encoding random bits in random BB84 bases . Their security proofs work only against a restricted Bob, for example one with bounded quantum memory (Damgård, Fehr, Salvail, Schaffner 2005). Unrestricted security is impossible for such tasks in the plain model.
Damgård, Fehr, Lunemann, Salvail and Schaffner (arXiv:0902.3918, CRYPTO 2009) proposed a generic commit-and-open compiler. Bob commits to his measurement bases and outcomes position by position. Alice opens a random fraction of the commitments and checks that wherever her basis agreed with Bob's. Their headline result, Theorem 4.2, says that the compiled protocol is computationally secure against any polynomial-time Bob. Its proof reduces everything computational to one information-theoretic statement: after the test, a dishonest Bob is β-benign (Definition 4.1), up to a negligible error. The paper's introduction presents this statement as the new tool. This mission formalizes it.
Alice holds qubits, one half of each of EPR pairs, in a register . Bob holds an arbitrary finite-dimensional register . The joint state right before the test is an arbitrary unit vector . This is the state after a dishonest Bob has received his halves and committed to and .
The test is a pair . is a uniformly random set of positions; for Alice's uniform bases is a uniform subset of . So . In the analysed version of the protocol (Fig. 4), Alice measures the positions in in Bob's bases and accepts iff for all . She then measures the remaining positions in her bases , producing .
The quantities of interest are:
A function is negligible if for every and all large .
The real cq state is . The set
collects the outcomes whose error rate on the unopened positions is predicted by the error rate on .
For every and there is a negligible such that, for every , , , finite and unit , there are unit vectors with
and such that, in the ideal state, every branch Alice accepts satisfies the bounds (1) of Definition 4.1:
No constant is hard-coded; is arbitrary.
The goal is what makes the compiler work. Combined with the security of the original protocol against benign Bob, it turns any BB84-type protocol that is secure in a restricted model into one secure against arbitrary dishonest Bob in the computational setting. The paper derives oblivious transfer and password-based identification this way (§6). The same statement also preserves bounded-quantum-storage security (§5.2). Its quantitative form, , shows how noise tolerance enters (§5.1).
The paper's headline Theorem 4.2 is computational: it quantifies over polynomial-time quantum adversaries and simulators in the common-reference-string model, with a dual-mode commitment scheme specified in prose. That wrapper is out of scope. The unconditional core claim, closing §4.3, is a statement about finite-dimensional states, entropies and a sampling distribution. To our knowledge no machine-checked proof of it, of Lemma 4.3, or of Corollary 4.4 exists. Formalizing it also produces reusable pieces: min- and max-entropy of superpositions, trace distance of pure and cq states, and a sampling bound for random subsets.
The statement mixes a quantum and a classical argument, and neither carries the whole weight. The obvious attempt, applying an entropic uncertainty relation directly to Bob's state, fails: Bob's register may be entangled with all of Alice's qubits, so nothing bounds its rank a priori. The bound appears only after the real state is replaced by a nearby one, and that replacement must be uniform over Bob's register and strategy. Uniformity is the delicate point: the negligible function must not depend on , , or the state.
The sampling step concerns sampling without replacement ( of fixed size), followed by an independent subsample that can be empty. The entropy bounds then need the Hamming-ball estimate at the real radius , valid only up to .
EuclideanSpace ℂ (Fin m → Bool)) and for a finite type E. Joint states are unit vectors of the product. The joint state is pure, which the paper argues is without loss of generality: a mixed state is purified and the purifier joins .Bool; bases are Bool with false = , true = . Positions are 0-based Fin m.Real.binEntropy divided by . The trace norm is the published WildeQIT.traceNorm, and the trace distance carries the factor .Contributions are welcome on any milestone. The sampling bound and the pure-state and block-diagonal trace-distance identities are independent of the rest. The trace-norm lemmas and the Hamming-ball bound are useful beyond this mission.
Photosynthetic light-harvesting complexes move an electronic excitation from the pigment that absorbed a photon to a reaction centre, where its energy is stored chemically. In the Fenna–Matthews–Olson (FMO) complex this transfer is close to lossless, and two-dimensional spectroscopy showed long-lived quantum coherence during it (Engel et al. 2007). This raised a concrete question in open-system quantum dynamics: does the environment, whose noise destroys coherence, hinder transport, or can it help?
Numerical studies of FMO models found that local dephasing raises transfer efficiency compared with purely coherent evolution (Mohseni et al. 2008; Plenio and Huelga 2008; Rebentrost et al. 2009). Caruso, Chin, Datta, Huelga and Plenio (arXiv:0901.4454, J. Chem. Phys. 2009) isolated a mechanism behind this in a model that can be solved exactly: the fully connected network (FCN). There, coherent evolution traps most of the excitation by destructive interference, and any amount of uniform dephasing removes the trap. This mission formalizes that exact result.
The network has sites. The single-excitation space has orthonormal basis : is the zero-exciton state (population lost to the environment), for is one excitation on site , and is the sink (the reaction centre). The operators and create and destroy the excitation on site .
The FCN Hamiltonian (with ) has , the site energies, and for every pair of distinct sites, and vanishes on and . For a real rate and an operator write
The state , a complex matrix, obeys the Lindblad master equation with
The terms are coherent hopping, dissipation to the environment at rates , pure dephasing at rates , and irreversible decay into the sink from a chosen site at rate . So . The initial state is , and transport is measured by the sink population
The goal concerns the FCN of §II.A: , , the sink attached at , and a uniform dephasing rate .
For , and :
The first limit is Eq. (5) of the paper. The second is the claim of §II.C, confirmed for uniform dephasing in Appendix A.3, Eq. (A30). The coupling , the sink rate and the dephasing rate are left free; neither limit depends on them.
The result. The noise-free limit shows that a perfectly coherent, fully symmetric network is a poor transporter: for only of the excitation reaches the sink, whereas a classical random walk on the same graph delivers all of it. The dephased limit shows that arbitrarily weak local noise restores complete transfer. Together they are the cleanest exactly solvable instance of dephasing-assisted transport. The invariant-subspace argument behind them (milestones 2–5) also predicts which states are protected from a sink, a mechanism related to coherent population trapping in quantum optics and condensed-matter systems.
Formalizing it. The paper derives these limits from Laplace-domain calculations and residue computations, some of them only sketched. A machine-checked proof would settle the exact constants, the hypotheses under which each limit holds (the necessity of and , and the case ), and the passage from the matrix exponential to the collective variables. As far as is known, none of these results has been formalized. The development also produces reusable pieces: the Lindblad generator of a single-excitation network with a sink, the trace identity (A7), and the spectrum of the complete-graph hopping Hamiltonian.
The obvious route is to compute , but acts on an -dimensional space for arbitrary , so no fixed-size computation applies. The noise-free limit hinges on an exact cancellation: of the weight lies in an -eigenspace that is invisible to the sink, and the remainder must be shown to drain completely, which is a statement about the spectrum of a non-normal generator on the complementary subspace. Under dephasing that invariant subspace no longer exists, but the reduced six-variable system still has to be shown to have as its only attracting steady state, for every and every . In the paper this is done through a final-value theorem applied to a fifth-order characteristic polynomial (A26), which is misprinted. A proof that the limit exists, and not only what it equals, is part of the task.
Fin (N + 2) in the paper's numbering (0 = zero-exciton state, 1…N = sites, N + 1 = sink), with natural-number indices cast into it. Operators are Matrix (Fin (N + 2)) (Fin (N + 2)) ℂ.semigroupEvolution of the published definition P16, that is, NormedSpace.exp of , applied to .A trivializing formalization is ruled out by construction: and are free, unfolds to an integral of an entry of the matrix exponential of the literal generator, and none of the limits is built into a definition.
Needed infrastructure includes calculus for (derivatives, HasDerivAt of entries, the fundamental theorem of calculus for ), invariant-subspace arguments for linear ODEs, and asymptotics of linear systems with a stable matrix. Contributions of general lemmas about Lindblad semigroups (trace preservation, Hermiticity preservation, stationary states) are welcome and reusable beyond this mission.
Not formalized here: Eq. (9) (static disorder), Eq. (10) (dissipation), §II.D–§V, the Laplace-domain route (A9)–(A13) and (A25)–(A29), the two-level system (A32), and the general networks of (A39)–(A40).
Positive maps give tests for entanglement in bipartite quantum states. A density matrix can pass one positive-map test and fail another, so the choice of map changes which states can be detected. Maps that behave predictably under unitary changes of basis are particularly structured, but that symmetry can appear restrictive. Bardet, Collins, and Sapra ask whether requiring unitary equivariance loses the ability to detect states that a given positive map detects. Their Theorem 5.1 says that it does not, provided one permits a sequence of larger output matrix algebras. Bardet, Collins, and Sapra, §5
The question sits between two familiar perspectives. The positive-map criterion tests a state by applying a map to one subsystem; unitary equivariance controls how that map reacts when the subsystem is rotated. The paper's result shows that a specified detector can be recovered, in the limit of a nested family, within this symmetric class. It addresses a fixed input map and a fixed ancillary dimension. The paper separately states a more uniform corollary about Schmidt number, but that corollary is outside this mission. Bardet, Collins, and Sapra, Theorem 5.1 and Corollary 5.4
Write for complex matrices and for their unitary group. A complex linear map is -positive if sends every positive semidefinite matrix on to a positive semidefinite matrix. It is completely positive if it is -positive for every natural number . A map is unitarily equivariant if, for each , there is one unitary satisfying for every . The choice of may depend on and , while the equality must hold for all . Bardet, Collins, and Sapra, Definition 2.1
A density matrix on is positive semidefinite and has trace one. The detection set of at ancillary dimension is
Here acts on the second tensor factor. A state outside is detected by : applying produces an operator that is not positive semidefinite. No trace preservation or unitality is required of . Bardet, Collins, and Sapra, equation (17)
Fix with and a -positive map that is not completely positive. The target is one family , chosen before any state , for which each member is unitarily equivariant and -positive, , and
Thus the family eventually detects every state detected by , and detection persists at later indices. The ancillary dimension is fixed before the family is chosen. Bardet, Collins, and Sapra, Theorem 5.1
The milestone statements cover the infinite dimensional lift of a linear map to , its inclusion , the finite dimensional invariant subspaces supplied by the Peter–Weyl decomposition, and the compression of the lift to such a subspace, which is a unitarily equivariant -positive matrix map with . These are the source's Lemma 5.3, Theorem 5.2 for its explicit witness, the consequence of equations (24)–(25) used in §5.2, and the compression step of the proof of Theorem 5.1 on pp. 14–15. The milestone for Theorem 5.2 names the particular fibrewise lift constructed in the paper as its witness and asserts its equivariance, its -positivity and the inclusion of detection sets. Bardet, Collins, and Sapra, §5.1–5.2
The theorem shows that symmetry alone does not prevent a positive map from detecting the states detected by a specified input map. It turns a single detector into a nested family with growing finite output dimensions, while keeping the same positivity order. The conclusion is pointwise in states but uses one sequence uniformly across all density matrices at the fixed ancillary dimension: each state outside is excluded from every sufficiently late . The result does not assert that any one finite output dimension suffices for every state. Bardet, Collins, and Sapra, Theorem 5.1
The paper proves this mathematical result. This mission records its statements in Lean, leaving proofs of the drafted goal and milestones to formalization work. The finite matrix definitions and the infinite dimensional interface can be reused for other questions about positive maps, regular representations, and finite dimensional compression. The published tensor superoperator and complete positivity definitions are shared with other quantum information developments rather than redefined here.
The immediate detector need not be unitarily equivariant. Replacing it by a single symmetric finite matrix map therefore gives no direct reason to preserve all of its detected states. The source passes through a fibrewise map indexed by every input unitary, so the intermediate output space is infinite dimensional. The remaining difficulty is to return to finite matrix outputs while retaining both equivariance and -positivity, and to choose the outputs so their detection sets are nested. A finite dimensional truncation without invariance under the regular action would not establish the claimed symmetry. Bardet, Collins, and Sapra, §5.1–5.2
Finite matrices are Matrix (Fin n) (Fin n) ℂ; positive semidefiniteness is Matrix.PosSemidef. The ancillary factor is first in Fin m × Fin n, and the existing QAlgorithms.idTensorSuperop applies the map to the second factor. Complete positivity is the published QAlgorithms.Entanglement.IsCompletelyPositive. The paper's indices become Lean natural numbers starting at zero. The density matrix test includes both positivity and trace one. The output dimensions form an actual function tending to infinity, and the maps form a dependent family whose codomain uses that function. The goal keeps the printed “not completely positive” hypothesis and all five stated conclusions. In particular, choosing detectors separately for each state would not meet it.
For the intermediate result, is a complex space over a Borel measure on . The lift is encoded by its sesquilinear form, whose kernel at is ; positivity on is tested by all block quadratic forms. A finite measure and two vectors make these integrals integrable because the matrix kernel is bounded. The regular action uses left invariance; the detection inclusion uses positivity of nonempty open sets; the Peter–Weyl milestone uses Haar probability measure. These are properties of the paper's Haar measure. The source's standing convention that linear maps preserve adjoints is already implied by -positivity for the goal and is not a separate assumption there. The general linear map in the lift milestones is stated exactly where the source permits it.
The development needs the shared matrix-map definitions, the and measure interfaces, and finite dimensional unitary representation theory. Work on the bounded-operator interpretation of the form, invariant truncations, and compression can be reused beyond this mission. The paper's inconsistent phrase “Schmidt number smaller than ” is not encoded, because the target uses only detection sets. Bardet, Collins, and Sapra, pp. 12–15
Measuring a quantum system disturbs it. The information–disturbance tradeoff asks how little a measurement that yields a given amount of information about an unknown state must change that state. The question underlies the security analysis of quantum key distribution, where an eavesdropper's information gain is paid for in detectable disturbance, and the design of measurements that must leave a system usable afterwards, as in sequential or weak measurement schemes.
A measurement has two separate parts: the POVM, which fixes the outcome statistics, and the instrument, which fixes the post-measurement state for each outcome. Many instruments realize the same POVM. The natural candidate for the least disturbing one is the square-root (Lüders) dynamics, which maps a state to on outcome . Whether this candidate is in fact optimal depends on how disturbance is averaged. H. Barnum (2002) showed that it is optimal when the average is over the uniform ensemble of pure states, and computed the resulting minimal disturbance for every POVM (arXiv:quant-ph/0205155). For general ensembles the same paper leaves optimality open (its "Possibility 4").
Fix a dimension and the Hilbert space with standard basis .
The unnormalized post-measurement state on outcome is , and the overall operation is .
The goal and the numbered milestones below are from Barnum, pp. 9–13, arXiv:quant-ph/0205155v1.
For every POVM and every finite instrument compatible with it,
The instrument may have several HK operators per outcome; this is what distinguishes Theorem 5 from Theorem 8.
Theorem 5 together with Theorem 8 gives a closed form for the minimal disturbance on the uniform ensemble of every POVM: (Eqs. (34)–(35)). For rank-one POVMs this is , one endpoint of the information–disturbance frontier that the rest of the paper studies. The result also shows that on this ensemble, extra Kraus operators per outcome never reduce disturbance, so the frontier may be computed over square-root instruments alone.
The milestones are of independent use. Lemma 9 and Eq. (32) are the standard second-moment formula for Haar-random pure states (the 2-design property). Eq. (33) is the Kraus-operator form of the average fidelity that appears throughout quantum channel benchmarking. Ando's concavity theorem is equivalent to Lieb's concavity theorem.
The results are proved in the paper (2002). This mission formalizes them; to the extent known, none of the paper's statements has a machine-checked proof. The platform already has the uniform ensemble and the average fidelity as published definitions, and Nielsen's formula relating average and entanglement fidelity, which is a different statement.
The polar-decomposition step suggests a pointwise argument: write and replace by . That fails. For a fixed , can exceed (take , , , ). The replacement is valid only after averaging over , through the explicit fourth-moment computation of Lemma 9. The second obstacle is merging several HK operators of one outcome into one, which needs Proposition 6. Proposition 6 is an inequality between non-commuting operators. The commuting case is elementary, but the general case rests on Ando's joint concavity, an operator-concavity theorem of Lieb's type that is not in Mathlib.
Operators are Matrix (Fin d) (Fin d) ℂ and vectors EuclideanSpace ℂ (Fin d), with 0 < d. The uniform ensemble is the published QAlgorithms.QuditFidelity.haarPureStateLaw d hd, the image of normalized Haar measure on the unitary group under . The average fidelity is the published averageFidelity d hd, whose integrand is . Disturbance is 1 - averageFidelity. POVMs are QAlgorithms.IsPOVM on a finite outcome type. An instrument is A : B → I → Matrix with one finite Kraus index type I for every outcome. Outcomes with fewer operators are padded with zeros, which changes neither the compatibility condition nor the operation. The square root is cfc Real.sqrt. Real powers in Theorem 7 use cfc of Real.rpow, so . Real-valued quadratic forms and traces of positive operators are taken as real parts. is defined entrywise.
The goal must not be read with I = Unit. That would be Theorem 8's one-term case, and the goal quantifies over every finite I. The ensemble is the Haar image itself, not a measure assumed to have the second moment of Lemma 9.
The wrapper disturbance accepts a raw superoperator, for which an integral need not exist. Every theorem here applies it only to a finite Kraus map, whose integrand is continuous and integrable on the Haar ensemble. A complete development needs Haar moment integrals on the unitary group (reusable for any unitary-design argument), the polar decomposition and the trace inequality for matrices, and an operator-concavity theorem (Ando/Lieb). Contributions of any of these, or of the commuting-case proof of Proposition 6 as a stepping stone, are welcome.
The time evolution of an open quantum system with no memory effects is described by a quantum dynamical semigroup (QDS): a family , , of completely positive, trace preserving maps on the density operators of a Hilbert space , with . Radiative decay, diffusion and dissipative state preparation are all modelled this way. For semigroups that are continuous in operator norm, Gorini, Kossakowski and Sudarshan (GKS76) and Lindblad (L76) showed in 1976 that the generator always has the form
with bounded operators , . Most physical generators are unbounded, and the corresponding semigroups are only strongly continuous. Davies (D77) introduced a "standard form" for such generators under additional assumptions, and Holevo (H97) and Fagnola extended the analysis. Holevo also exhibited generators that are not of standard form. Which strongly continuous QDS have a Lindblad-type generator built from Hilbert-space operators has therefore remained a structural question.
Alazzawi and Baumgartner (arXiv:1306.4531) answer it for trace preserving semigroups with a single condition, matrix normality, and prove an infinite-dimensional, unbounded version of the Kraus representation of completely positive maps along the way.
is a separable complex Hilbert space with inner product , conjugate-linear in the first slot. is the space of trace-class operators with the trace norm , and is the rank-one operator . The semigroup acts on , is completely positive and trace preserving, and is strongly continuous: as . Its generator is
the limit taken in trace norm, on the domain where it exists. A set is a core if its closure in the graph norm is all of .
For an orthonormal basis write and . The QDS is matrix normal if is a core for for some basis. It is not enough that : the paper's example is the Dirichlet Laplacian on an interval.
A generalized standard form of consists of operators (countably many) and on , densely defined, with the following properties. is closed and generates a strongly continuous semigroup on . Each is defined on and is relatively bounded with respect to . For all ,
Finally, the finite sums of such dyads form a core for . This is the paper's Definition 1, written in its own adjoint-free form (19)–(20).
and then : every basis that witnesses matrix normality carries a standard form whose contains in its domain.
The direction from matrix normality to the standard form (§3.1) runs through the following statements:
The converse direction (§3.2) consists of:
Theorem 3 identifies the trace preserving QDS whose generators admit a Lindblad-type description by Hilbert-space operators: they are exactly those determined by their action on the matrix units of a basis. Matrix normality is a condition on matrix elements, which can be checked from the differential equations that physical models provide. The standard form is the structure that dilation, stochastic-unravelling and conservativity results take as their input. Theorem 14 is of independent use: it is a Kraus decomposition, with no boundedness assumption, for completely positive maps into quadratic forms in infinite dimension.
The results are proved in the paper. None of them has a machine-checked proof that we know of. The finite-dimensional Choi-to-Kraus theorem is formalized on Prove2Me; the unbounded, form-valued version and the generator characterization are not. The mission formalizes the statements of §§2–3 and the Appendix exactly as printed. A faithful formal proof also has to settle the steps the paper only asserts: why the extend uniquely from to , and why (3) and the core property extend to all of .
Every operator in the standard form may be unbounded. The adjoints and are in general only "generalized operators" into an algebraic dual, so the familiar identities cannot be used as written. The obvious route, applying the Stinespring or Kraus theorem to , fails because is neither bounded nor defined on all of . The Choi matrix is itself only a quadratic form in infinite dimension, so the Kraus operators cannot be read off from a square root of a Choi operator. On the other side, the converse direction needs core arguments in two graph norms at once, on for and on for .
The trace class, trace norm and trace come from the published definitions QAlgorithms_Papers_Independent_Dependency50_P13, the semigroup and its trace-norm generator graph from QAlgorithms_Papers_Independent_Next46_P09, and contraction semigroups on from QAlgorithms_Papers_Independent_Claimed50_P50. The local module GenKraus.StdForm.Setting defines:
The formalization commits to the following conventions:
A formalization in which replaces the core condition, (4) is weakened to an inequality, or the core clause of Definition 1 is dropped, states a different and weaker theorem. These are excluded.
Corollary 17 (trace preserving gives bounded Kraus operators) is not used for Theorem 3 and is not included, and the two physical examples of §5 are illustrations without numbered claims. Contributions toward reusable infrastructure are welcome: generator cores, relatively bounded perturbations, the Lumer–Phillips theorem on Hilbert space, and Gram realizations of positive kernels.
NOON states, , put photons into one of two optical modes in coherent superposition. They are the standard example of a non-Gaussian, maximally path-entangled state of light and the resource behind phase estimation at the Heisenberg limit (Dowling, Contemp. Phys. 49, 2008). They are also fragile: they are hard to prepare with large and are degraded by loss and noise. A natural question is what happens when such a state is sent through a phase-insensitive amplifier, the device that compensates loss but must add noise by the laws of quantum mechanics (Caves, Phys. Rev. D 26, 1982).
G. S. Agarwal, S. Chaturvedi and A. Rai (arXiv:0912.5134, 2009) answer this question in closed form. For amplification of both modes with the same gain they derive the exact density matrix of the output for every gain, show that it is a two-mode photon-added thermal state, and use it to follow the entanglement of the amplified state. An earlier study by Agarwal and Chaturvedi (arXiv:0906.2743, 2009, the paper's ref. [9]) had found the gains at which Gaussian two-mode squeezed states lose their entanglement under the same amplifier; the NOON computation is the non-Gaussian counterpart.
Two bosonic modes and have the number basis , ( photons in , in ). An operator on the two-mode Fock space is described by its matrix . For an integer the input is
The amplifier of amplitude gain acts on one mode through the Kraus operators , , the weighted raising shifts
with all other entries zero. Symmetric amplification applies it to both modes:
the series converging in trace norm. The paper describes states also by the Q function , where is the two-mode coherent state. The amplified two-mode vacuum is the product thermal state
and , (and , ) are the -th powers of the creation and annihilation operators.
for all and , together with the facts that the output series converges in trace norm and that its limit is a density operator. This is the paper's main analytic result.
The result. Formula (17) gives every matrix element of the amplified NOON state at every gain. It identifies the output as a photon-added thermal state in which either mode carries the added photons, a family studied for single modes by Agarwal and Tara (Phys. Rev. A 46, 1992). The paper computes the partial transpose (18) of this matrix to obtain the logarithmic negativity of the amplified state as a function of gain (its Fig. 1), and observes that the zeros of the Q function, a signature of nonclassicality, survive amplification.
Formalizing it. The result is proved in the paper, by a phase-space argument; it has no machine-checked proof. A formal proof certifies the constants, the index shifts and the convergence of the infinite series, which the paper does not discuss, and produces a reusable two-mode layer (matrices, Kraus sums, coherent states, Q functions, photon addition) on top of the published single-mode Fock-space definitions.
The paper's route goes through the Q function: (13) is read off from the single-mode scaling law , and the density matrix (14) is then recognized from its Q function. The last step uses that a Q function determines the density operator, an analytic-continuation fact that is not in Mathlib, and neither step addresses convergence. The goal is a statement about a double infinite sum of operators in trace norm, not only about matrix entries: entrywise agreement of matrices does not by itself give trace-norm convergence of the Kraus series, nor that its limit is a positive, trace-one operator.
bipartiteKet (n, m) is . Operators come from the published module QAlgorithms_Papers_Independent_Dependency50_P39 (Fock spaces as , bounded operators, trace class, trace-norm summation TraceHasSum, densities, the amplifier matrix, coherent coefficients), which is referenced and not redefined.Dependency50.P39.amplifierHusimiScaling. The single-mode amplified vacuum (8) is part of the open Dependency50.P39.amplifierInputExamples; neither is posed again here.We show a continuity theorem for Stinespring's dilation: two completely positive maps between arbitrary C*-algebras are close in cb-norm iff we can find corresponding dilations that are close in operator norm. The proof establishes the equivalence of the cb-norm distance and the Bures distance for completely positive maps. We briefly discuss applications to quantum information theory.
This mission is the statement-level formalization of A Continuity Theorem for Stinespring's Dilation (arXiv:0710.2495v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Continuity of Stinespring dilation, with attainment and minimal direct sum (Theorem 1, (6)–(7), direct-sum refinement, 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.
Prior entanglement between sender and receiver, which exactly doubles the classical capacity of a noiseless quantum channel, can increase the classical capacity of some noisy quantum channels by an arbitrarily large constant factor depending on the channel, relative to the best known classical capacity achievable without entanglement. The enhancement factor is greatest for very noisy channels, with positive classical capacity but zero quantum capacity. Although such quantum channels can be simulated classically, no violation of causality is implied, because the simulation requires at least as much forward classical communication as the entanglement-assisted classical capacity of the channel being simulated. We obtain exact expressions for the entanglement-assisted capacity of depolarizing and erasure channels in d dimensions.
This mission is the statement-level formalization of Entanglement-Assisted Classical Capacity of Noisy Quantum Channels (arXiv:quant-ph/9904023v5). 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 Abstract main result / equation (3): depolarizing assisted capacity (Abstract main result / equation (3): depolarizing assisted capacity, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
4 results of the paper are not stated yet, because the library lacks an interface they need:
Squashed entanglement [Christandl and Winter, J. Math. Phys. 45(3):829-840 (2004)] is a monogamous entanglement measure, which implies that highly extendible states have small value of the squashed entanglement. Here, invoking a recent inequality for the quantum conditional mutual information [Fawzi and Renner, Commun. Math. Phys. 340(2):575-611 (2015)] greatly extended and simplified in various work since, we show the converse, that a small value of squashed entanglement implies that the state is close to a highly extendible state. As a corollary, we establish an alternative proof of the faithfulness of squashed entanglement [Brandao, Christandl and Yard, Commun. Math. Phys. 306:805-830 (2011)]. We briefly discuss the previous and subsequent history of the Fawzi-Renner bound and related conjectures, and close by advertising a potentially far-reaching generalization to universal and functorial recovery maps for the monotonicity of the relative entropy.
This mission is the statement-level formalization of Squashed entanglement, k-extendibility, quantum Markov chains, and recovery maps (arXiv:1410.4184v4). 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 Small squashed entanglement implies proximity to k-extendibility (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.
We classify extended Poincaré Lie super algebras and Lie algebras of any signature (p,q), that is Lie super algebras and Z_2-graded Lie algebras g = g_0 + g_1, where g_0 = so(V) + V is the (generalized) Poincaré Lie algebra of the pseudo Euclidean vector space V = R^{p,q} of signature (p,q) and g_1 = S is the spinor so(V)-module extended to a g_0-module with kernel V. The remaining super commutators {g_1,g_1} (respectively, commutators [g_1, g_1]) are defined by an so(V)-equivariant linear mapping vee^2 g_1 -> V (respectively, wedge^2 g_1 -> V). Denote by P^+(n,s) (respectively, P^-(n,s)) the vector space of all such Lie super algebras (respectively, Lie algebras), where n = p + q = dim V and s = p - q is the signature. The description of P^+-(n,s) reduces to the construction of all so(V)-invariant bilinear forms on S and to the calculation of three Z_2-valued invariants for some of them. This calculation is based on a simple explicit model of an irreducible Clifford module S for the Clifford algebra Cl_{p,q} of arbitrary signature (p,q). As a result of the classification, we obtain the numbers L^+-(n,s) = \dim P^+-(n,s) of independent Lie super algebras and algebras, which take values 0,1,2,3,4 or 6. Due to Bott periodicity, L^+-(n,s) may be considered as periodic functions with period 8 in each argument. They are invariant under the group Gamma generated by the four reflections with respect to the axes n=-2, n=2, s-1 = -2 and s-1 = 2. Moreover, the reflection (n,s) -> (-n,s) with respect to the axis s=0 interchanges L^+ and L^- : L^+(-n,s) = L^-(n,s).
This mission is the statement-level formalization of Classification of -(super)-extended Poincaré algebras and bilinear invariants of the spinor representation of (arXiv:math/9511215v1). 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 Paper result: real extension dimensions, periodicity and reflection supersymmetry (Paper result: real extension dimensions, periodicity and reflection supersymmetry, 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.
53 results of the paper are not stated yet, because the library lacks an interface they need:
The paper contains a detailed computation about the algebra of canonical commutation relation, the representation of the Weyl unitaries, the quasi-free states and their von Neumann entropy. The Markov triplet is defined by constant entropy increase. The Markov property of a quasi-free state is described by the representing block matrix. The proof is based on results on the statistical sufficiency in the quantum case. The relation to classical Gaussian Markov triplets is also described.
This mission is the statement-level formalization of Markov triplets on CCR-algebras (arXiv:0812.3724v2). 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 Markov quasifree triplets characterized by a separating projection (Theorem 2.3 (paper headline), 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.
12 results of the paper are not stated yet, because the library lacks an interface they need:
We present a functional calculus approach to the study of rates of decay in mean ergodic theorems for bounded strongly continuous operator semigroups. A central role is played by operators of the form , where is the generator of the semigroup and is a Bernstein function. In addition, we obtain some new results on Bernstein functions that are of independent interest.
This mission is the statement-level formalization of Bernstein functions and rates in mean ergodic theorems for operator semigroups (arXiv:1112.0286v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
30 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.4. (Theorem 3.4., 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.
5 results of the paper are not stated yet, because the library lacks an interface they need:
Reflection positivity originates from one of the Osterwalder-Schrader axioms for constructive quantum field theory. It serves as a bridge between euclidean and relativistic quantum field theory. In mathematics, more specifically, in representation theory, it is related to the Cartan duality of symmetric Lie groups (Lie groups with an involution) and results in a transformation of a unitary representation of a symmetric Lie group to a unitary representation of its Cartan dual. In this article we continue our investigation of representation theoretic aspects of reflection positivity by discussing reflection positive Markov processes indexed by Lie groups, measures on path spaces, and invariant gaussian measures in spaces of distribution vectors. This provides new constructions of reflection positive unitary representations.
This mission is the statement-level formalization of Reflection Positive Stochastic Processes Indexed by Lie Groups (arXiv:1510.07445v3). 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 Consistent convolution path laws and their sigma-finite extension (Lemma 4.8, PDF p. 30). 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.
28 results of the paper are not stated yet, because the library lacks an interface they need:
A host algebra of a (possibly infinite dimensional) Lie group is a -algebra whose representations are in one-to-one correspondence with certain continuous unitary representations . In this paper we present a new approach to host algebras for infinite dimensional Lie groups which is based on smoothing operators, i.e., operators whose range is contained in the space of smooth vectors. Our first major result is a characterization of smoothing operators that in particular implies smoothness of the maps . The concept of a smoothing operator is particularly powerful for representations which are semibounded, i.e., there exists an element for which all operators , , from the derived representation are uniformly bounded from above in some neighborhood of . Our second main result asserts that this implies that coincides with the space of smooth vectors for the one-parameter group . We then show that natural types of smoothing operators can be used to obtain host algebras and that, for every metrizable Lie group, the class of semibounded representations can be covered completely by host algebras. In particular, it permits direct integral decompositions.
This mission is the statement-level formalization of Smoothing operators and -algebras for infinite dimensional Lie groups (arXiv:1505.02659v2). 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 Smoothing operators for Frechet--Lie groups (Abstract, first main result: smoothing versus norm-smooth orbit (Fréchet specialization), 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.
28 results of the paper are not stated yet, because the library lacks an interface they need:
The information carrying capacity of the d-dimensional depolarizing channel is computed. It is shown that this capacity can be achieved by encoding messages as products of pure states belonging to an orthonormal basis of the state space, and using measurements which are products of projections onto this same orthonormal basis. In other words, neither entangled signal states nor entangled measurements give any advantage for information capacity. The result follows from an additivity theorem for the capacity of the product of the depolarizing channel with an arbitrary channel. We establish the Amosov-Holevo-Werner p-norm conjecture for this product channel for all p >= 1, and deduce from this the additivity of the minimal entropy and of the Holevo quantity.
This mission is the statement-level formalization of The capacity of the quantum depolarizing channel (arXiv:quant-ph/0204172v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Depolarizing channel: exact unassisted classical capacity (Theorem 1 / abstract: exact unassisted classical capacity and basis strategy, 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.
The quantum analog of the classical erasure channel provides a simple example of a channel whose asymptotic capacity for faithful transmission of intact quantum states, with and without the assistance of a two-way classical side channel, can be computed exactly. We derive the quantum and classical capacities for the quantum erasure channel and related channels, and compare them to the depolarizing channel, for which only upper and lower bounds on the capacities are known.
This mission is the statement-level formalization of Capacities of Quantum Erasure Channels (arXiv:quant-ph/9701015v2). 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 Exact capacities of the qubit quantum erasure channel (Eq. (2), 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.
In this letter we define a family of entanglement distribution protocols assisted by feedback classical communication that gives an operational interpretation to reverse coherent information, i.e., the symmetric counterpart of the well known coherent information. This lead to the definition of a new entanglement distribution capacity that exceeds the unassisted capacity for some interesting channels.
This mission is the statement-level formalization of Reverse Coherent Information (arXiv:0808.0210v2). 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 Operational lower bound and single-letter reverse coherent information (pp.1–3, Eqs.(4)–(7), 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.
4 results of the paper are not stated yet, because the library lacks an interface they need:
The cyclotomic Birman-Murakami-Wenzl (BMW) algebras B_n^k, introduced by R. Häring-Oldenburg, are a generalisation of the BMW algebras associated with the cyclotomic Hecke algebras of type G(k,1,n) (aka Ariki-Koike algebras) and type B knot theory. In this paper, we prove the algebra is free and of rank k^n (2n-1)!! over ground rings with parameters satisfying so-called "admissibility conditions". These conditions are necessary in order for these results to hold and originally arise from the representation theory of B_2^k, which is analysed by the authors in a previous paper. Furthermore, we obtain a geometric realisation of B_n^k as a cyclotomic version of the Kauffman tangle algebra, in terms of affine n-tangles in the solid torus, and produce explicit bases that may be described both algebraically and diagrammatically. The admissibility conditions are the most general offered in the literature for which these results hold; they are necessary and sufficient for all results for general n.
This mission is the statement-level formalization of On the freeness of the cyclotomic BMW algebras: admissibility and an isomorphism with the cyclotomic Kauffman tangle algebras (arXiv:0911.5284v1). 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 Proposition 2.2 (Proposition 2.2, 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.
16 results of the paper are not stated yet, because the library lacks an interface they need:
Based on the monogamy of entanglement, we develop the technique of quantum conditioning to build an {\it additive} entanglement measure: the conditional entanglement of mutual information. Its {\it operational} meaning is elaborated to be the minimal net "flow of qubits" in the process of partial state merging. The result and conclusion can also be generalized to multipartite entanglement cases.
This mission is the statement-level formalization of An additive and operational entanglement measure: conditional entanglement of mutual information (arXiv:0804.3683v2). 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 Proposition 1: bipartite additivity (Proposition 1: bipartite additivity (the page-1 seed pinned to its numbered theorem), 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.
4 results of the paper are not stated yet, because the library lacks an interface they need:
Since 1984, various optical quantum key distribution (QKD) protocols have been proposed and examined. In all of them, the rate of secret key generation decays exponentially with distance. A natural and fundamental question is then whether there are yet-to-be discovered optical QKD protocols (without quantum repeaters) that could circumvent this rate-distance tradeoff. This paper provides a major step towards answering this question. We show that the secret-key-agreement capacity of a lossy and noisy optical channel assisted by unlimited two-way public classical communication is limited by an upper bound that is solely a function of the channel loss, regardless of how much optical power the protocol may use. Our result has major implications for understanding the secret-key-agreement capacity of optical channels---a long-standing open problem in optical quantum information theory---and strongly suggests a real need for quantum repeaters to perform QKD at high rates over long distances.
This mission is the statement-level formalization of Fundamental rate-loss tradeoff for optical quantum key distribution (arXiv:1504.06390v1). 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 Five-party pure-state subadditivity of squashed entanglement (Lemma 2: five-party pure-state subadditivity, 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.
12 results of the paper are not stated yet, because the library lacks an interface they need:
We derive a new entropic quantum uncertainty relation involving min-entropy. The relation is tight and can be applied in various quantum-cryptographic settings. Protocols for quantum 1-out-of-2 Oblivious Transfer and quantum Bit Commitment are presented and the uncertainty relation is used to prove the security of these protocols in the bounded quantum-storage model according to new strong security definitions. As another application, we consider the realistic setting of Quantum Key Distribution (QKD) against quantum-memory-bounded eavesdroppers. The uncertainty relation allows to prove the security of QKD protocols in this setting while tolerating considerably higher error rates compared to the standard model with unbounded adversaries. For instance, for the six-state protocol with one-way communication, a bit-flip error rate of up to 17% can be tolerated (compared to 13% in the standard model). Our uncertainty relation also yields a lower bound on the min-entropy key uncertainty against known-plaintext attacks when quantum ciphers are composed. Previously, the key uncertainty of these ciphers was only known with respect to Shannon entropy.
This mission is the statement-level formalization of A Tight High-Order Entropic Quantum Uncertainty Relation With Applications (arXiv:quant-ph/0612014v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.3: general high-order entropic uncertainty relation (paper headline) (Theorem 3.3: general high-order entropic uncertainty relation (paper headline), 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.
10 results of the paper are not stated yet, because the library lacks an interface they need:
A finite-energy pseudoholomorphic curve in the symplectization of a strictly star-shaped hypersurface approaches, near a non-removable puncture, a periodic Reeb orbit . The previous mission in this series formalizes this in the form of C. Wendl's Lectures on Symplectic Field Theory, Theorem 9.8: along suitable sequences of loops around the puncture the curve converges to the orbit. Most applications need much more precise information about the end. H. Hofer, K. Wysocki and E. Zehnder showed in 1996 (Ann. IHP 13) that at a nondegenerate orbit the convergence holds for the whole end and is exponentially fast, and that the leading term of the difference is times an eigenvector of the asymptotic operator ; R. Siefring sharpened the formula to its present form. The asymptotic eigenvector is the input for winding numbers, fast planes and the intersection theory of punctured curves, for example in U. Hryniewicz's characterization of the Reeb orbits that bound disk-like global surfaces of section (arXiv:1105.2077).
This mission formalizes these asymptotic results in general dimension, in the setting of the previous mission. It follows Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, § 2.2.3 (Definitions 2.5 and 2.9, Theorem 2.11, Lemma 2.12), and the linear theory of C. Wendl's Lectures on Symplectic Field Theory (2026 notes, §§ 4.6 and 4.8). It is the eighth mission in a series on symplectic field theory.
All objects are those of FiniteEnergyPlane_Setting: , a strictly star-shaped level with Reeb field and contact planes , a compatible complex structure on , the symplectization structure on , and finite-energy curves.
Let be a finite-energy -holomorphic curve on the punctured unit disk , and let be a nondegenerate puncture of , asymptotic to a periodic Reeb orbit with sign . Then converges to the trivial cylinder over exponentially fast in . If moreover does not vanish identically near , then has an asymptotic eigenvalue with and an asymptotic eigenvector of at (Hryniewicz, Theorem 2.11 and Lemma 2.12).
HryniewiczCriterion setting.The results. The goal is the standard description of a finite-energy end used throughout symplectic field theory: it is what makes the asymptotic eigenvalue, the winding of the asymptotic eigenvector, the asymptotic Conley–Zehnder index and the asymptotic intersection theory of punctured curves meaningful. The goal does not assume that the limit orbit is nondegenerate, only that the end decays exponentially; this hypothesis is part of the definition of fast planes over possibly degenerate orbits (Hryniewicz, Definition 2.14). Milestone 12 is the form in which planes asymptotic to nondegenerate orbits are used, and milestone 13 connects it to the open HryniewiczCriterion mission. Milestones 6–8 are results about linear Cauchy–Riemann equations on a half-cylinder, independent of the geometry.
Formalizing them. All results are classical and proved in the cited sources (the linear results in Wendl's notes and in R. Siefring, Relative asymptotic behavior of pseudoholomorphic half-cylinders, CPAM 61 (2008)). None of them has been formalized in a proof assistant, as far as a literature search shows; Mathlib has no asymptotic operators of Reeb orbits and no theory of Cauchy–Riemann equations on cylinders.
The asymptotic operator acts on sections of along the orbit, defined intrinsically in with no preferred frame, and its spectral theory lives on loops in a moving subspace. The hypothesis of the goal is only exponential convergence, while the conclusion is convergence and a precise leading term with a single eigenvector. The eigenvector formula is stated in a tube around the orbit with its own phase function , so the leading term is measured transversally to the orbit rather than against the parametrization . For multiply covered orbits the tube is only a covering of a neighbourhood of the orbit, and the phase is a real lift.
FiniteEnergyPlane; the definition module FiniteEnergyPlane_Asymptotics imports FiniteEnergyPlane_Setting (previous mission) and CauchyRiemannIndex_Setting (fifth mission) for Mat n, J₀ n, Vec n, IsSymLoop, IsNondegenerate and crOp. The bridge item also imports HryniewiczCriterion_ConleyZehnder.iteratedFDeriv and require smoothness on some . Matrix-valued convergence is entrywise.Contributions welcome: general lemmas on linear ODEs along periodic orbits and on smooth families of subspaces over the circle.
We define "coherent communication" in terms of a simple primitive, show it is equivalent to the ability to send a classical message with a unitary or isometric operation, and use it to relate other resources in quantum information theory. Using coherent communication, we are able to generalize super-dense coding to prepare arbitrary quantum states instead of only classical messages. We also derive single-letter formulae for the classical and quantum capacities of a bipartite unitary gate assisted by an arbitrary fixed amount of entanglement per use.
This mission is the statement-level formalization of Coherent Communication of Classical Messages (arXiv:quant-ph/0307091v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 1: coherification of one-way classical communication (Proposition 1: coherification of one-way classical communication, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
It is not a problem to complement a classical bit, i.e. to change the value of a bit, a 0 to a 1 and vice versa. This is accomplished by a NOT gate. Complementing a qubit in an unknown state, however, is another matter. We show that this operation cannot be done perfectly. We define the Universal-NOT (U-NOT) gate which out of N identically prepared pure input qubits generates M output qubits in a state which is as close as possible to the perfect complement. This gate can be realized by classical estimation and subsequent re-preparation of complements of the estimated state. Its fidelity is therefore equal to the fidelity F= (N+1)/(N+2) of optimal estimation, and does not depend on the required number of outputs. We also show that when some additional a priori information about the state of input qubit is available, than the fidelity of the quantum NOT gate can be much better than the fidelity of estimation.
This mission is the statement-level formalization of Optimal Manipulations with Qubits: Universal NOT Gate (arXiv:quant-ph/9901053v1). 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 Optimal universal NOT error (Theorem (unnumbered), PDF p.3: optimal universal NOT error, 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.
Given a completely positive (CP) map , there is a theorem of the Radon-Nikodym type [W.B. Arveson, Acta Math. {\bf 123}, 141 (1969); V.P. Belavkin and P. Staszewski, Rep. Math. Phys. {\bf 24}, 49 (1986)] that completely characterizes all CP maps such that is also a CP map. This theorem is reviewed, and several alternative formulations are given along the way. We then use the Radon-Nikodym formalism to study the structure of order intervals of quantum operations, as well as a certain one-to-one correspondence between CP maps and positive operators, already fruitfully exploited in many quantum information-theoretic treatments. We also comment on how the Radon-Nikodym theorem can be used to derive norm estimates for differences of CP maps in general, and of quantum operations in particular.
This mission is the statement-level formalization of Radon-Nikodym derivatives of quantum operations (arXiv:math-ph/0303056v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Stinespring Radon–Nikodym theorem (Theorem 3.1: Stinespring Radon–Nikodym theorem (seed resolved from 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.
6 results of the paper are not stated yet, because the library lacks an interface they need: