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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many infinite-dimensional Lie groups arising in geometry and physics — loop groups, gauge groups, groups of diffeomorphisms and of volume-preserving diffeomorphisms — have interesting central and abelian extensions, and these extensions are usually found first at the level of Lie algebras, as continuous 2-cocycles. Whether such a Lie algebra extension comes from a Lie group extension is a genuine question: in infinite dimensions there is no Lie's third theorem, and topological obstructions from and appear. K.-H. Neeb's paper [Ne04] answers it for abelian extensions of a connected Lie group by an arbitrary smooth -module whose identity component is a quotient of a vector space by a discrete subgroup. It generalises the central case treated in [Ne02] and the classical finite-dimensional theory.
Timeline:
Let be a connected real Lie group modelled on a Banach space, with Lie algebra , the bracket being that of left-invariant vector fields. A smooth -module is an abelian Lie group with a smooth action by group automorphisms. Throughout, its identity component is : there is a smooth homomorphism from a Banach space which is a local diffeomorphism onto with discrete kernel . The action differentiates to an action of on and an action of on ; write .
A continuous 2-cocycle is an alternating continuous bilinear map satisfying the Chevalley–Eilenberg cocycle identity; it defines the Lie algebra on with bracket
It integrates if there is a Lie group extension — a principal -bundle whose conjugation action on is the given one — whose Lie algebra is equivalent to .
Three invariants enter:
For , the extension integrates to with connected if and only if
If is connected, the second condition reads .
The criterion turns the existence of a Lie group extension, a global geometric object, into two homomorphisms that can be computed from and the topology of : periods on and fluxes on . The paper applies it to diffeomorphism groups, to acting on spaces of -densities, and to Lichnerowicz cocycles on groups of volume-preserving diffeomorphisms; it also underlies the exact sequence relating to (Theorem VII.2).
The results are proved in the paper; none of them, nor the objects they are stated in (period group, flux, characteristic homomorphism, abelian Lie group extensions), has been formalized before. Formalizing them produces the first machine-checked integrability criterion for Lie algebra extensions, together with a reusable layer for abelian extensions of Banach–Lie groups on top of Mathlib's LieGroup and GroupLieAlgebra.
The necessity of both conditions follows from the long exact homotopy sequence of the principal bundle , once the connecting maps are identified with on and with the flux on ; each identification is a Stokes-theorem computation on a group that is not given in coordinates. Sufficiency is harder. The obvious approach, building directly from a local group cocycle, fails when is not simply connected: the cocycle on the universal cover does not descend, and the obstruction is exactly the flux. One has to construct the extension over , show that the lifted splits centrally, take the quotient, and then recognise the resulting kernel as by comparing characteristic homomorphisms. Mathlib has no long exact homotopy sequence of a bundle, no integration of differential forms on manifolds, and no construction of Lie groups from local data.
All Lie groups are real and modelled on Banach spaces, with smooth meaning ((⊤ : ℕ∞), not analytic); this is a special case of the paper's sequentially complete locally convex spaces over or . All types are in Type. Conventions committed to:
Extension) is a Lie group charted on with smooth , surjective smooth , , a smooth local trivialisation near , the prescribed conjugation action, and a topological linear isomorphism compatible with , and the brackets."Integrates" is never a restatement of the two conditions: it asserts the existence of such an extension, and dropping the bracket clause, the conjugation clause or the local trivialisation would make it a different statement.
Lemma III.7 is stated with an isomorphism; with a mere homomorphism, as printed, it is false. A complete development needs path lifting and the homotopy sequence for principal bundles, Stokes' theorem for maps , the universal covering group of a Banach–Lie group, and quotients of Lie groups by discrete central subgroups; all of this is reusable beyond this mission. Contributions of any of these pieces, and of further results of the paper (Proposition IV.5, Corollaries VI.5 and VI.6, Theorem VII.2), are welcome.
A convex form is a homogeneous polynomial of even degree whose value is convex as a function of its real variables. Every convex form is nonnegative, so it is natural to ask whether it can always be written as a sum of squares (SOS) of real polynomials. This matters in polynomial optimization because an SOS certificate can be searched for through semidefinite programming, while pointwise nonnegativity is generally harder to certify. Parrilo posed the convex versus SOS question in 2007. Blekherman proved nonconstructively that convex forms outside the SOS cone exist in sufficiently many variables. Saunderson constructed an explicit quartic example in 272 variables, together with a finite certificate of its failure to be SOS Saunderson, pp. 1–3.
An octonion is an eight-dimensional real normed division algebra. Write for conjugation and for the sum of squares of its eight coordinates. For two lists and of octonions, let and . The octonionic Cauchy–Schwarz form is
Each octonion contributes eight real coordinates, so this is a quartic polynomial in real variables. The paper's companion form is
To measure the SOS relaxation, and are the minimum and maximum of a form on the Euclidean unit sphere. For a degree- form, is the largest for which is SOS. When , the paper defines
These are values of the specific polynomial, not free parameters. The SOS predicate concerns finite sums of squares in the real multivariate polynomial ring Saunderson, pp. 2–4.
For every , the target is the full Theorem 1.2:
The milestone list includes the near-constant-on-the-sphere convexity criterion, its bound-based corollary, the octonionic inequality, the matrix identity for , the symmetry-reduced SOS characterization, the explicit feasibility system, and the exact SOS threshold at . The threshold is a separate claim: is SOS for and is not SOS for Saunderson, Theorems 1.2 and 4.11.
The theorem supplies an explicit counterexample to the assertion that convexity of an even-degree homogeneous polynomial forces an SOS representation. At , it is a concrete quartic in variables. Its gap also gives an explicit case where the basic SOS lower bound for optimization on a sphere is more than a factor two away in the paper's normalized measure. Thus the example links an algebraic separation of two cones with a numerical limitation of an optimization relaxation Saunderson, pp. 2–4.
The mathematical theorem is proved in the cited paper. The work here is to encode its octonion multiplication table, quartic polynomial, symmetry action, and finite feasibility certificate in Lean, then close the formal proofs. The group and polynomial definitions can also support other examples based on Clifford systems or structured SOS relaxations. The statements in this proposal compile with sorry; they are proof targets, not machine-checked proofs.
Nonnegativity of follows from octonionic Cauchy–Schwarz, and near-constant values on the sphere yield convexity after the stated correction. The obstacle is proving that has no SOS representation: evaluating a nonnegative polynomial at a few points cannot rule out SOS. The paper uses its symmetry to reduce the SOS question to eight nonnegative coefficients and then exhibits an infeasible three-row system. The corresponding positive SOS decomposition at marks the exact boundary Saunderson, §§3–4.
The variables are indexed by and the forms live in MvPolynomial over . The first eight rows of each matrix column are , the last eight are . The octonion product is computed from the paper's right-multiplication table; the inner product conjugates its first argument. The squared Euclidean norm is the polynomial , and the unit sphere is defined by the corresponding real sum, not by the default norm on a function type. The SOS predicate is Mathlib's polynomial IsSumSq.
The symmetry group called in the paper is represented by its concrete matrix model preserving the span of nine Clifford matrices. The eight use the equivalent orthogonal-projection formula: supplies the normalized basis of the Clifford subspace, and the three matrix projections select scalar, traceless symmetric, and skew-symmetric parts. The paper's printed unscaled are orthogonal with squared trace norm ; the factor in the definition accounts for this normalization. No assumption that the polynomial is SOS enters the definition of ; it is built from the octonion product itself.
For the general degree- milestones, and a nonempty finite variable type make explicit the paper's positive-degree, positive-dimension setting. Lemma 2.2 uses arbitrary lower and upper bounds, as its proof and its application at do. The scalar extrema and SOS bound are represented by real sSup and sInf; these operations return default values on empty or unbounded sets. The goal has , where the sphere is nonempty and compact and the extrema have their intended meaning. Formal work is welcome on these endpoint facts, the octonionic identities, invariant polynomial spaces, and the finite infeasibility certificate.
Active-set methods for optimization and variational problems run in two phases. A globally convergent first phase identifies which constraints are active at the solution; once they are identified the problem simplifies locally, and a second phase converges fast, typically by linearizing the simplified problem. Sequential quadratic programming for nonlinear programming is the classical instance: near a solution satisfying the standard second-order conditions, the graph of the normal-cone operator and the space are manifolds meeting at a single point, and one Newton step linearizes the first, intersects with the second, and restores the result.
The property behind the first phase, finite identification of an active manifold, is formalized by partial smoothness, introduced by Lewis (SIAM J. Optim., 2002) after Wright's identifiable surfaces (SIAM J. Control Optim., 1993); its constant-rank characterization is in Lewis and Liang, arXiv:1807.03134. Lewis and Wylie (arXiv:1902.00724) isolate what drives the second phase in the same geometric language: two manifolds intersecting transversally at an isolated point, a semi-linearization step, and a constant-rank map between the manifolds that splits the restoration step into a primal and a dual update. Their Theorem 5.1 is the general result; applied to the graph of a set-valued map it gives an active-set Newton method for generalized equations with partly smooth.
Let be a Euclidean space with norm . A set is a -manifold around a point if there are a -smooth map with surjective derivative and an open set with .
The tangent space is the linear span of the tangent cone of at , and the normal space is . For a manifold, . Two manifolds , around intersect transversally at if , and is an isolated point of intersection if for some open .
The semi-linearization point of is the unique point where the linear approximation meets near : only is linearized.
A map from into is -smooth and constant rank nearby if it is on a neighborhood of and the rank of on is the same for all near . For a neighborhood of the image is the active manifold. is the nearest-point projection onto a set . An iteration converges quadratically to if, from every start close enough to , the iterates stay in near , converge to , and satisfy with one constant .
Let be an isolated, transversal point of intersection of two -manifolds and around , and let fix and be -smooth and constant rank nearby. Then for every sufficiently small ball around :
and for every such and the iteration converges quadratically to .
The result. Theorem 5.1 turns an abstract Newton scheme into an active-set method. Corollary 3.5 needs a Lipschitz restoration map from back into , which in applications is coupled and opaque; Theorem 5.1 builds from a constant-rank map, so the primal variables are updated by projecting onto the active manifold and the dual variables by a fiber projection with the primal part held fixed. With , and this yields the paper's Theorem 5.5 for partly smooth generalized equations, and through it Newton-type methods for variational inequalities over partly smooth sets (§6).
Formalizing it. The theorems are proved in the paper; none is machine-checked. The mission produces a statement of Theorem 5.1 at the level of sets in a Euclidean space, with every hypothesis explicit, and the intermediate results it depends on. A proof needs, in Lean, the identification of the tangent cone of a zero-set manifold with the kernel of the derivative, the semi-linearization estimate via the implicit function theorem, the constant-rank theorem for maps between embedded submanifolds, and local Lipschitz continuity of nearest-point projections onto submanifolds. Several of these are absent from Mathlib in this form.
The convergence claim follows from Corollary 3.5 once (a)–(c) are available, and Corollary 3.5 follows from the quadratic estimate (3.2). The hard part is (a)–(c). Mathlib has no constant-rank theorem, which is what makes a manifold. And the image is not closed, so neither the nearest point of to a point of nor the nearest point of a fiber need exist: both projections are single-valued and Lipschitz only near , and the obvious argument (project onto a closed set) does not apply. A second obstacle is that enters at points , so the identification of the tangent cone with the classical tangent space is needed at every point of near , not only at .
EuclideanSpace ℝ (Fin m). Smoothness is ContDiff ℝ r with a natural number. All maps (, , , , ) are total functions on ; mapping and Lipschitz conditions are imposed only on the paper's domains (, ), never globally.ProjLikeRetr.Retractor.tangentBundle (span of tangentConeAt and its orthogonal complement), so they do not depend on a choice of .Contributions welcome: the tangent-cone/kernel identity (reusable for any zero-set manifold), a constant-rank theorem for maps between embedded submanifolds of a Euclidean space, and local Lipschitz continuity of the projection onto a submanifold. All three are useful well beyond this mission.
A mechanism designer chooses a rule for turning agents’ messages into an outcome. When agents know their own types but have only beliefs about the others, the designer cannot assume that they use a single equilibrium strategy. Interim correlated rationalizability instead keeps every message that is a best response to some belief consistent with the agent’s information and with the other agents’ surviving messages. A rule that produces the desired outcome for all such messages is robust to this uncertainty about strategic play. Kunimoto, Saran, and Serrano study which social choice functions can be implemented under this solution concept. Their sufficiency result identifies two conditions on a suitable version of the target rule: weak interim rationalizable monotonicity and a weak no-worst-rule condition. The published article is Kunimoto, Saran, and Serrano (2024); this mission follows the authors’ October 2020 Bravo working-paper version, whose pagination and theorem labels are used below.
The paper separates necessity from sufficiency. Theorem 4.5 shows that implementability implies weak interim rationalizable monotonicity of some equivalent social choice function. Theorem 6.3 gives sufficiency when the equivalent function also satisfies weak no-worst-rule. Its Example 7.1 uses the sufficiency theorem to exhibit implementation in rationalizable strategies beyond the stronger conditions discussed in the earlier literature. This mission targets Theorem 6.3 and its stated supporting results.
There is a finite set of agents. Agent has a finite nonempty type set and, upon learning , holds an interim belief about the other agents’ types. The full type space is . A finite set contains the pure outcomes, and is its set of lotteries. Agent evaluates a lottery by the expected value of a state-dependent utility over pure outcomes . A social choice function is .
The designer cares about a set containing every state to which at least one agent assigns positive interim probability. Two social choice functions are equivalent, written , when they agree on . A mechanism has a nonempty countable message space for every agent and an outcome rule .
For a proposed correspondence , the operator retains a message if it is a best response to some probability distribution over . This distribution must have type marginal and assign positive weight only to the other agents’ messages in . The correspondence is the largest fixed point of . The mechanism implements when there is an equivalent such that is nonempty for every type and every rationalizable message profile at every state yields . The uniqueness condition ranges over all of , including states outside .
Weak interim rationalizable monotonicity (weak IRM) is a condition on deceptions. A deception lets each true type be reported as one of several types, including itself. If some allowed report profile changes the chosen lottery, the deception is unacceptable. Weak IRM requires every unacceptable deception to be refutable: for some responsive misreport, and against every compatible belief over true other-agent types and announced full type profiles, there is an alternative social choice function that gives the true type a strict incentive to expose the deception while meeting the paper’s restrictions on each announced-type section.
The weak no-worst-rule condition (weak NWR) says that for every agent, type, and distribution over two copies of , the lotteries in the weakly worse contour of do not all have the same expected utility under that distribution. The two distributions in this definition serve different roles: one describes the true other-agent types and the other indexes the outcome assigned by a candidate rule.
Theorem 6.3 is the mission goal:
The goal asks for an implementing mechanism with countable nonempty message spaces. It fixes no canonical-mechanism parameter or numerical bound. The milestone list follows the paper’s fixed-point observation, Lemmas 5.2 and 6.2, and Steps 1–3 of the proof of Theorem 6.3. Lemma 5.2 links weak IRM to strict-if-responsive Bayesian incentive compatibility. Lemma 6.2 supplies strict payoff comparisons from weak NWR. The steps establish the behavior and nonemptiness of rationalizable messages in the canonical mechanism.
The result gives a sufficient test for implementation when agents may choose any interim correlated rationalizable messages. It specifies conditions on a social choice function rather than asking the designer to inspect every equilibrium of an arbitrary mechanism. The paper uses it to certify its later example of a rule that is implementable under this solution concept while failing stronger implementation conditions.
Formalizing the result would add a reusable finite-type model of interim beliefs, correlated best-response beliefs over countable message spaces, and a greatest-fixed-point account of rationalizable messages. It would also add precise definitions of deceptions and weak refutability. The paper proves the theorem; the Lean statements in this proposal are open proof obligations. The definitions and their encoding of countable expected payoffs can be reused in later implementation-theory developments.
The main obstacle is the universal reach of the solution concept. To exclude a message from the greatest fixed point, the argument must address every compatible correlated belief, not one selected equilibrium belief. In the canonical mechanism, different messages activate different outcome rules, so a deviation that is profitable against one class of beliefs need not work against another. The proof also uses strict payoff comparisons after replacing arbitrary lotteries by a countable dense family of challenges. Simply restricting attention to truthful direct reports would miss the message profiles whose elimination is the point of rationalizable implementation.
The Lean model uses finite agent, type, and outcome sets; each type set is nonempty because the paper’s interim probability beliefs presuppose that the other-type profile space can carry a distribution. A lottery is a real vector in the standard simplex, and utility on lotteries is linear in that vector. Other-agent profiles are dependent functions on indices distinct from . Beliefs over other-agent types and messages are nonnegative real functions with the required marginal expressed by a convergent sum. Expected payoffs use countable sums, and the best-response predicate explicitly requires their summability. Thus a non-summable family cannot obtain a default zero payoff and become a spurious best response.
The greatest rationalizable correspondence is the supremum of all post-fixed message correspondences for the mechanism’s actual best-response operator. It is never a free correspondence supplied as a hypothesis. Implementation keeps the paper’s countability, nonemptiness, and all-state uniqueness requirements. These choices rule out vacuous implementations obtained by using an empty message set, a least fixed point, or uniqueness only on .
The canonical proof uses a countable dense set , positive integers for the second message component, and full-support lotteries and challenge mixtures. Its Rule 2 weights are and ; Rule 3 assigns each agent’s pure outcome weight and the remainder to a full-support baseline lottery. The paper’s finite enumeration written as an infinite geometric series may not normalize, so the formalization takes normalized full-support mixtures with exactly the property used later. Steps 1–3 use at least two agents because Rule 2-1 does not choose a unique type with one agent. The main theorem has no such restriction; its one-agent case is a separate direct-mechanism proof obligation. Lemma 6.2(a) is stated in the cross-type form invoked in Step 1, which specializes to the printed same-type lemma. Step 3 assumes BIC, the part of Lemma 5.2 that its argument uses. Contributions toward density, summability, finite convex mixtures, and the one-agent case are welcome.
A sum of rational functions is a common objective when several performance measures each have a polynomial numerator and a positive polynomial denominator. Such problems appear, for example, in the applications to computer vision and signal processing cited by Guo, Wang and Zheng in their 2024 preprint. Even when all constraints and numerators are polynomial, the objective need not be convex, and its global minimum can be difficult to certify. Bugarin, Henrion and Lasserre studied a hierarchy based on a measure reformulation of this problem in Minimizing the sum of many rational functions. Guo, Wang and Zheng develop its polynomial dual and exploit sign symmetries to obtain a hierarchy with block-diagonal semidefinite matrices.
The mission targets the convergence assertion in Theorem 4.7(ii) of the pinned preprint, arXiv:2405.09419v1. Its mathematical question is precise: do the lower bounds from the sign-symmetry-adapted semidefinite relaxations increase to the true global infimum? The statement is already proved in the paper. Its formal proof and the supporting algebra are the work posed here.
Fix real variables, ratios, and polynomial inequality constraints. For polynomials , let
Assumption 1.1 says that is compact and each is strictly positive on . The mission also requires : the paper's definition of the distinguished support set can omit the constraint supports when , and the advertised sparse convergence then fails. This repair is explicit in the formal goal.
A polynomial is a sum of squares (SOS) if it is a finite sum of squares of real polynomials. The quadratic module comprises with every SOS. Its order- truncation restricts the degrees of and to . The Archimedean condition asks for some with ; it is a separate hypothesis in the convergence theorem.
For a finite monomial-exponent set , the sign-symmetry group consists of the vectors for which is even for every . Its closure contains every exponent fixed by all these parity tests. The sign action substitutes for . The paper forms from the supports of , and all for ; contains the first numerator and denominator supports and the other .
The sparse quadratic module represents each SOS multiplier with a positive semidefinite Gram matrix indexed by monomials of bounded degree. A matrix entry at exponents must vanish when . The program (SDk) uses for the distinguished ratio and for each other ratio. Its auxiliary polynomials have support in and degree at most . The resulting optimal value is .
The main theorem is the paper's Theorem 4.7(ii): under Assumption 1.1 and the Archimedean condition, the sparse bounds rise to the original optimum,
The formal statement spells this out as monotonicity for , the lower-bound inequality , and convergence to . Here is the maximum of the rounded-up half-degrees of all numerators, denominators, and constraints, as defined on page 4 of the paper. No convergence rate is asserted.
The milestone list follows the source's claims: invariance of the data under sign flips (Lemma 4.2), cancellation of nonsymmetric monomials in the averaging argument, two-sided polynomial approximation in the proof of Theorem 3.1, equality of the polynomial dual value with (Theorem 3.1), equality of the sign-symmetric dual value with (Theorem 4.3), the sign-symmetric Positivstellensatz (Theorem 4.5), monotonicity in the proof of Theorem 4.7(ii), and the sparse-versus-dense inequality in Theorem 4.7(i). These are mathematical targets, not assumed facts in the goal.
A finite level of (SDk) supplies a certified lower bound on the global sum-of-ratios minimum. Theorem 4.7(ii) says that increasing the degree loses no value asymptotically while preserving the sign-induced zero pattern in the Gram matrices. The pattern can split a semidefinite constraint into smaller blocks; the paper demonstrates this computationally, but the theorem itself concerns correctness of the limiting bounds, not a runtime guarantee. The related term-sparsity framework is developed by Wang, Magron and Lasserre in TSSOS.
A Lean development of the known result would supply reusable definitions for support-based parity symmetries, sparse SOS Gram certificates, and extended-real optimal values of polynomial dual programs. None of this mission's proposed results has an existing machine-checked proof in the local prior-art search. The original paper establishes the mathematics; this mission asks solvers to formalize that proof and its stated intermediate results.
Ordinary SOS certificates do not automatically respect a prescribed zero pattern in their Gram matrices. Likewise, restricting the auxiliary polynomials to the symmetry-closed supports changes the dual feasible set. Thus the dense hierarchy's convergence theorem alone does not yield the sparse claim. The decisive issue is whether strictly positive polynomials with the relevant support admit sparse certificates, while the approximation steps retain the sign symmetries and the exact degree restrictions of (SDk).
Lean uses MvPolynomial (Fin n) ℝ and points Fin n → ℝ. The paper's ratio is Lean index 0; means i ≠ 0. Sign vectors are Fin n → ZMod 2, monomial exponents are finitely supported natural-number vectors, and the Gram matrices are finite matrices over the monomials of degree at most the relevant order. The zero pattern is tested against , not against . Every optimum is an EReal supremum or infimum, so an infeasible (SDk) has value and an empty gives . On , the positivity assumption makes every ratio well-defined as intended.
The hypothesis is necessary for the paper's formula to contain the constraint supports. It rules out a one-ratio counterexample to the sparse claim; it is disclosed in the goal and the affected milestones. Degrees use natural-number arithmetic only at orders , where the subtractions match the paper's bounds. A valid formalization must retain positive semidefiniteness, the matrix pattern, the correct support sets, and the exact degree bound. Dropping any of these would state a different hierarchy.
Reusable contributions include the polynomial and SOS definitions, the parity action, the Gram construction, and the sparse Positivstellensatz. Solvers may develop auxiliary lemmas for the monotone inclusions or the approximation argument, while keeping each audited theorem statement faithful to the source. The moment-side formulation, convergence rates, correlative sparsity, and numerical examples lie outside this mission.
Mean field games describe the limit of stochastic differential games with a large number of statistically identical players, each interacting with the others only through the empirical distribution of their states (Lasry and Lions, Mean field games, 2007; Huang, Malhamé and Caines, 2006). Models whose players move among finitely many states (an infection status, a cyber-security level, a choice among a few technologies) are used in epidemiology, botnet defense (Kolokoltsov and Bensoussan, 2016; reference [19] of the paper) and economics. For these finite state games the analytic approach of Gomes, Mohr and Souza (Continuous time finite state mean field games, 2013) characterizes equilibria by a coupled system of ordinary differential equations, and so restricts attention to Markovian controls and to interactions through the distribution of states only.
Carmona and Wang (arXiv:1808.07635, 2018; Mathematics of Operations Research, 2021) treat the finite state game in the weak formulation, by a change of measure on the canonical path space, following the diffusion case of Carmona and Lacker (A probabilistic weak formulation of mean field games and applications, 2015). This handles two extensions at once: strategies may be arbitrary closed-loop, path-dependent controls, and the rates and costs may depend on the distribution of the controls themselves (an extended mean field game).
There are states, identified with the basis vectors of . The canonical space consists of the càdlàg paths that are continuous at ; is the canonical process and its natural filtration. The reference measure makes a continuous-time Markov chain with a given initial law and rate matrix (diagonal entries , off-diagonal entries ).
Controls take values in a compact set . Write for the probability simplex of , for the probability measures on and for the 1-Wasserstein distance on . A strategy is an -predictable process with values in . A mean field is a pair of measurable flows (states) and (controls). Transition rates , a running cost and a terminal cost are given.
A strategy and a mean field change into , whose density is the Doléans-Dade exponential of (5)–(7); under it jumps from to at rate . The cost is
A Nash equilibrium (Definition 2.8) is a triple such that minimizes over , and for every , is the law of and the law of under .
The reduced Hamiltonian is , and .
Under Assumption 2.2 (each is a Q-matrix, off-diagonal rates lie in with , rates are Lipschitz in ), Assumption 2.7 ( and Lipschitz) and Assumption 3.4 ( has a unique minimizer , independent of , measurable and Lipschitz in the sense of (21)),
The theorem gives equilibria for finite state mean field games without the Markovian restriction and with interaction through the distribution of controls, in a setting where the analytic (ODE) approach does not apply. The same weak formulation supports the paper's uniqueness result under a Lasry–Lions monotonicity condition and the construction of approximate Nash equilibria for the -player game (Theorems 5.4 and 6.5), which are not part of this mission.
The result is proved in the paper; nothing here is open mathematics. No part of it is machine-checked. A formalization would add, beyond the theorem itself: the reference Markov chain on the canonical càdlàg space, Girsanov changes of measure for chains with bounded rates, backward SDEs driven by a Markov chain (Cohen and Elliott's theory), the J1 topology on finite-valued paths, and the stable topology of Jacod and Mémin. While drafting, Proposition 4.5 of the paper was found to be false as printed (see Formalization scope); the formalization records the corrected argument structure.
The obvious approach, a fixed point of the laws under the best response, fails for lack of compactness: sets of measurable flows or have no useful compact subsets. The paper replaces the state flow by a law on path space, where compactness comes from tightness in the Skorokhod topology, and the control flow by a measure on with the stable topology, where compactness requires fixing the time marginal. Continuity of the fixed-point map then needs stability of Markov-chain BSDEs and control of Girsanov densities, both uniform in the mean field. In Lean, Schauder's fixed point theorem, Prokhorov's theorem on Skorokhod space, Girsanov's theorem for jump processes and BSDE theory are all absent from Mathlib.
All declarations are in the namespace ExtFSMFG.Existence. Time is indexed by , and paths are frozen after (in bijection with the paper's paths on ); states are Fin m. The reference measure is a hypothesis, IsReference, fixing the finite-dimensional distributions through . is defined by the closed form of (an exponential of the compensator times the product of the rates at the finitely many jumps), and stochastic integrals against the chain's martingale are pathwise. is Euclidean. carries the weak topology and its Borel -field; and are infima over couplings. appears as an argument of Assumption 3.4, which pins it down.
One hypothesis is added and disclosed: and are jointly measurable and is bounded (RegularData). The paper uses both (for (5), (12) and the BSDE drivers) without stating them. BSDE solutions have a predictable (the paper writes "left-continuous"); has the marginal constraint that (40) omits; (42) uses the rates of (5).
The equilibrium is stated through Definition 2.8 itself, so a formalization in which the equilibrium is a fixed point of , the strategy set is shrunk to Markov feedback controls, the density is a junk value, or optimality is phrased through an infimum that may default to , is ruled out: optimality is " for every predictable -valued ".
Proposition 4.5 (" is compact, metrizable, and Polish") is not a milestone: as printed it is false, since has no cluster point in for the stable topology (test with ). Only the compactness of (Lemma 4.7) is used. Lemmas 3.1, 3.3, 4.3, Propositions 4.12, 4.14, 4.16 are further steps of the proof that may be added as milestones later. Contributions welcome: a proof of the sanity-level facts (the density integrates to ; is a metric on ), Lemma 3.7 and Lemma 4.8, which are elementary, and Markov-chain BSDE infrastructure.
A transformation achieving the optimal symmetric N-to-M cloning of coherent states is presented. Its implementation only requires a phase-insensitive linear amplifier and a network of beam splitters. An experimental demonstration of this continuous-variable cloner should therefore be in the scope of current technology. The link between optimal quantum cloning and optimal amplification of quantum states is also pointed out.
This mission is the statement-level formalization of Optimal cloning of coherent states with a linear amplifier and beam splitters (arXiv:quant-ph/0012046v1). 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 Optimal coherent-state cloning by concentration, amplification, and distribution (Unnumbered main result; Eqs.(10)–(12), 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.
We consider two examples of dynamical semigroups obtained by singular perturbations of a standard generator which are special case of unbounded completely positive perturbations studied in detail in [10]. In the section 2 we propose a generalization of an example from [1] aimed to give a positive answer to a conjecture of Arveson. In the section 3 we consider in greater detail an improved and simplified construction of a nonstandard dynamical semigroup outlined in our short communication [13].
This mission is the statement-level formalization of On singular perturbations of quantum dynamical semigroups (arXiv:1706.04866v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Rebound diffusion is conservative and nonstandard (§3.2, unnumbered main result: the rebound diffusion is nonstandard, 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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
An expression is derived characterizing the set of admissible rate pairs for simultaneous transmission of classical and quantum information over a given quantum channel, generalizing both the classical and quantum capacities of the channel. Although our formula involves regularization, i.e. taking a limit over many copies of the channel, it reduces to a single-letter expression in the case of generalized dephasing channels. Analogous formulae are conjectured for the simultaneous public-private capacity of a quantum channel and for the simultaneously 1-way distillable common randomness and entanglement of a bipartite quantum state.
This mission is the statement-level formalization of The capacity of a quantum channel for simultaneous transmission of classical and quantum information (arXiv:quant-ph/0311131v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: simultaneous capacity region and alphabet bound (Theorem 1: simultaneous capacity region and alphabet bound, 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.
4 results of the paper are not stated yet, because the library lacks an interface they need:
The concept of translation of an operator allows to consider the analogous of shift-invariant subspaces in the class of Hilbert-Schmidt operators. Thus, we extend the concept of average sampling to this new setting, and we obtain the corresponding sampling formulas. The key point here is the use of the Weyl transform, a unitary mapping between the space of square integrable functions in the phase space and the Hilbert space of Hilbert-Schmidt operators on , which permits to take advantage of some well established sampling results.
This mission is the statement-level formalization of Average sampling in certain subspaces of Hilbert-Schmidt operators on (arXiv:2011.05871v2). 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 §3, Eq. (3), unnumbered: average sampling of one-generator HS subspaces (§3, Eq. (3), unnumbered: average sampling of one-generator HS subspaces, PDF p. 8). 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.
Monte Carlo tree search repeatedly chooses actions using estimates built from earlier simulations. The rewards attached to an action need not form an independent, identically distributed sequence: deeper parts of the search tree change as the search proceeds. Shah, Xie and Xu isolate this difficulty in a non-stationary multi-armed bandit and study a version of upper confidence bound selection with a polynomial exploration bonus. Their bandit theorem is the concentration result used in their subsequent analysis of tree search; it is a distinct finite-sample result with explicit assumptions and constants. Shah, Xie and Xu, §5–§7
The mission concerns Theorem 3 of arXiv:1902.05213v4, including both its expected-reward bound and its two-sided concentration bound. It provides the bandit foundation for the paper's later Monte Carlo tree search statements. The latter require a separate model of the search tree and are outside this mission. Shah, Xie and Xu, Theorems 1 and 3
A reward table has arms and random variables , where is the reward obtained on the th play of arm . Every reward lies in for a fixed . The arm's empirical mean after plays is , and the expectations of these means converge to . Rewards may depend on earlier rewards, including rewards from other arms. The model imposes no independence or identical-distribution assumption. Shah, Xie and Xu, §5, equation (12)
The per-arm concentration assumption fixes , , and . For every , both tails of beyond have probability at most . This describes each arm's complete reward sequence without specifying a filtration or a sampling law. The limiting optimal arm has mean ; each other arm has gap . Shah, Xie and Xu, §5, equation (13)
A run chooses arm at round . Its count records how many rounds through chose arm , and its average reward is . The polynomial UCB index is for , with . At round , the run maximizes the index formed using counts and bonus time . An unplayed arm has infinite priority, and ties among eligible arms are arbitrary. Shah, Xie and Xu, §5.1–§5.2, equations (14)–(16)
Theorem 3.A bounds the gap between expected run reward and the best limiting arm mean. With a positive lower bound for every , and , the target for is
The first term is the optimal arm's own finite-sample bias. The remaining term is explicit in the bandit parameters. Lemma 2 and the displayed decomposition on page 18 are the curated targets for this part. Shah, Xie and Xu, Theorem 3.A and §6
Theorem 3.B states that one constant , depending only on , bounds both tails for every admissible reward table, measurable UCB run, horizon , and :
The tuning parameter satisfies and . Lemma 1, the event inclusion (34), the play-count tail (36), and Lemma 3 are the curated targets for this part. The same theorem statement carries parts A and B. Shah, Xie and Xu, Theorem 3 and §6.1–§6.3
The expected-reward bound relates the run's finite-horizon mean to the optimal arm's own mean and to an explicit penalty for sampling other arms. The concentration bound says that the run's cumulative reward inherits polynomial two-sided tails at a derived exponent. Together these claims let the paper apply a bandit guarantee in its analysis of Monte Carlo tree search, where an action's reward process changes as the search continues. Shah, Xie and Xu, §6–§7
The result is proved in the cited paper; the mission seeks a machine-checked Lean development of that known result. Its reward-table model and finite-sample count estimates may be reused when a sequential choice rule is analyzed without independent arm rewards. The mission currently provides compiled definitions and theorem statements as proof targets, not verified proofs of those targets.
A standard stationary-bandit analysis would replace each arm's history by independent draws from a fixed law. Here the assumptions give only convergence of expected arm means and polynomial per-arm concentration. A run also samples arms adaptively, so the random number of observed rewards on an arm cannot simply be inserted into a fixed-sample tail inequality. The finite-sample guarantee has to retain the exact dependence on the bonus, arm gaps, pull counts, and the tuning window. The paper's intermediate results identify the required count and tail statements. Shah, Xie and Xu, §6.1–§6.3
Lean uses a probability space , a table , and a run . Play numbers begin at one; index zero is unused. The model makes reward measurability, boundedness, limiting expected means, and both concentration inequalities explicit. The run requires measurable arm-selection events so that its probabilities and bounded expectations are genuine. The model does not add independence, an identical-distribution condition, or a filtration.
The real index is compared only when every arm under comparison has a positive count; a separate clause gives unplayed arms the paper's priority. The time argument of the index at round is . The thresholds and use the paper's closed ceiling formulas. The paper's is represented by a positive lower bound on all suboptimality gaps; setting recovers the printed statement when that minimum is defined. Theorem 3 explicitly requires and . The existential precedes the probability space, rewards, run, , and , so it cannot change with an instance or horizon. Both parts of Theorem 3 are present, and the model's hypotheses are satisfiable for ordinary bounded bandits.
The mission needs reusable definitions for reward tables, empirical and run averages, pull counts, measurable runs, UCB selection and polynomial play thresholds. Contributions proving the six curated milestones, connecting them to the goal, or establishing reusable measurability and finite-sum facts are in scope. The pathwise two-sided reward decomposition is also posed as a supporting theorem.
In reinforcement learning, each policy update may require new interaction with an environment. When interaction is costly, an optimizer can retain past trajectories and use them again, provided it corrects for the different policy that generated them. Lin, Wang, and Zhou study this idea for natural policy gradient, using importance weights to reuse earlier state-action samples. Their rate result identifies how reuse changes the covariance of the optimization error, rather than measuring progress solely by the number of iterations. The result appears as Theorem 2 of their 2025 preprint, subsequently published in Operations Research.
The question is subtle because the reused data are correlated with the sequence of policies. A fresh sample drawn at iteration has the current occupancy distribution, while an old sample was drawn under an earlier policy and receives a likelihood ratio that depends on the current iterate. The inverse Fisher-information estimate adds another random factor. The covariance therefore has separate terms for gradient sampling and for the interaction between gradient sampling and the inverse-information estimate. The paper's §4 and Theorem 2 quantify both.
A discounted Markov decision process has states , actions , transition probabilities , rewards , an initial-state law , and a discount factor . A parameter specifies a stochastic policy . Its objective is the expected sum of discounted rewards. The discounted occupancy distribution is the probability of observing when the time is geometrically distributed with parameter . It is this distribution, rather than the one-step transition law, that supplies the algorithm's samples.
At each iteration, the method draws state-action pairs from . Its gradient estimate combines the current batch with earlier batches. A reused pair from iteration is weighted by . The preconditioner is the inverse of a regularized empirical Fisher information matrix. The iterate moves in that preconditioned gradient direction and is projected back onto the feasible set . The source's equations (3)–(6) and Algorithm 1 define these operations; the paper fixes reuse to the gradient estimate alone for its convergence analysis in §3, p. 7.
Write for the single-sample policy-gradient contribution, for the score outer product, for the mean regularized inverse Fisher estimate, and for the covariance of . The two matrices governing the rate are
where averages over a fresh Fisher batch. All three matrices are derived from the MDP and policy; none is supplied as a free covariance parameter.
Suppose the RNPG iterates converge almost surely to , the paper's regularity and step-size conditions hold, and the linearization of the mean natural-gradient field at is a Hurwitz matrix . For the normalized error , the goal is the marginal central limit conclusion of Theorem 2, p. 11:
Here stacks matrix columns and is the Kronecker sum. The milestone list follows Lemmas 4–8 and display (10), pp. 12–13: three conditional covariance limits for the fresh-gradient and random-preconditioner terms, their combined covariance, then two limits for the fixed-state memory process. The formulas retain the paper's factors , , , and .
The limit law gives a quantitative description of the parameter error when the step size is small: the covariance is to first order. In the noise matrix, the contribution is divided by , exposing the benefit of reusing gradient samples under the paper's assumptions. It also recovers the single-batch regime at , where the memory terms vanish. These are claims about the algorithm's asymptotic statistical behavior, not guarantees that every finite run improves.
The paper proves the theorem analytically. This mission presents Lean statements and definitions; the open task is to give machine-checked proofs of those statements. A completed development would supply reusable finite-MDP occupancy and importance-weighted sampling interfaces, plus conditional-moment tools for stochastic approximation with finite memory. The marginal convergence claim is the goal; the source's additional process-level weak convergence to a stationary stochastic differential equation remains outside this mission.
Treating the gradient batches as independent at every iteration gives the wrong covariance. An old batch appears in several successive estimates, and each reuse weight depends on the changing policy. Even the random inverse Fisher estimate cannot simply be replaced by its mean inside a covariance. The paper distinguishes the conditional fluctuation from the term carried by the stored history; the two have different limits, and a cross term survives in the accounting. The required result is a joint limit over a late starting time and a long averaging window, not a one-step variance calculation. This dependence is the central obstacle for the milestone chain in §4 and Appendix A.7–A.11.
Lean uses finite, nonempty state and action types with discrete measurable structures, real rewards and parameters in a Euclidean space of positive dimension. All state-action and batch expectations are finite weighted sums. The objective itself is the unnormalized infinite discounted return from equation (1); occupancy is normalized. The policy family is defined on all of , while the bounds in Assumption 1 are imposed on . The theorem additionally requires : at a boundary limit a projected iterate can have a one-sided normalized error, contradicting a nondegenerate centered Gaussian. The paper discusses the interior case just below Assumption 2 on p. 10.
The run draws separate independent gradient and Fisher batches, realizing Assumption 1(A.1.7). Before batches exist, its gradient estimate averages all batches available. A general filtration records the past; conditional matrix expectations are taken entrywise. The fixed-state lemmas condition on a stored-memory process whose future batches follow the occupancy law at fixed . The finite model writes the distributional continuity of Assumption 2(A.2.4) as pointwise continuity of the finite sample functions. The complete process-level SDE claim of Theorem 2, the separate almost-sure convergence Theorem 1, and the numerical examples are not formalized here.
The covariance matrices and limit law are computed from the policy, MDP, and RNPG run. An arbitrary covariance inserted as an extra hypothesis would erase the paper's main claim. Work on the published goal and the six paper-indexed milestones is welcome, as are supporting results for occupancy positivity, score identities, conditional expectations, and finite-memory stochastic approximation.
Hawkes processes are point processes in which every event raises the rate of future events. They are used to model contagion in financial markets, earthquake aftershocks, the spread of posts on social networks and arrivals to service systems (Hawkes 1971; Hawkes and Oakes 1974). Hawkes and Oakes showed that a stationary Hawkes process is a Poisson stream of immigrants, each of which starts an independent cluster of descendants. Many questions about a Hawkes process therefore reduce to questions about a single cluster: how many events it contains, when they occur, and how long it lasts.
For a homogeneous Poisson process, the classical conditional uniformity property says that, given the number of points in an interval, the points are distributed as sorted i.i.d. uniforms. A. Daw, Conditional Uniformity and Hawkes Processes (arXiv:2202.05335; Mathematics of Operations Research, 2024), establishes the analogue for a Hawkes cluster. After the random time change by the compensator, the event times of a cluster of known size are uniform on a polytope. Sampling from that polytope is organized by a combinatorial object, a uniformly random parking function. This mission formalizes that result.
Let be the excitation kernel, with
A cluster starts with an event at . Each event at time adds to the intensity, so the intensity is (eq. (3) of the paper). Since , the cluster is almost surely finite. Its events are , and is the cluster size.
The compensator points are
the values of the compensator at the event times (eq. (6)). For , the polytope is
and the unit polytope is with .
A parking function of length is a vector whose increasing rearrangement satisfies for every (Definition 2). denotes the set of parking functions of length . A -step Dyck path is recorded as a non-decreasing integer vector with ; denotes the set of them. Each determines the region
(eq. (10)), and counts the coordinates of equal to .
In the Lean development these are rho, bigG, compensator, polytope, unitPolytope, parkingFunctions, dyckPaths, dyckRegion and kappa, all in the namespace HawkesParking.Spine.
Given , with uniform on and uniform on independent of ,
The law of the compensator points does not depend on beyond . Their spine is a uniformly random parking function.
The result. Theorem 1 gives an exact description of a Hawkes cluster of known size. Combined with the Borel law of , it yields an exact simulation algorithm: draw , draw a uniform parking function and independent uniforms, and invert the compensator. In the paper this is Algorithm 1 and Proposition 4. For the exponential kernel it also yields a representation of the cluster duration as a sum of conditionally independent exponentials (Theorem 2). The result links self-exciting point processes to the combinatorics of parking functions and Dyck paths, which count labelled trees and are enumerated by Cayley-type formulas.
Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The mission formalizes the proof chain of Theorem 1: Pollak's count of parking functions, the Dyck decomposition of the polytope, the volume of each region, the identification of region probabilities with sorted-parking-function probabilities, and the change of variables behind Lemma 2. None of these objects, and no result about them, has a machine-checked proof on Prove2Me or in Mathlib. Mathlib has neither parking functions nor this encoding of Dyck paths.
Every step is elementary on paper; the difficulty is in the formal measure theory and combinatorics. The change of variables of Lemma 2 maps the ordered epochs to the polytope by a triangular, non-linear map whose Jacobian is the product of the pre-event intensities. This is exactly the factor in the cluster's likelihood. For a general integrable kernel, is only absolutely continuous and may be flat on intervals, so the multivariate change-of-variables theorem for diffeomorphisms does not apply directly.
Proposition 3 needs the number of parking functions sorting to a given Dyck path, , and their total count , whose standard proof is Pollak's circular argument. Proposition 2 needs the law of order statistics of shifted uniforms with repeated shifts. The goal then assembles four measure identities, including a mixture over a finite set and a disjoint decomposition up to null sets.
clusterLaw g k is the measure on with densityon ordered epochs , with . This is the Janossy density of the point process with intensity (3) on , and the proof of Lemma 2 (p. 11) works from the same quantity. Mathlib has no point processes with compensators, and the step from the intensity to the likelihood is classical, not part of this paper. No intensity-based definition is formalized. The model is checked by milestone 7: its total masses are the Borel probabilities.
IsKernel g bundles on , integrability on and from the page. It adds two hypotheses: is measurable, and . The latter is needed because for the event is null and is undefined.i : Fin k with value . . Order statistics are v ∘ Tuple.sort v. "Given " is the cluster law normalized by its total mass. The law of is written as the uniform mixture over . Theorem 1 is stated for the joint law, which implies the coordinatewise eq. (8). Eq. (4) is indexed by .We establish a quantum version of the classical isoperimetric inequality relating the Fisher information and the entropy power of a quantum state. The key tool is a Fisher information inequality for a state which results from a certain convolution operation: the latter maps a classical probability distribution on phase space and a quantum state to a quantum state. We show that this inequality also gives rise to several related inequalities whose counterparts are well-known in the classical setting: in particular, it implies an entropy power inequality for the mentioned convolution operation as well as the isoperimetric inequality, and establishes concavity of the entropy power along trajectories of the quantum heat diffusion semigroup. As an application, we derive a Log-Sobolev inequality for the quantum Ornstein-Uhlenbeck semigroup, and argue that it implies fast convergence towards the fixed point for a large class of initial states.
This mission is the statement-level formalization of Geometric inequalities from phase space translations (arXiv:1606.08603v2). 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 Lemma 1: convolution data processing (Lemma 1, (30), 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.
14 results of the paper are not stated yet, because the library lacks an interface they need:
Let {\rho} the density matrix of a mixed Gaussian state. Assuming that one of the Robertson--Schr"odinger uncertainty inequalities is saturated by {\rho}, e.g. ({\Delta}^{{\rho}}X_1)^2({\Delta}^{{\rho}}P_1)^2={\Delta}^{{\rho}}(X_1,P_1)^2+(1/4)\hbar^2, we show that there exists a unique pure Gaussian state whose Wigner distribution is dominated by that of {\rho} and having the same variances and covariance {\Delta}^{{\rho}}X_1,{\Delta}^{{\rho}}P_1, and {\Delta}^{{\rho}}(X_1,P_1) as {\rho}. This property can be viewed as an analytic version of Gromov's non-squeezing theorem in the linear case, which implies that the intersection of a symplectic ball by a single plane of conjugate coordinates determines the radius of this ball.
This mission is the statement-level formalization of The Unique Pure Gaussian State Determined by the Partial Saturation of the Uncertainty Relations of a Mixed Gaussian State (arXiv:1205.5222v1). 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 Saturation of one Robertson–Schrödinger inequality gives minimal symplectic capacity (Section 4, First step (continued on p.8), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
We show that Araki and Masuda's weighted non-commutative vector valued -spaces [Araki & Masuda, Publ. Res. Inst. Math. Sci., 18:339 (1982)] correspond to an algebraic generalization of the sandwiched R'enyi divergences with parameter . Using complex interpolation theory, we prove various fundamental properties of these divergences in the setup of von Neumann algebras, including a data-processing inequality and monotonicity in . We thereby also give new proofs for the corresponding finite-dimensional properties. We discuss the limiting cases leading to minus the logarithm of Uhlmann's fidelity, Umegaki's relative entropy, and the max-relative entropy, respectively. As a contribution that might be of independent interest, we derive a Riesz-Thorin theorem for Araki-Masuda -spaces and an Araki-Lieb-Thirring inequality for states on von Neumann algebras.
This mission is the statement-level formalization of R'enyi divergences as weighted non-commutative vector valued Lₚ-spaces (arXiv:1608.05317v2). 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 Finite-dimensional identification of Araki–Masuda and sandwiched Rényi divergences (§4.1 Eq.(39); Definition 2 and Eq.(10), p.5; Definition 7, p.8, 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.
18 results of the paper are not stated yet, because the library lacks an interface they need:
The Littlewood-Richardson coefficients give the multiplicity of an irreducible polynomial -representation in the tensor product of polynomial representations . In this paper, we generalize these coefficients to an -fold tensor product of rational representations, and give a new method for computing them using an analogue of statistical contingency tables. We demonstrate special cases in which our method reduces to counting statistical contingency tables with prescribed margins. Finally, we extend our result from the general linear group to both the orthogonal and symplectic groups.
This mission is the statement-level formalization of Contingency tables and the generalized Littlewood-Richardson coefficients (arXiv:2012.06928v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Stable rational GL multiplicities as weighted hollow LR tables (Theorem 3, 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.
This article provides an elementary introduction to Gaussian channels and their capacities. We review results on the classical, quantum, and entanglement assisted capacities and discuss related entropic quantities as well as additivity issues. Some of the known results are extended. In particular, it is shown that the quantum conditional entropy is maximized by Gaussian states and that some implications for additivity problems can be extended to the Gaussian setting.
This mission is the statement-level formalization of Gaussian quantum channels (arXiv:quant-ph/0505151v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Gaussian states maximize quantum conditional entropy at fixed moments (§3.3, Eq. (23): Gaussian conditional-entropy extremality (abstract seed), PDF p. 8). 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 prove that it is impossible to distill more entanglement from a single copy of a two-mode bipartite entangled Gaussian state via LOCC Gaussian operations. More generally, we show that any hypothetical distillation protocol for Gaussian states involving only Gaussian operations would be a deterministic protocol. Finally, we argue that the protocol considered by Eisert et al. [quant-ph/0204052] is the optimum Gaussian distillation protocol for two copies of entangled Gaussian states.
This mission is the statement-level formalization of Gaussian transformations and distillation of entangled Gaussian states (arXiv:quant-ph/0204069v2). 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 Finite Gaussian contraction and normalized covariance update (Eqs.(1),(3)–(7), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
7 results of the paper are not stated yet, because the library lacks an interface they need:
We develop an approximation approach to infinite dimensional quantum channels based on detailed investigation of the continuity properties of entropic characteristics of quantum channels and operations (trace-nonincreasing completely positive maps) as functions of a pair ``channel, input state''. The obtained results are then applied to the following problems: continuity of the -capacity as function of a channel; strong additivity of the -capacity for infinite dimensional channels; the analytical expression for the convex closure of the output entropy of arbitrary quantum channel.
This mission is the statement-level formalization of On approximation of quantum channels (arXiv:0711.2245v1). 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 topology of quantum operations is metrizable (§3, unnumbered: metrizability of the operation topology, 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.
36 results of the paper are not stated yet, because the library lacks an interface they need:
We address the problem of learning an unknown unitary transformation from a finite number of examples. The problem consists in finding the learning machine that optimally emulates the examples, thus reproducing the unknown unitary maximum fidelity. Learning a unitary is equivalent to storing it in the state of a quantum memory (the memory of the learning machine), and subsequently retrieving it. We prove that, whenever the unknown unitary is drawn from a group, the optimal strategy consists in a parallel call of the available uses followed by a "measure-and-rotate" retrieving. Differing from the case of quantum cloning, where the incoherent "measure-and-prepare" strategies are typically suboptimal, in the case of learning the "measure-and-rotate" strategy is optimal even when the learning machine is asked to reproduce a single copy of the unknown unitary. We finally address the problem of the optimal inversion of an unknown unitary evolution, showing also in this case the optimality of the "measure-and-rotate" strategies and applying our result to the optimal approximate realignment of reference frames for quantum communication.
This mission is the statement-level formalization of Optimal quantum learning of a unitary transformation (arXiv:0903.0543v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Covariance without loss for a delayed learning comb (§III A, Eq.(9): covariance without loss for a learning comb, 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.
11 results of the paper are not stated yet, because the library lacks an interface they need:
The coding theorem for the entanglement-assisted communication via infinite-dimensional quantum channel with linear constraint is extended to a natural degree of generality. Relations between the entanglement-assisted classical capacity and the -capacity of constrained channels are obtained and conditions for their coincidence are given. Sufficient conditions for continuity of the entanglement-assisted classical capacity as a function of a channel are obtained. Some applications of the obtained results to analysis of Gaussian channels are considered. A general (continuous) version of the fundamental relation between the coherent information and the measure of privacy of classical information transmission by infinite-dimensional quantum channel is proved.
This mission is the statement-level formalization of On the entanglement-assisted classical capacity of infinite-dimensional quantum channels (arXiv:1210.6926v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1, (14): general constrained entanglement-assisted coding theorem (Theorem 1, (14): general constrained entanglement-assisted coding theorem, 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:
A polynomial that is positive away from the origin can be certified by writing it as a sum of squares after multiplication by a suitable power of the squared Euclidean norm. This is the uniform denominator theorem of Reznick (1995). In polynomial optimization, the size of a sum of squares certificate is governed by the number of variables in each square. A dense certificate can therefore lose the computational advantage of a polynomial whose terms involve only small groups of variables. Mai, Magron and Lasserre establish a version of Reznick’s result in which every numerator retains its own variable block. The question addressed here is the exact algebraic statement of that certificate, including its denominators and degree bounds.
A form of degree is a homogeneous polynomial in real variables ; it is positive definite when for every . The variables are covered by nonempty blocks , with . Write for the coordinates in block and for any coordinate set . A sparse form has a decomposition , where each is a degree- form in . Individual need not be positive.
The running intersection property assigns every block an earlier parent . Its overlap with preceding blocks, , must be contained in . This condition lets the certificate keep each numerator in one block. The paper defines a polynomial by multiplying squared norms of (except at the first block) and of later overlaps whose parent is . It then sets . The set consists of finite sums of squares of polynomials in the variables with total degree at most .
A second class of objects appears in the supporting results. A continuous rational form is a continuous, homogeneous function represented by a quotient of polynomials wherever the denominator is nonzero. It is positive definite on a block when it is positive wherever the coordinates of that block are not all zero. This block condition is weaker than positivity at every nonzero point of the full ambient space, since the form ignores coordinates outside its block.
The goal is Corollary 2.1 of the pinned preprint. For a positive definite form of degree , with and each supported on , it asserts the existence of a single and blockwise sums of squares such that
This is an identity of rational functions, evaluated where its denominators are nonzero. The degree index is part of the target: leaving it free would discard the quantitative certificate. In the formal statement, every overlap with is assumed nonempty so that the printed is a nonzero polynomial.
Theorem 2.1 is the last milestone. It begins with a positive definite rational form , in which is homogeneous of degree , and yields the same blockwise degree bound with a common exponent . The polynomial goal follows by taking every . Earlier milestones state the paper’s continuity, approximation, block-splitting, and uniform denominator results.
The result supplies a certificate whose numerator for block uses only variables in that block. That is the structural property needed when a polynomial optimization problem is represented by smaller semidefinite constraints instead of one dense constraint. The running intersection hypothesis is explicit, so the theorem also records when that sparsity claim applies. The common exponent and exact bound on each numerator make the certificate suitable for a hierarchy indexed by degree, as described in the source paper.
The 2020 preprint proves these mathematical results; this mission asks for machine-checked proofs of the statements in Lean. The definitions of sparse sums of squares, rational forms on blocks, and running intersection data are reusable in other polynomial optimization formalizations. No proof of the target is claimed by the draft statements themselves.
A dense Reznick certificate does not identify numerators in individual blocks. Even if the sum is positive definite, a summand can be negative, so a separate application of a positivity theorem to each cannot establish the target. The supporting statements must express how positivity is recovered on each block while preserving both the rational representation and variable support. The denominator factors also overlap: their degree contribution depends on the parent map , so the final bound must track each factor rather than only a global degree.
Lean uses MvPolynomial (Fin n) ℝ, with blocks as finite sets of coordinate indices and a zero-based Fin p block index. The paper’s first block is index zero in Lean. The standing condition from page 3 is explicit in supporting lemmas that do not assume the running intersection property; that property already implies it for the other results. Its squared Euclidean norm is the polynomial ; the function norm on Fin n → ℝ is not used for this purpose. A sparse sum of squares is represented explicitly as a finite sum of squares whose bases lie in Mathlib’s supported subalgebra. The paper’s is encoded by its combinatorial formula, which is even under the nonempty-overlap assumption. Lemma 3.3 requires the approximating polynomials to have exact total degree , as printed.
The printed formulas divide by , although the stated running intersection property allows an empty overlap and then makes that polynomial zero. The goal and Theorem 2.1 add nonempty overlaps for later blocks; Lemma 3.6 similarly requires every denominator block to be nonempty. Lemma 3.5 adds , used by its cited continuity result. These are disclosed restrictions to the printed statements, rather than conclusions hidden in definitions. Rational identities are pointwise on the set where every displayed denominator is nonzero; at a zero denominator, Lean’s total division returns zero. The quotient in the continuity lemma takes that zero value at the origin.
The supporting statements retain the restriction that every is a sum of squares in , the fixed degree bound, and positivity on each block’s own nonzero inputs. The nonempty-overlap conditions ensure the rational identity has points where all denominators are nonzero. Work on the algebraic preordering and real spectrum, homogeneous polynomial approximation, continuous rational forms, and degree control is within scope. The paper’s other main result, its sparse Putinar–Vasilescu certificate, is a separate target and is not stated here.
In a contextual bandit a decision maker repeatedly observes a context , chooses one of two actions, and sees the reward of that action only. Personalised medicine, dynamic pricing and online advertising have this structure: the reward of the action not taken is never observed, so learning and earning must be balanced. Performance is measured by the regret, the expected reward lost against the oracle that knows which action is better at every context.
Two regimes were well understood before this paper. When the mean rewards are linear (parametric) in the context, the regret is of order (up to dimension factors) under a sharp margin condition (Bastani and Bayati 2020, doi:10.1287/opre.2019.1902). When they are only Lipschitz or Hölder with exponent at most one (non-differentiable), the optimal regret is (Rigollet and Zeevi 2010, arXiv:1003.1630; Perchet and Rigollet 2013, arXiv:1110.6084). Hu, Kallus and Mao (arXiv:1909.02553, Operations Research 2022) treat mean rewards with derivatives' worth of smoothness and obtain a rate that moves continuously from the non-differentiable rate at to the parametric rate as .
The context takes values in a compact set and has a Lebesgue density between and on . At each round , nature draws i.i.d., with rewards ; the decision maker sees , pulls an arm using the history, and receives . Write , the conditional average treatment effect , the oracle policy if and otherwise, and the regret
For let be the largest integer strictly below . A function is -Hölder if it is -times continuously differentiable and its Taylor polynomial of order at approximates it at within . A Lebesgue-measurable set is weakly -regular at if for the closed ball , and a -regular set if this holds at each of its points for all . The class consists of the instances with:
The algorithm, SmoothBandit (Algorithm 1), partitions into cubes of side and runs in epochs of geometrically growing length , with error tolerance . Each cube is assigned to an exploitation region (always pull that arm) or to the randomisation region (toss a fair coin). After each epoch it estimates at the cube centres by local polynomial regression of degree with bandwidth , using data from inside and outside each cube. It moves a cube to when the estimated effect exceeds in favour of arm , and hands to the other arm the cubes where the data of arm are too sparse to estimate (the inestimable regions ).
With , uniformly over the class (constants depending only on the parameters):
for all , where is Algorithm 1 run with horizon .
In the order the proof uses them:
Together with the paper's lower bound (Theorem 3, not part of this mission), Theorem 2 identifies the minimax regret of smooth contextual bandits as up to logarithmic factors when . The two known regimes are endpoints of this rate: recovers the non-differentiable rate , and as the exponent tends to the parametric value , which is without a margin condition () and polylogarithmic under a sharp margin (). The result says how much the smoothness of the reward functions is worth in a sequential decision problem, and its algorithm shows that local polynomial estimators, which use data outside each cube, are needed to get there.
The theorem is proved in the paper; no machine-checked proof of it, or of any smooth () nonparametric bandit bound, is known. A formal proof would also check the paper's analysis, which has gaps recorded in this mission: Theorem 2's -form fails for when and its explicit constant needs , Lemma 5's fourth statement needs the sample-size event of the current epoch, and a display of Lemma 3 is misprinted. The definitions layer (the Hölder class with derivatives, regular sets, the local polynomial estimator, an epoch-based algorithm on a probability space with coins) is reusable for other nonparametric bandit and estimation results.
The goal's own proof is short once its ingredients are available: the decomposition (13), Theorem 1 and Lemma 2, then a geometric sum. The weight is in Theorem 1 and Lemma 16. The samples of each epoch are collected adaptively: which contexts are sampled for arm depends on regions computed from earlier data, so the samples are i.i.d. only conditionally on the past, with a conditional density that vanishes on the other arm's exploitation region. The classical analysis of local polynomial regression assumes a design density bounded below on a neighbourhood of every point and so does not apply. The paper restores a usable condition through the regularity of the regions (Assumption 2) and the screening rule (6); making this rigorous requires conditioning on events of the past epochs, a lower bound on the smallest eigenvalue of the local Gram matrices uniformly over the grid, and a union bound over cubes. Bounding the estimation error at one point is not enough: the accuracy event is a supremum over a region that is itself random.
Contexts live in EuclideanSpace ℝ (Fin d) with ; arms are Bool (true is ); Lean rounds start at . An instance is a structure on a probability space that carries the contexts, the potential rewards of both arms, i.i.d. fair coins independent of the data, the support and the mean rewards . Its laws are stated through iIndepFun, identical distributions and the integral form of . The Hölder condition uses on an open neighbourhood of and iteratedFDeriv. The density condition is stated on measurable subsets of . All standing parameter conditions are explicit (, , , , , , ).
Algorithm 1 is a concrete, total function of the contexts, the coins and the rewards of the pulled arms, with the paper's constants , , , the epoch lengths (10) and every tie-break as printed. Its conventions:
The goal must be proved for this algorithm. A statement for an abstract policy assumed to satisfy Lemma 5, or with regions or good events taken as hypotheses, would reduce Theorem 2 to the decomposition (13) and is not the theorem. The constants , and are chosen before the instance. The -form clause excludes only the parameters where it fails as printed ( with ) and the boundary .
Welcome contributions: proofs of the milestones; the conditional i.i.d. structure (Lemma 6) and the Gram-matrix bound (Lemma 7), which are used inside Lemma 16 but not stated here; and general lemmas on local polynomial regression and on regular sets.
Optimal transport asks how cheaply several prescribed probability distributions can be coupled. Adding a divergence penalty relative to their independent product makes the problem amenable to numerical methods, but changes its value. A quantitative bound on that change tells users of regularized transport how much bias a chosen regularization parameter can introduce. Eckstein and Nutz study this question through quantization of an optimal plan. Their Theorem 3.8 gives an entropic bound and a bound for a broader family of divergence penalties when the cost has a bounded second derivative. The result concerns the value of the transport problem; it does not assert convergence of optimal couplings or dual potentials.
There are marginals. For , is a closed convex subset of a Euclidean space and is a probability measure on with finite second moment. Their product has the Euclidean product metric. A coupling is a probability measure on whose th marginal is . The reference measure makes the coordinates independent.
The transport value is the infimum of over these couplings. The cost is continuous and has growth of order two, so its integral and the value are finite in this setting. For a strictly convex, lower bounded generator with and , the -divergence integrates against when ; it is otherwise. The regularized value is
Entropic regularization has , with . A law belongs to when it is supported on at most points of . An optimal plan has quantization rate when, for each , some satisfies . Here is the Wasserstein distance for the Euclidean product norm. The rate hypothesis is on the joint optimal plan, not merely on its individual marginals.
The goal is the corrected form of Theorem 3.8. Assume is twice continuously differentiable on a neighborhood of , , , , and is an optimal plan with . The Hessian bound is two-sided and holds for every direction in the ambient product space:
For entropy and , the first target is
For two marginals, suppose on , where is nondecreasing and concave there. Write and . If is strictly increasing on , , put . The second target includes and as and, when , , and ,
The source prints in both bounds and a one-sided condition in (3.4). The squared quantization estimate requires , and the Hessian condition must control both signs in every ambient direction. The mission records these corrections explicitly rather than changing the quantization hypothesis.
The first estimate controls entropic bias at order when an optimal joint plan admits the stated quantization rate. The second expresses a rate for other divergence generators through an inverse function determined by . These are established analytical results in the cited paper, though the corrected formulation is needed for the stated constants and hypotheses. The formalization target is a machine-checked statement of those rates and their supporting cost and divergence bounds. No completed machine-checked proof of this mission's goal is claimed here.
A finite approximation of the optimal plan need not retain the prescribed marginals. Restoring them can increase cost and divergence. A direct first-order cost estimate also misses the improvement sought here: the result uses cancellation associated with martingale quantization, while the remaining cost change is quadratic in the Wasserstein error. The requested infrastructure therefore includes a transport model with actual probability couplings, finite-support quantizers on the joint space, and a divergence that keeps its infinite value outside absolute continuity.
Lean represents each marginal space by EuclideanSpace ℝ (Fin (d i)) and the product by PiLp 2, whose norm is the paper's Euclidean product metric. The paper's marginal is Lean's index i : Fin N. The formal statement requires , closed convex supports, probability marginals concentrated on those supports with finite second moments, growth of order two for , and regularity on an open neighborhood. The real value OTval is used only under those conditions; OTreg and fDiv use extended real values, so an infinite divergence cannot silently become zero. The divergence definition assigns when its density integrand is not integrable, consistent with a lower-bounded generator under a probability reference measure. The condition covers without division by zero. The function is constrained only on , allowing generators with a nonzero value at zero.
The development reuses the published WassersteinDRO.Duality.wassersteinDistance for . Its new definitions of couplings, product reference law, divergence, quantization, and martingale coupling are reusable for related finite-dimensional transport results. The milestones isolate the Taylor estimate, the marginal-restoring coupling and its data-processing bound, the corrected cost estimate, and the entropic discrete-marginal bound of Lemma 2.3(iii). Lemma 2.3(i) is not posed here because the proposed positive-argument interpretation of does not control , and its stated divergence bound then has a two-point counterexample. A valid closure must use joint-plan quantization and a two-sided Hessian bound; replacing the regularized infimum by a default real value, restricting the Hessian to directions inside , or quantizing only the marginals would change the result.