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.
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?
Given a monic polynomial with integer coefficients, one can reduce it modulo each prime and factor it over the finite field . The way factors changes with , and the question of how often each factorization pattern occurs has a precise answer: Chebotarëv's density theorem (1922). It is the common generalization of Dirichlet's theorem on primes in arithmetic progressions (1837) and a theorem of Frobenius (1880, published 1896), and it underlies a large part of algebraic number theory, for example the fact that a Galois extension of a number field is determined by the set of primes that split completely in it. This mission follows the elementary exposition of P. Stevenhagen and H. W. Lenstra, Jr. (Math. Intelligencer 18 (1996)), which states all three theorems over with a minimum of terminology.
Timeline.
Let be monic of degree with nonzero discriminant , so that has distinct complex zeros . Let be its splitting field and its Galois group. Every permutes the zeros; the lengths of the cycles (including cycles of length 1) form the cycle pattern of , a partition of .
For a prime , the degrees of the irreducible factors of over form the decomposition type of modulo , again a partition of .
A Frobenius substitution of is an element such that, for some prime ideal of the ring of integers lying over ,
For these elements form a single conjugacy class of , written .
A set of primes has (analytic, or Dirichlet) density if
and natural density if as .
For every conjugacy class of ,
Chebotarëv's theorem shows that every conjugacy class of the Galois group occurs as a Frobenius class for infinitely many primes, with a predictable frequency. Its standard consequences include: the Frobenius elements are equidistributed; a Galois extension is determined by its completely split primes; if has a zero modulo almost every prime then is linear or reducible; prime ideals are equidistributed over ideal classes. The theorem is the first step in many arguments in arithmetic geometry (e.g. Serre's work on -adic representations).
The theorem is classical and proved; this mission is about formalizing it. Mathlib contains Frobenius elements in Galois extensions of Dedekind domains and Dirichlet's theorem in the form "infinitely many primes in each coprime residue class", but, to our knowledge, neither the density form of Dirichlet's theorem nor Frobenius's or Chebotarëv's density theorem.
The Galois-theoretic parts (milestones 3–6) are standard but require connecting Frobenius elements in with factorization of modulo , including the fact that forces to be unramified in . The analytic core is harder: one needs Dedekind zeta functions and -functions of number fields and their behaviour at . The reduction of the general case to the cyclotomic case (Chebotarëv's "crossing" with cyclotomic extensions) needs the density statement over an arbitrary number field as base, not only over ; in particular, the statement over alone cannot be proved by induction on itself.
All declarations live in the namespace ChebotarevDensity and share one definition file.
SplittingField of viewed in ; is Polynomial.Gal; is Mathlib's Polynomial.discr.IsArithFrobAt at some prime ideal of containing ; "" means that some Frobenius substitution of lies in (for this is equivalent to all of them lying in , by milestone 4).Equiv.Perm.partition of the permutation induced on the complex zeros of ; it includes fixed points.Welcome contributions: Dedekind zeta functions and Hecke -functions at , the density form of Dirichlet's theorem, unramifiedness of primes not dividing the discriminant, and the general number-field version of the theorem.
A classical way to recognize an algebraic function is through the arithmetic of its Taylor coefficients. Eisenstein's theorem (1852) says that if a power series is algebraic over , only finitely many primes occur in the denominators of its coefficients. The converse fails in general: many transcendental power series have integer coefficients. Lam and Litt (arXiv:2501.13175) conjecture that the converse does hold for power series that solve an algebraic differential equation at a non-singular point, and that even a weak control on denominators — primes may appear, but only after roughly coefficients — already forces algebraicity.
For linear differential equations, the conjecture is a strengthening of the Grothendieck–Katz -curvature conjecture, one of the central open problems about algebraic solutions of linear differential equations (arXiv:2501.13175). The bounded-denominator form is Problem 1 on Litt's list of open problems (problemsilike.com/1).
Timeline.
Let be a formal power series with rational coefficients and write for its -th formal derivative. Let be a rational function in variables. The series solves the algebraic ODE defined by if
and is defined at . Concretely, for polynomials with and .
For , is the subring generated by . For a function from the primes to , the coefficients of are -integral if for every prime the numbers lie in (denominators prime to ); is superlinear if .
For solving an algebraic ODE as above, the following are equivalent:
Together the four milestones imply the goal; the last two are the open content of the conjecture.
A proof would give an arithmetic criterion for algebraicity of solutions of arbitrary algebraic differential equations, and, for linear equations, would imply the Grothendieck–Katz -curvature conjecture (arXiv:2501.13175). Lam and Litt draw algebro-geometric consequences from the cases they prove.
For formalization: the conjecture is open, so the goal and the two open milestones are research targets. Eisenstein's theorem is a classical result; formalizing it is concrete, self-contained work. The implication (2)⇒(3) is elementary. The cases proved by Lam and Litt are candidates for further milestones.
Integrality of coefficients alone does not detect algebraicity: there are transcendental power series with integer coefficients that satisfy linear differential equations, such as . Its equation is singular at , which the non-singularity hypothesis on excludes; the conjecture asserts that at non-singular points such examples cannot occur. Even for linear equations the statement contains the Grothendieck–Katz conjecture, which is open in general.
PowerSeries ℚ with the formal derivative; rational functions are the fraction field of MvPolynomial (Fin (n + 1)) ℚ, where variable 0 is and variable i + 1 is .IsAlgebraic (Polynomial ℚ) f, i.e. over (equivalently over ).List.TFAE of the three conditions.Useful infrastructure: formal derivatives and substitution for power series, algebraic power series and their coefficient arithmetic (Eisenstein), and -adic valuations of coefficients. Formalizations of Eisenstein's theorem and of the special cases proved by Lam and Litt are welcome.
FormalConjectures/LittProblems/1.lean. https://github.com/google-deepmind/formal-conjecturesIn a Walrasian pure exchange economy, agents trade a fixed stock of commodities, and a price vector is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).
Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.
There are commodities and agents. Prices are vectors , and the paper's implicit summation is written . Agent has an expenditure function (minimal cost of reaching a fixed utility level), and the market weighs agents with constants ; the aggregate expenditure is
The economy controls the price velocity and minimizes the cost functional (eq. (7))
whose value function is . The Hamiltonian (eq. (8)) is
the optimal policy (eq. (9)) is , and the HJB equation (eq. (10)) reads
Here always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent with . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: .
If is and solves the time-reversed HJB equation, and the price path follows the optimal policy , then on any interval on which
the function is strictly decreasing; if moreover , it is strictly positive on .
The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.
Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.
All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption is kept; positivity of and is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. , , with small on a bounded interval), so the goal is not vacuous.
The mean value problem, also called Smale's mean value conjecture, was posed by Stephen Smale in 1981 in his study of the complexity of root-finding algorithms for polynomials (Smale 1981). For a real differentiable function the mean value theorem produces, between two points, a point where the derivative equals a difference quotient. For a complex polynomial no such point need exist on a segment, and Smale asked for a substitute in which the special point is a critical point of the polynomial (a zero of its derivative). Estimates of this kind control how far Newton-type iterations can move, which is where Smale's original interest came from. The problem appears in lists of unsolved problems in mathematics, including Smale's own list of problems for the next century.
No absolute constant is known that works in every degree.
Let be a polynomial with complex coefficients of degree , and write for its derivative. A critical point of is a complex number with ; since , is a nonconstant polynomial of degree , so has at least one and at most distinct critical points. Fix a complex number that is not a critical point, . For every critical point we then have , and the difference quotient
is well defined. The question is how small this quotient can be made, relative to , by choosing the critical point well.
For every complex polynomial of degree and every with there is a critical point of with
The same with replaced by ; the example shows this constant cannot be lowered.
The result itself. A positive answer gives a sharp, degree-independent mean value inequality for complex polynomials: for every non-critical point, some critical value is reachable along a chord whose slope is at most the local derivative. Bounds of this type feed into the analysis of Newton's method and of path-following root finders, and into the study of how critical values of a polynomial are distributed relative to its values. The conjecture is part of a family of open extremal problems on the geometry of critical points, alongside Sendov's conjecture.
Formalizing it. The goal and the optimal-constant form are open. The milestones are published theorems, none of which is known to have a machine-checked proof. Formalizing Smale's bound and Tischler's special cases would put the classical tools of the subject (critical points of polynomials, univalent function estimates, root location) on a formal footing that later attempts can reuse.
The obvious strategies control the quotient through one critical point at a time: for instance, bounding by integrating along the segment from to . Such estimates lose a constant factor that depends on how the critical points are spread out, and the known uniform arguments all pass through distortion theorems for univalent functions, whose constants lead to close to . Reaching requires using all critical points simultaneously, and no argument doing this in every degree is known. The equality case , in which every critical point is equally bad, shows that any successful argument must be sharp for polynomials with maximally symmetric critical configurations.
Polynomials are elements of ℂ[X] (Mathlib's Polynomial ℂ); the degree is natDegree, the derivative is Polynomial.derivative, evaluation is Polynomial.eval, and the roots of are the multiset P.roots (counted with multiplicity). A critical point is a c : ℂ with P.derivative.eval c = 0. The absolute value is the norm ‖·‖ on ℂ, and the constants and are computed in ℝ from the cast of natDegree.
Every statement assumes . This is the standard normalization and is essential in Lean: division by zero returns , so without it the choice would make the inequality trivially true whenever is itself a critical point. With the hypothesis, every critical point differs from and the quotient is a genuine difference quotient.
Crane's bound is stated as the existence, for each degree , of a constant strictly below that works for all polynomials of degree exactly ; this is equivalent to the best constant in degree being strictly below that value.
A complete development needs basic facts on critical points of complex polynomials (existence, the Gauss–Lucas theorem), and, for the classical bounds, results from the theory of univalent functions such as the Koebe quarter theorem and coefficient estimates. These are reusable well beyond this mission. Contributions of any milestone, of supporting lemmas, and of partial results in fixed small degree are welcome.
Linear programming is usually described as "solvable in polynomial time", but that statement is about rational inputs given exactly. In Smale's list of problems for the 21st century (Smale 1998), Problem 9 asks for a polynomial-time algorithm over the reals deciding the feasibility of , and Smale explicitly calls for "models which process approximate inputs and which permit round-off computations". Real data such as , entries of a discrete cosine transform, or even in floating point can only be accessed approximately.
Bastounis, Hansen and Vlačić pose the extended Smale's 9th problem: in a model where the algorithm can only query approximations of the input to any requested accuracy, can one compute minimisers of linear programming, basis pursuit and Lasso to correct digits? Their Main Theorem I (Theorem 3.4) shows that the answer depends on in a sharp way: for a suitable class of well-conditioned, bounded inputs, no algorithm at all (not only no efficient one) produces correct digits, while digits are computable (but not in bounded time) and digits are computable in polynomial time.
This mission targets the first, impossibility, half of Theorem 3.4(i) for linear programming.
Linear program. For , and , the solution set is
It is a subset of with the norm, . An input is a pair , and the evaluations of are its coordinates and entries .
Extended model (-information). Let . An oracle representation of is a family , indexed by evaluations and accuracies , with and . An algorithm must succeed on every oracle representation of every input.
General algorithm. To make impossibility results independent of the machine model, the paper uses general algorithms (Definition 9.3): a map from inputs to ( = no output) together with a nonempty set of evaluations read on . This set is finite whenever halts. The output is determined by the values read, and any input that agrees on those values reads the same set. Turing machines and BSS machines with an oracle are special cases; general algorithms can even solve the halting problem.
Error and breakdown epsilon. The error is , with distance from . The strong breakdown epsilon is the supremum of all such that every general algorithm has error on some input (Definition 9.17).
For every integer , all dimensions and every there is a nonempty class of inputs with nonempty solution sets, and , such that
The theorem shows that for LP with inexact input, being non-computable in Turing's sense does not rule out a finer complexity theory. The paper builds a " / / digits" classification on this. It also explains why established solvers can return wrong answers with a success flag on small, well-conditioned LPs (§4 of the paper), and it bears on computer-assisted proofs that rely on inexact LP, such as the Flyspeck proof of the Kepler conjecture.
The result is proved on paper. As far as the proposer knows, it has not been machine-checked. This mission formalizes the deterministic impossibility part for LP and puts in place reusable infrastructure: general algorithms, breakdown epsilons and -information. That infrastructure is the base for later missions on the randomised parts of Theorem 3.4(i)–(ii), the weak breakdown epsilon (iii), the exit-flag theorem (Theorem 5.1), and basis pursuit and Lasso.
The obvious objection is that LP is in P for rational inputs, so some rounding scheme ought to work. It fails because an algorithm must halt after reading finitely many approximations. Two inputs that agree to that accuracy but have minimisers far apart then receive the same output. Setting this up needs a notion of algorithm strong enough to cover every computational model, a precise -information model in which the adversary controls the approximations, and explicit LP geometry in which an arbitrarily small perturbation of moves the minimiser by a fixed amount.
PiLp p (Fin N → ℝ).run : Ω → Option M (none = NH) and a read set queried, satisfying the axioms (i)–(iii) of Definition 9.3.ℝ≥0∞), and the error of NH is . The infimum over an empty solution set is . The goal also requires nonempty solution sets, so no junk value enters.ℕ+). An oracle input is stored as a pair (input, oracle family), and algorithms can read only the oracle family.This mission formalizes N. Monod, Groups of piecewise projective homeomorphisms, Proceedings of the National Academy of Sciences 110 (2013) 4524–4527, doi:10.1073/pnas.1218426110: the groups of piecewise projective homeomorphisms of the line are non-amenable and have no free subgroups whenever .
The paper opens with the Banach–Tarski paradox and von Neumann's notion of amenability: "Tarski readily proved that amenability is the only obstruction to paradoxical decompositions. However, the known paradoxes relied more prosaically on the existence of non-abelian free subgroups. Therefore, the main open problem in the subject remained for half a century to find non-amenable groups without free subgroups" (p. 1). That problem, the so-called von Neumann conjecture, was answered by Ol'shanskii around 1980, with Tarski monsters. Monod's groups give "straightforward torsion-free counter-examples", "so simple that many additional properties can be established" (p. 1).
Monod's groups are close relatives of Thompson's groups: Thurston's model identifies Thompson's group with piecewise maps of the line with rational breakpoints (p. 2). Whether is amenable is a notorious open problem, and whether is amenable is Monod's Problem 12 (p. 2).
The projective line is OnePoint ℝ, on which acts through by Möbius transformations (mob, using Mathlib's action on OnePoint). For a subring of (A : Subring ℝ; is ⊥, is ⊤), P A is , the set of fixed points of hyperbolic elements (trace of absolute value greater than ).
A homeomorphism of is piecewise in with breakpoints in (IsPiecewiseProjOn A E f) when, off some finite subset of , it agrees near every point with a Möbius transformation from . Monod's (Gpp) is the group generated by the homeomorphisms piecewise in , with breakpoints anywhere, and (Hpp) is its stabilizer of (fixInf). For a subring , (G A) is the subgroup of generated by its elements that are piecewise in with breakpoints in (IsPiecewiseProj A), and (H A) is its stabilizer of ; is H ⊥. GRat is the subgroup of generated by its elements piecewise in with breakpoints in , and HRat its stabilizer of : the rational-breakpoint variants of and (p. 2).
Amenability is Garrido.IsAmenable (a finitely additive left-invariant probability measure on all subsets), and "no non-abelian free subgroup" is Chou.NoFreeSubgroupOfRankTwo; both are published definitions, in the bundles Garrido_Amenability and Chou_Classes. Co-amenable subgroups (IsCoamenable), inner amenability (IsInnerAmenable) and pointwise stabilizers (fixSubgroup), all on p. 3, are defined in the bundle in the same style.
A relation is amenable for a measure (IsAmenableRel μ R, p. 2) when it has a left invariant mean in the sense of Connes–Feldman–Weiss: a positive, unital map from bounded measurable functions on to functions on , linear up to -null sets and invariant under the partial transformations of . volP1 is the Lebesgue measure class on .
The goal is Theorem 1, "The group is non-amenable if " (p. 1), introduced as "the main result of this article". The proof (p. 2) passes to a countable dense subring of , compares the orbits of and on (Proposition 9), and concludes from two facts about measured equivalence relations: the orbit relation of an amenable group's action is amenable, and, by a theorem of Carrière and Ghys, the orbit relation of on is not.
The milestones are, in the paper's order: consists exactly of the elements of piecewise in with breakpoints in ; ; preserves orientation, is left-orderable and torsion-free; Proposition 9; the countable dense subring; the orbit relation of a measurable action of an amenable group is amenable; the orbit relation of on is not amenable (Carrière–Ghys, external); Lemma 13 and Theorem 14 leading to Theorem 2 ( has no free subgroups); Corollary 3; Proposition 6 (bi-orderability); Lemma 16, Proposition 7 (co-amenability of pointwise stabilizers), Proposition 15 and Proposition 5 (inner amenability); and Thurston's identification of the rational-breakpoint variants of and with and .
The result. Theorem 1 and Theorem 2 together make , for instance , a torsion-free counterexample to the von Neumann conjecture, with finitely generated examples (Corollary 3). The groups are concrete enough to carry many further properties (Propositions 5–7).
Formalizing it. Nothing on amenability of groups of homeomorphisms of the line, or on measured equivalence relations, is in Mathlib. Amenability and Følner's theorem are on this platform from Garrido I, the Banach–Tarski paradox from Garrido II, Brin–Squier's theorem from its own mission, and Thompson's and (CannonFloydParry, CannonFloydParry_T) from the Cannon–Floyd–Parry missions.
The algebraic half, Theorem 2 and Propositions 5–9, follows Brin–Squier and elementary dynamics on the circle. The analytic half is the passage through measured equivalence relations in the proof of Theorem 1. The mission defines amenability of a relation as Connes–Feldman–Weiss do, by an invariant mean valued in , which is the form under which an amenable group's orbit relation is amenable without extra set-theoretic hypotheses. The step taken from the literature, that the orbit relation of on is not amenable for countable and dense, rests on Carrière–Ghys's theorem and on Zimmer's theory of amenable actions (Adams–Elliott–Giordano). The milestone is proved (Monod.not_isAmenableRel_mob) by an elementary route that needs neither: a ping-pong argument in that contradicts an invariant mean directly.
OnePoint ℝ and acts through Matrix.SpecialLinearGroup (Fin 2) A; since acts trivially the orbits are those of .OnePoint ℝ, each defined as the subgroup generated by the maps the paper describes; the milestones state that is exactly its set of such maps and that .volP1).This mission formalizes Geoghegan's conjecture that Thompson's group is not amenable, in the form stated by Cannon, Floyd and Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996), §4, p. 227 (doi:10.5169/seals-87877), together with the landmark results of the literature on the question.
A discrete group is amenable when it carries a finitely additive, translation-invariant probability measure on all of its subsets. Groups containing a non-abelian free subgroup are not amenable, and the question whether every non-amenable group contains one (the von Neumann problem) made Thompson's group the first natural candidate for a counterexample: it contains no non-abelian free subgroup, and it is not elementary amenable. Geoghegan conjectured in 1979 that is not amenable; several announced solutions in each direction did not survive. In 2026 OpenAI released a proof that is not amenable, with a Lean formalization; adapted to this mission's definitions, it is the solution of the goal.
Timeline.
Let UI be the unit interval . Thompson's group (CannonFloydParry.F) is the group, under composition, of the order-preserving homeomorphisms of that are piecewise linear with finitely many breakpoints, every breakpoint a dyadic rational and every slope a power of . It is generated by two elements and finitely presented (Cannon–Floyd–Parry, Corollary 2.6 and Theorem 3.4).
A mean on a set is a function from the subsets of to with , for disjoint , and . A group is amenable (Garrido.IsAmenable G) when it carries a mean with for all and , where . This is equivalent to the definition Cannon, Floyd and Parry give on p. 227, whose means take values in .
The milestones use four further notions, defined precisely in the definitions item and in their own statements:
The question was open until 2026. OpenAI's proof of the conjecture (see the timeline), transferred to CannonFloydParry.F and Garrido.IsAmenable, proves this statement.
The milestones are results from the literature, stated as their sources state them: has no non-abelian free subgroup (Cannon–Floyd–Parry, Corollary 4.9) and is not elementary amenable (Theorem 4.10), and Følner's criterion, all three already proved and linked as references; Moore's tower lower bound on Følner sets of ; Kaimanovich's theorem that random walks on with finitely supported strictly non-degenerate steps are not Liouville; Chornyi's reformulation of amenability of as extensive amenability of its action on the dyadic rationals; Stankov's embedding of into Monod's ; Monod's theorem that is not co-amenable in ; and the theorem of Juschenko, Matte Bon, Monod and de la Salle that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable.
Monod's Problem 12 asks whether is amenable; it is stated as ¬ Garrido.IsAmenable (Monod.H ⊥), where ⊥ is the smallest subring of , namely ; this is parallel to the goal. Through Stankov's embedding, the proof of the goal proves it. By the theorem of Juschenko, Matte Bon, Monod and de la Salle, it is equivalent to the statement that the action of on the line is not extensively amenable; that theorem is proved on this platform, through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn), and for the subgroups of also in a sharper form, with extensive amenability on the set of possible breakpoints only (the breakpoint criterion).
The result. A proof of the conjecture would make a finitely presented, torsion-free, non-amenable group with no non-abelian free subgroup, with a concrete description as a group of homeomorphisms of the interval. A disproof would make an amenable group that is not elementary amenable, and by Moore's theorem one whose Følner sets are at least tower-sized.
Formalizing it. Corollary 4.9 and Theorem 4.10 of Cannon–Floyd–Parry are formalized and proved on this platform and enter as references. Chornyi's corollary is proved here; its "if" direction is proved directly, by establishing the case that Chornyi applies of the Juschenko–Matte Bon–Monod–de la Salle criterion. Moore's theorem is formalized and published together with the lemmas of its proof, and the milestone here has a solution that reduces it to that statement. Kaimanovich's theorem, Stankov's embedding, Monod's 2023 theorem and the theorem of Juschenko, Matte Bon, Monod and de la Salle are proved here as well, the last through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn). The definitions of Følner sets, harmonic functions on groups and extensive amenability are reusable beyond this mission.
The obstructions to amenability that settle the question for most groups are absent here: has no non-abelian free subgroup, and its elementary structure is well understood. In the other direction, the usual constructions of invariant means fail: by Moore's theorem any Følner set of is at least tower-sized, so no explicit search can exhibit one, and by Kaimanovich's theorem the finitely supported random walks on are not Liouville, so the random-walk route to amenability through a trivial Poisson boundary is closed.
Lean representation and conventions.
UI; and are subgroups of the homeomorphisms of OnePoint ℝ. Groups of maps multiply by composition, ; statements from sources that write the product in the other order are restated for this convention, with the equivalence explained in their natural-language statements.What is left out.
What a development needs. Thompson's group and its dyadic action (Cannon–Floyd–Parry §4), its tree diagrams and presentations, and amenability, Følner's criterion and the closure properties of amenable groups (Garrido I) are published and proved on this platform, as are Monod's groups and the isomorphism (Monod.contDiff_and_exists_mulEquiv_HRat_F). Mathlib has Følner filters for measurable groups and Schreier graphs of quivers, but no random walks on groups; the proofs of the landmarks here supply what they need, and the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn) is reusable beyond this mission. Reductions of the goal or of Problem 12 to new, sharper statements are welcome, as is a disproof of either.
A periodic point of a map is a point with for some . A nonwandering point is a much weaker form of recurrence: every neighbourhood of eventually returns to meet itself, for some . Every periodic point is nonwandering, but a nonwandering point need not be periodic, and the orbit of such a point may never come back to exactly.
Pugh's closing lemma asserts that this gap can be closed by an arbitrarily small change of the system: if is nonwandering for a diffeomorphism of a compact manifold, then some diffeomorphism , as close to as desired in the topology, has as a periodic point (Wikipedia, "Pugh's closing lemma"). The result was proved by C. C. Pugh in 1967 (Pugh 1967), in the same paper as the General Density Theorem: for a -generic diffeomorphism the periodic points are dense in the nonwandering set. The source article describes the lemma as establishing a close relationship between chaotic and periodic behaviour and notes that it underlies some autonomous convergence theorems. The article also points to Smale's problems as related material.
Let be a compact smooth manifold of dimension , Hausdorff and without boundary. Write for the set of diffeomorphisms : bijections such that and are continuously differentiable. For , denotes its tangent map on the tangent bundle.
The topology on is the coarsest topology for which is continuous, where the space of continuous self-maps of carries the compact-open topology. Two diffeomorphisms are -close when they, and their derivatives, are uniformly close.
For a map of a topological space:
For every and every ,
Milestones 1–4 are elementary background facts that are not stated in the source article; milestone 5 is the second theorem named in the title of the source's reference.
The result. The closing lemma turns a topological recurrence property into periodicity after a -small perturbation. Combined with genericity arguments it gives the General Density Theorem, so that for generic diffeomorphisms the whole nonwandering set is the closure of the periodic orbits. It is one of the basic perturbation tools of generic dynamics.
Formalizing it. The theorem is classical and proved in the literature. The drafter is not aware of a machine-checked proof. A formalization needs the topology on diffeomorphism groups, local perturbation lemmas in charts and the combinatorics of the closing argument. None of these is currently available in Mathlib as far as the drafter knows.
The first idea is to take the returning piece of orbit near and push it back to with a small local perturbation. This fails in the topology. Moving a point by distance with a bump supported in a ball of radius costs size about , and the return may happen at a distance comparable to the size of the only available ball. The perturbation then fails to be -small. The derivative along the return can also distort any fixed neighbourhood shape without bound. Controlling this distortion is the central difficulty.
BCWCentralizer_Basic. is M ≃ₘ^1⟮𝓡 d, 𝓡 d⟯ M, and the topology is induced by into C(TangentBundle, TangentBundle) with the compact-open topology. On a compact manifold this is the usual topology.PughClosingLemma_nonwandering, shared by all statements. It is reusable for any topological dynamics mission.Welcome contributions: a general theory of the topology on (for example, that it is Baire), local perturbation lemmas, and proofs of the milestones.
Two commuting diffeomorphisms of a manifold share all of their dynamics: permutes the orbits of and preserves every smooth and topological invariant of . The centralizer of ,
always contains the cyclic group , and has trivial centralizer when . S. Smale asked whether diffeomorphisms with trivial centralizer are dense, residual, or even open and dense in (one of Smale's problems for the 21st century).
Timeline: Kopell (1970) answered the question for on the circle; Palis–Yoccoz, Fisher and Burslem obtained results under hyperbolicity or partial hyperbolicity assumptions; Togawa treated generic Axiom A diffeomorphisms in the topology; Bonatti–Crovisier–Vago–Wilkinson showed that trivial-centralizer diffeomorphisms do not contain an open dense set in ; and Bonatti–Crovisier–Wilkinson (this paper, arXiv:0804.1416) proved residuality in for every compact manifold.
is a closed (compact, boundaryless), connected smooth manifold of dimension . is the space of diffeomorphisms of with the topology; a subset is residual if it contains a countable intersection of open dense sets.
There is a residual subset such that for every and every with , one has for some .
Following Section 2 of the paper: the classical upper-semicontinuity lemma used for Proposition 2.5, the wandering part of Theorem A (unbounded distortion is -generic), Proposition 2.5 (density of trivial Lipschitz centralizers implies residuality) and Theorem 2.3 (residuality of trivial Lipschitz centralizers when ).
The theorem answers the second (and hence the first) part of Smale's question in the topology, and exhibits a precise link between dynamical properties of (large derivative and unbounded distortion) and the algebraic structure of inside the group . The result is proved in the literature; it has not been formalized.
The density of trivial centralizers comes from perturbation results (Theorems A and B) that change the derivative without changing the topological dynamics (tidy perturbations in topological towers). Density alone does not give residuality, since the set of diffeomorphisms with the large derivative property is not residual (Appendix); the passage from dense to residual needs the Lipschitz centralizer and a semicontinuity argument.
is a charted space over with a atlas, Hausdorff, compact and connected; is Mathlib's type of diffeomorphisms. The topology is encoded as the topology induced by into the compact-open topology on continuous self-maps of the tangent bundle . Powers , , are taken in the permutation group of . Bi-Lipschitz homeomorphisms are defined chart-locally (equivalent on a compact manifold to bi-Lipschitz for a Riemannian distance). Jacobians are computed with respect to an arbitrary continuous Riemannian metric; the unbounded-distortion property does not depend on this choice.
Contributions welcome: the topology API (Baire property, continuity of composition), the Kupka–Smale and closing-lemma genericity results, and the perturbation machinery of Sections 3–7.
The Thomson problem asks for the configuration of electrons, constrained to the surface of the unit sphere and repelling each other according to Coulomb's law, that minimises the total electrostatic potential energy. J. J. Thomson posed it in 1904 in connection with his "plum pudding" atomic model. The same energy-minimisation question reappears in the arrangement of protein subunits in spherical virus shells, in colloidosomes, in fullerene patterns and in multi-electron bubbles, and it is a special case () of the Riesz -energy problem on the sphere; the logarithmic variant is Smale's 7th problem.
Despite its elementary statement, the minimum is rigorously known only for a handful of values of .
Timeline of exact solutions (as reported in the source).
A configuration of points is a map . It is admissible if every point lies on the unit sphere, , and the points are pairwise distinct. In units with and its Coulomb energy is
An admissible is an energy minimiser (solves the Thomson problem for ) if for every admissible -point configuration .
Explicit candidate configurations are fixed in the definitions file: the antipodal pair (), an equatorial equilateral triangle (), the regular tetrahedron (), the triangular bipyramid (), the regular octahedron (), the pentagonal bipyramid (: the two poles plus a regular pentagon on the equator) and the regular icosahedron ().
This asserts admissibility of the seven points and the inequality against every admissible seven-point configuration . It fixes no numerical value of the minimum and does not assert uniqueness.
The result. Among the values of listed in the source, is the smallest one whose optimum was, until the 2026 claim, supported only by numerical computation; the cases and were settled earlier. Settling extends the short list of rigorously known Thomson minimisers.
Formalizing it. The result reported in the source is recent and described there as a claimed Lean-kernel-checked proof; a formalization on this platform against a public, reviewed statement would corroborate it independently. For the milestones, the source attributes the cases to published proofs (Föppl 1912, Schwartz 2013, Yudin 1992, Andreev 1996); the source does not describe machine-checked proofs of these, and each is a self-contained formalization target.
The energy is a non-convex function on the configuration space with many critical points, so numerical minimisation — which is how most entries of the source's table of smallest known energies were obtained — does not certify global optimality. The case, the most recent classical entry before , was resolved only with a computer-assisted proof (Schwartz 2013).
Points live in EuclideanSpace ℝ (Fin 3); configurations are functions Fin N → EuclideanSpace ℝ (Fin 3). Admissibility requires unit norm and injectivity (distinct points), matching the source's " distinct points". The energy sums over ; Lean's convention is harmless because coincident points are excluded by admissibility. The candidate configurations are fixed in one particular orientation; since the energy is invariant under orthogonal maps and relabelling, this is no loss of generality. The statement " is an energy minimiser" includes admissibility of itself, so the goal cannot be satisfied by a degenerate candidate.
Reusable infrastructure welcome: energy invariance under isometries and permutations, existence of minimisers by compactness, linear-programming (Delsarte–Yudin) bounds on the sphere, and interval-arithmetic tooling for certified numerical bounds.
The second part of Hilbert's 16th problem (Paris, 1900) asks for the maximal number and the relative position of the limit cycles of a planar polynomial differential system
where are real polynomials of degree at most . Smale listed it in 1998 among the mathematical problems for the next century and remarked that, apart from the Riemann hypothesis, it seems the hardest of Hilbert's problems (Smale 1998). Even for it is not known whether the number of limit cycles is uniformly bounded.
J. Llibre's survey Sobre el problema 16 de Hilbert (La Gaceta de la RSME 18 (2015), 543–554) organises the question into seven problems and concentrates on a more tractable restriction: algebraic limit cycles, i.e. limit cycles contained in a real algebraic curve. For this restriction there is an explicit conjecture for the maximal number (Conjecture 1 of the survey, first stated in Llibre–Ramírez–Sadovskaia 2010). This mission formalizes that conjecture as its goal, together with the results of the survey on which it rests.
Timeline (as reported in the survey):
A polynomial vector field is a pair of real polynomials in ; its degree is . A solution is a differentiable curve with for all . A periodic orbit is the image of a non-constant periodic solution. A limit cycle is a periodic orbit that is isolated among periodic orbits: some open set contains no periodic orbit other than .
A limit cycle is algebraic if it is contained in the zero set of a non-zero real polynomial . The algebraic Hilbert number is the supremum, over all polynomial vector fields of degree at most , of the number of algebraic limit cycles (a value in ).
A curve is invariant with cofactor if . A family of irreducible curves is generic if (i) no curve is singular, (ii) the top-degree homogeneous part of each curve is square-free, (iii) distinct curves meet transversally, (iv) no three distinct curves share a point, and (v) the top-degree homogeneous parts of distinct curves are coprime.
The equality asserts both that the number of algebraic limit cycles is bounded by the right-hand side for every field of degree at most , and that the bound is attained.
A proof of the goal would settle Problems 6 and 7 of the survey: it would give a uniform bound, depending only on the degree, for the number of algebraic limit cycles, and identify the sharp value. The conjecture is consistent with every example known to the survey: the generic bound of Theorem 4 is sharp for even , and the known non-generic examples exceed the generic bound only in odd degree and by one. Conjecture 2 () is its first open case.
On the formal side, the milestones require a reusable library of planar dynamics that is currently absent from Mathlib: periodic orbits and limit cycles of planar vector fields, hyperbolicity via the divergence integral, inverse integrating factors, invariant algebraic curves and Darboux-type arguments, and topological configurations of Jordan curves. Theorems 1, 2, 4 and 5, Proposition 3 and the cubic example are proved in the literature but, as far as the proposal author knows, not formalized; the goal and Conjecture 2 are open.
The obvious route bounds the number of ovals of the invariant curve (Harnack's theorem) and relates the degree of the curve to the degree of the field. This fails because a field of degree can have invariant curves of arbitrarily high degree, so no a-priori degree bound on the curve is available; Theorem 4 obtains one only under the genericity conditions (i)–(v), and the degree-3 example shows that non-generic curves behave differently. On the formal side, the dynamical milestones (Theorems 2 and 5, the cubic example) need Poincaré–Bendixson-type planar topology and uniqueness of solutions, which Mathlib does not yet provide.
MvPolynomial (Fin 2) ℝ with variable 0 as and 1 as ; points are ℝ × ℝ. The degree of a field is the maximum of the total degrees of and , and ranges over fields of degree at most , matching equation (1) of the survey.Set.encard values in ℕ∞, so an infinite family is , never silently ; is an iSup in ℕ∞, so the goal also asserts finiteness.HasDerivAt at every real time). A limit cycle is isolated among periodic orbits contained in a neighbourhood. An algebraic limit cycle lies in the zero set of some non-zero polynomial, with no degree restriction on the curve.ℕ∞, not an inequality over a possibly empty family.Contributions welcome: a planar ODE library (uniqueness, flows, Poincaré–Bendixson), Darboux theory of integrability, and proofs of the classical milestones.
A base-stock (order-up-to) policy orders, in every period, exactly enough to bring the inventory position (stock on hand plus stock on order minus backorders) up to a target level. It is the policy used in practice for repairable and consumable service parts, and the analysis of every later chapter of Muckstadt's book assumes it. Its optimality is therefore a foundational question, and there are three classical ways to prove it.
This mission formalizes the third approach, in the finite-horizon single-location form presented in Section 2.2.1 of Muckstadt (2005).
A single item is reviewed in periods . An exogenous, time-homogeneous Markov chain on a finite set is observed at the start of period ; given , the demand has law and is independent of . Excess demand is backordered.
Every unit of demand is a customer, and customers are indexed in arrival order, the initially waiting customers first. A customer's distance is once served, while waiting, and for future customers in the order they will arrive. Units are indexed by location: (used), (on hand), (in transit) and (at the supplier, which holds countably many units). The state is
with the location of unit and the distance of customer . In period : units in transit move one location closer and the released units move from to (so an order is on hand periods later); the demand brings the customers at distances to distance and moves the others steps closer; units on hand serve waiting customers, lowest indices first; then is charged per unit on hand and per waiting customer, with . The criterion is the expected cost over the periods, discounted by .
A policy for the whole system chooses a finite set of units at the supplier to release. It is monotone if it releases lower-indexed units first, and committed if unit only ever serves customer . The subsystem is unit with customer under commitment, with state and actions Release and Hold. The set contains the optimal actions of a subsystem whose unit is at the supplier and whose customer is at distance , and the critical distance is
Every policy that, in each period and Markov state , releases the lowest-indexed units at the supplier to raise the inventory position to
is optimal for among all policies, from every starting state. Such a policy exists. The levels are not fixed numbers but the critical distances of the single-unit problem, so the goal asserts the structure of an optimal policy and identifies its levels, without committing to any constant.
and managing every subsystem independently and optimally is optimal for . 3. Lemma 2 (p. 28): implies . 4. Section 2.2.1.2.2 (p. 29): the critical distance policy, release if and only if , is optimal for every subsystem.
The result shows that under Markov-modulated demand a single-location system is optimally run by a state-dependent base-stock policy. The same unit–customer argument gives echelon base-stock optimality in serial systems with noncrossing stochastic lead times (Sections 2.2.2–2.2.3). The decomposition also yields the levels themselves: they are the critical distances of a two-action problem, which can be solved one customer at a time.
The theorems are proved in the literature (Muharremoglu and Tsitsiklis 2008) and in the book. To our knowledge no machine-checked proof of any base-stock optimality theorem exists, by dynamic programming or by decomposition. The book's proof is informal in three places a formalization has to settle:
A formal development makes each of these precise.
The obvious argument says that costs are linear, so the cost of is the sum of unit–customer costs and everything decouples. That is only half of Theorem 4. The pairing of unit with customer holds only under monotone policies, and a general policy for observes the whole infinite state , not just . The lower bound therefore needs Lemma 1 together with the fact that extra information about the demand history does not help a Markov decision problem. The upper bound needs the lowest-index matching to cost no more than committed matching.
The second difficulty is that the threshold structure is not the obvious consequence of Lemma 2. The set of distances at which releasing is optimal must be shown to be an initial segment when ties are allowed. Unbounded demand makes that set possibly unbounded (it is, in the last periods). Finally, the release decisions of the subsystems must be counted to recover an inventory position, which uses the invariant that future customers occupy consecutive distances.
Everything is in the namespace ServiceParts.UnitDecomp, with three definition files.
Model. Model bundles the chain, the demand law, , , and with the standing assumptions , , , together with the per-unit and per-customer motions and a generic finite-horizon expected-cost recursion. Costs are in .
Subsystem. Subsystem defines a subsystem, its optimal cost, , and the critical distance policy.
System. System defines with lowest-index matching, its policies (finite release sets), monotone and committed policies, starting states, the inventory position and the order-up-to release.
Conventions and pinnings:
Corrections to the book:
Out of scope: stochastic noncrossing lead times (Section 2.2.2), serial systems (Section 2.2.3; compare the disproved platform statement SupplyChainTheory.clark_scarf_sequential), and continuous review (Section 2.2.4, which the book calls intuitive).
Proofs of any milestone are welcome. A reusable by-product would be a general lemma that Markov policies are optimal among history-dependent ones for finite-horizon problems with countable randomness and costs in .
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission extends the best possible constant for complex diagonal matrices from to every real . The result is proved in Lean. The constant and its formula are unchanged from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. For each exponent, it works for every triple of diagonal matrices, whatever their size, and no smaller constant does.
The mission started from a supplied pen-and-paper proof. Lowering the cutoff took more than replacing 256 with 90: several estimates in the original argument had to be strengthened. The research note proves the bound for real entries first, then transfers it to complex entries and shows that the constant cannot be improved. The goal theorem below gives the exact formula and statement.
This is the second step of the sharp diagonal Hlawka campaign, and it reuses the foundation's definitions and supporting results. The campaign invites further improvements below 90, keeping the same formula.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryA Markov chain Monte Carlo sampler is often assembled from simpler parts. A practitioner who has several proposal mechanisms for a Metropolis–Hastings sampler can combine them in two ways. Either each drives its own Metropolis–Hastings kernel and the sampler picks kernel with probability at each step, or the mixture is used as a single proposal inside one Metropolis–Hastings kernel. Both samplers leave the target invariant, so the choice is about efficiency.
Section 4 of Tierney (1998) settles the comparison: when both samplers use the maximal acceptance probability, the second never does worse in terms of asymptotic variances of sample-path averages. The statement that carries this is Proposition 5, an ordering of kernels in Peskun's off-diagonal order; the variance comparison then follows from Theorem 4 of the same paper, the general-state-space extension of Peskun (1973).
Timeline. Peskun (1973) introduced off-diagonal domination for finite state spaces and showed that the Metropolis–Hastings acceptance probability is maximal in that order. A version of Proposition 5 for discrete chains appears in the appendix of Tierney (1991) and in the rejoinder of Besag, Green, Higdon and Mengersen (1995). Tierney (1998) states and proves it for general state spaces, using the measure-theoretic description of Metropolis–Hastings kernels from §2 of the same paper.
Let be a measurable space and a probability measure on it, the target. A proposal kernel is a Markov kernel on . Given a measurable acceptance probability , the Metropolis–Hastings kernel is
where is the point mass at (mhKernel Q α).
Put and . With and (canonDensity), let
(canonR, canonRatio). The set is symmetric, and are mutually absolutely continuous on and mutually singular off it (Proposition 1 of the paper). The Metropolis–Hastings acceptance probability is
(alphaMH π Q), and the kernel with is the maximal Metropolis–Hastings kernel for (maxMHKernel π Q).
For kernels on , dominates off the diagonal, (OffDiagDominates π P₁ P₂), if for -almost every , for all . For a countable family of kernels and weights , the mixture is the kernel (mixKernel β K).
Let be a finite or countable family of proposal kernels and with . Let be the maximal Metropolis–Hastings kernel for and the maximal Metropolis–Hastings kernel for . Then
Both sides use maximal kernels: uses of the mixture proposal, each its own , and the same weights form both mixtures.
A companion item states the maximality of (§3, p. 7): every measurable acceptance probability whose kernel is reversible satisfies -a.e., so the maximal kernel dominates every reversible Metropolis–Hastings kernel with the same proposal.
The result. Proposition 5, combined with Theorem 4 of the paper (off-diagonal domination orders asymptotic variances of reversible kernels), shows that for every function with finite variance the asymptotic variance of under the mixture-proposal sampler is at most that under the mixture of samplers. Per-iteration cost can be higher for the mixture proposal, since then needs the densities of all components; Proposition 5 isolates the statistical side of that trade-off. The maximality companion states the fact behind the name "maximal kernel": is the largest acceptance probability that keeps a Metropolis–Hastings kernel reversible.
Formalizing it. The paper's proof is a computation of about six lines with Radon–Nikodym densities. A formal version must make explicit what the computation leaves implicit: that , defined from one dominating measure, has the same density form for every symmetric dominating measure; that the measure inequality on passes to the kernel-level statement with one null set for all ; and that the mixture proposal and the mixture of kernels are handled as countable sums of kernels. As of September 2026 neither Mathlib nor this platform has a machine-checked version of Proposition 5, of the maximality of , or of reversibility of the Metropolis–Hastings kernel on a general state space; only finite-state Metropolis chains have been formalized on the platform.
The obvious argument works pointwise with densities: write every kernel as a density against a common reference measure and compare of sums with sums of minima. On a general state space there is no common reference measure given in advance, and is only defined up to -null sets, through a Radon–Nikodym derivative with respect to , a measure that differs for and for each . The step that needs care is relating these different versions: the densities of the against a common symmetric , the density of , and the transpose densities , which are densities of only because is symmetric.
The second difficulty is the passage from measures to kernels. The inequality between measures on gives, for each fixed , the kernel inequality for -almost every , with a null set that depends on . The order requires one null set for all , and the diagonal must be removed, which needs the diagonal to be measurable.
The formalization is in Lean 4 with Mathlib, in the namespace TierneyMH.Mixture. The state space is a type E with a σ-algebra; π is a probability measure; proposal kernels are Markov kernels Kernel E E. Acceptance probabilities and densities take values in (ℝ≥0∞); a general is assumed measurable with . is π ⊗ₘ Q, its image under Prod.swap, detailed balance is Kernel.IsReversible. Mixtures are indexed by a countable type ("a sequence", which includes finite families), with weights in ℝ≥0 and HasSum β 1.
Added hypotheses, both labelled in the statements: singletons are measurable (implicit in the paper's and ), on the goal and the maximality companion; and, on the goal only, the σ-algebra of is countably generated. The second is an addition to the paper: it is what makes the exceptional null set in uniform over in the passage from the measure inequality to the kernels. It is not assumed in the measure-level milestones.
is one fixed version, built from Mathlib's rnDeriv exactly as in the proof of Proposition 1 (with , not an arbitrary dominating measure), and all statements are insensitive to the version. The ratio is set to 1 on the null subset of where is infinite, so that and hold everywhere, as Proposition 1 asks.
Trivializations ruled out: is the indicator of times , never an arbitrary acceptance function or a single shared by all components; compares , not (on the rejection masses differ and the comparison is false); and the conclusion is about the Metropolis–Hastings kernels themselves, not about the measure identity alone. All hypotheses are satisfiable, for instance on = Bool with uniform, two proposals and and weights .
Needed infrastructure, reusable for other Metropolis–Hastings results: Radon–Nikodym calculus for product measures and their transposes, countable sums of kernels, and a monotone-class argument over a countable generating family. The Metropolis–Hastings kernel, , and off-diagonal domination are defined identically in the companion missions I (detailed balance, Theorem 2) and II (Peskun ordering, Theorem 4) of this series. Proofs of milestones in any order, and proofs of the goal from the milestones, are welcome.
The discrete logarithm problem modulo a prime asks, given a prime , a generator of the multiplicative group modulo , and a nonzero residue , for the exponent with . Its presumed classical hardness underlies Diffie–Hellman key exchange, ElGamal encryption and the Digital Signature Algorithm. The best classical algorithm known when Shor wrote, Gordon's adaptation of the number field sieve, runs in time .
In §6 of Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (SIAM J. Comput. 26(5), 1997; doi:10.1137/S0097539795293172, arXiv:quant-ph/9508027), Shor gave a quantum algorithm that uses two modular exponentiations and two quantum Fourier transforms and outputs, with constant probability, a pair from which can be computed. The quantitative core of that analysis is a single number: the circuit produces a "good" output with probability at least . This mission formalizes that bound and the three estimates it is assembled from.
Let be a prime and a generator of , so that are all the nonzero residues. Fix the unknown with and put . Let be the power of with .
The Fourier matrix is the matrix with entries for (§4, eq. (4.1)). Rows index input basis vectors and columns output basis vectors.
The algorithm uses three registers: two holding numbers and one holding a nonzero residue modulo . It starts from the state
(preFourierState), applies to each of the first two registers (finalState), and measures all three registers. The probability of observing is the squared modulus of its amplitude (outcomeProb).
For integers and , the symmetric residue is the residue of modulo in (symmRes). Put
An observed state is good (IsGood) when
Goodness depends only on .
The constant is the one the page carries forward. The goal fixes no threshold on : it is stated for every prime that admits a power of two strictly between and .
The result. The bound is what turns the circuit into an algorithm. Repeating the circuit times in expectation yields a good output, and from a good pair one reads off an equation that determines modulo divisors of (§6, eqs. (6.18)–(6.20)). Together with the quantum Fourier transform circuit and reversible modular exponentiation, this places the discrete logarithm modulo a prime in quantum polynomial time. Every later analysis of quantum attacks on discrete-logarithm cryptography starts from this success probability or a sharpened version of it.
Formalizing it. The result has been proved since 1994–1997 and is textbook material; it is not open. As far as is known, no machine-checked proof of Shor's discrete-logarithm analysis exists. The paper's proof of eq. (6.17) replaces a sum by an integral with an error term whose constant is not given, yet states for every prime. A formal proof must therefore either control that error explicitly or find another argument, and so settles a point the paper leaves informal. Numerically, the smallest value of over good states is about for all primes , so the unconditional claim is not in doubt for small . The page also contains two small slips, recorded under Formalization scope; a complete development pins down exactly what is true.
The exponential sum (6.4) runs over pairs satisfying a congruence modulo , while the phases are taken modulo . The two moduli are unrelated: is a power of two and is arbitrary. Eliminating through the congruence introduces a floor function , and the resulting phase is not linear in . The obvious estimate treats the sum as a geometric series in and bounds it by its first-order phase; this fails because the floor term perturbs every phase by an amount of size up to . Condition (6.11) only keeps this perturbation within of the main phase; it does not remove it. The per-state bound must survive this perturbation uniformly in , and , including small primes where the paper's integral approximation gives no explicit control.
The count of good pairs needs a separate argument about how often a multiple lies within of a multiple of when is large.
Fin q × Fin q × (ZMod p)ˣ → ℂ. The first two registers range over ; the third over the units modulo .finalState is defined this way from (6.1) and . It is not typed in as the closed form (6.3) or (6.4). A formalization that defined the final state by (6.4) directly would make milestone 1 trivial, and is ruled out.Fact p.Prime). The generator is encoded as orderOf g = p - 1. is a parameter, with . is given by q = 2 ^ l together with . No large- threshold is added anywhere.x⁻¹ ^ b in the unit group. is computed in and inside and the congruences, and as natural-number subtraction only where makes it exact. is real.Needed infrastructure: finite exponential sums and their modulus, the symmetric residue and its basic properties, and counting multiples in residue classes of . The exponential-sum estimates of milestones 1 and 2 are reusable in the order-finding analysis of §5 of the same paper. Proofs of any milestone, of the normalization , and of auxiliary lemmas about symmRes are welcome.
Feedback laws in engineering are applied with a lag: sensors, actuators and communication channels introduce a time delay between the measurement of a state and the control that reacts to it. For finite-dimensional systems small delays are usually harmless. For distributed systems such as the wave equation they need not be: Datko, Lagnese and Polis (SIAM J. Control Optim. 24, 1986) and Datko (SIAM J. Control Optim. 26, 1988) showed, for one-dimensional examples, that an arbitrarily small delay in a stabilizing feedback can destroy stability. The question matters to anyone who designs boundary or internal controllers for vibrating structures and wants to know whether a stabilizing law is robust to delay.
Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006)) study the wave equation on a bounded domain of with a damping term that combines an instantaneous and a delayed velocity feedback, with coefficients and . They show that the system is exponentially stable when (Theorems 1.1 and 1.3), and that when stability can fail (Theorems 1.2 and 1.4). This mission is Theorem 1.4, the internal-damping instability result, in the case the paper proves.
Let and let be a bounded open set with boundary of class , split as with and . Write for the outer unit normal and for the normal derivative. Let , and let be the delay. With damping coefficient the problem is
with initial data , and a history on . The standard energy of a solution is
The condition is the paper's assumption (1.8). The paper's problem (1.12)–(1.16) carries a general coefficient with and near ; is one such coefficient.
If (1.8) fails, i.e. , then
and the same holds with "" replaced by "", for every . The goal asserts only non-decay, not a rate of growth or the value of the energy, so it survives any sharpening of the examples.
The result shows that the stability threshold of Theorem 1.3 is sharp in the sense that matters for design: at or beyond the threshold there is no delay margin, since delays as small as desired already produce solutions whose energy does not decay. Together with Theorem 1.3 it gives a complete dichotomy in the coefficients for the internally damped wave equation with delay, in any dimension, and it identifies the mechanism (roots of the characteristic equation on or to the right of the imaginary axis) that later work on delayed stabilization has had to avoid.
The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission's product is a formal proof of the case together with its algebraic core: the reduction of the transcendental characteristic equation, the analysis of both cases, and the two-sided bounds on the delays. The spectral input it needs, an unbounded sequence of eigenvalues of the mixed Dirichlet–Neumann Laplacian with regular eigenfunctions, is reusable well beyond this paper.
The scalar part is elementary. The difficulty is the spectral input. The small delays come from with , so the proof needs infinitely many eigenvalues of the Laplacian with mixed Dirichlet–Neumann conditions on a domain, with eigenfunctions that are inside and up to the boundary. This requires compactness of the embedding , the spectral theorem for compact self-adjoint operators, and elliptic regularity for a mixed problem, none of which is available in Mathlib for domains in . A single eigenpair gives only the large delays (letting ); it does not give the small ones.
A second point: the paper's own bound bounds only from below, so it does not by itself give ; the upper bound of milestone 6 is needed.
EuclideanSpace ℝ (Fin n) with . The boundary is given by a global defining function (, , on ); ; the surface measure is pinned by the Gauss–Green formula for all fields.Boundary feedback stabilization of the wave equation asks whether a damping term placed on part of the boundary drives the energy of every solution to zero. Without delay the answer is classical: the feedback on a part of the boundary gives exponential energy decay under geometric conditions (Chen, Lagnese, Lasiecka–Triggiani, Komornik–Zuazua). In practice a feedback is applied with a lag, and a small lag can destroy stability. Datko, Lagnese and Polis (doi:10.1137/0324007) and Datko (doi:10.1137/0326040) showed, in one space dimension, that a purely delayed boundary feedback destabilizes the system for arbitrarily small delays.
Nicaise and Pignotti (doi:10.1137/060648891) study a feedback made of an instantaneous part and a delayed part, with weights and , in any space dimension. Their Theorem 1.1 gives exponential decay when . This mission formalizes the converse, Theorem 1.2: when , some delays admit solutions whose energy does not decay at all.
Timeline.
Let and let be a bounded open set with boundary of class . The boundary is split as , with and . Write for the outer unit normal and for the surface measure. Together these data form a mixed domain (MixedDomain n in Lean).
Fix and a delay . The problem (1.1)–(1.3) is
with initial data , and a history on (1.4)–(1.5). The standard energy of a solution is (3.7)
Condition (1.8) of the paper is . This mission concerns the complementary case .
For real functions on , (5.11) defines and .
If , there exist delays and, for each , a classical solution of (1.1)–(1.3) with delay and a constant such that
The statement fixes no formula for the delays and no value of the energy. It asserts only the existence of infinitely many delays for which the energy does not decay.
The result. Theorem 1.2 shows that the threshold of Theorem 1.1 is sharp in the following sense: once the delayed weight reaches the instantaneous one, no geometric assumption restores asymptotic stability for every delay. Together, Theorems 1.1 and 1.2 separate robust from non-robust boundary feedbacks by a single inequality between the two gains. The explicit delays of case (a), , become arbitrarily small or large. So even an arbitrarily short lag in an equally weighted feedback can remove decay.
The formalization. The paper proves the result. It has not been formalized, and Mathlib has no wave equation on domains, no mixed eigenvalue problems and no Sobolev spaces on domains. This mission produces:
Milestones 1 and 2 are calculus and trigonometry. The difficulty sits in producing . The goal needs a nonzero function that is in and up to the boundary and solves an eigenvalue problem with mixed Dirichlet and Neumann (case (a)) or Dirichlet and Robin-type (case (b)) boundary conditions. Existence requires compactness of and of the trace into , followed by elliptic regularity up to a boundary. None of these is in Mathlib.
A shortcut does not work: in case (b) the frequency enters the boundary condition, so is not an eigenfunction of a fixed self-adjoint operator. The page instead minimizes a non-quadratic functional, and its first-variation computation (5.18)–(5.19) needs care: the functional is not 2-homogeneous, so the normalization by does not literally give , although the first-order condition is right.
Taking real parts does not give a real-valued solution with constant energy: in case (b) the energy of oscillates.
A complete development needs the following:
These pieces are reusable well beyond this mission. Contributions of any of them, or of an alternative route to a with the required properties, are welcome.
Many problems in statistics, signal processing and machine learning minimize a sum of a smooth loss and a nonsmooth regularizer: least squares with an or penalty, and constrained problems in which the regularizer is the indicator of a nonconvex set. The proximal gradient method (also called forward–backward splitting) is the standard first-order algorithm for such problems. Each step takes a gradient step on the smooth part and then applies the proximal mapping of the nonsmooth part, which for many nonconvex regularizers (hard thresholding, projection onto sparse vectors) has a closed form.
For a smooth part whose gradient is -Lipschitz, the classical analysis allows any constant step size , and every cluster point of the iterates is stationary; Li and Pong cite Bredies and Lorenz (Minimization of non-convex, non-smooth functionals by iterative thresholding, preprint, 2009) for this. Attouch, Bolte and Svaiter (Math. Program., 2013) added convergence of the whole sequence when has the Kurdyka–Łojasiewicz property. When is nonconvex, however, is governed by the most negative curvature of as much as by the most positive one, and the admissible step sizes can be much smaller than the convex part of alone would require.
Li and Pong (SIAM J. Optim., 2015; preprint arXiv:1407.0753v6) show that the concave part of imposes no restriction on the step size: it suffices to bound the curvature of after it has been offset by a convex function. This mission formalizes that result, Theorem 4 of their paper. It is the fourth mission of a series on the paper; the first three treat its results on the alternating direction method of multipliers.
Work in with the Euclidean inner product and norm . The problem is
under the paper's standing assumptions: is twice continuously differentiable with a bounded Hessian ; is proper (never , finite somewhere) and closed (lower semicontinuous); and for every and the proximal problem has a minimizer. Neither nor is assumed convex.
A vector is a regular subgradient of at (with ) if for all near , for every . The limiting subdifferential collects the limits of regular subgradients at points with . A point is stationary if
Given a step size and an arbitrary starting point , the proximal gradient method generates by
Any minimizer may be selected. A cluster point of is the limit of a subsequence .
The step-size condition involves a convex function and a constant with
where is the Loewner order on symmetric linear maps.
Suppose is twice continuously differentiable and convex, , (44) holds, and is generated by (43) with . Then
and every cluster point of , if one exists, satisfies .
The goal does not assert that a cluster point exists, nor that the whole sequence converges; both are false without further assumptions.
In the order of the paper's proof:
The result. For a difference of convex functions with being -Lipschitz, (44) holds with and , so the step size may be taken in whatever the curvature of . For an indefinite quadratic the admissible range becomes instead of , and for a concave quadratic every positive step size is admissible. Because the method is a descent method under this rule, its iterates stay in a sublevel set of , so the sequence is bounded whenever is coercive. The same estimates feed the whole-sequence convergence argument for Kurdyka–Łojasiewicz functions.
Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it requires the limiting subdifferential of an extended-real-valued function, its closedness property (3), and a Fermat rule for a smooth-plus-nonsmooth sum, none of which is in Mathlib. These are reusable for any nonconvex first-order method analysed through cluster points.
The descent part rests on (45), a descent inequality for whose Lipschitz constant is read off from a two-sided Hessian bound; the familiar descent lemma is stated for alone and does not apply, since may have a much larger Lipschitz constant than .
The stationarity part is where the naive argument fails. Passing to the limit in (47) needs not only but also , because the limiting subdifferential is closed only under -attentive convergence. Lower semicontinuity gives one inequality; the other must come from the minimizing property (43) compared against . The objective may be at , so summability of the steps has to be extracted without assuming a finite starting value.
The space is EuclideanSpace ℝ (Fin n). and are real-valued; takes values in EReal, and every objective value is compared in EReal, never through EReal.toReal. The Hessian is the derivative of the gradient map, a continuous linear self-map; the Loewner order is Mathlib's partial order A ≤ B ↔ (B - A).IsPositive, and both sides of (44) are kept. The regular subgradient is encoded in its -neighbourhood form, and the limiting subdifferential requires all three convergences , , . Stationarity is . The update (43) is a relation on sequences: minimizes the bracket over all of , with no uniqueness and a free starting point. A cluster point is the limit of for a strictly increasing .
Trivializing formalizations are ruled out: (44) is not replaced by " is -Lipschitz", which is the classical special case ; , boundedness of the sequence and existence of a cluster point are not assumed; and a limiting subdifferential without is not used, since that would make stationarity a weaker statement.
Contributions welcome: the closedness (3) and the Fermat rule behind (47) for the limiting subdifferential, a descent lemma from a two-sided Hessian bound, and the telescoping and limit arguments of the proof.
The alternating direction method of multipliers (ADMM) is a standard method for problems of the form , in which a smooth loss is composed with a structured, possibly nonsmooth regularizer through a linear map . Its convergence theory was developed for convex problems, yet it is routinely run on nonconvex ones: sparse recovery with the constraint, low-rank matrix problems, and total-variation-type models with nonconvex penalties. For such problems a practitioner wants a guarantee about the iterates actually produced, not only about the existence of good subsequences.
Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave the first such guarantee for the classical ADMM on nonconvex composite problems with a surjective . Their Theorem 1 shows that cluster points of the (proximal) ADMM are stationary; their Theorem 3, the subject of this mission, shows that for semi-algebraic data the whole sequence converges. The argument adapts the Kurdyka–Łojasiewicz (KL) framework of Attouch, Bolte and Svaiter (Math. Program. 137, 2013) to a setting where the ADMM only decreases its merit function in the -block.
Fix linear, twice continuously differentiable with bounded Hessian, and proper (finite somewhere) and closed (lower semicontinuous). For the augmented Lagrangian is
The ADMM produces from arbitrary by
Assumption 1 with asks for , and symmetric maps with , and for all , , and .
The limiting subdifferential of consists of limits of regular subgradients at points with . A point is stationary if .
A set in is semi-algebraic if it is a finite union of sets cut out by finitely many polynomial equations and strict inequalities ; a function is semi-algebraic if its graph is. A proper has the KL property at if there are , a neighbourhood of and a continuous concave with , , , such that whenever and . A KL function is proper, closed, and KL at every point of .
In the Lean development is augLag h P M β x y z, and also augLagX h P M β as a single function on the triple space with the Euclidean inner product.
Under the standing assumptions and Assumption 1 with , if and are semi-algebraic and the ADMM sequence has a cluster point , then
No constants are fixed: every parameter is quantified exactly as in the paper.
Milestones 6, 7 and 8 together imply the goal.
The result. Theorem 3 upgrades subsequential convergence to convergence of the whole iterate sequence, with finite length of the -trajectory, for a nonconvex ADMM without any convexity of or . Semi-algebraicity covers the paper's applications: polynomial losses, the constraint, and indicators of polyhedral or algebraic sets. Remark 4(1) isolates the only property actually used, the KL property of , so the result extends to any class of functions for which that property is known (for instance, globally subanalytic or o-minimal definable data).
Formalizing it. The result is proved in the paper and, as far as is known, formalized nowhere. The mission produces a machine-checked version of the paper's convergence argument, a Lean definition of the KL property with the correct convention for empty subdifferentials, and a semi-algebraic set predicate over MvPolynomial. Milestone 8 is a published theorem of real algebraic geometry and nonsmooth analysis (Bolte–Daniilidis–Lewis 2007) that the paper quotes without proof; it is part of what a complete development of the goal requires.
The obvious route is to invoke the abstract convergence theorem of Attouch–Bolte–Svaiter for descent methods. It does not apply: its sufficient-decrease hypothesis requires to drop by a multiple of , while the ADMM only guarantees a drop proportional to (Remark 4(2)). The relative-error bound (35) is likewise in terms of the -step alone, and relating the - and -blocks back to the -block uses the surjectivity of and the specific structure of the multiplier update. The neighbourhood on which the KL inequality holds is a neighbourhood of the full triple, whereas the trajectory is controlled only in .
The semi-algebraic part has a separate difficulty: showing that is semi-algebraic needs closure of semi-algebraic sets under projection (the Tarski–Seidenberg theorem), and the KL property of semi-algebraic functions needs the Łojasiewicz inequality for subanalytic or semi-algebraic functions. Mathlib has neither.
Spaces are EuclideanSpace ℝ (Fin n); is a continuous linear map and its adjoint. and take values in EReal, never passed through toReal except where the value is provably finite. is Mathlib's Loewner order on self-maps; the Hessian is fderiv ℝ (gradient h). The ADMM is the proximal-ADMM relation with ; argmin steps are "value at most the value anywhere", with no uniqueness; is unconstrained. The triple space is the nested product, so its inner product is the sum of the block inner products.
The KL inequality is stated for every , which encodes . Writing it with Metric.infDist 0 (∂f x) would give and make the KL property fail at every point with empty subdifferential, so that "semi-algebraic implies KL" becomes false and the goal becomes a statement about a different notion. The KL property is required only at points of , only on a neighbourhood and only for values in ; is differentiable only on the open interval. Semi-algebraicity of an extended-valued function is that of its graph over its real values. is a positive real, which is equivalent to the paper's .
The hypotheses and are part of the theorem, not a simplification: the analogous statement for the proximal ADMM is open (Remark 4(3)). The cluster point is assumed, not derived.
Needed infrastructure: calculus of the limiting subdifferential (a smooth-plus-separable sum rule), the Tarski–Seidenberg theorem, and the Łojasiewicz/KL inequality for semi-algebraic functions. The last two are reusable far beyond this mission; contributions toward them, and toward the analytic core (milestones 1–6), are welcome.
The alternating direction method of multipliers (ADMM) splits a problem of the form into a sequence of simpler subproblems, one in which the nonsmooth term enters only through its proximal map and one in which only the smooth term appears. For convex problems its convergence theory is classical. In signal processing and statistics, however, the method is routinely run on nonconvex models, such as - or -regularized least squares, where is nonconvex and possibly discontinuous and convex theory does not apply.
Li and Pong (arXiv:1407.0753, SIAM J. Optim. 25(4), 2015) gave a convergence analysis of a proximal variant of the ADMM for this nonconvex setting. Their Theorem 1 shows that every cluster point of the iterates is a stationary point. That statement is only informative if cluster points exist. Theorem 2, the subject of this mission, gives conditions on , and under which the whole sequence of iterates is bounded, so that cluster points exist and Theorem 1 applies.
Let . The data are:
The augmented Lagrangian is
and the Bregman distance of is . A sequence is generated by the proximal ADMM if, from arbitrary ,
For a linear self-map , write , and write , for the semidefinite and definite order of symmetric maps. Assumption 1 asks for with (so is surjective), bounds , maps with , with , a bound , and with
Suppose Assumption 1 holds and, with the same and , there is with
Suppose that either (i) is invertible and , or (ii) and . Then
The milestones are the numbered displays of the paper's proof:
The result. Theorem 2 supplies the existence of cluster points that Theorem 1 assumes. The two together give an unconditional statement: under Assumption 1, (29) and either coercivity condition, the proximal ADMM has a cluster point and every one of them is stationary. The hypotheses cover the models that motivate the paper. Least squares with a coercive nonconvex regularizer falls under case (i) with , and a strongly convex quadratic with a regularizer that is bounded below and a general surjective falls under case (ii) (Examples 4–6 of the paper). Boundedness is also a standing hypothesis of the paper's Theorem 3, the Kurdyka–Łojasiewicz argument for convergence of the whole sequence.
Formalizing it. The result has been proved since 2015. As far as a search of the platform shows, neither it nor the underlying Lyapunov-type estimates for the ADMM has been machine-checked. This mission formalizes the known proof. The estimates (20), (30) and (31) are shared with the stationarity analysis of the same algorithm, so they serve any later formal work on nonconvex ADMM variants.
The obvious approach is to bound the iterates by the monotone quantity of Eq. (30). That quantity involves , which contains and is not bounded below a priori, so its decrease alone does not bound anything. The dual term has to be absorbed. It is controlled through and the last primal step, and the part involving is then paid for out of itself. Condition (29) exists to make exactly this trade possible, which is why it couples to the of Assumption 1. The two cases then extract boundedness in opposite orders: (i) goes from through to using invertibility of , and (ii) goes from through to . In case (i) the lower bound on that the argument needs is not assumed and must itself be derived from coercivity and lower semicontinuity.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and is a continuous linear map with Mathlib's adjoint. , and every inequality containing them live in EReal, stated additively so that no extended-real subtraction occurs.Ruling out trivial versions. A formalization that bounds only , fixes or to an example's values, lets (29) use a fresh , adds a lower bound on in case (i), or assumes minimizers that make the sequence constant proves a different, weaker theorem, and is not the target.
Definitions needed. Proper and closed extended-valued functions, the Hessian as fderiv of gradient, the augmented Lagrangian, the Bregman distance, the proximal-ADMM relation and Assumption 1 are all provided. They mirror the definitions of the companion mission on cluster points of the same algorithm. A solver will need standard facts beyond them: first-order optimality for a differentiable function, the mean-value bound from the Hessian sandwich, and strong convexity of the -subproblem. Proofs of individual milestones are welcome independently.
Approximate policy iteration and policy-gradient methods stop when they can no longer find a direction of improvement. Kakade and Langford (ICML 2002) asked what such a stopping point guarantees. Their algorithm, conservative policy iteration, halts at a policy for which no policy can improve much on as measured under a restart distribution ; the quantity that is small is the optimal policy advantage . Theorem 6.2 of the paper translates this local condition into a global statement: the performance of is close to optimal, with a loss controlled by how well covers the states an optimal policy visits.
The bound is the origin of the distribution mismatch coefficient , which reappears in the analysis of approximate dynamic programming (concentrability coefficients, Munos 2003), of conservative and trust-region methods, and of the convergence of policy gradient methods (Agarwal, Kakade, Lee, Mahajan 2021), where it governs the rate. The performance difference lemma (Lemma 6.1) used in its proof has become a standard tool of reinforcement learning theory.
A finite Markov decision process has a finite nonempty state set , a finite nonempty action set , transition probabilities (for each a probability distribution over ), a reward function with , and a discount factor . A stochastic policy is, for each state , a probability distribution over actions. A state distribution is a probability vector on .
The normalized value function is , where , and . The state–action value is and the advantage is . The discounted future state distribution from is
and the performance of from is .
The policy advantage of with respect to and is : the expected advantage of over on the states itself visits. Its maximum over all stochastic policies is (Definition 4.3). An optimal policy satisfies for every policy and every state . For nonnegative on , (p. 5).
If and is optimal, then for every state distribution
The goal states both inequalities and the outer bound. The evaluation distribution is arbitrary and unrelated to the restart distribution ; taking , the start distribution, gives Corollary 4.5 (p. 5).
For any policies , and any starting distribution ,
The states are weighted by the future state distribution of the new policy , the advantage is that of the old policy .
Theorem 6.2 is the quality guarantee for conservative policy iteration: combined with the paper's Theorem 4.4 (the algorithm stops with after polynomially many calls), it bounds the suboptimality of the returned policy for any target distribution, independently of the size of the state space except through the mismatch coefficient. It also explains the role of the restart distribution: a more uniform makes small. Lemma 6.1 is used throughout later theory, from trust-region policy optimization to the global convergence of policy gradient methods.
Both results are proved in the paper, with short arguments. The contribution of this mission is a machine-checked version of the infinite-horizon discounted statement in the paper's normalization, with the ratios handled exactly, including states where a denominator vanishes. Neither the discounted performance difference lemma for stochastic policies nor the distribution mismatch bound is known to be formalized in Mathlib; a finite-horizon performance difference identity has been formalized separately and is a different statement.
The mathematics is short; the difficulty is in the infinite-horizon bookkeeping. The value function and are infinite series, and Lemma 6.1 relates the series of two different policies: its natural one-line argument uses the Bellman equation for , which is not the definition here, together with interchanges of infinite sums over time with finite sums over states and actions, each of which needs summability. Theorem 6.2 then needs two facts that are not stated as results in the paper: that equals (the supremum over policies is attained by a greedy policy, and ), and that . Reading the ratio with real division would give a false statement when a denominator is zero; the statement avoids this.
States and actions are finite nonempty types; policies and kernels are real-valued functions π s a (the paper's ) and P s a s' (the paper's ), with their distribution properties as explicit hypotheses. The published definitions IsTransitionKernel, IsPolicy, InducedTransition, OccupationDist, InducedReward and PolicyValue from the Foundations of Machine Learning series are reused; is times PolicyValue, the defining series. is the supremum of the policy advantages over stochastic policies, which is the paper's maximum. Optimality of is relative to stationary stochastic policies, the paper's policy class; the existence of an optimal policy (the paper's "well known result", p. 2) is not part of this mission.
Every hypothesis is explicit: rewards in with , , a kernel, and stochastic policies, and state distributions. Each bound is stated multiplicatively: "" is " for every with for all ". When some no such exists and the bound is empty, which matches ; no full-support assumption is made on or . The hypothesis is on the supremum itself, not on the closed form , which is a step of the proof; a formalization that assumed the closed form, or that divided by in real arithmetic, would not be this theorem. The proof of the theorem uses only that is a policy; optimality is kept as a hypothesis because the paper states it.
The proof on p. 7 twice writes ; the inequality it uses, and the one stated on p. 5, is . This slip is in the proof, not in the statement. Pages are PDF pages; the paper has no printed page numbers.
Useful reusable infrastructure: summability and Bellman equations for the normalized discounted value, as a probability distribution with , and attainment of by a greedy policy. Contributions of any of these as separate lemmas are welcome.
Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.
The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.
Timeline.
There are items and three machines. Item needs processing time on machine 1, on machine 2 and on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.
A schedule assigns each item start times . It is feasible when all start times are at least on machine 1, the processing intervals of distinct items on the same machine do not overlap, and , . The three machines may process the items in different orders. The total elapsed time (makespan) is .
An ordering lists the items, being the item in position . Its as-soon-as-possible schedule processes the items in the order on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions , Johnson defines
the sums running over the items in the first (resp. ) positions.
Johnson's three-stage rule says that item definitely precedes item when
and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.
If every is at least every , then an ordering consistent with (IV) exists, and for every such ordering the as-soon-as-possible schedule of is feasible and satisfies
the "maximum walk" of p. 68. 3. Special case (p. 67). If then , so the makespan is . 4. (III) (IV) (p. 67). Interchanging the items in positions changes and only at , and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every is at least every .
The result. Theorem 2 gives an exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.
Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).
The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves , and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis is what makes nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.
Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with , so the empty instance has makespan . An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's , . Statements with maxima over positions assume .
Hypotheses made explicit or corrected:
Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form , would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.
A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.
Federated learning combines information from several clients without pooling their raw training records. A client may later request removal of its contribution. Retraining on the retained records supplies a natural comparison model, but repeating the training process can be costly. Jin, Chen, Zhang, and Li introduce a linearized learning pipeline and a server-side removal procedure in Forgettable Federated Linear Learning with Certified Data Unlearning, arXiv:2306.02216v3. Their linearization makes the training objective quadratic, so the distinction between an exact Newton correction and an approximate correction can be studied explicitly.
This mission formalizes a corrected finite-run error bound motivated by that analysis. It is not a transcription or validation of the printed Theorem 2. The source audit found that the supplementary argument drops a finite-training term when passing to a limit, uses an invalid general inverse-perturbation inequality, and does not justify its three-term squared-norm constant. The draft preserves the removal problem while stating its error factors explicitly. The source anchors are Section III-C, Theorem 2, PDF pp. 5–6, and supplementary Section C5, PDF p. 16. The preprint first appeared in 2023; this mission fixes the revised May 2026 version so later source changes cannot silently alter its meaning.
A parameter is a vector . Record has a fixed linear feature map , an offset , and a target . Its prediction is . This represents the fixed linearization in the paper's equation (3); arbitrary real targets are permitted, and one-hot classification targets are a special case. Neither approximation accuracy for a nonlinear neural network nor an infinite-width limit is asserted.
Let be the full finite dataset and a nonempty subset of retained indices. Client removal is represented by retaining precisely the indices whose owner differs from the removed client. More general record removals are also allowed. For a fixed regularization parameter , define
Write , , and . Define and let use the full dataset. These reference parameters are computed from the data. The accepted child proofs establish the Hessian positivity and invertibility needed for the error bound; the broader unique-minimizer theorem is a separate supporting statement. The construction comes from Section III-A, PDF pp. 3–4, equations (3)–(5).
A separate nonempty server dataset has Gram operator and regularized Hessian . All operator norms below are Euclidean operator norms. The datasets and feature maps are fixed throughout the probability calculation.
Let be the trained parameter, the parameter returned by retraining on , and an approximate removal correction. The removed parameter is . Their joint probability model has finite outcome space , with masses summing to one. They may be dependent. This covers the outputs of finite randomized runs on finite data with fixed initialization; no independence assumption is used.
For each trained parameter , define the server removal objective and its exact minimizer by
This is the quadratic surrogate in Section III-B, PDF p. 5, equation (6). Define
The corrected goal is
The two completed milestones used by the accepted proof are the surrogate gap bound and the corrected signed removal-error identity:
The broader ridge-structure, exact-Newton-removal and inverse-perturbation statements remain available as separate open theorems. Their milestone entries were removed because the accepted proof does not depend on their full statements.
Formalization note: the completed root is a corrected, paper-derived error bound. Its formal bridge uses the two source-backed child theorems above, anchored to Section III-B (Section 3), PDF p. 5, equation (6), and Section III-C (Section 3), PDF p. 5 and PDF p. 6, Theorem 2; supplementary C5, PDF p. 16, unnumbered displays. The coefficients in the boxed goal are conservative; no optimality claim is made.
The result connects the removal solver's objective gap, the difference between the server and retained Hessians, and the actual optimization errors to an observable parameter discrepancy. Exact Hessian matching sets . Exact removal optimization sets , but finite retraining error still remains. This distinguishes exact optimization of the retained objective from reproducing an unfinished retraining run.
The original paper motivates the comparison; the displayed corrected bound is a new formulation derived from its quadratic setting. The root Lean theorem and its two dependency milestones are now Proved. Their accepted proofs match the original formal statements exactly; the three separate supporting statements remain open. The requested OpenProblem classification describes the formalization task and does not assert that the elementary corrected inequality is an unresolved research conjecture.
An approximate server Hessian cannot be substituted for the retained Hessian without a sensitivity term. A bound on the difference of the Gram operators alone does not bound its action on every parameter vector. Likewise, a small training error relative to the full-data optimum does not imply that the full and retained optima coincide. The displacement therefore remains visible. Formalization must respect the normalization of each empirical objective, the sign of the correction, and the operator norm used in the perturbation estimate.
The model uses finite-dimensional real Euclidean spaces, continuous linear maps and adjoints, finite index sets, a total ring inverse, and finite weighted expectations. Positive regularization must justify every use of the inverse; it is not an invertibility assumption hidden inside the dataset. Nonempty retained and server data exclude division by an empty sample count. Zero-dimensional feature or parameter spaces are permitted and harmless. A finite law on an empty outcome type has no inhabitant because its masses cannot sum to one.
The root theorem quantifies over arbitrary output maps . It is an error-propagation theorem in terms of their actual errors and surrogate gap, not a convergence theorem for a particular implementation. Obtaining algorithm-specific bounds on those quantities is separate future work. In particular, the draft does not import the source's unsupported all-smaller-learning-rates FedAvg contraction claim. It also makes no differential-privacy, distributional indistinguishability, nonlinear-network, or empirical accuracy assertion.
The Lasso (Tibshirani 1996, doi:10.1111/j.2517-6161.1996.tb02080.x) is -penalized least squares regression, one of the standard estimators of statistics and machine learning because it selects sparse coefficient vectors. Explaining why a learned Lasso predictor generalizes is less routine than it looks. The two classical routes are uniform convergence over the hypothesis class and algorithmic stability (Bousquet and Elisseeff 2002, JMLR 2:499–526). The stability route is closed for the Lasso: Xu, Caramanis and Mannor (IEEE Trans. Inf. Theory 56(7), 2010, doi:10.1109/TIT.2010.2048503) showed that its uniform stability bound does not decrease with the sample size, a fact reproduced as Theorem 7 of Xu and Mannor (2012).
Xu and Mannor, Robustness and Generalization (Mach Learn 86 (2012) 391–423, doi:10.1007/s10994-011-5268-1), propose a third route, algorithmic robustness: if the sample space can be split into cells such that a test point in the same cell as a training point has nearly the same loss, then the algorithm generalizes (their Theorem 1). Their Example 6 shows that the Lasso is robust in this sense, with a number of cells given by a covering number and a robustness level depending on the training responses. This mission formalizes Example 6 together with the general criterion it rests on (Theorem 6) and the Lipschitz estimate for the Lasso loss (Lemma 3).
A sample is a point with a response and a feature vector , so the samples live in . The sample space is a compact set, and carries the norm . A training set is .
A learning algorithm maps each training set to a hypothesis ; with a loss , it is -robust (Definition 2, p. 396) if can be partitioned into disjoint sets , fixed independently of the data, such that for every , every training point , every and every ,
For a metric on and , a set is an -cover of if every point of is within distance of a point of ; the covering number is the least cardinality of such a cover (Definition 1, p. 394).
For a coefficient vector let . Given , the Lasso is
a Lasso algorithm returns a minimizer of (5) for each , and the loss is the absolute prediction error . Finally .
For every compact , every , every Lasso algorithm and every ,
The statement holds for every selection of a minimizer, since (5) need not have a unique solution.
Combined with Theorem 1 of the same paper, Example 6 yields a generalization bound for the Lasso of the form with a covering number of the sample space, a bound that uses no stability of the algorithm and no uniqueness of the minimizer. Theorem 6 is the reusable part: it converts any data-dependent local Lipschitz or continuity estimate of the loss into robustness, and the paper derives its examples for the SVM, the Lasso, neural networks and PCA from it. The authors note (p. 404) that the resulting bound is weaker than VC-dimension bounds for linear predictors, since it depends exponentially on the dimension; the value of the example is the method, not the rate.
The results are proved in the paper, with short arguments. No machine-checked version of Theorem 6, Lemma 3 or Example 6 is known to exist. The formal work is to connect Mathlib's covering numbers to partitions of a set, to handle the / pairing on , and to state robustness so that later missions of this series (the generalization bound of Theorem 1, mission I) can consume it.
The constant in the robustness level depends on the training set through , while the partition in Definition 2 must be chosen before the training set is seen. A formalization that lets the cells depend on proves a much weaker, nearly empty statement, so the data dependence has to be carried entirely by and the cells must depend only on and . A cover by balls is not a partition, and the radius of the cover () and the closeness threshold in Theorem 6 () differ by the factor that the diameter of a cell requires. The Lipschitz estimate must bound a Lasso solution without any information beyond optimality, and the pairing between and is the one that makes the constant come out as printed; a Euclidean norm on either side gives a different constant.
ℝ × (Fin m → ℝ), a point being (z^{(y)}, z^{(x)}). Lean's norm on this product is the maximum of the absolute values of all coordinates, which is exactly . is written out as , since the default norm on Fin m → ℝ is the sup norm; is dotProduct w x.Z with IsCompact Z. Robustness (IsRobustOn) asks for cells C : Fin K → Set α that lie in Z, cover Z and are pairwise disjoint (empty cells allowed), chosen before the universally quantified training set; training sets are maps Fin n → α with all points in Z. No measurability is involved anywhere in this mission.Metric.coveringNumber at radius Real.toNNReal (γ / 2): closed balls, centres in Z (the metric space of Definition 1 is itself), value in ℕ∞, converted with toNat. Theorem 6 assumes its finiteness, as the paper does; without that hypothesis toNat would return and the statement would be false for nonempty Z. Example 6 does not assume it: it follows from compactness.A with ∀ s, IsLassoSolution c s (A s); it is not defined by a choice of minimizer. The regularization parameter satisfies , which the paper leaves implicit. The factor is a real division; for it is in Lean, the objective reduces to , and all statements remain true.Useful infrastructure beyond this mission: a lemma turning a finite cover of a set into a partition of it with cells of diameter at most twice the radius, and finiteness of Mathlib's internal covering number for compact sets. Contributions of either as separate theorems are welcome.
Classical generalization bounds control the gap between the expected loss of a learned hypothesis and its average loss on the training sample. The average is sensitive to outliers: when a non-negligible fraction of the sample is corrupted, the mean loss stops describing the quality of a solution, and quantile-type summaries such as the median become the natural measurement. Quantile losses have long been used for this reason in statistics and econometrics (Koenker and Bassett 1978; Huber 1981). The standard tools for proving generalization bounds — symmetrization, Rademacher and VC arguments — are built around the expected loss and do not extend to quantiles in any direct way.
Xu and Mannor (Mach Learn 86 (2012) 391–423) introduced algorithmic robustness: an algorithm is robust if the sample space can be partitioned into finitely many cells such that a test point falling in the same cell as a training point incurs a similar loss. Because the argument works cell by cell and needs no symmetrization, it transfers to loss functionals other than the mean. Sect. 4.1 of the paper uses this to bound the quantile value and the truncated mean of the testing error, and Sect. 5 relaxes robustness to pseudo robustness, which only asks the cell condition for a subset of the training samples. This mission formalizes the resulting Theorem 5 (p. 402), whose proof is Appendix C (pp. 415–418).
Let be a measurable sample space, a set of hypotheses and a loss, with each measurable. A training set consists of i.i.d. draws from a probability measure on ; its empirical distribution is . A learning algorithm is a map , and is the hypothesis learned from .
For a real random variable and a level , the -quantile value is
and, writing , the -truncated mean is
where the second term vanishes when . It is the contribution to of the leftmost fraction of the distribution. For a hypothesis and a measure on put and with .
The algorithm is pseudo robust, with and , if can be partitioned into disjoint sets , fixed in advance, such that every training set has a subset of samples with: whenever and lie in a common cell, . With this is -robustness.
Let and . If is pseudo robust, and , then with probability at least : whenever and ,
The constants are the paper's, and , , , , , and the algorithm are arbitrary.
The result. Theorem 5 shows that any pseudo-robust algorithm has a testing-error quantile and truncated mean that are bracketed by the empirical ones at levels shifted by , up to the robustness tolerance . The quantile of the testing error can therefore be estimated from training data for every algorithm to which the robustness framework applies — among them majority voting, SVMs, Lasso and principal component analysis (Sect. 6 of the paper) — without a separate complexity analysis of the loss class. The pseudo-robust form covers algorithms that are robust only away from a small set of training samples, which is the typical situation in the presence of outliers. The robust case is the paper's Theorem 2 (p. 400).
Formalizing it. The paper states Theorem 5 and proves it in Appendix C; no machine-checked proof exists. The appendix contains misprints (see Formalization scope) and the argument uses minimizers of the loss over each cell, which need not exist; a formal proof settles which steps are sound as written. The definitions of quantile value and truncated mean of a law on developed here are reusable beyond this mission.
The concentration step is the same as for the expected loss: on the event the empirical cell frequencies are close to the cell probabilities. The difficulty is converting this into a statement about quantiles. Quantile values are not linear in the distribution and are discontinuous in the level, so the triangle-inequality argument that bounds the mean-loss gap does not apply. Mass that moves between cells shifts every level of the quantile function, and the up to samples outside carry no guarantee at all, so an arbitrary fraction of the empirical law is uncontrolled. For the truncated mean this must be done for the whole lower tail up to level , not just at one point, and the atoms of the loss distribution (the second branch of the definition) have to be accounted for exactly.
XuMannorRobust.Quantile. is a type with a measurable space structure, an arbitrary type, a training set a function Fin n → Z, and the i.i.d. law the product measure Measure.pi (fun _ => μ).