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?
Linear, second-order cone and semidefinite programming are three instances of one format: minimize a linear objective subject to the requirement that an affine image of the decision vector lie in a fixed convex cone. Ben-Tal and Nemirovski's Lectures on Modern Convex Optimization (SIAM 2001) builds its whole treatment of modelling and algorithms on this conic programming format, and the first result it needs is a duality theorem for it. That theorem is what certifies optimality of a solution returned by an interior-point solver, what turns a robust or semidefinite reformulation into a tractable problem, and what every later lecture of the book uses when it passes to a dual problem. Conic duality in this form goes back to Nesterov and Nemirovski's monograph on interior-point methods (SIAM 1994); the Lagrangian form of the same phenomenon (Slater's condition) is the textbook version in Boyd and Vandenberghe (Cambridge 2004).
This mission is the second of a series formalizing the book's capstone results, and covers Lecture 2, §2.3–2.4.
Let be a good cone: a nonempty set closed under addition and under multiplication by nonnegative reals (a convex cone), pointed (if and then ), closed, and with nonempty interior. Write for and for . The dual cone is
Given an matrix , and , the conic problem and its conic dual are
A point is feasible for (CP) if ; (CP) is strictly feasible if for some ; it is bounded below if is bounded below on the feasible set (an infeasible problem counts as bounded below); it is solvable if some feasible attains the infimum . The same notions for (D) use , , , and upper bounds. Throughout the book (from p. 53 on) Assumption A is in force: the columns of are linearly independent.
Under the standing assumptions:
Item 1 of the printed theorem (the dual of the dual is equivalent to the primal) is an informal equivalence of problems and is not part of the target.
One strengthened variant is posed beside the goal: items 2 and 3.a of Theorem 2.4.1 for every matrix , without Assumption A (finding F3: the printed proof of 3.a never uses the rank of ). The faithful theorem remains the goal.
The theorem gives, for any of the cones used in practice (nonnegative orthant, Lorentz cones, positive semidefinite matrices and their products), the existence of a dual certificate of optimality and the absence of a duality gap under strict feasibility. The rest of the book uses it constantly: the conic-quadratic and semidefinite representations of Lectures 3–4, the S-lemma, the analysis of semidefinite relaxations and the primal-dual path-following method of Lecture 6 all pass to a dual problem through it. Propositions 2.4.2 and 2.4.3 are the conic analogues of the theorem on alternatives and the inhomogeneous Farkas lemma.
The result is classical and fully proved in the book. Related statements are machine-checked on the platform in other forms: a Lagrangian strong duality under a generalized Slater condition (ConvexOptimization.conic_slater_strong_duality), duality for equality-form conic quadratic programs (ConicQuadIPM.Homogeneous.*), and the bipolar theorem for proper cones. None of them is the pair (CP)/(D) of this book with attainment in both directions and the optimality conditions of item 4. The mission produces the book's statement and its supporting results as a coherent, reusable layer for the rest of the series.
Weak duality and the gap identity are one-line computations. The content lies in items 3.a and 3.b. The obvious attempt—copying the LP proof via Farkas' lemma—fails because the image of a nonpolyhedral cone under a linear map need not be closed, so a limit of dual certificates need not be a certificate. The book's Example 2.4.1 is strictly feasible and bounded below with optimal value but no optimal solution, and Example 2.4.2 is solvable with an infeasible dual: any argument that does not use strict feasibility essentially is wrong. Separation is needed in finite dimension for convex sets that are neither open nor closed, which is not the form in which Mathlib states it, and item 3.b, which the book obtains from 3.a by symmetry, depends on the dual-cone facts of Theorem 2.3.1, including and .
Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, inner products ⬝ᵥ; the topology is the product (Euclidean) topology. The cone properties, the dual cone, feasibility, strict feasibility, boundedness, optimal solutions and optimal values are explicit predicates in one definition file, ModernConvex.ConicDuality.ConicProblem. Optimal values are never a real-valued sInf/sSup: " is the optimal value" is IsGLB/IsLUB of the set of feasible objective values, which no real satisfies for an infeasible or unbounded problem, and "" is stated through an optimal solution whose value is the other problem's infimum or supremum. A formalization that dropped strict feasibility, or that expressed the optimal values as sInf/sSup with their junk value , would make the conic duality theorem either false or trivially true; the targets rule this out by stating attainment and value equality as explicit predicates. Assumption A is Function.Injective A.mulVec, an explicit hypothesis wherever the book has it in force, including Propositions 2.4.2–2.4.3 per the book's Remark 2.4.1.
Needed infrastructure: finite-dimensional separation of convex sets (Mathlib has geometric_hahn_banach_open and relatives for open sets; the nonopen finite-dimensional case goes through relative interiors), dual-cone facts (Mathlib's innerDualCone lives on inner-product spaces, while this mission works on Fin m → ℝ with the dot product), and closedness arguments for cones. The definitions and Theorem 2.3.1 are reusable by the later missions of this series. Proofs of individual milestones, and proofs or refutations of the variant, are welcome.
Conic quadratic programs (second-order cone programs) minimize a linear objective subject to finitely many constraints of the form . They are solved by interior-point methods in polynomial time, and a large share of convex models in engineering, statistics and robust optimization can be rewritten in this form. Whether a given convex problem can be so rewritten is a question about its feasible set and objective: can they be described by conic quadratic inequalities, possibly after adding auxiliary variables? Ben-Tal and Nemirovski answer this question in Lecture 3 of Lectures on Modern Convex Optimization (SIAM, 2001, doi:10.1137/1.9780898718829) with a calculus of conic quadratic representability: a list of elementary representable sets and functions together with operations that preserve representability, each operation producing an explicit representation from given ones. The same calculus underlies modelling tools such as CVX and YALMIP.
The more advanced operations in §3.3 — conic hulls, projective transformations, polars, Legendre transformations, convex hulls of unions and recessive cones — are only nearly representability-preserving: each holds exactly under a closedness or strict feasibility condition, and otherwise produces a set sandwiched between the target and its closure. The rule for convex hulls of unions is credited in the book to Nesterov.
For the ice cream cone (Lorentz cone) is . Let be a direct product of ice cream cones, and write for and for .
A set is CQr (conic quadratic representable) if there are such a , a number of additional variables and data with
the system is a conic quadratic representation (CQR) of . No rank condition is imposed on it. A function is CQr when its epigraph is.
For the mission uses the convex hull and its closure; the conic hull and its closure ; the polar ; and the recessive cone . For as above it uses the Legendre transformation and the projective transformation , whose epigraph is the closure of .
Let be nonempty convex CQr sets, , and let
Then
and if (i) all are closed and bounded, or (ii) with closed and bounded and convex and closed, all three sets are equal and CQr.
The goal shows that a disjunction of conic quadratic constraints — " lies in one of " — can be convexified exactly, under a compactness-type condition, by a conic quadratic system whose size is the sum of the sizes of the given representations. This is the conic quadratic analogue of Balas's disjunctive programming formulation for polyhedra and is the basis of perspective reformulations in mixed-integer conic optimization. The milestones are the other closure rules of the calculus: they let a modeller pass to conic hulls, perspectives, polars, conjugates and recession cones without leaving the conic quadratic class, always with an explicit representation.
These results are classical and proved in the book; none of them is formalized on the platform, and there is no formal library of conic quadratic representability. The mission produces that library's core definitions and its main closure theorems as machine-checked statements. Propositions 3.3.3 and 3.3.4 depend on conic duality, which a companion mission of this series (II: The Conic Duality Theorem) states.
The inclusions are not symmetric in difficulty. is a direct substitution, but contains points with some , where the block inequality no longer certifies membership in any ; such points are only limits of convex combinations, and showing they lie in the closure requires the nonemptiness of every . The equality under (i) or (ii) is a closedness statement for a convex hull, which fails in general (two closed convex sets can have a non-closed convex hull of their union), so the compactness of the must be used. Closedness of projections (Lemma 3.3.1) is the analogous obstacle in the milestones: the projection of a closed convex set is not closed in general.
Vectors are Fin n → ℝ; the Euclidean norm is written out (eucNorm) because Mathlib's norm on this type is the sup norm. A product of ice cream cones is a structure IceCreamProduct with factors of dimensions , its vectors indexed by (block, coordinate) pairs, the last coordinate of each block being the dominant one. cqrSet K A B b is the represented set and IsCQr X says equals some cqrSet; the existential is over the fixed shape (finitely many Lorentz factors and an affine map), so an arbitrary set is not CQr by fiat. Pairs of the conic hull are vectors of Fin (n+1) → ℝ with last coordinate . Functions into are EReal-valued and assumed never ; the Legendre transformation is an EReal supremum, in which points with contribute . Conv is convexHull ℝ, and closures are topological closures. Every "is CQr" conclusion is stated together with the book's explicit representation as an equality or sandwich of sets; stating "is CQr" alone would be a weaker theorem.
Beyond the paper. Proposition 3.3.2 as printed omits and is false for (the right-hand side contains while the left-hand side is empty; a Lean refutation of the formal statement was built during drafting). The faithful statement is kept as a milestone, and a corrected variant adds the missing hypothesis.
Reusable beyond this mission: the definitions of ice cream products, CQr sets, conic hull, polar, recessive cone and projective/Legendre transformations, and Lemma 3.3.1 as a closedness criterion. Contributions toward a general "closed projection" lemma and conic duality for products of Lorentz cones are welcome.
Every linear program comes with a second linear program, its dual, whose feasible points certify lower bounds on the first program's optimal value. The duality theorem says that these certificates are complete: the best bound equals the optimal value whenever either is finite. It is the reason an LP solver can return a proof of optimality alongside a solution, the basis of sensitivity analysis and of primal–dual algorithms, and the template for every duality theory in convex optimization.
This mission opens a series formalizing A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization (SIAM 2001, doi:10.1137/1.9780898718829). Lecture 1 develops LP duality from a theorem on the alternative for mixed strict and non-strict linear inequalities, and proves that theorem from the homogeneous Farkas lemma by way of the theorems of Helly and Radon. Lecture 2 reruns the same argument for conic programs, so the statements here are the ones later missions of the series generalize.
Let have rows , and let , . Vector inequalities are componentwise. The LP program and its dual are
A point with is feasible, and (LP) is feasible if such a point exists. (LP) is bounded below if is bounded below on the feasible set. It is solvable if some feasible point minimizes . A real is a lower bound on the optimal value if for every feasible . The optimal value is , which is for an infeasible and for an unbounded program. The same notions apply to the dual with "bounded above" and "maximizes". No rank condition is imposed on .
The system on the alternative is
and its two certificate systems in are
In Lean, vectors are functions Fin n → ℝ, is c ⬝ᵥ x, and the definitions live in ModernConvex.LPDuality.LinearProgram and ModernConvex.LPDuality.AlternativeSystems.
LP duality underlies most of the book's later material. The conic duality theorem of Lecture 2 has the same statement with the nonnegative orthant replaced by a cone. Robust counterparts, the S-lemma and the semidefinite relaxations of Lecture 4 are all proved by dualizing an inner problem. A machine-checked version in exactly this form, with explicit predicates for "bounded" and "solvable", is the base that later missions of the series can cite.
The results here are classical and proved. The platform already has proved LP duality theorems, in other standard forms: LinearOptimization.lp_strong_duality (general form with equalities), MatousekLP.Duality.duality_theorem (max/ form, four-case statement) and VanderbeiLP.StrictComp.strong_duality. It has Farkas lemmas in several forms (LinearOptimization.farkas_cone_corollary, which is one direction of Lemma 1.4.1, and MatousekLP.Duality.farkas_geometric). It also has Helly and Radon in Mathlib's form (FamousTheorems.helly_theorem, which assumes at least sets and subfamilies of size exactly ; FamousTheorems.radon_theorem, which assumes affine dependence). The open MangasarianFJ.GenFJ.motzkin_transposition is a related alternative theorem. None of them states the book's inequality-form pair (LP)/(LP), the five-way equivalence, or the mixed strict/non-strict theorem on the alternative. These are the remaining work. Several of them should follow quickly from the existing items, and solvers are encouraged to reuse them.
The obstacle is the existence of certificates of infeasibility. Proposition 1.3.1 is a one-line computation, but its converse, Theorem 1.3.1, is not: the existence of a certificate is a global statement about the system that no local computation produces. The mixed system needs care: when only can certify, and the homogenization that reduces Theorem 1.3.1 to the Farkas lemma has to keep strict and non-strict rows apart. In the duality theorem, the step from "feasible and bounded below" to "solvable" is where attainment must be shown. It is true for LPs and false for general convex programs (), so a proof cannot avoid the linear structure.
The book's own proof of item 1 has a sign slip. The displayed dual of the rewritten (LP) has the constraint with , which describes rather than a program equivalent to (LP). The formal statement uses the correct computation, with .
Vectors are Fin n → ℝ. Indices are 0-based, so the strict rows of are i < ms, and ms ≤ m is a hypothesis. Optimal values are never written as sInf/sSup, whose junk value on empty or unbounded sets would make the equal-values clause trivially true. A lower bound is the predicate . " is the optimal value" is IsGLB/IsLUB of the set of objective values, which no real satisfies for an infeasible or unbounded program. Item 1 of the goal is not formalized as True. It states the explicit feasible-set correspondence that "equivalent" means in the book's proof. The five properties are a List.TFAE.
In Bernstein's theorem the sup-norm inequality is stated as "every bound on over gives the bound on ". Coefficients are complex, which covers the real case.
The book prints the trigonometric polynomial as , with the same two coefficients in every term. This is a subscript typo: the theorem is stated for every trigonometric polynomial of degree , and its own tightness example is not of the printed form for . The formal statement uses general coefficients .
A complete development needs only Mathlib's finite-dimensional linear algebra and convexity (convexHull, Convex). The definitions of the LP pair and of the alternative systems are reusable by any later mission that dualizes a linear inner problem.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
In this paper we introduce Schwartz operators as a non-commutative analog of Schwartz functions and provide a detailed discussion of their properties. We equip them in particular with a number of different (but equivalent) families of seminorms which turns the space of Schwartz operators into a Frechet space. The study of the topological dual leads to non-commutative tempered distributions which are discussed in detail as well. We show in particular that the latter can be identified with a certain class of quadratic forms, therefore making operations like products with bounded (and also some unbounded) operators and quantum harmonic analysis available to objects which are otherwise too singular for being a Hilbert space operator. Finally we show how the new methods can be applied by studying operator moment problems and convergence properties of fluctuation operators.
This mission is the statement-level formalization of Schwartz operators (arXiv:1503.04086v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The form topology makes Schwartz operators a Frechet space (Proposition 3.3, 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.
51 results of the paper are not stated yet, because the library lacks an interface they need:
We describe how to achieve optimal entanglement generation and one-way entanglement distillation rates by coherent implementation of a class of secret key generation and secret key distillation protocols, respectively. This short paper is a high-level descrioption of our detailed papers [8] and [10].
This mission is the statement-level formalization of Relating quantum privacy and quantum coherence: an operational approach (arXiv:quant-ph/0307053v1). 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 Coherent information is achievable in all four resource conversions (Conclusion; scenarios 1–4, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
We investigate whether the use of a noiseless, classical feedback channel will increase the capacity of a quantum discrete memoryless channel to transmit classical information. This problem has been previously analyzed by Bowen and Nagarajan for the case of protocols restricted to product input states. They showed that feedback did not increase the information capacity. In this paper we introduce a quantum analogue of classical causality and prove a capacity theorem (in regularized form) for the transmission of classical information.
This mission is the statement-level formalization of Classical feedback for quantum channels (arXiv:quant-ph/0409207v3). 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 Whole-codeword Markov property of the executed feedback protocol (§2, paragraph continuing PDF p.5, 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.
6 results of the paper are not stated yet, because the library lacks an interface they need:
The maximum likelihood strategy to the estimation of group parameters allows to derive in a general fashion optimal measurements, optimal signal states, and their relations with other information theoretical quantities. These results provide a deep insight into the general structure underlying optimal quantum estimation strategies. The entanglement between representation spaces and multiplicity spaces of the group action appear to be the unique kind of entanglement which is really useful for the optimal estimation of group parameters.
This mission is the statement-level formalization of Maximum likelihood estimation for a group of physical transformations (arXiv:quant-ph/0507007v1). 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 Optimal input states and the likelihood ceiling (Theorem 3 (optimal input states), Eqs.(24)–(25); capstone selected from the p.1 abstract, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
10 results of the paper are not stated yet, because the library lacks an interface they need:
We derive the optimal input states and the optimal quantum measurements for estimating the unitary action of a given symmetry group, showing how the optimal performance is obtained with a suitable use of entanglement. Optimality is defined in a Bayesian sense, as minimization of the average value of a given cost function. We introduce a class of cost functions that generalizes the Holevo class for phase estimation, and show that for states of the optimal form all functions in such a class lead to the same optimal measurement. A first application of the main result is the complete proof of the optimal efficiency in the transmission of a Cartesian reference frame. As a second application, we derive the optimal estimation of a completely unknown two-qubit maximally entangled state, provided that N copies of the state are available. In the limit of large N, the fidelity of the optimal estimation is shown to be 1-3/(4N).
This mission is the statement-level formalization of Optimal estimation of group transformations using entanglement (arXiv:quant-ph/0506267v2). 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 Theorem 1: optimal canonical input states (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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
This paper is devoted to the study of various maximal ergodic theorems in noncommutative -spaces. In particular, we prove the noncommutative analogue of the classical Dunford-Schwartz maximal ergodic inequality for positive contractions on and the analogue of Stein's maximal inequality for symmetric positive contractions. We also obtain the corresponding individual ergodic theorems. We apply these results to a family of natural examples which frequently appear in theory of von Neumann algebras and in quantum probability.
This mission is the statement-level formalization of Noncommutative maximal ergodic theorems (arXiv:math/0505308v2). 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 Operator block matrix norm comparison (Lemma 3.2, PDF p. 13). 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.
62 results of the paper are not stated yet, because the library lacks an interface they need:
We study the Weyl representation of metaplectic operators associated to a symplectic matrix having no non-trivial fixed point, and justify a formula suggested in earlier work of Mehlig and Wilkinson. We give precise calculations of the associated Maslov-type indices; these indices intervene in a crucial way in Gutzwiller's formula of semiclassical mechanics, and are simply related to an index defined by Conley and Zehnder.
This mission is the statement-level formalization of On the Weyl Representation of Metaplectic Operators (arXiv:math/0503708v1). 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 Symplectic Cayley transform and its inverse (§3.1, unnumbered, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
9 results of the paper are not stated yet, because the library lacks an interface they need:
A pro-Lie group is a projective limit of a family of finite-dimensional Lie groups. In this note we show that a pro-Lie group is a Lie group in the sense that its topology is compatible with a smooth manifold structure for which the group operations are smooth if and only if is locally contractible. We also characterize the corresponding pro-Lie algebras in various ways. Furthermore, we characterize those pro-Lie groups which are locally exponential, that is, they are Lie groups with a smooth exponential function which maps a zero neighborhood in the Lie algebra diffeomorphically onto an open identity neighborhood of the group.
This mission is the statement-level formalization of Pro-Lie groups which are infinite-dimensional Lie groups (arXiv:math/0609684v1). 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 Pro-Lie groups admit compatible Lie structures exactly when locally contractible (Theorem 1.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.
31 results of the paper are not stated yet, because the library lacks an interface they need:
We introduce a measure of decoherence for a class of density operators. For Gaussian density operators in dimension one it coincides with an index used by Morikawa (1990). Spatial decoherence rates are derived for three large classes of the Galilean covariant quantum semigroups introduced by Holevo. We also characterize the relaxation to a Gaussian state for these dynamics and give a theorem for the convergence of the Wigner function to the probability distribution of the classical analog of the process.
This mission is the statement-level formalization of Decoherence rates for Galilean covariant dynamics (arXiv:0710.1344v2). 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 Theorem 4.3, cases 1 and 3: leading spatial decoherence rates (seed from abstract) (Theorem 4.3, cases 1 and 3: leading spatial decoherence rates (seed from abstract), 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.
9 results of the paper are not stated yet, because the library lacks an interface they need:
We give an algorithm for constructing the algebraic hull of a given matrix Lie algebra in characteristic zero. It is based on an algorithm for finding integral linear dependencies of the roots of a polynomial, that is probably of independent interest.
This mission is the statement-level formalization of Constructing algebraic Lie algebras (arXiv:math/0611414v1). 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 Trivial permutation component and power traces (Lemma 5: trivial permutation component and trace, 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:
Typical quantum communication schemes are such that to achieve perfect decoding the receiver must share a reference frame with the sender. Indeed, if the receiver only possesses a bounded-size quantum token of the sender's reference frame, then the decoding is imperfect, and we can describe this effect as a noisy quantum channel. We seek here to characterize the performance of such schemes, or equivalently, to determine the effective decoherence induced by having a bounded-size reference frame. We assume that the token is prepared in a special state that has particularly nice group-theoretic properties and that is near-optimal for transmitting information about the sender's frame. We present a decoding operation, which can be proven to be near-optimal in this case, and we demonstrate that there are two distinct ways of implementing it (corresponding to two distinct Kraus decompositions). In one, the receiver measures the orientation of the reference frame token and reorients the system appropriately. In the other, the receiver extracts the encoded information from the virtual subsystems that describe the relational degrees of freedom of the system and token. Finally, we provide explicit characterizations of these decoding schemes when the system is a single qubit and for three standard kinds of reference frame: a phase reference, a Cartesian frame (representing an orthogonal triad of spatial directions), and a reference direction (representing a single spatial direction).
This mission is the statement-level formalization of Quantum communication using a bounded-size quantum reference frame (arXiv:0812.5040v2). 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 Canonical-token effective channel (Paper result: canonical-token effective channel, Eqs.(1)–(3), (38)–(40), 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.
3 results of the paper are not stated yet, because the library lacks an interface they need:
In this note we show that the representation of the additive group of the Hilbert space on given by the multiplication operators is continuous but its space of smooth vectors is trivial. This example shows that a continuous unitary representation of an infinite dimensional Lie group need not be smooth.
This mission is the statement-level formalization of A non-smooth continuous unitary representation of a Banach-Lie group (arXiv:0811.4234v1). 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 The phase representation is continuous and has only the zero smooth vector (Theorem 2.3, 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.
In this survey, we report on the state of the art of some of the fundamental problems in the Lie theory of Lie groups modeled on locally convex spaces, such as integrability of Lie algebras, integrability of Lie subalgebras to Lie subgroups, and integrability of Lie algebra extensions to Lie group extensions. We further describe how regularity or local exponentiality of a Lie group can be used to obtain quite satisfying answers to some of the fundamental problems. These results are illustrated by specialization to some specific classes of Lie groups, such as direct limit groups, linear Lie groups, groups of smooth maps and groups of diffeomorphisms.
This mission is the statement-level formalization of Towards a Lie theory for locally convex groups (arXiv:1501.06269v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Fundamental results of locally convex differential calculus (Proposition I.2.3, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
99 results of the paper are not stated yet, because the library lacks an interface they need:
Based on the ideas in [CKP], we introduce the weighted analogue of the branching rule for the classical hook length formula, and give two proofs of this result. The first proof is completely bijective, and in a special case gives a new short combinatorial proof of the hook length formula. Our second proof is probabilistic, generalizing the (usual) hook walk proof of Green-Nijenhuis-Wilf, as well as the q-walk of Kerov. Further applications are also presented.
This mission is the statement-level formalization of The weighted hook length formula (arXiv:1006.0043v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Four weighted branching identities (Theorem 2(a)–(d), 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.
3 results of the paper are not stated yet, because the library lacks an interface they need:
Dynamical semigroups have become the key structure for describing open system dynamics in all of physics. Bounded generators are known to be of a standard form, due to Gorini, Kossakowski, Sudarshan and Lindblad. This form is often used also in the unbounded case, but rather little is known about the general form of unbounded generators. In this paper we first give a precise description of the standard form in the unbounded case, emphasizing intuition, and collecting and even proving the basic results around it. We also give a cautionary example showing that the standard form must not be read too naively. Further examples are given of semigroups, which appear to be probability preserving to first order, but are not for finite times. Based on these, we construct examples of generators which are not of standard form.
This mission is the statement-level formalization of Unbounded generators of dynamical semigroups (arXiv:1707.02266v1). 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 No-event semigroups admit a C0 contraction implementation (Definition II.1, asserted realization of no-event semigroups, 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.
19 results of the paper are not stated yet, because the library lacks an interface they need:
Let be a 1-connected Banach-Lie group or, more generally, a BCH--Lie group. On the complex enveloping algebra of its Lie algebra we define the concept of an analytic functional and show that every positive analytic functional is integrable in the sense that it is of the form for an analytic vector of a unitary representation of . On the way to this result we derive criteria for the integrability of *-representations of infinite dimensional Lie algebras of unbounded operators to unitary group representations. For the matrix coefficient of a vector in a unitary representation of an analytic Fr'echet-Lie group we show that is an analytic vector if and only if is analytic in an identity neighborhood. Combining this insight with the results on positive analytic functionals, we derive that every local positive definite analytic function on a 1-connected Fr'echet--BCH--Lie group extends to a global analytic function.
This mission is the statement-level formalization of On Analytic Vectors for Unitary Representations of Infinite Dimensional Lie Groups (arXiv:1002.4792v2). 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 Analytic functionals: seminorm and Banach norm criteria (Proposition 3.4, 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.
17 results of the paper are not stated yet, because the library lacks an interface they need:
We consider the family of energy-constrained diamond norms on the set of Hermitian-preserving linear maps (superoperators) between Banach spaces of trace class operators. We prove that any norm from this family generates the strong (pointwise) convergence on the set of all quantum channels (which is more adequate for describing variations of infinite-dimensional channels than the diamond norm topology). We obtain continuity bounds for information characteristics (in particular, classical capacities) of energy-constrained quantum channels (as functions of a channel) with respect to the energy-constrained diamond norms which imply uniform continuity of these characteristics with respect to the strong convergence topology.
This mission is the statement-level formalization of Energy-constrained diamond norms and their use in quantum information theory (arXiv:1706.00361v2). 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 Proposition 3 A–B: general-input ECD convergence and strong topology (Abstract topology result, precisely Proposition 3 A–B, 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:
A single-party strategy in a multi-round quantum protocol can be implemented by sequential networks of quantum operations connected by internal memories. Here provide the most efficient realization in terms of computational-space resources.
This mission is the statement-level formalization of Minimal computational-space implementation of multi-round quantum protocols (arXiv:1006.1780v1). 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 Lemma 1 and Eq.(8): Haar averaging preserves the optimum and yields covariance (Lemma 1 and Eq.(8): Haar averaging preserves the optimum and yields covariance, 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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Let be a finite dimensional Lie algebra over a field of characteristic . Then by the original Levi theorem, where is the solvable radical and is some maximal semisimple subalgebra. We prove that if is an -(co)module algebra for a finite dimensional (co)semisimple Hopf algebra , then is -(co)invariant and can be chosen to be -(co)invariant too. Moreover, the nilpotent radical of is -(co)invariant and there exists an -sub(co)module such that and . In addition, the -(co)invariant analog of the Weyl theorem is proved. In fact, under certain conditions, these results hold for an -comodule Lie algebra , even if is infinite dimensional. In particular, if is a Lie algebra graded by an arbitrary group , then can be chosen to be graded, and if is a Lie algebra with a rational action of a reductive affine algebraic group by automorphisms, then can be chosen to be -invariant. Also we prove that every finite dimensional semisimple -(co)module Lie algebra over a field of characteristic is a direct sum of its minimal -(co)invariant ideals.
This mission is the statement-level formalization of Structure of H-(co)module Lie algebras (arXiv:1205.0778v7). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
36 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 13 (abstract structural capstone; original seed) (Theorem 13 (abstract structural capstone; original seed), 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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper, a new axiomatization for unbounded functional calculi is proposed and the associated theory is elaborated comprising, among others, uniqueness and compatibility results and extension theorems of algebraic and topological nature. In contrast to earlier approaches, no commutativity assumptions need to be made about the underlying algebras. In a second part, the abstract theory is illustrated in familiar situations (sectorial operators, semigroup generators, normal operators). New topological extension theorems are proved for the sectorial calculus and the Hille--Phillips calculus. Moreover, it is shown that the Stieltjes and the Hirsch calculus for sectorial operators are subcalculi of a (small) topological extension of the sectorial calculus.
This mission is the statement-level formalization of On the Fundamental Principles of Unbounded Functional Calculi (arXiv:2009.04733v1). 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 Theorem 6.1 (Extension Theorem) (Theorem 6.1 (Extension Theorem), PDF p. 13). 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.
17 results of the paper are not stated yet, because the library lacks an interface they need:
When two independent analog signals, X and Y are added together giving Z=X+Y, the entropy of Z, H(Z), is not a simple function of the entropies H(X) and H(Y), but rather depends on the details of X and Y's distributions. Nevertheless, the entropy power inequality (EPI), which states that exp [2H(Z)] \geq exp[2H(X)] + exp[2H(Y)], gives a very tight restriction on the entropy of Z. This inequality has found many applications in information theory and statistics. The quantum analogue of adding two random variables is the combination of two independent bosonic modes at a beam splitter. The purpose of this work is to give a detailed outline of the proof of two separate generalizations of the entropy power inequality to the quantum regime. Our proofs are similar in spirit to standard classical proofs of the EPI, but some new quantities and ideas are needed in the quantum setting. Specifically, we find a new quantum de Bruijin identity relating entropy production under diffusion to a divergence-based quantum Fisher information. Furthermore, this Fisher information exhibits certain convexity properties in the context of beam splitters.
This mission is the statement-level formalization of The entropy power inequality for quantum systems (arXiv:1205.3409v2). 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 Entropy power inequality for the 50:50 beam splitter (Theorem VII.2, (89); paper-level seed pp.1–2, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need: