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?
Noncommutative -spaces built from a von Neumann algebra come in two kinds. When carries a normal faithful trace, is a space of (unbounded) operators affiliated with , and much of classical analysis — martingale inequalities, square functions, maximal inequalities, interpolation — has been carried over to this tracial setting. Algebras of type III, which occur naturally in quantum field theory and quantum statistical mechanics, have no such trace; their -spaces are Haagerup's, defined through a crossed product and the dual weight.
Haagerup, Junge and Xu (arXiv:0806.3635, Trans. AMS 362 (2010)) give a general method for transferring tracial results to type III algebras. Its engine is a reduction theorem, due to Haagerup and circulated as an unpublished manuscript since the late 1970s: after enlarging to a crossed product, the algebra is approximated by an increasing sequence of finite von Neumann algebras, in a way that respects the state and its modular group. This mission formalizes that theorem, §2 of the paper.
Timeline. Haagerup constructs his -spaces in 1979 (Colloq. Internat. CNRS 274) and proves the reduction in the manuscript [H3]. Junge and Xu use it for noncommutative Burkholder–Rosenthal inequalities (Ann. Probab. 2003) and maximal ergodic theorems (J. AMS 2007). The 2008 preprint, revised in 2009, gives the first published proof together with its applications to approximation, extension of maps to crossed products, and martingale and maximal inequalities.
is a von Neumann algebra on a Hilbert space with a normal faithful state . Up to spatial isomorphism is in standard form: there is a unit vector , cyclic and separating for , with . Tomita–Takesaki theory supplies the modular operator and the modular automorphism group .
is the group of dyadic rationals with the discrete topology. On define
for , . The crossed product is the von Neumann algebra generated by and . With , the dual state is ; on generators equals for and otherwise. Its modular group is , and .
For a bounded functional on an algebra , the centralizer is . With (branch ), and , the subalgebras are . A von Neumann algebra is finite if every isometry in it is unitary. A conditional expectation from onto a subalgebra is a positive linear -bimodular map onto fixing .
There is an increasing sequence of von Neumann subalgebras of such that each is finite, is w*-dense in , and for each there is a normal faithful conditional expectation with
The goal asserts existence only, as printed; the construction is the content of the milestones.
The reduction theorem lets a statement about Haagerup be proved by checking it on the finite algebras , where traces exist, and passing to the limit: the expectations extend to contractive projections on and their ranges exhaust , which contains complementably. The paper uses this to obtain noncommutative Burkholder–Gundy, Stein, Burkholder–Rosenthal and Doob inequalities, and maximal ergodic inequalities, for type III algebras; for some of these no other proof is known. The theorem has since become a standard tool in noncommutative probability and harmonic analysis.
The theorem is proved (in the cited paper, with details on pp. 7–11). It has not been formalized: Mathlib has von Neumann algebras as double commutants but no crossed products, conditional expectations, modular theory or Haagerup -spaces. This mission produces a formal statement of the reduction theorem and of each lemma of its proof, built on the published standard-form encoding of Tomita–Takesaki data, and invites solvers to formalize the known proof.
The modular group of a type III algebra is outer and aperiodic, so no centralizer is large enough to be finite and dense at once. The proof works around this by perturbing to states whose modular groups are periodic, and the delicate step is density: showing that the centralizers eventually see every element of . This rests on uniform estimates in the -norm (Lemma 2.6) that need the distribution of under (Lemma 2.2), analytic elements (Lemma 2.5), and an approximation of the logarithm by trigonometric polynomials. Norm density of is false in general; only weak*-type density holds. For finite the statement is easy ( is already finite); the content is the type III case.
is given by the published OAI.BoundedRecovery.StandardModularData H: a von Neumann algebra on , a unit cyclic separating vector , as a nondegenerate functional calculus, and , tied together by the closed Tomita relation; is its sigma. Every σ-finite von Neumann algebra with a normal faithful state is spatially isomorphic to such data, and every statement is invariant under spatial isomorphism.
The crossed product is built on lp (fun _ : dyadic => H) 2, as the double commutant of and their adjoints. , and are the bounded operators characterized by their pointwise formulas; is the Laurent operator of on in the shift , which is (Mathlib has no Borel functional calculus). Centralizers use the commutation form for bounded functionals. Finiteness is the published OAI.FiniteFactor.IsFiniteAlgebra (every isometry is unitary). W*-density is equality of the double commutant with ; σ-strong convergence of bounded sequences is strong convergence. Order on operators is the Loewner order. Lemma 2.2 is stated for continuous , which already determines the distribution.
Hypothesized modular data. The platform has no Tomita–Takesaki existence theorem, so the modular data of (and of in Lemma 2.4 (i)) enter as hypotheses with and ; the first milestone proves such exists, so the goal is not vacuous. The formalization does not restrict to finite, finite-dimensional or tracial (where the goal is empty); is never defined by a formula; finite means "every isometry is unitary", not finite-dimensional; and density is never norm density.
Reusable beyond this mission: the dyadic crossed product and dual state, conditional expectations, the commutation-form centralizer, and Lemma 2.5 for arbitrary standard-form data. Welcome contributions include the existence of modular data for crossed products, the shift and Laurent operators on of a discrete group, and the averaging construction of conditional expectations from periodic modular groups.
Quantum information protocols often require a finite collection of unitary gates whose averages reproduce those of the full unitary group. A unitary design gives a precise finite-moment version of that requirement. When gates are sampled from an exact design, a practitioner needs to know how many independent draws make the empirical collection a reliable approximation. Dulian and Sawicki give an explicit probability bound for that question in Theorem 1 of their paper. The bound depends on the sample count, the desired accuracy, and the dimensions of the irreducible representations visible at the chosen moment order.
The result joins two subjects. Matrix concentration controls the norm of a sum of random operators. Representation theory identifies which operator blocks occur in the moment being estimated and supplies their dimensions. Neither ingredient alone gives the numerical bound stated by the paper. This mission formalizes their combination for independent gates drawn from any exact -design, including Haar-distributed gates.
Fix integers . Write for the group of complex unitary matrices and for its Haar probability measure. For a gate , its mixed tensor representation is
where the bar conjugates every matrix entry. For a probability measure on , the moment operator is . An exact -design is a probability measure satisfying . The design distance is , using the spectral operator norm.
Draw independent gates from an exact -design , with . Their empirical measure counts every draw, including repetitions, with weight . Thus . This convention implements the sum used in the paper's concentration argument and remains meaningful when the sampling distribution has atoms.
The moment representation splits into a trivial part and nontrivial irreducible blocks indexed by . An index is a nonzero weakly decreasing integer tuple with and . Its block dimension is the Weyl dimension
This explicit index set and dimension formula come from equations (20), (22), and (23) of the source. The zero- and one-dimensional cases are included in the formal statement; their nontrivial index set can be empty.
The goal is the corrected positive-threshold form of Theorem 1, for and :
The paper prints “any .” Its formula fails for some nonpositive : a negative threshold makes the event certain while the displayed expression can decrease below one as grows. At , an empty also gives a zero right-hand side for a certain event. The positive-threshold range is the meaningful form of its result.
The milestone list follows the paper's numbered claims. Fact 2 provides a master concentration bound for independent complex matrices through Hermitian dilation. Theorem 18 specializes it to one irreducible block, with its two equivalent closed forms of the tail factor. Lemma 16 and equation (24) connect the full design distance to the norms of those blocks and state the resulting union bound. Fact 9 supplies the decomposition indexed by and the Weyl dimensions needed to turn the block sum into Theorem 1's explicit sum.
The bound gives a finite-sample guarantee for the mixed tensor moment of random gates. It exposes how an accuracy threshold and a representation-theoretic dimension sum determine the chance that the empirical moment differs from Haar averaging. A reader can evaluate the right-hand side once , , , and are fixed. The bound also covers Haar random gates because Haar measure itself is an exact design at every order, as the paper observes in Section 6.
The mathematical result was proved by Dulian and Sawicki; the machine-checked development requested here remains to be built. Existing published Prove2Me modules already provide a spectral matrix norm, a Hermitian dilation, and a general matrix master bound. The new formalization must establish the paper's mixed tensor representation model, its irreducible decomposition and weight dimensions, the one-block estimate, and their assembly into the displayed inequality. These components can serve later results on random unitary designs and matrix concentration.
The operator acts on a space of dimension , so applying a single matrix tail bound directly to it leaves a prefactor governed by that large ambient dimension. The paper's sharper expression depends on separating the nontrivial irreducible blocks, removing the Haar-invariant part, and identifying the dimensions of exactly the blocks that occur. The critical representation-theoretic step is the complete, multiplicity-aware decomposition in Fact 9. A bound for an arbitrary collection of block matrices would not identify the paper's or its Weyl dimension sum.
Lean represents as Matrix.unitaryGroup (Fin d) ℂ with the measurable space induced from the published Borel structure on complex matrices. The mixed tensor basis is indexed by a pair of functions from Fin t to Fin d; ordinary factors come first, conjugate factors second. The measure is required to be a left- and right-invariant probability measure. An exact design is a probability measure with equality of the full mixed th moment, not merely a first moment or a one-sided tensor power. Independent samples use the product measure, and the empirical moment is their average with multiplicity.
The norm is the published operator norm on matrices. The set is a finite set of integer tuples; bounds follow from its defining constraints. The Weyl product uses zero-based Fin d indices, which preserve every difference . All real exponents are real powers, with positive bases in the stated threshold range. The supremum over zero nontrivial blocks is defined to be zero, matching the zero design distance in that case.
The representation structure requires positive dimensions and multiplicities, irreducibility, pairwise inequivalence, orthogonal isometric embeddings, completeness, and intertwining with the concrete mixed tensor action. Those requirements prevent a vacuous or incomplete block family from making the goal automatic. Contributions are welcome on the representation decomposition, the Haar projection onto the trivial part, the non-Hermitian matrix bound, and the probability-to-block reduction. The source's highest-weight labels are kept: the block indexed by has as its highest weight, expressed through weights of the diagonal torus and the dominance order of the simple roots , and its dimension is the Weyl product .
An ordinary Lie algebra has a vector space and an antisymmetric bracket satisfying the Jacobi identity. In a Lie 2-algebra, the vectors become the objects of a linear category, and the Jacobi identity is witnessed by a morphism called the Jacobiator. This lets the Jacobi identity hold coherently rather than as a strict equation. Baez and Crans developed this notion to make the relation between categorified Lie algebra structures and short chain complexes precise (Baez–Crans, §§3–4). The result of interest here is their equivalence between semistrict Lie 2-algebras and two-term -algebras, Theorem 36.
A 2-vector space is a category internal to vector spaces over a field : its objects and morphisms are vector spaces; source , target , identity , and composition are linear. Composition is read in diagrammatic order, so means first , then . The identity laws require . Lemma 6 shows that linearity forces the composition of composable and to be
The arrow part of is . It remembers the displacement of after its source is translated to zero. A 2-vector space can therefore be compared with the two-term complex . Conversely, a complex gives arrows with source , target , and identity (Baez–Crans, Proposition 8).
A semistrict Lie 2-algebra is a 2-vector space with a skew-symmetric bilinear bracket functor and a completely antisymmetric trilinear natural isomorphism
The Jacobiator obeys the Jacobiator identity, an equality between two composites of morphisms through the octagon in Definition 22. A homomorphism is a linear functor equipped with a bilinear natural transformation satisfying Definition 23’s square. The resulting one-cell category is (Baez–Crans, pp. 18–21).
A 2-term -algebra has vector spaces , a differential , brackets of degrees adding to at most one, and a trilinear map . Its equations are precisely (a)–(i) of Lemma 33. In particular, measures the failure of the ordinary Jacobi identity, and equation (i) is its four-input coherence law. Homomorphisms are chain maps with a skew bilinear comparison map satisfying all three equations of Definition 34. They form (Baez–Crans, pp. 28–30).
The goal is Theorem 36, an equivalence of the two one-cell categories:
The milestone path begins with Lemma 6’s forced composition law. Proposition 8 states the underlying linear equivalence , and the 2-cell part of Theorem 12 identifies linear natural transformations between linear functors with chain homotopies between the corresponding chain maps, through their arrow parts. Propositions 25 and 35 establish identity, composition, and associativity for the homomorphisms on each side. Equation (3) reconciles the two expressions for the bracket of morphisms under the construction . The proof of Theorem 36 then supplies on objects and morphisms and the reverse construction . The goal additionally requires functoriality and natural isomorphisms, which the paper asks the reader to check or construct (Baez–Crans, pp. 30–36).
The equivalence says that the categorical and chain-complex descriptions carry the same one-cell algebraic information. It permits constructions expressed with morphisms, functors, and a Jacobiator to be studied with a differential and higher brackets, and conversely. Later classifications of skeletal Lie 2-algebras in the paper use the two-term viewpoint (Baez–Crans, §§5–6).
Theorem 36 is proved in the cited paper; the machine-checked proof is the work this mission seeks. The local files compile the definitions and open theorem statements, and a sorry-free check exhibits nonzero carriers satisfying the principal structures. The milestones expose the individual obligations that a complete Lean proof must discharge. This mission does not claim a formal proof of the result or of the stronger 2-categorical statement.
A bilinear bracket on objects and morphisms is not enough to define a bracket functor: it must preserve source, target, identity, and simultaneous composition. In the direction, two ways of decomposing a pair of morphisms suggest different bracket formulas. Their equality is equation (3), using Lemma 33(f). In the direction, the interaction of two degree-one elements comes from the bracket functor’s preservation of a commuting square. The Jacobiator’s naturality and octagon must then correspond to the remaining identities. Finally, the constructions must act on homomorphisms and yield natural isomorphisms of functors (Baez–Crans, pp. 31–36).
The field has characteristic different from two in Theorem 36 and its §4.3 milestones, matching the standing assumption on p. 27. The §3 and §4.1 results retain the paper’s broader field convention. All vector spaces are unrestricted in dimension. A 2-vector space stores and defines its composition by Lemma 6. A 2-term -algebra is represented directly by Lemma 33(a)–(i), with and ; the general graded Definition 32 is outside scope.
The two categories are represented by raw object and morphism data with explicit predicates for lawful homomorphisms. An equivalence consists of functors preserving lawful morphisms, identities, and composites, together with natural isomorphisms in both directions. This representation keeps Propositions 25 and 35 as proof obligations and expresses the one-categorical content of Theorem 36. The stronger Theorem 39 asserts a 2-equivalence, but its 2-cell work is left without proof in the source and is not the goal here.
The Lie 2-algebra side retains the bracket’s functoriality on composable morphisms, the full naturality square, and the Jacobiator octagon. Its coherence is not replaced by Lemma 33’s equations: doing so would collapse the goal into a comparison of two copies of the same definition. The infrastructure for two-term complexes, 2-vector spaces, raw categories, curried multilinear maps, and their homomorphisms is reusable. Of Theorem 12 only the 2-cell correspondence is stated; the 2-functoriality of and the 2-naturality of the comparison isomorphisms are not. Of Proposition 25 only the one-cell category laws are stated; the 2-homomorphisms of Definition 24 are not. A formalization in which the Lie 2-algebra side is defined by arrow-part equations, or in which the equivalence omits the natural isomorphisms or the category laws, would trivialize the goal and is excluded. Contributions proving the displayed category laws, the and constructions, their functoriality, and the two natural isomorphisms are welcome.
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
Quantum mechanics is usually written in linear-algebraic terms: states are vectors of a complex Hilbert space, observables are Hermitian operators, and expectation values pair the two. Classical mechanics is written geometrically: states form a symplectic manifold, observables are functions on it, and dynamics is a Hamiltonian flow. A line of work starting with Kibble (1979) and continued by Cirelli, Lanzavecchia, Heslot, Ashtekar–Schilling (arXiv:gr-qc/9706069) and Brody–Hughston (arXiv:quant-ph/9906086) recasts quantum mechanics in the classical language: the Hilbert space, seen as a real manifold, carries a Kähler structure (a symplectic form, a Euclidean metric and a compatible complex structure), and observables become real quadratic functions on it.
Cariñena, Clemente-Gallardo and Marmo (arXiv:math-ph/0701053v2) organise this correspondence around one map, the momentum map of the unitary group acting on Hilbert space. The algebra of observables carries two products, a Lie product (the commutator) and a Jordan product (the anticommutator). The paper's Proposition 5 states that the momentum map carries both products, read as tensors on the dual of the unitary Lie algebra, to the symplectic and Euclidean parts of the Kähler structure of Hilbert space. This mission formalizes that statement in finite dimension.
Fix and let , with . The space of observables is the real vector space of Hermitian complex matrices. On it the paper defines:
Through (4), the dual is identified with Hermitian matrices . Each observable gives a linear function . On the paper defines the Lie–Poisson tensor (11), , and the Jordan tensor (12), .
On the Hilbert space side, use real coordinates . Every complex matrix defines the quadratic function . The canonical Poisson bracket is , and the contravariant Euclidean structure is . The momentum map is
For Hermitian and every :
In the paper's notation: , and .
In attack order:
Proposition 5 says that the algebra of observables can be read off Hilbert space geometrically:
This is the dictionary behind geometric treatments of the Schrödinger equation as a Hamiltonian flow. It also underlies variance and uncertainty relations written through the metric, and the reduction to projective space and density states that the paper discusses in §§2.5 and 4. The paper presents it as an alternative to the GNS construction for pure states.
The paper's proof is "Direct verification", and Lemmas 1–3 and Proposition 1 are classical facts about Hermitian matrices. No step is open. What the mission adds is a machine-checked version with every normalisation pinned, as listed in Formalization scope:
The paper uses both the Hermitian picture (3), (4), (6) and the anti-Hermitian picture (5), (11). The formal statement fixes the signs and factors needed to read their relation precisely. The prior-art search for this mission found no published Prove2Me statement with the same finite-dimensional objects and conclusion.
The algebraic milestones are short computations once the definitions are unfolded. The work concentrates in the goal, whose two sides live in different worlds.
The left side is built from real partial derivatives of real-valued functions on , viewed as . Its derivatives must be computed in the directions and and then recombined into complex inner products.
The right side is a trace of a product of matrices with the rank-one matrix .
The difficulty is that the derivative formulas use real coordinates while the tensor formulas use complex matrix products and traces. Their normalizations and sign conventions must agree at the level of the full identity, including the in and the factors of in the quadratic functions.
Replacing the derivative-defined brackets by their closed forms would make the goal trivial and is not permitted, see below.
All objects are defined in one definitions module in the namespace GeomQM.MomentumMap, over Mathlib's Matrix (Fin n) (Fin n) ℂ and vectors Fin n → ℂ.
Committed conventions.
IsHermitian hypothesis. Lemma 5 is about an arbitrary complex matrix, and equivariance needs no hypothesis. is allowed, since every statement then holds trivially, as in the paper.fderiv ℝ applied to Pi.single k 1 and Pi.single k I. This is the paper's .Ruled out. The brackets on are defined through real derivatives of arbitrary functions, never as or . The tensors on are trace formulas, never rewritten as quadratic functions of . Either shortcut would make bullets 2 and 3 hold by definition.
Not in scope. The following are not formalized:
Welcome contributions. Proofs of the milestones and of the goal, and general lemmas that would be reusable beyond this mission:
Fin n → ℂ;Integrable spin chains with a Lie superalgebra symmetry are lattice regularizations of two-dimensional field theories with target-space supersymmetry, such as the Gross–Neveu models and sigma models on superspaces, which appear in the study of disordered systems, polymers and the AdS/CFT correspondence. Their spectra are described by the nested Bethe ansatz: each eigenvalue of the transfer matrix corresponds to a family of complex numbers, the Bethe roots, solving a system of algebraic equations, the Bethe ansatz equations (BAE). The nested algebraic Bethe ansatz for general closed chains was carried out by Belliard and Ragoucy (arXiv:0804.2822).
C. Candu, Continuum Limit of gl(M|N) Spin Chains (arXiv:1012.0050), studies the antiferromagnetic chain of alternating fundamental and dual representations. Its §4 shows that a class of solutions of the BAE is fully characterized by solutions of the BAE, which embeds the spectrum into the spectrum. This is the algebraic counterpart of cohomological reduction (Candu–Creutzig–Mitev–Schomerus, arXiv:1001.1344), in which the chain is the cohomology of an odd nilpotent element acting on the chain. The paper uses this relation to compare all chains with fixed, and concludes that their continuum limits share the Gross–Neveu-like particle content.
This mission formalizes that restriction and lift of Bethe ansatz equations.
Let and . A grading assigns to each position a parity and a sign ; counts the even and the odd positions. The loop weight is . The simple roots are , ; is odd when .
For a chain of length the source terms are
For each type let be a finite set of pairwise distinct complex numbers and , with . The BAE (2.9) state that for every and every root ,
With (2.11), the energy (2.18) of a solution is
The paper works throughout under .
Fix with A1 ( odd) and A2 ( has no source term, ). R1 identifies the roots of types and . The reduced system deletes grading positions and root types : it is the BAE of a chain with simple roots .
Under A1, A2, R1 and non-degeneracy of the roots,
and . The forward direction is the restriction R1–R2; the backward direction is the reduction of the lift to "a solution … to either eq. (4.2) or eq. (4.4)".
The restriction gives an explicit map from Bethe solutions to Bethe solutions that preserves the energy. Iterated, it relates every chain to the chain, which is how the paper identifies the vacuum and the massive excitations of the chains in the continuum limit (§5–§6). It is also a concrete, equation-level check of cohomological reduction.
The result is proved in the paper by direct algebra. The result is not formalized anywhere on Prove2Me, which has no Bethe ansatz equations of any kind. This mission produces a precise statement of the nested BAE with their grading-dependent signs, shifts and boundary conventions, and a verified version of the restriction, including the bookkeeping that the paper leaves implicit: the reindexing of types, the change of the source terms of the reduced chain, and the invariance of the energy.
Each step is elementary algebra; the difficulty is bookkeeping. The sign , the shifts , and the boundary cases differ between the original and the reduced system: after deletion, the neighbour of type is type , and the last source term and the partial sums in (2.11) are those of a different grading. A naive argument that matches equations by position, or that treats the reduced system with the original source terms, misses these shifts. The backward direction needs non-degeneracy, because recovering (4.4) from (4.6) and (4.2) requires dividing by the two sides of (4.2).
Everything is in the namespace SuperBAE.Restriction and works over . Positions and types are natural numbers, and a grading is a Boolean function (true = odd), with . Root sets are Finset ℂ, which encodes the paper's requirement that no two roots of the same type coincide. equals outside . Only the homogeneous chain is modelled. The BAE are in division form, so every theorem carries a regularity hypothesis: at each root of type , the values , , , and are nonzero. This is the non-degeneracy the division form presupposes; it is imposed on the original system only. The standing assumption is kept as , although the algebra of §4 does not use it. A1 is the Boolean condition , and A2 is , .
The reduced system is the same BAE predicate applied to the deleted grading on positions and the reindexed roots, with its own source terms and its own loop weight. A formalization that writes the reduced equations by hand, or passes to the reduced chain as a parameter, is trivializing and is ruled out. Without the regularity hypothesis, Lean's convention would make degenerate configurations satisfy (2.9) vacuously; regularity excludes this, and a verification file checks that the hypotheses of the goal are jointly satisfiable and that regularity is not vacuous.
Out of scope: the Yang–Baxter and Yangian structure, the walled Brauer algebra, the weight constraints (4.1) and (4.8), existence and uniqueness of lifted type- roots, inhomogeneous chains, the boundary case of §4.3, and the thermodynamic limit. Proofs of the milestones are welcome, as are lemmas that put the finite-product manipulations of -polynomials into a reusable form.
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.Quantum key distribution (QKD) is the first quantum information task to reach the level of mature technology, already fit for commercialization. It aims at the creation of a secret key between authorized partners connected by a quantum channel and a classical authenticated channel. The security of the key can in principle be guaranteed without putting any restriction on the eavesdropper's power. The first two sections provide a concise up-to-date review of QKD, biased toward the practical side. The rest of the paper presents the essential theoretical tools that have been developed to assess the security of the main experimental platforms (discrete variables, continuous variables and distributed-phase-reference protocols).
This mission is the statement-level formalization of The Security of Practical Quantum Key Distribution (arXiv:0802.4155v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is I.B.5: intercept-resend information and disturbance (I.B.5: intercept-resend information and disturbance, 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.
28 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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:
Let be an algebra over a commutative ring . If is noetherian and is pure in , then the categories of rational left -modules and right -comodules are isomorphic. In the Hopf algebra case, we can also strengthen the Blattner-Montgomery duality theorem. Finally, we give sufficient conditions to get the purity of in .
This mission is the statement-level formalization of Duality and Rational Modules in Hopf Algebras over Commutative Rings (arXiv:math/0011207v1). 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 2.1 (Proposition 2.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.
11 results of the paper are not stated yet, because the library lacks an interface they need:
A 2-group is a "categorified" version of a group, in which the underlying set G has been replaced by a category and the multiplication map has been replaced by a functor. Various versions of this notion have already been explored; our goal here is to provide a detailed introduction to two, which we call "weak" and "coherent" 2-groups. A weak 2-group is a weak monoidal category in which every morphism has an inverse and every object x has a "weak inverse": an object y such that x tensor y and y tensor x are isomorphic to 1. A coherent 2-group is a weak 2-group in which every object x is equipped with a specified weak inverse x* and isomorphisms i_x: 1 -> x tensor x* and e_x: x* tensor x -> 1 forming an adjunction. We describe 2-categories of weak and coherent 2-groups and an "improvement" 2-functor that turns weak 2-groups into coherent ones, and prove that this 2-functor is a 2-equivalence of 2-categories. We internalize the concept of coherent 2-group, which gives a quick way to define Lie 2-groups. We give a tour of examples, including the "fundamental 2-group" of a space and various Lie 2-groups. We also explain how coherent 2-groups can be classified in terms of 3rd cohomology classes in group cohomology. Finally, using this classification, we construct for any connected and simply-connected compact simple Lie group G a family of 2-groups G_hbar (for integral values of hbar) having G as its group of objects and U(1) as the group of automorphisms of its identity object. These 2-groups are built using Chern-Simons theory, and are closely related to the Lie 2-algebras g_hbar (for real hbar) described in a companion paper.
This mission is the statement-level formalization of Higher-Dimensional Algebra V: 2-Groups (arXiv:math/0307200v3). 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 Strong monoidal functors preserve weak inverses (Proposition 3: strong monoidal functors preserve weak inverses, 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.
37 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 propose a general security definition for cryptographic quantum protocols that implement classical non-reactive two-party tasks. The definition is expressed in terms of simple quantum-information-theoretic conditions which must be satisfied by the protocol to be secure. The conditions are uniquely determined by the ideal functionality F defining the cryptographic task to be implemented. We then show the following composition result. If quantum protocols pi_1,...,pi_k securely implement ideal functionalities F_1,...,F_k according to our security definition, then any purely classical two-party protocol, which makes sequential calls to F_1,...,F_k, is equally secure as the protocol obtained by replacing the calls to F_1,...,F_k with the respective quantum protocols pi_1,...,pi_k. Hence, our approach yields the minimal security requirements which are strong enough for the typical use of quantum protocols as subroutines within larger classical schemes. Finally, we show that recently proposed quantum protocols for oblivious transfer and secure identification in the bounded-quantum-storage model satisfy our security definition, and thus compose in the above sense.
This mission is the statement-level formalization of Composing Quantum Protocols in a Classical Environment (arXiv:0804.1059v2). 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 2.1: three approximate conditional-independence bounds (Lemma 2.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.
13 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:
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:
We provide a model of the String group as a central extension of finite-dimensional 2-groups in the bicategory of Lie groupoids, left-principal bibundles, and bibundle maps. This bicategory is a geometric incarnation of the bicategory of smooth stacks and generalizes the more naïve 2-category of Lie groupoids, smooth functors, and smooth natural transformations. In particular this notion of smooth 2-group subsumes the notion of Lie 2-group introduced by Baez-Lauda. More precisely we classify a large family of these central extensions in terms of the topological group cohomology introduced by G. Segal, and our String 2-group is a special case of such extensions. There is a nerve construction which can be applied to these 2-groups to obtain a simplicial manifold, allowing comparison with with the model of A. Henriques. The geometric realization is an -space, and in the case of our model, has the correct homotopy type of String(n). Unlike all previous models our construction takes place entirely within the framework of finite dimensional manifolds and Lie groupoids. Moreover within this context our model is characterized by a strong uniqueness result. It is a unique central extension of Spin(n).
This mission is the statement-level formalization of Central Extensions of Smooth 2-Groups and a Finite-Dimensional String 2-Group (arXiv:0911.2483v3). 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 51: double inverse is naturally identity (Lemma 51, PDF p. 20). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
36 results of the paper are not stated yet, because the library lacks an interface they need:
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:
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: