Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Polynomial optimization asks for the minimum of a polynomial over a set cut out by polynomial inequalities. Lasserre's moment relaxation (Lasserre 2001) replaces the minimization over points by a minimization over probability measures on , and then over linear functionals on polynomials that satisfy semidefinite constraints. The bridge between measures and semidefinite constraints is Putinar's theorem (Putinar 1993): on a compact basic semialgebraic set with an Archimedean description, a linear functional comes from a measure exactly when it is nonnegative on the quadratic module of the constraints.
Many problems of practical size are invariant under a group of linear transformations: permutations of variables, sign changes, rotations of a polygon. Gatermann and Parrilo (2004) showed how such symmetry block-diagonalizes sums-of-squares programs. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 2013) carry the reduction to the moment side. Their first step, Theorem 3.2, is a symmetric version of Putinar's theorem: for invariant data it suffices to consider functionals that are themselves invariant, and these are characterized by positivity of symmetrized localizing forms. This mission formalizes that theorem.
Write . Let be a finite subgroup of . A matrix acts on points by and on polynomials by
the linear substitution . A polynomial is -invariant if for every .
Fix and the feasible set
Assumption 2.1 requires to be compact and some polynomial , with sums of squares , to have a compact superlevel set . Put .
A linear map is -linear if for all and all . Its symmetrized localizing forms are
For a Borel measure on , is its image under , and is -invariant if for all . A measure on is one with .
If the are -invariant and Assumption 2.1 holds, then for a -linear :
The result. Theorem 3.2 turns the moment relaxation of a -invariant problem into one over -linear functionals. Such a functional is determined by its values on the invariant ring , so its moment variables are indexed by a basis of invariants instead of all monomials (Example 3.3 of the paper: five variables instead of fifteen for on in degree 2). The block-diagonalized relaxations and the convergence result of §3 (Theorems 3.4–3.7) rest on it.
Formalizing it. The theorem is proved in the paper, modulo Putinar's theorem, which is cited. Neither Putinar's theorem nor any Archimedean Positivstellensatz is in Mathlib or on the platform. A complete formalization therefore needs (i) Putinar's theorem itself, in its dual moment form, and (ii) the determinacy of compactly supported finite measures by polynomial moments in several variables. Both are reusable well beyond this paper: every moment-SOS hierarchy result in the literature cites them.
The group-theoretic steps (milestones 2–4) are finite averaging and change of variables. The weight of the theorem sits in two analytic facts. The first is Putinar's theorem: nonnegativity on the quadratic module is an algebraic condition, and producing a measure from it requires the Archimedean hypothesis of Assumption 2.1 in an essential way; without that hypothesis the statement is false in general. The second is that the measure Putinar's theorem returns has to be shown -invariant. Equality of the polynomial moments of and does not by itself identify two measures; it does so here because both are finite and carried by a compact set, where polynomials are dense in the continuous functions. A further detail: Putinar's theorem is stated for normalized functionals, and Theorem 3.2 is not normalized, so the degenerate case must be shown to force .
Polynomials are MvPolynomial (Fin n) ℝ, points Fin n → ℝ, and a Subgroup (GL (Fin n) ℝ) with a Fintype instance. The action on polynomials is the linear substitution aeval, so is an arbitrary finite matrix group, not only a permutation group. Sums of squares are Mathlib's IsSumSq. "psd" for the symmetric form means for every polynomial , with no degree truncation; () is included. Measures live on the Borel σ-algebra of , is Measure.map along the continuous (hence measurable) map , and "measure on " is .
Committed conventions and disclosed readings:
Trivializing formalizations are ruled out: integrals are taken only against finite measures carried by a compact set, so no statement holds because a Bochner integral of a non-integrable function is ; positivity is through the forms on all of , not replaced by pointwise nonnegativity; and the invariance of is a conclusion of milestone 5, never a hypothesis.
Contributions welcome: Putinar's theorem (milestone 1) and multivariate moment determinacy on compact sets are the reusable infrastructure; the averaging milestones are a natural first entry point.
Distance covariance is a statistic for testing whether two random variables are independent. Székely, Rizzo and Bakirov introduced it for Euclidean spaces (Ann. Statist. 2007): the population distance covariance of a joint law is exactly when is a product measure, so a consistent test of independence follows. Lyons (arXiv:1106.5758) extended the statistic to arbitrary metric spaces and showed that the characterization of independence holds on a pair of metric spaces precisely when both have strong negative type (his Theorem 3.11 and Proposition 3.15). That makes strong negative type the property a statistician has to check before using distance covariance on a given space. Functional data, the main case in practice, live in Hilbert spaces.
This mission formalizes Lyons's Theorem 3.16: every separable Hilbert space is of strong negative type. Kosorok (2009, cited by Lyons) had asked whether the characterization of independence extends to Hilbert spaces.
Timeline.
Let be a separable metric space with its Borel -field. A Borel probability measure has a finite first moment if for some . For two such measures write and
the integral of against the square of the signed measure .
The space has negative type if, for all , all and all real with ,
By approximation, negative type gives for all probability measures with finite first moments. The space has strong negative type if it has negative type and only when . Strict negative type is the same condition restricted to finitely supported measures.
The proof works on and uses the following objects. is the law on of an IID standard normal sequence ; is Lebesgue measure on ; . For put . The Gaussian Crofton embedding sends to the function
on . For probability measures on , its barycenter at is the function .
The goal has no constants. Each milestone states a claim of the paper in the paper's strength.
The result. With Theorem 3.11, Theorem 3.16 shows that for random elements of separable Hilbert spaces, zero distance covariance is equivalent to independence. Distance-covariance tests are therefore consistent for curves, images and other functional data. It also yields Corollary 3.18: if is a separable metric space of negative type, then has strong negative type, so a test of independence is available on every separable space of negative type after a change of metric. Remark 3.17 shows that separability cannot simply be dropped: a non-separable Hilbert space is of strong negative type exactly when its dimension is a cardinal of measure zero.
The formalization. The theorem is proved, and to our knowledge no proof of it, or of negative type of Hilbert spaces, is machine-checked. A complete development needs four things:
Measure.infinitePi and gaussianReal;Each of these is reusable outside distance covariance: the first in Gaussian measure theory, the last whenever laws on sequence spaces are compared.
The first idea is to approximate. Euclidean spaces have strict negative type, finite-dimensional projections of a Hilbert space are Euclidean, and probability measures are limits of finitely supported ones. Approximation preserves the inequality , but it does not preserve the equality case. A limit of strictly negative quantities may be even though . Remark 3.3 of the paper exhibits a space of strict but not strong negative type, so this gap is real.
The second idea is to transport the finite-dimensional Crofton embedding, in which is the measure of half-spaces separating and . It fails because has no rotation-invariant Lebesgue measure on its half-spaces. The Gaussian measure replaces it. But is defined only -almost surely, and its exceptional set depends on . As a result, " almost everywhere" does not immediately give information for every direction and level . That passage from almost every to every is the step the 2018 Errata had to justify.
Lean conventions, all disclosed in the items:
InnerProductSpace ℝ H with CompleteSpace H, as Errata (viii) prescribes; a complex space has the distances of its realification. Separability is SecondCountableTopology, which matches the standing separability of Errata (i). is lp (fun _ : ℕ => ℝ) 2 with the Borel -field, declared in the Setting file because Mathlib supplies none.Trivializing encodings are ruled out:
Contributions are welcome on any milestone. The reduction of a general separable to (by an isometry onto a closed subspace) is not posed separately and belongs to the goal's proof. Mathlib's Measure.ext_of_charFun, for finite measures on complete second-countable real inner product spaces, is a natural tool for milestone 5. Separability of lp is not yet an instance in Mathlib.
Training a model in machine learning usually means minimizing a nonconvex function with first-order methods. Finding a global minimum of a general nonconvex function is NP-hard, so the classical guarantee for gradient descent (GD), , is weaker: with step size it reaches a point with within iterations, independently of the dimension (Nesterov, 1998). Such a point can be a saddle point. For many learning problems (matrix sensing and completion, phase retrieval, dictionary learning, tensor decomposition), every approximate second-order stationary point is an approximate global minimum, so an algorithm that avoids saddle points solves the problem.
Jin, Netrapalli, Ge, Kakade and Jordan (arXiv:1902.04811, J. ACM 2021) show that simple perturbed versions of GD and SGD find approximate second-order stationary points in essentially the number of iterations GD needs for first-order stationarity, up to polylogarithmic factors in the dimension. Their §5 gives a short, self-contained proof for a variant of perturbed GD (Algorithm 4). That proof is the subject of this mission.
Timeline:
Let , , with gradient and Hessian ; is the Euclidean norm on vectors and the spectral norm on matrices. Assumption A: is -gradient Lipschitz, , and -Hessian Lipschitz, . A point is an -second-order stationary point (-SOSP) if
Write and .
Algorithm 4 (Perturbed GD, Variant). With step size , radius , time interval and tolerance , start with . At iteration : if and , replace by with and set ; then . The parameters are those of Eq. (6):
where is a logarithmic factor, and .
For (which equals ) and every with
with probability at least over the perturbations,
The paper writes the count as with .
The result. Theorem 18 says that adding occasional small random perturbations to gradient descent costs only a polylogarithmic factor over the first-order rate and buys second-order stationarity. Combined with the landscape results above, it gives polynomial-time guarantees for gradient methods on those learning problems. Lemma 20, on its own, is a quantitative statement that strict saddle points are unstable under perturbed GD; Lemmas 21 and 22 are reusable tools for any analysis of first-order methods near saddle points.
Formalizing it. The results are proved in the paper; none of them is formalized. A formal development would give machine-checked versions of the descent lemma for Hessian-Lipschitz functions, the improve-or-localize lemma, the coupling argument and the probabilistic escape bound. It would also settle the issue disclosed under Formalization scope.
Lemmas 19 and 21 are short. The difficulty is in Lemma 22 and Lemma 20. The obvious approach, linearizing GD around the saddle and following the unstable eigendirection, fails because the stuck region (starting points that do not escape within steps) has no simple shape once is not quadratic. The coupling argument controls the difference of two runs instead. It needs an induction in which the non-quadratic error term stays below half of the leading term for all steps, with the constants of Eq. (6) used exactly (). Lemma 20 then turns a statement about pairs of points into a measure bound: a set whose every line parallel to meets it in a segment of length at most has volume at most times the -volume of the ball. In Lean this needs Fubini over a rotated coordinate system and measurability of the stuck region. Theorem 18 requires a probabilistic accounting over the whole run, under the product law of the perturbations.
is EuclideanSpace ℝ (Fin d) with . The Hessian is fderiv ℝ (gradient f) x, the derivative of the gradient map, with the operator norm. Statements about use the quadratic form: is "some unit has ", and is " for all ". is normalized Lebesgue measure on the open ball. Algorithm 4 is a deterministic function of the perturbation vectors, which have the product law on . The -th iterate is the point tested at the start of iteration , and "half of its iterations" counts . Probability statements bound the failure event from above.
The paper's is instantiated as the proof does:
A Hessian not tied to , an arbitrary unit vector in place of the bottom eigenvector in Lemma 22, a per-realization or existential statement in place of the product-law probability, or a vacuous would each trivialize the statements; none is used.
Disclosed gap. The proof of Theorem 18 (p. 16) bounds the number of perturbations by applying Lemma 20 at each one. Algorithm 4 also perturbs at points that are already -SOSPs, where Lemma 20 does not apply, and the iterations after such a perturbation are not counted. The goal is posed as printed; a solver who finds it false should report this in the discussion. The milestones do not depend on the gap.
Needed infrastructure: second-order Taylor bounds for Hessian-Lipschitz functions, symmetry of the Hessian and existence of a bottom eigenvector, volumes of Euclidean balls (in Mathlib through ), a Fubini-type slicing bound for sets of bounded width along a direction, and measurability of the GD iterates. The volume-ratio and slicing lemmas are reusable beyond this mission. Proofs of any milestone, and alternative proofs, are welcome.
In an aggregative game, each player's decision affects a common quantity, such as total production or total demand. An agent may be able to calculate its own preferred response while lacking direct access to that aggregate. Koshal, Nedić, and Shanbhag study how agents can estimate it by exchanging information only with neighbours on a communication graph. Their asynchronous gossip algorithm lets one randomly selected agent contact a neighbour at each tick; both agents update their estimates and decisions. The constant stepsize regime matters when agents cannot steadily reduce their stepsizes or want to keep responding to new information. It gives an error bound rather than exact convergence: the decisions remain near an equilibrium by an amount controlled by the step, the game, and the graph. The model and this bound are from Koshal, Nedić, and Shanbhag, 2016.
The same paper analyzes a synchronous scheme with diminishing steps and a gossip scheme with update-count steps. This mission isolates the constant-step case in §4.3, and targets the equal-probability, equal-stepsize display at the end of that section. It uses the paper's numbered Lemmas 2, 3, and 11 and relations (30), (31), (44), and (55) as intermediate targets. The restriction to the final special case is material: the argument printed for general player-specific steps and update probabilities has gaps in (53) and (54), while both problematic terms disappear when the steps and update probabilities are equal.
There are players, each choosing from a nonempty compact convex set . Write for feasible profiles and for feasible aggregates. Player has a component map , evaluated at its own decision and an aggregate argument. At a feasible profile , the game map is . An equilibrium target is the solution of the variational inequality : for every , . The paper derives this map from player payoff gradients under its Assumption 1; the present formalization starts with the component maps used by the algorithm.
A connected undirected graph lists the players that may exchange information. At tick , a uniform random player wakes and contacts a neighbour with probability . These draws are independent across ticks. Only the contacted pair average their current estimates to obtain , then project a step using onto . All agents update their estimate by ; for agents outside the pair this leaves both state variables unchanged. The mean estimate is . Lemma 2 identifies it with the mean decision. The update probability of player is . These definitions and the discrete gossip algorithm are given in §4.1 of the source.
Suppose is strongly monotone with modulus , every player uses the same positive step , and all update probabilities equal . Let bound the gradient evaluations as in Lemma 3. Let be a mean-square contraction constant for the gossip matrix , as in (30). If are the aggregate Lipschitz constants of Assumption 3 and bounds the diameter of each , put . Under the inherited assumptions of Proposition 4 and , the goal is existence and uniqueness of together with the last display on PDF page 29:
The milestones separately assert the unique VI solution, the aggregate identity, the bounded gradient evaluations, the contraction estimates (30)–(31), the one-step disagreement relation (44), Lemma 11's limiting disagreement bounds, and the equal-case recursion (55). Together they expose the quantities appearing in the target without weakening its constant or its dependence on and .
The bound separates the effects of the step, game regularity, number of agents, decision dimension, and communication quality. In particular, for fixed other parameters the right-hand side scales linearly in and worsens as approaches one. It is a quantitative guarantee for a decentralized procedure that sees neighbour messages instead of the exact aggregate. The VI existence and uniqueness target also identifies the equilibrium to which the error is measured. The paper proves the special case in its concluding bound on page 29, subject to the domain correction described below; it is not an unresolved research conjecture.
Formalizing the result produces a reusable interface for graph gossip matrices, random pair draws, relational Euclidean projection, and nonnegative expected disagreement. The intermediate contraction and tracking statements can support other constant-step distributed optimization arguments. The theorem declarations in this proposal are open Lean proof obligations; a successful local build checks their types and definitions, not the mathematical claims. Contributions that establish these obligations, sharpen a bound under the same model, or isolate reusable probability and projection results are in scope.
The estimates are coupled to both random pair averaging and the agents' decision changes, so graph connectivity alone does not state a numerical disagreement bound. The proof has to respect the actual distribution of waking and contacted agents when moving from a one-player inequality to an expected profile error. The printed general version illustrates the risk: Assumption 8 controls changes in at a fixed aggregate and therefore cannot justify (53), where the aggregate changes; (54) also replaces coefficients on signed terms by their minimum. The final equal-step, equal-probability case removes these two obstacles, but still requires the exact constants in Lemma 11 and the error recursion.
Players are indexed by Fin N, decisions use EuclideanSpace ℝ (Fin n), and a profile's squared Euclidean norm is the sum of squared block norms. Coordinate vectors across players also use a Euclidean norm; the ordinary Lean norm on Fin N → ℝ would be a supremum norm. The run starts from a deterministic feasible profile. This fixes the initial state before the independent discrete gossip draws, representing the source's Poisson-clock protocol at its tick times. A projection is a nearest-point relation on a nonempty compact convex set, with no arbitrary value on an empty set. Positive contact probabilities on all graph edges keep the connected graph active.
Assumption 1 is expressed through nonempty compact convex and continuity of on , the part of the payoff regularity used by the algorithm. Assumption 3 is stated for every aggregate argument in , a disclosed strengthening of its printed domain : can leave , as the paper's footnote on page 10 acknowledges. Assumption 8 remains a hypothesis inherited from Proposition 4 even though its term vanishes for equal steps. The constants , , and carry their defining bounds as hypotheses; the conclusion does not assume Lemma 11 or (55). Expected nonnegative quantities use extended-real lintegrals and an extended-real limit superior, preventing a failed Bochner integral from silently becoming zero. The formalization asserts existence of a VI solution, so an empty solution set cannot trivialize the goal.
Counting the proper -colorings of a graph, and sampling one uniformly at random, are basic problems of approximate counting with a long history in statistical physics, where proper colorings are the zero-temperature antiferromagnetic Potts model. On bipartite graphs these problems are tied to #BIS, the problem of approximately counting independent sets in a bipartite graph, whose complexity is unresolved. Galanis, Štefankovič, Vigoda and Yang showed that approximately counting proper -colorings is #BIS-hard on bipartite graphs of maximum degree whenever (SIAM J. Comput. 45(6), 2016). A positive result in that regime therefore has to use structure beyond bipartiteness and bounded degree.
Jenssen, Keevash and Perkins (SIAM J. Comput. 49(4) 2020) use expansion. Their Theorem 5 says that for there is an FPTAS and a polynomial-time sampler for proper -colorings on almost every -regular bipartite graph. This answered Conjecture 1 of the authors' SODA 2019 extended abstract. Liao, Lin, Lu and Mao (APPROX/RANDOM 2019) independently proved a similar result under a slightly stronger condition on . The organizing idea, that most colorings of a strongly expanding bipartite graph follow one of a few patterns, comes from the work of Peled and Spinka on rigidity of colorings of (arXiv:1808.03597).
This mission is the fourth of a series formalizing the four main results of that paper; it covers Theorem 5.
Fix integers , and . The vertex set is , two sides of vertices each (so ). is the finite set of labelled simple graphs on whose edges all join to and in which every vertex has degree . A property holds for almost every -regular bipartite graph if the fraction of graphs in having it tends to as .
For the vertex boundary is the set of vertices outside with a neighbour in , and . The graph is a bipartite -expander if for every inside one side with .
A proper -coloring is a map with on every edge; is their set and . A pattern is a pair of disjoint sets with ; there are of them. A coloring agrees with at if and , or and . For , is the set of proper colorings that disagree with at every vertex of and agree everywhere else.
joins two vertices at -distance at most . A set is little if . A polymer is a little set that is connected in ; is the set of polymers, and two polymers are compatible if their -distance exceeds . For a pattern , the weight and the polymer partition function are
the sum over all families of pairwise compatible polymers, the empty family included. Finally is an -relative approximation to if .
There is an absolute constant such that for all and , almost every -regular bipartite graph satisfies
and, for every pattern and every polymer , the Kotecký–Preiss condition
The constant is left existential, as in the paper.
In the order of the proof:
The goal is the whole mathematical content of Theorem 5. The paper's algorithm (its Theorem 8, adapted from Helmuth, Perkins and Regts, Algorithmic Pirogov–Sinai theory) takes exactly these two facts as input. Given the Kotecký–Preiss condition, the cluster expansion of each converges and truncating it gives the estimator; the reduction transfers the estimate to . With the goal proved, the remaining distance to the FPTAS is algorithmic bookkeeping, not combinatorics.
The result has been proved since 2019 and is not formalized anywhere. A formal proof would add a machine-checked polymer-model reduction for a spin system with exponentially many ground states, a reusable model of uniformly random regular bipartite graphs, and a checked instance of the "expansion implies few ground states" argument used throughout this literature.
The obvious first idea is a one-ground-state expansion, as for the hard-core model, where configurations are close to "all even" or "all odd". For colorings there are patterns. A coloring can lie close to several of them, so the reduction must show that the sets with little overlap only negligibly. That needs an inclusion–exclusion step whose error is exponentially small in . A second difficulty is the size of polymers: little sets are times larger than the sets of the hard-core analysis. Claim 30 is what keeps the union of compatible polymers from becoming a large set that the expansion no longer controls. Finally, the constants must be uniform in . The single condition has to cover the expansion lemma, the reduction and the Kotecký–Preiss estimate at once.
The FPTAS and the sampling algorithm are not formalized. Mathlib has no machine model in which "polynomial time" could be stated, and the running times carry unquantified constants. The goal is the mathematics the algorithm rests on: the reduction and the Kotecký–Preiss condition, with the paper's constants , and . Neither half may be dropped. Replacing by an existential error, or summing the Kotecký–Preiss condition over compatible rather than incompatible polymers, would make the goal trivial or wrong.
Conventions committed to in Lean:
Fin m ⊕ Fin m, and is the set of labelled -regular graphs with edges only between the two fixed sides. The paper does not fix a bipartition; this fixed-sides model is a disclosed choice, matching §5's .edist, so vertices in different components are at distance and never incompatible.log is the natural logarithm; the binomial estimate is used in nats.Added hypotheses:
The goal needs none of these, since its limit is in and its constant absorbs .
A complete development needs a counting theory of random regular bipartite graphs (for Lemma 23, through Bassalygo's expansion theorem), counts of connected sets in bounded-degree graphs, and inclusion–exclusion over patterns. The random-graph model and the polymer-model definitions are reusable across this series and beyond. Proofs of any milestone, and alternative routes to Lemma 23, are welcome.
Testing whether two random quantities are independent is one of the basic tasks of statistics. Classical correlation only detects linear dependence. Distance covariance, introduced by Székely, Rizzo and Bakirov (Ann. Statist. 2007) for random vectors in Euclidean spaces, is a dependence measure that vanishes exactly under independence. It only needs the distances between sample points, and its empirical version is a simple V-statistic. These properties made it a standard tool for nonparametric independence testing.
Lyons (Ann. Probab. 41 (2013), arXiv:1106.5758) asked in which metric spaces this characterization of independence survives. The answer is the class of metric spaces of strong negative type, which includes all separable Hilbert spaces. On such spaces, distance covariance gives a test of independence that is consistent against every alternative. This mission formalizes that result, Theorem 3.11 of the paper, together with the chain of results its proof rests on.
Timeline. Schoenberg (1937, 1938) characterized metric spaces of negative type by isometric embeddings of into Hilbert space. Székely, Rizzo and Bakirov (2007) defined distance covariance on and proved that it vanishes only under independence. Lyons (2013) extended the theory to general metric spaces and identified strong negative type as the exact condition. The Errata (Ann. Probab. 46 (2018), 2400–2405; included in arXiv:1106.5758, pp. 24–29) added a standing separability assumption and repaired a gap in Lemma 3.8. The Second Errata appeared in Ann. Probab. 49 (2021).
Let and be separable metric spaces with their Borel -fields. A finite measure on has a finite first moment if for some (equivalently every) . For such define
For a probability measure on whose marginals and have finite first moments, the distance covariance is
is a product measure if .
has negative type if for all , all points and all real weights with . For finite measures with finite first moments, is the integral of against . On spaces of negative type for probability measures . The space has strong negative type if, in addition, only when .
An embedding is a map into a real Hilbert space with . Its barycenter map is . The tensor embedding takes values in the Hilbert tensor product . denotes the finite signed measures whose variation has finite first moment. denotes those on the product whose variation has marginals of finite first moment.
If and have strong negative type and the marginals of the probability measure have finite first moments, then
The converse, that a product measure has (p. 5), is included as a companion statement.
The result. Theorem 3.11 makes the empirical distance covariance a consistent test of independence against all alternatives on any pair of separable metric spaces of strong negative type. Examples are separable Hilbert spaces and their subsets, and every space of negative type after replacing by , . Its companion, Proposition 3.15 (a separate mission of this series), shows that strong negative type is exactly the right hypothesis. Proposition 3.7 also identifies distance covariance with Brownian covariance and with the original Euclidean definition, through specific choices of embedding.
Formalizing it. The result is proved, with the gap in Lemma 3.8 closed by the Errata (2018). No part of it has a machine-checked proof that we know of. A formalization needs barycenters of Hilbert-space-valued maps against measures, the Hilbert tensor product of two real Hilbert spaces, and Schoenberg's embedding theorem. None of these is in Mathlib in this form, and all are reusable well beyond distance covariance.
The obvious route reads as "the barycenters of and of coincide in " and concludes by injectivity. Strong negative type only gives injectivity of on probability measures, while is a signed measure on a product space. Getting from injectivity on single factors to injectivity on of the product is where the original proof had a gap: an auxiliary signed measure built from was not shown to have a finite first moment. The errata version changes the embeddings so that this can be done. Two smaller obstacles are integrability (the definition of is meaningful only by Lemma 2.1) and the construction of the Hilbert space in Schoenberg's theorem.
All spaces are Lean metric spaces with their Borel -fields and SecondCountableTopology. This is the separability the author adds in Errata (i), which makes measurable on the product. Measures are Mathlib Measures. A probability on has marginals θ.map Prod.fst and θ.map Prod.snd. "Product measure" means equals the product of these marginals. Hilbert spaces are real (Errata (viii)). Existential embeddings land in , which suffices for separable spaces. The Hilbert tensor product is the completion of the algebraic tensor product with its inner product. is defined by its bilinear expansion. Injectivity on and is stated for pairs of finite measures, which is equivalent to injectivity on signed measures via the Jordan decomposition.
Every integral here is a Bochner integral, which is for a non-integrable integrand. Each statement therefore carries the finite-first-moment hypotheses of the paper, and integrability itself is a milestone. Negative type and strong negative type are defined by (3.1) and by the condition on , not through an embedding or a barycenter map, so Schoenberg's theorem and Proposition 3.1 are not definitional. A statement with a "product measure" whose factors are free, or with dcov defined without the moment hypotheses, would be a different and trivializable theorem.
Welcome contributions: barycenter calculus for Hilbert-valued integrals, tensor-product integrals, Schoenberg's theorem, and proofs of any milestone.
Most training objectives in machine learning are smooth and nonconvex, and they are minimized by stochastic gradient descent (SGD) and its variants. For nonconvex the classical guarantee is convergence to an -first-order stationary point, : Ghadimi and Lan (arXiv:1309.5549) showed that SGD reaches one in stochastic gradient queries, independently of the dimension. A first-order stationary point may be a saddle point, however, and for many problems (matrix sensing and completion, phase retrieval, tensor decomposition, dictionary learning) every second-order stationary point is a global minimum. For these problems, a guarantee for second-order stationary points is a guarantee of global optimality.
Timeline:
Let be bounded below with , and write . Assumption A: is -gradient Lipschitz, , and -Hessian Lipschitz, in operator norm. A point is an -second-order stationary point if
The algorithm sees only a stochastic gradient with . Assumption B asks that and that the error is norm-subGaussian: for . The optional Assumption C asks that each is -Lipschitz. The two cases combine into
with when Assumption C is not used.
Perturbed SGD (PSGD, Algorithm 2) draws and an independent Gaussian at every step and updates
For a log factor , the proof uses the parameters of Eq. (8): , , , , and runs for iterations. The goal states that there is an absolute constant such that, for with ,
The proof's two engines, in the paper's order: the concentration inequalities for norm-subGaussian martingale differences (Lemmas 36–39), the descent lemma (Lemma 23), improve-or-localize (Lemma 24), the coupling analysis around a saddle point (Lemmas 27–31), escape from a saddle point (Lemma 25), and the two claims that bound the number of iterates with large gradient and the number near saddle points.
The theorem shows that adding isotropic Gaussian noise to SGD suffices to find second-order stationary points at essentially the cost SGD pays for first-order points: queries when Assumption C holds (matching Ghadimi–Lan up to logarithms) and in general. Combined with landscape results such as "every second-order stationary point is a global minimum", it yields global convergence of a simple first-order stochastic method from arbitrary initialization for the problems listed above.
The result is proved on paper. As far as is known, none of it is machine-checked: neither the escape-from-saddle-point argument by coupling sequences nor the vector-valued concentration inequalities of Appendix C, whose proofs the paper defers to a separate technical note (arXiv:1902.03736). Formalizing them yields reusable norm-subGaussian martingale bounds in , a checked version of the coupling technique that later saddle-escape analyses reuse, and a check of every constant hidden in the paper's .
The descent lemma alone cannot rule out that the iterates stall near a strict saddle point, where the gradient is small and the negative curvature is invisible to first-order information. The obvious argument, which says that the perturbation has a component along the negative eigendirection and that component grows, fails as stated: the stochastic gradient noise, the Hessian's variation along the trajectory, and the perturbation all interact over steps. Controlling these interactions needs concentration bounds for vector-valued martingales whose scale is itself random (Lemma 37), which have no counterpart in Mathlib. Bounding how often the iterates can return to saddle regions over the whole run is a separate difficulty, since the times at which the iterates are near a saddle point are random.
is EuclideanSpace ℝ (Fin d) with ; the Hessian is the derivative of the gradient map, and is the Rayleigh-quotient infimum over the unit sphere. The randomness is the infinite product measure of the pairs , and the PSGD run is a deterministic function of it. Conventions committed to:
A formalization that keeps the printed "" in Assumption B, or allows in the tail bound, makes every statement vacuous or trivial; both are excluded. Infrastructure needed: norm-subGaussian vectors and their martingale concentration (reusable well beyond this mission), Gaussian anti-concentration in one direction, and stopping-time arguments for the Markov chain of PSGD. Contributions to any milestone, and to the concentration layer in particular, are welcome.
An online retailer that serves many kinds of customers must decide, for each arriving customer, which handful of products to display. Showing too many items is impossible (screen space, shelf space), and which items sell depends on who is looking. The retailer does not know the customers' preferences in advance and learns them only from the choices customers make among the items shown. This is dynamic assortment personalization: an online learning problem in which every display both earns revenue and produces data.
Kallus and Udell (arXiv:1610.05604) study the regime in which the number of customer types and the number of items are both large, so that learning each type's preferences separately would take on the order of interactions. Their premise is that preferences across types are governed by a few latent features, which makes the matrix of preference parameters approximately low rank. The non-contextual problem — one customer type, multinomial-logit choice — was studied by Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013); the paper extends it to many types and proposes an explore-then-exploit policy whose estimates come from nuclear-norm regularized maximum likelihood, the standard convex surrogate for low rank used in matrix completion.
There are customer types and items. Each type has a revenue vector (row of ; is the expected revenue when type buys item ) and a preference vector (row of the unknown matrix ). Types arrive independently from an unknown distribution in the simplex .
For an assortment and a parameter vector , the multinomial-logit (MNL) choice probability of item is
and the customer buys nothing with probability . The expected revenue of is , and is the set of maximizers of over . The revenue gap is the optimal revenue minus the best revenue of a non-optimal assortment.
In round a customer of type arrives, the retailer offers with , and the customer chooses from the MNL law with parameters . The regret (Definition 1) of a policy after rounds is the expected revenue of the -greedy policy, which always offers an element of , minus the expected revenue of the policy.
Algorithm 2, , keeps a sample of exploration observations. At round , if it explores: it offers a uniformly random subset of size exactly and records . Otherwise it exploits: it offers an element of , where is a solution of
with the average negative log-likelihood (4) of the sample, the nuclear norm and the largest absolute entry.
Let , for all , , and , . With
for every selection of from the solutions of (5) and of the exploited assortment,
From the printed proof of Theorem 6 (pp. 47–48): the Lipschitz bound ; the revenue bound ; the comparison of optimal sets; the stability of the optimal set; and the count of exploration rounds. From the deterministic part of the recovery analysis (Sec. 8): Lemma 2 (a quadratic lower bound on the Bregman divergence of ), Lemma 5 (an upper bound from the regularized objective) and Lemma 6 (the nuclear-norm error is controlled by times the Frobenius error and the spectral tail of ).
Theorem 6 is the paper's guarantee that a policy exploiting low-rank structure pays regret of order rather than the order that the paper shows (Theorem 5) for policies treating each type separately. The intermediate results are reusable: the Lipschitz bounds for MNL choice probabilities and revenue apply to any MNL assortment policy that plugs in estimated parameters, and Lemmas 2, 5 and 6 are the deterministic core of nuclear-norm regularized estimation for a likelihood that is not an entrywise loss.
To the best of current knowledge none of these results has a machine-checked proof. The mission produces a formal model of a contextual MNL assortment process with an adaptive policy, its trajectory law and regret, together with formal statements and proofs of the Lipschitz and stability facts that any explore-then-exploit analysis of MNL assortment needs. Several printed statements needed correction (see Formalization scope); machine-checked proofs settle the corrected forms.
The goal is a statement about the law of a -round adaptive process: the offered set at round depends on the whole past through the exploration test and through an estimate defined only as some minimizer of (5). Any argument must handle this dependence exactly, for every admissible selection of minimizer and of optimal assortment, rather than for one convenient choice.
The constants are explicit and the horizon is restricted, so the inequality has to hold with the paper's normalization exactly as stated, including the box constraint of (5). The printed proof routes through the paper's high-probability recovery bound (Theorem 3), which is believed false as printed and is not part of this mission, so a proof cannot simply cite it. Lemmas 5 and 6 require Hölder's inequality for the spectral/nuclear pairing and a decomposition of the error relative to the singular subspaces of ; Lemma 2 requires a curvature estimate for the log-sum-exp function uniformly on the box.
The source is the arXiv preprint arXiv:1610.05604, an unstamped PDF pinned by sha256 2b010481…216a; its printed page numbers equal the PDF page numbers.
Types and items are Fin m and Fin n, 0-based; the no-purchase option is none. Matrices are MatrixCompletion.RealMatrix m n; the nuclear, spectral and Frobenius norms, the Frobenius inner product and are the published MatrixCompletion definitions, and is the published ChoiceCDLP.MNL.mnlObjective with weights and no-purchase weight . All probabilities and expectations are finite sums over histories in Fin T → Fin m × Finset (Fin n) × Option (Fin n). Regret is Definition 1 after the tower property: the greedy policy earns per round and Algorithm 2 earns in expectation. The gap condition is stated as "every non-optimal assortment of size at most earns at most the optimum minus ", since itself is undefined when every assortment is optimal.
Added hypotheses and corrections, each disclosed in the item's note:
Theorem 3 (static recovery) and Lemma 4 (gradient concentration) are not posed: both are believed false as printed. Lemmas 3 and 7 are not posed either.
A trivializing formalization is ruled out: the estimator is any minimizer of (5) with its box constraint, the exploited set is any optimal assortment for the estimate, and both are quantified universally; exploration draws uniformly from subsets of size exactly ; and the benchmark is the -greedy policy under the same arrival law. Fixing the estimator to , dropping the box, or comparing to the best fixed assortment would change the theorem.
Contributions welcome: proofs of the milestones (the Lipschitz lemmas are calculus on the softmax function; Lemmas 5 and 6 are matrix analysis reusable for other nuclear-norm estimators), a proof that the definition of is the gradient of , and a proof that the history weights form a probability distribution.
A retailer that personalizes the set of products it shows to each customer needs to know who its customers are. In the low-rank multinomial-logit model of Kallus and Udell, Dynamic Assortment Personalization in High Dimensions (arXiv:1610.05604), every arriving customer belongs to one of customer types, and the type of each arrival is drawn independently from an unknown type distribution . Planning a non-personalized assortment, or weighting the per-type preference estimates, requires an estimate of from the observed types. When is large (types may be fine-grained customer profiles), the question is how many observations are needed before that estimate is reliable, and in which norm.
Theorem 4 of the paper answers this for the simplest estimator, the empirical frequencies, with an explicit, non-asymptotic bound in every norm, . The bound has two regimes: one that is good when the sample size is only slightly larger than , and one that is good when is large compared with .
Customer types are labelled . The type distribution is a vector in the probability simplex
The observation model (Sec. 3.2, p. 13) consists of records , : the type of the -th customer, the item the customer chose, and the assortment offered. The types are independent and identically distributed with . The items and assortments play no role for the type distribution.
The empirical type frequencies (Sec. 3.2.1, p. 14) are
For and the norm is , and ; the convention at is used throughout.
The proof works with the empirical Rademacher complexity of the sample: with the indicator vector of the -th type,
For every and , with probability at least ,
The goal keeps the paper's constants and its single statement over all , including .
The first term of the minimum shows that is consistent in every norm as soon as grows faster than , and gives -consistency in , i.e. in total variation. A coordinatewise argument alone cannot give this: for it yields a bound that does not vanish unless grows faster than . The second term is the sharper one in the regime , for instance in , where it gives the familiar rate. In the paper the estimate of enters non-personalized assortment planning, where the expected revenue of an assortment is averaged over types.
On the formalization side, the result is proved in the paper; nothing about it is open. As far as a search of the Prove2Me catalog shows, no machine-checked version of this statement, or of an concentration bound for empirical frequencies with these constants, exists. A complete development would also supply, in finite and elementary form, a coordinatewise Hoeffding bound for binomial proportions and an deviation bound for categorical samples, both reusable well beyond this mission.
The second term is a union bound and a binomial tail bound. The first term is where the work is. The obvious route, bounding each coordinate separately and summing, costs a factor in the norm and gives a useless rate when is comparable to . The proof instead treats as the supremum of an empirical process over the unit ball, controls its mean through the Rademacher complexity (where the absolute value of a sum of random signs must be bounded by ), and then needs concentration of the supremum around its mean with constants good enough to produce the stated and . The paper's p. 44 citation of a symmetrization result states it with the empirical rather than the expected complexity, so that step has to be redone with care rather than transcribed.
2b0104810fa9d656f2b79f8a44f791b2a3da388f3f6707564f4619da2050216a. Its printed page numbers equal the PDF page numbers.Fin m and draws Fin N, both 0-based. A sample is a map x : Fin N → Fin m.stdSimplex), which forces , and , added because is undefined for an empty sample. The milestones' tail bounds assume , which the paper leaves implicit. For the events are certain and the printed bounds can be smaller than .PiLp norm on for , with an extended nonnegative real; and use an exponent defined as at and otherwise. is the natural logarithm.Adversarial training asks a classifier to work even after an input has been changed within a prescribed perturbation budget. Tsipras, Santurkar, Engstrom, Turner, and Mądry studied why the classifier that performs best on ordinary inputs can behave very differently under these changes. Their explicit model separates one reliably predictive feature from many individually weak features. It lets the same distribution support a highly accurate ordinary classifier and a less accurate but robust classifier Tsipras et al., §2.1–2.2. This mission formalizes the paper's comparison for soft-margin support vector machines at the population level.
The model is relevant to anyone using a training objective as a proxy for performance under perturbations. Its conclusion concerns the optimizer of an expected loss, not the effect of a particular finite sample or optimization algorithm. That distinction makes the example a direct statement about the objectives being optimized.
A label is drawn uniformly from . An input has real coordinates. Its first coordinate, , equals with probability and with probability , where . Conditional on , each of the remaining coordinates is an independent Gaussian variable with mean and variance one, independently of . Thus is a moderately reliable feature while the other coordinates can be weak predictors individually. These are exactly the ingredients of distribution in equation (3) Tsipras et al., p. 4.
For a weight vector , the linear classifier assigns the sign of . Its standard accuracy is the probability that for a fresh pair from . Its robust accuracy at radius is the probability that this equality holds for every perturbation with . Both accuracies average the two labels with probability each.
The soft-margin SVM objective combines expected hinge loss and quadratic regularization:
The distributional adversarial objective replaces the hinge loss for each observed pair by its maximum over the ball before taking the expectation:
This order follows equation (2), the distributional adversarial loss Tsipras et al., pp. 2, 16–18.
The goal is Theorem 2.2 Tsipras et al., p. 6. Under , , and , a global minimizer of whose squared Euclidean norm is one satisfies
For a global minimizer of with and either or , the target is
The milestone list follows Appendix D's stated claims: the Gaussian law of the pooled weak feature, Lemmas D.1–D.5, and the displayed adversarial objective identity. The lemmas give nonstrict and bounds where the theorem states strict inequalities Tsipras et al., pp. 16–18.
The result gives a concrete distribution on which the ordinary population hinge objective favors weak features enough to achieve near-perfect standard accuracy while remaining vulnerable to a small coordinatewise perturbation. The adversarial objective instead selects a classifier using the first feature, whose standard and robust accuracies are both . It therefore distinguishes the behavior of the two objectives even without sampling error or a particular training algorithm.
The paper proves these claims informally. The Lean items here compile as definitions and theorem statements with open proofs; they are not yet machine-checked proofs. A completed development would supply the Gaussian probability estimates, optimizer properties, and accuracy calculations needed to close the statements. The law of a pooled Gaussian vector and the relation between perturbations and the weight norm are reusable beyond this example.
The first weak feature alone carries little information, but their normalized sum has a strong Gaussian signal. Consequently, reasoning about one coordinate at a time does not determine what the ordinary SVM minimizer predicts. The theorem also concerns every global minimizer with the stipulated norm, so testing a convenient weight vector does not settle it. The stated strict accuracy constants require quantitative Gaussian tails and an optimizer comparison at the specified and thresholds. In the adversarial part, the conclusion about accuracy requires more than proving that weak-feature weights vanish: the remaining first-feature coefficient must have the correct sign and be nonzero.
Lean represents an input as a function on Fin (d+1); index zero is the paper's , and index i.succ is . The function norm is the sup norm, so is exactly the ball. Squared norm and norm of a weight vector are written as and . The conditional law is a product of the two-point first-feature law and the independent Gaussian weak-feature law, assembled into one input vector. GaussianReal's variance argument is one. Labels and predictions are real , and a zero score is assigned . The tie has probability zero for the nondegenerate classifiers in the theorem.
The robust event can be outside the Borel sigma algebra. Its measure in Lean is an outer measure, agreeing with probability under completion. Gaussian affine hinge functions are integrable; the adversarial hinge has the explicit finite closed form supplied by a milestone when the radius is nonnegative. The supremum is over exactly the admissible perturbations. The mission does not reduce the target to a chosen classifier or assume any of the milestone conclusions as goal hypotheses.
Several hypotheses make implicit conditions or a necessary correction explicit. The condition prevents from becoming Lean's default value at zero. Appendix D assumes that has been tuned so an ordinary global minimizer has ; that is represented directly. Evaluation radii are nonnegative, so their balls are not empty. The upper bound is needed for the second claim: for larger training radii the zero vector may minimize the adversarial objective and its constant classifier has accuracy , contrary to the printed sentence when . At that constant classifier has accuracy , so the case is kept for every training radius. This correction is disclosed rather than silently attributing it to the paper. Appendix D's displayed maximum outside expectation also differs from equation (2); the formalization follows (2), whose per-sample maximum has the displayed closed form. The paper's proof specializes to although Theorem 2.2 states ; the target retains the printed theorem's range.
The hard-core model assigns weight to independent vertex sets of a graph. Its partition function counts those sets when the activity is one and weights larger sets more heavily when the activity increases. Counting independent sets on bipartite graphs is a standard benchmark for approximate counting: the general problem is difficult, while random regular graphs have additional expansion that can make approximation possible. Jenssen, Keevash and Perkins prove an approximation and sampling theorem for almost every sufficiently high degree regular bipartite graph when the activity is above an explicit threshold Jenssen–Keevash–Perkins, Theorem 2.
The question is specific to a random graph model. It does not assert the same conclusion for every regular bipartite graph. The authors use a criterion attributed to Bassalygo to show that almost every graph in the model has the expansion needed by their argument Jenssen–Keevash–Perkins, Theorem 22 and Lemma 23. Liao, Lin, Lu and Mao independently obtained related counting results under somewhat stronger parameter conditions Liao–Lin–Lu–Mao, 2019.
Let be a simple graph with two labelled sides and , each containing vertices, and let every vertex have degree . An independent set contains no adjacent pair. For activity , the hard-core partition function is
For a vertex set , its vertex boundary consists of vertices outside with a neighbor in . The graph is a bipartite -expander when every subset of either side with size at most has boundary of size at least times its size. The expansion parameters used here are and . A set is tiny when its size is at most Jenssen–Keevash–Perkins, Definition 21 and §4.4.
The graph joins distinct vertices whose distance in is at most two. On either side, a polymer is a nonempty, tiny, -connected vertex set. Two polymers on the same side are compatible if every pair of their vertices is more than distance two apart in . A polymer has weight . Summing products of weights over mutually compatible polymer families gives the partition functions and Jenssen–Keevash–Perkins, §§4.1, 4.4.
“Almost every” means that, for fixed , the fraction of labelled -regular bipartite graphs satisfying a property tends to one as tends to infinity. The random graph is chosen uniformly from graphs on the two fixed sides Jenssen–Keevash–Perkins, p. 3.
The first target is the authors' expansion premise: for all sufficiently large , almost every graph is a bipartite -expander. The main target combines two deterministic claims on almost every such graph. For every , write and
First, is an -relative approximation in the paper's exponential convention:
Second, each of the two polymer models obeys the Kotecký–Preiss condition with decay :
The same graph event must support every activity above the threshold; the activity quantifier is inside the limiting probability. The intermediate targets are Bassalygo's entropy criterion, the high probability expansion lemma, the tiny-side lemma for independent sets, the approximation lemma at its weaker activity threshold, a published binomial-entropy estimate, and the per-vertex polymer sum bound Jenssen–Keevash–Perkins, Theorem 22, Lemmas 23–25 and §4.5.
The reduction expresses a weighted independent-set count through two finite polymer partition functions whose weights decay under the same expansion condition. The KP bound supplies the convergence condition used by the paper's general polymer approximation theorem. Together these are the mathematical inputs to its algorithmic Theorem 2 Jenssen–Keevash–Perkins, Theorems 2, 8.
A formal proof would make the expansion assumptions, distance convention, graph probability limit, and error normalization explicit. The target is a formalization of a published result, not an open conjecture. The proposal contains statements and definitions; their proofs remain to be supplied. The binomial estimate is already machine checked on Prove2Me and is included by reference.
An independent set can occupy vertices on both sides of a bipartite graph. Merely taking one side as the dominant phase double counts sets that are sparse on both sides. The tiny-side lemma and the polymer decomposition identify and control that overlap. The random graph step also requires an expansion estimate strong enough to apply to every small subset of either side, rather than only to a typical subset Jenssen–Keevash–Perkins, §§4.4–4.5.
Lean uses finite simple graphs on , with the left and right summands serving as the odd and even sides. This fixes a labelled bipartition for the uniform random graph model. Distances use extended natural graph distance, so vertices in different components have infinite distance. Polymer families include the empty family, and graph connectivity excludes the empty polymer. Sizes are natural numbers; thresholds involving logarithms are real inequalities. Binary entropy in the cited expansion theorem is measured in bits, while Mathlib's binary entropy is converted from natural units. The approximation uses exponential relative error exactly as in Definition 10 of the paper.
The FPTAS, sampling algorithm, and running-time assertion are outside this mission because Mathlib has no matching machine and cost model. The goal formalizes both the partition-function reduction and its KP condition, the mathematical inputs consumed by the paper's algorithm theorem. It quantifies over all activities above the threshold within the almost-every event, preventing a separate favorable graph set for each activity. The fixed-sides model and the explicit domain of Bassalygo's entropy formula are disclosed representation choices. The tiny-side milestone (Lemma 24) carries a graph-size threshold depending on the degree: as printed, for every graph size, it fails on small dense graphs (the complete bipartite graph minus disjoint complete blocks), and the main result uses it only as the graph size grows. Reusable contributions include finite graph expansion lemmas, polymer partition-function identities, and bounds on connected vertex sets.
In an aggregative game, each player's cost depends on its own decision and on the sum of all players' decisions. That form appears in resource sharing, production, and network games: a player may know its own choice while lacking a central feed of the aggregate. A distributed algorithm therefore has to estimate the aggregate through local communication as it updates decisions. Koshal, Nedić, and Shanbhag study this setting and give both synchronous and gossip schemes in Distributed Algorithms for Aggregative Games on Graphs. This mission concerns their asynchronous scheme, in which a random pair communicates at each tick.
The question is whether irregular, local updates still find the game's equilibrium when no agent knows in advance how often it will be selected. Each agent uses its own update count to set its step length. The paper's Proposition 3 states almost-sure convergence under strict monotonicity, compact strategy sets, and a connected graph. The result is a convergence claim about the complete random process, including who wakes, whom they contact, which estimate they exchange, and which projected step they take.
There are agents. Agent chooses , with nonempty, compact, and convex. A strategy profile is in , and its aggregate is . The map is the player's first-order response when its own decision is and its aggregate argument is . The game map is . A solution of the variational inequality is feasible and satisfies
The paper obtains from differentiable convex player costs, making VI solutions Nash equilibria. The formal statements take as the primitive map used by the algorithm. Strict monotonicity means for different feasible profiles . Along with continuity and compact convex strategy sets, it makes the VI solution unique. The paper's Assumptions 1–3 also impose a uniform Lipschitz bound on how changes with .
Agents occupy a connected, undirected graph. At a discrete tick , a uniformly selected agent contacts a neighbour with probability on every edge. The ordered pairs are independent across ticks. Each agent maintains an aggregate estimate ; the selected pair average their estimates to form . Those agents take a projected step using and then add their decision change to the estimate. Other agents retain their decisions and estimates. Initially . The number counts agent 's updates through tick , and its step length at an update is . Equations (23)–(29) of the paper define these operations.
Under Assumptions 1–3 and connectedness of the gossip graph, Proposition 3 asserts that there is a unique solving and that the generated process satisfies
The goal includes existence and uniqueness of , rather than conditioning convergence on a possibly nonexistent solution. Its random draws have the rate-one-clock law: .
The five milestones record the VI's unique solution from the proof of Proposition 1, conservation of the agents' average estimate in Lemma 2, the almost-sure stepsize bounds of Lemma 7, their summability consequences in Corollary 1, and the mean-square gossip contraction in relations (30)–(31). They cover the equilibrium, tracking, step length, and network-mixing parts of the claim. Their source wording, indices, and PDF pages are attached to the mission items.
The result shows that a shared aggregate can be learned well enough through pairwise, random exchanges to reach the same equilibrium characterized by the centralized VI. Update counts permit agents to choose diminishing steps without a common iteration clock or a schedule ensuring equal participation on each finite interval. Connectedness and positive contact probabilities ensure every graph edge can carry information. The convergence assertion is almost sure, so it concerns individual sample paths outside a null set, rather than merely an average error.
Formalizing the result would connect finite graph gossip, random update counts, projected VI iteration, and almost-sure convergence in one reusable development. The paper proves Proposition 3; this mission supplies an open machine-checked target, not a claim that the result is unresolved mathematically. A proof would need honest probability statements for the draw law and summability and a projection interface that does not assign arbitrary values on empty sets. The VI existence and uniqueness milestone can also serve other compact, strictly monotone games.
Pairwise averaging preserves the mean estimate, but it does not make each agent's estimate equal to that mean at every step. A projected decision change immediately perturbs the local estimate again. The selected agents and their step lengths also depend on the same update history, so deterministic simultaneous-update arguments do not directly apply. The paper controls this interaction using update-count asymptotics, contraction of the random gossip matrix, and almost-sure summability. None of those conclusions follows from connectedness alone if a nominal edge has zero contact probability.
Lean represents each decision in EuclideanSpace ℝ (Fin n) and profiles as functions on Fin N. The aggregate is a finite sum. A projection is the relation saying that the selected point lies in its set and minimizes Euclidean distance, rather than a total function with an arbitrary output on an empty set. The profile topology used for convergence is the finite product topology. For vectors indexed by agents, relations (30)–(31) use the explicit Euclidean coordinate norm; the default norm of Fin N → ℝ is a sup norm.
The continuous-time Poisson clocks are encoded through their induced independent discrete tick pairs and exact joint law. Initial decisions are fixed and feasible. The source allows random initial decisions; the formal goal covers every deterministic start. This restriction is recorded because the paper's stated random initialization would require an explicit independence relation with future clock draws. Tick indices start at zero in Lean; a selected agent has , so the value assigned to never drives an update. The positive-time series and bounds still begin at .
The paper gives the Lipschitz condition on aggregate arguments only in the feasible aggregate set . Its algorithm can evaluate outside that set, as its own footnote acknowledges. This development explicitly extends that condition to all of to make those evaluations controlled. The change is substantive and disclosed on each affected item; the preprint's Lemma 3 proof contains the corresponding domain gap. The goal assumes neither the stepsize estimates nor the network contraction nor convergence of the estimate errors; they remain mathematical work. Further contributions may formalize the omitted intermediate lemmas, or refine the initialization and domain assumptions while preserving a meaningful statement.
Distributionally robust optimization handles an uncertain parameter whose distribution is only partly known. A decision must satisfy an expectation constraint for every distribution in an ambiguity set, the set of distributions consistent with the available information. Wiesemann, Kuhn and Sim (Optimization Online preprint 3757, 2013; Operations Research 62(6), 2014, doi:10.1287/opre.2014.1314) introduce a standardized ambiguity set. Its members are joint distributions of and auxiliary random vectors , constrained by expectation conditions and by probability bounds on conic confidence sets. Worst-case expectation constraints over such a set have tractable conic reformulations. The practical question is which kinds of distributional information this format can express. A set over describes information about through its -marginals, so the precise claim is that some set of distributions of equals the projection of a standardized set.
Section 3 of the paper settles this question for several common descriptors of dispersion. One of them is the absolute mean spread, the gap between the mean of a random variable above a threshold and its mean below it. Levi, Perakis and Uichanco used it to describe demand uncertainty in data-driven newsvendor models (Oper. Res. 63(6), 2015). The paper notes that, unlike variance or coefficient-of-variation bounds, spread information "can no longer be constructed via straightforward application of Theorem 5", its general lifting result for conic-representable moment bounds. Proposition 2 provides a dedicated lifting instead.
Fix , a threshold , a spread budget and a probability level . For a probability distribution on under which has a finite mean, write
The absolute mean spread of at is . The target set (spreadSet) consists of the with whose spread is at most .
The lifted ambiguity set (liftedSpreadSet) consists of the probability distributions of on with and , satisfying almost surely
The marginal is the law of under , and .
For the companion result, the Huber loss (8) is if and otherwise, for .
The page states the conclusion as for a given in the right-hand set. The set identity is the content, and it is the goal.
The milestones follow the two inclusions of the proof (pp. 40–41).
Combining them gives
and hence is contained in the target set. 2. For in the target set, and satisfy
Consequently equals the spread, and the target set is contained in . 3. A companion, Proposition 3, assertion 3 (p. 21): for and , the distributions with are exactly the -marginals of a lifted set on with auxiliary variables .
The proposition places absolute mean spread information inside the paper's standardized framework. Every result proved there for standardized sets therefore applies to spread-constrained ambiguity sets. The lifted set of Proposition 2 violates the paper's nesting condition (N), so Theorem 1's exact reformulation does not apply. Instead, Theorem 3 and Observation 1 give conservative approximations, which here are linear programs (p. 18). The Huber companion does the same for an expected Huber loss bound, a robust alternative to a variance bound.
Both results are proved in the paper. Neither has a machine-checked proof that this mission is aware of. A formalization adds three things: a checked equality of the two sets, with every integrability and positivity side condition made explicit; reusable lemmas on elementary conditional means of a scalar projection; and a check of the companion. The companion's printed proof contains an incorrect intermediate identity (see Difficulty), although the proposition itself holds.
The obvious reading of the inclusion target is "the constraint on bounds the spread pointwise". That reading fails, because the spread is a ratio of expectations over two complementary events, and and are not determined by . Only their difference is fixed, almost surely. The bound must hold for every coupling of with that respects the constraints. The reverse inclusion needs an explicit lift of an arbitrary . The lift has to meet the moment condition exactly, not just as an inequality. The paper leaves that step implicit.
In Lean the main friction is measure-theoretic bookkeeping: integrability of the auxiliary coordinates (which is derived, not assumed), set integrals over the two half-spaces, and push-forwards along the first projection. In the Huber companion, the identity the proof states for the minimized integrand is false in general: with and the left side is and the right side is . The inclusion needs a different pointwise inequality.
Fin nP → ℝ, with written f ⬝ᵥ z. The lifted outcome space is (Fin nP → ℝ) × (ℝ × ℝ × ℝ), and are the projections uOf, vOf, wOf. The Huber lift uses Fin 5 → ℝ with components .μ.map Prod.fst. Both theorems are stated as set identities between Set (Measure _).condMeanGe, condMeanLt). σ-algebra conditioning is not used. Both events have probability or , both positive because , so no division by zero occurs.Prod.fst are reusable beyond this mission. Proofs of the individual milestones are welcome, as are reusable lemmas on lifts of the form .A Markov decision process (MDP) is evaluated with a transition kernel that, in practice, is estimated from data. The expected total reward of a policy can be very sensitive to small errors in that estimate (Mannor, Simester, Sun and Tsitsiklis, 2007). Robust MDPs address this by letting the kernel range over an ambiguity set and optimizing the worst-case expected reward. Iyengar (2005) and Nilim and El Ghaoui (2005) showed that when the ambiguity set is (s, a)-rectangular (the transition law of each state–action pair varies independently of all others), the robust problem is solved by a robust Bellman recursion and a deterministic stationary policy is optimal.
Wiesemann, Kuhn and Rustem (Robust Markov Decision Processes, Mathematics of Operations Research 38(1), 2013) widen this to s-rectangular ambiguity sets, in which the transition laws of different actions in the same state may be coupled. Their Theorem 4.1 shows that robust policy improvement over such sets is still solved by a robust Bellman fixed point, but the optimal stationary policy may need to randomize. This mission formalizes that theorem and the chain of results its proof uses.
Timeline:
States form a finite set , actions a finite set . Choosing action in state and moving to pays a reward ; rewards are discounted by and the initial state has a known law in the probability simplex .
The uncertain parameter lies in
with symmetric negative semidefinite, bounded and containing a Slater point. Transition probabilities are affine in the parameter, for . The ambiguity set is the set of kernels , . It is s-rectangular if , where collects the blocks of members of : the parameter may be chosen separately in each state.
A stationary randomized policy assigns to each state a distribution over actions. It induces the Markov reward process
and the reward to-go . The worst-case expected total reward of is .
Two robust Bellman maps on carry the results:
In Lean these are phiEval and phiImprove, in the namespace WiesemannRMDP.SRect.
For an s-rectangular , has a unique fixed point , per-state maximizers exist, and the glued policy together with the constant function attains
Theorem 4.1 reduces robust policy improvement over s-rectangular sets to computing the fixed point of one map on , each evaluation of which is a finite convex program; the paper derives a polynomial-time method from it (Corollary 4.2). It also shows that the optimal policy is stationary but generally randomized, which separates s-rectangular from (s, a)-rectangular robust MDPs. Theorem 3.2 is the evaluation counterpart and is used again when the paper compares s-rectangular and general ambiguity sets (Proposition 3.10).
The results are proved in the paper; none is formalized. On the platform, the (s, a)-rectangular analogue with deterministic policies and costs (Nilim and El Ghaoui) and a related robust linear-programming characterization in another model (Derman, Geist and Mannor) exist, but neither covers coupled actions, randomized policies or rewards depending on the next state. A complete development would give machine-checked robust value iteration for s-rectangular sets and reusable facts on the reward to-go of a finite Markov reward process.
The obvious argument copies the nominal proof: the optimum of the constant- restriction is the fixed point , so the constant function is optimal. That only solves the restriction to constant ; the problems optimize over all continuous reward to-go functions , and showing that no non-constant does better is where s-rectangularity enters. Without it the claim is false: the paper's Example 3.11 gives a non-rectangular set where the constant bound is strictly below the worst-case reward. A second subtlety is that depends on only through the row , which is what lets per-state maximizers be assembled into a single policy; the maximizers are in general not deterministic.
States and actions are finite nonempty types; policies are functions satisfying the published IsPolicy, and the simplex condition on is the published IsTransitionKernel. and are built from the published InducedTransition and InducedReward. The model is a structure Model with the standing assumptions in Model.Standing. The reward to-go is defined by the series , not as the solution of the evaluation equation, so Proposition 3.1 (b) is not definitional. The minimum over and the maximum over are infima and suprema over subtypes, attained under the standing assumptions; the objective is used only for continuous on , and where arbitrary appear (the middle line of (10)) the infimum is taken in the extended reals. Inequalities on are componentwise; contractions are with respect to the sup norm. The paper's in (3b) carries the index , as elsewhere in the paper.
A statement that compares the fixed point only with constant reward to-go functions, or that takes and as hypotheses satisfying the conclusion, is not Theorem 4.1; the goal asserts existence and uniqueness of , existence of the maximizers, and optimality against every policy and every continuous feasible .
Useful infrastructure: Neumann series for times a row-stochastic matrix, continuity of infima over compact parameter sets, and contraction properties of min/max Bellman operators. Proofs of the milestones, and of nonvacuity of richer instances, are welcome.
High-frequency prices move by discrete ticks, and successive moves are strongly correlated: an upward tick tends to be followed by a downward one. Bacry, Delattre, Hoffmann and Muzy (BDHM12, BDHM13b) proposed to model the upward and downward price jumps as the two components of a bidimensional Hawkes process, a pair of counting processes in which every event raises the rate of future events of both kinds. In this model the price is the difference , and its microstructure features (discreteness, negative autocorrelation of increments) are built in. Under the stability condition on the excitation kernels, the price rescaled over long horizons converges to a Brownian motion with a constant volatility BDHM12.
Empirical calibrations of Hawkes models on financial data, however, find kernel norms (branching ratios) very close to the critical value (HBB13, FS12). Jaisson and Rosenbaum (JR15) study exactly this regime: a sequence of models whose stability condition is almost violated, observed over a time horizon of the right order. Their Theorem 3.1 shows that the rescaled price then converges to a Heston-type process, a Brownian motion time-changed by a Cox–Ingersoll–Ross (CIR) variance. This gives a microstructural foundation for stochastic volatility models of Heston type Hes93, which are standard in option pricing.
Fix and two nonnegative measurable kernels on with , finite mean , nonzero on a set of positive measure, and differentiable with bounded integrable derivatives (Assumption 3). Let be positive numbers with , , and set .
For each observation horizon (along a sequence ), the bidimensional Hawkes process is a pair of counting processes started at , with unit jumps and no common jumps, whose intensities with respect to their joint history are
"Intensity" means: for and every event of the history up to time , .
The renormalized price is
Two further conditions fix the regime. Display (3): for some . Assumption 4: with and , there is with for all and all . Write and .
Under (3) and Assumptions 3 and 4, converges in law, for the Skorohod topology on , to the process defined by
with a two-dimensional Brownian motion. The goal asserts that this system has a solution and that converges in law to the -coordinate of every solution.
In the order of the proof (§4.4):
The theorem identifies the scaling limit of a microstructure price model at near-criticality, and the limit is not a Brownian motion with constant volatility but a stochastic-volatility process: the variance is itself a CIR diffusion driven by a Brownian motion independent of the one driving the price. It explains, from the order-flow level, why Heston-type dynamics arise at macroscopic scales, and it identifies which features of the microscopic excitation survive in the macroscopic volatility and price diffusion.
The result is proved in the paper; nothing about it is open. It has not been formalized. A machine-checked version would formalize a complete scaling-limit argument for point processes: the resolvent calculus of Hawkes processes, the martingale central limit theorem for pure-jump martingales, joint Skorohod convergence, and the identification of the limit of stochastic integrals. Each of these is reusable well beyond this paper.
The price is a difference of two processes whose sum is nearly unstable. One might expect the CIR limit of the one-dimensional case (Theorem 2.2 of the same paper, applied to ) to give the result directly. It does not: the price is driven by the difference of the martingales, with a volatility that depends on the sum of the intensities, and the limit requires the joint convergence of the variance proxy and the price martingale , with one time change for both coordinates. Marginal convergence of each coordinate is not enough to pass to the limit in . Joint convergence in turn needs the cross-bracket of and to vanish, which depends on the imbalance being negligible (Lemma 4.12), and the zero set of the CIR process having Lebesgue measure zero. The signed kernel produces a signed resolvent, for which the positivity arguments of the one-dimensional case are unavailable.
EthierKurtz.SolvesBrownianSDE, IsStandardBrownian, state space ): strong solutions, global in time, restricted to . "The process defined by" the system is encoded as existence of a solution plus convergence to every solution.The formalization rules out the trivializing readings: the Hawkes predicate follows p. 5 clause by clause and is satisfied by a pair of independent Poisson processes when , so it is not vacuous; the kernels are , not ; the limit is pinned by its equation, its coefficients and its initial value, not "some process"; and the convergence is in the Skorohod topology, not of finite-dimensional laws only.
Needed infrastructure: convolution powers and resolvents on , pathwise Stieltjes integrals against counting processes, the martingale property of compensated Hawkes processes, a martingale functional CLT for pure-jump martingales, Skorohod-topology tools on , and convergence of stochastic integrals under joint convergence. The one-dimensional CIR limit (mission 2 of this series) is used inside Lemma 4.15; the definitions are restated here. The martingale functional CLT used for Lemma 4.14 is Theorem VIII.3.11 of Jacod and Shiryaev (1987), as cited in JR15. Contributions to any milestone, or to reusable lemmas they need, are welcome.
In an aggregative game, a player's cost depends on its own decision and on a summary of all players' decisions. An electricity producer, for example, may choose its output while the market price depends on total output. When players communicate only with neighbours, each player must estimate the aggregate before making an update. Koshal, Nedić, and Shanbhag study this setting with communication links that can change over time, and prove convergence of a synchronous algorithm using only local messages Koshal–Nedić–Shanbhag, 2016.
The mission targets Proposition 2 of the pinned preprint. It treats the algorithm itself as a mathematical object: the claim must hold for every sequence satisfying its graph, weight, stepsize, and projected update conditions. The result addresses a concrete information constraint. Players cannot read the true aggregate while the algorithm runs; they have individual estimates constructed from their neighbours' estimates.
There are players. Player chooses , with each nonempty, compact, and convex. Write , , and . The attainable aggregate set is . A map gives the component of the game's gradient field at player 's decision and aggregate argument . Its profile field is .
The target point is a solution of the variational inequality : it belongs to and satisfies
The paper obtains this field from differentiable player costs. The convergence theorem is stated for the field and the VI, while the connection to a Nash equilibrium is established separately in Proposition 1 Koshal–Nedić–Shanbhag, pp. 4–6. Strict monotonicity of on says that whenever feasible . Together with compactness and continuity, this yields the unique VI solution used in the target.
At time , player keeps a decision and an estimate of the average decision, initially . A matrix mixes estimates along an undirected communication graph. Each row and column of sums to one; non-neighbours receive zero weight, while every neighbour and the player itself receive at least . The union of the communication graphs over any consecutive times is connected. The local aligned estimate and the two updates are
Here denotes Euclidean nearest-point projection. The stepsizes decrease, their sum diverges to , and their squares are summable. The paper calls these graph, weight, and stepsize conditions Assumptions 4–6 Koshal–Nedić–Shanbhag, pp. 7–9.
The first milestone makes the existence and uniqueness statement used in the proof explicit:
The other milestones follow the paper's numbered Lemmas 1–4 and 6 and its displayed relations (19)–(20). They state that the mean of the players' estimates is the true mean decision, that the matrix products mix geometrically, that the relevant gradients and estimate errors are controlled, and that the weighted estimate errors have finite total sum Koshal–Nedić–Shanbhag, pp. 9–14.
For every synchronous run under Assumptions 1–6, the goal asserts both a unique VI solution and convergence of the whole decision sequence:
The target is a qualitative convergence result. It does not prescribe a convergence rate for Koshal–Nedić–Shanbhag, Proposition 2, p. 13.
The theorem says that local estimate mixing is sufficient for every player's projected gradient decision to approach the same equilibrium, even when the communication graph changes, provided connectivity recurs within a fixed window. The result gives a precise condition under which access to the aggregate can be replaced by neighbour messages. Its milestone on the matrix products supplies an explicit estimate for how information spreads; the summability milestones connect that estimate to the optimization error.
The paper contains a mathematical proof, but this mission's Lean declarations are open statements with sorry bodies. A completed formalization would turn the paper's VI existence, mixing, projection, and convergence arguments into individually reusable verified results. The general product-set VI and nearest-point relation are separated from the paper's particular synchronous model so later developments can use them without importing graph-specific definitions.
The obvious single-agent projected-gradient argument assumes each update uses . Here it uses instead, and the estimate errors depend on a changing product of weight matrices. Connectivity of each individual graph is not assumed, so a one-step contraction statement is unavailable. The proof must control time-varying mixing and accumulate its error without losing convergence. Strict monotonicity then identifies the limit, but it does not by itself bound the transient disagreement.
The printed hypotheses also leave a domain issue. The algorithm evaluates at , which need not lie in ; the paper's footnote on p. 10 acknowledges that may leave its apparent feasible aggregate region. The printed Lipschitz condition covers only , so the target explicitly requires it for all aggregate arguments. The printed Lemma 3 also gives only unit column sums, which allow arbitrarily large negative and positive entries; its mission item carries the graph and positive-weight assumptions needed for the bound. These changes are recorded in the item notes and in the source analysis Koshal–Nedić–Shanbhag, pp. 7–10.
Decisions live in EuclideanSpace ℝ (Fin n) and players in Fin N; Lean player zero is the paper's player one. A profile is a finite function, and its squared Euclidean norm is the sum of the squared norms of its blocks. The conclusion uses the equivalent finite product topology. The variational inequality's inner product is written as a sum over players, avoiding the sup norm carried by a Lean function space. Graphs are undirected SimpleGraphs; self-neighbours are included explicitly. The product places the newest matrix on the left. Projection is a relation requiring a genuine nearest point in , rather than a total function with an arbitrary value on an empty set.
The target fixes , , and nonempty . It uses continuity of on as the field-level part of Assumption 1, and the extended all- form of Assumption 3 stated above. The stepsize sum is represented by partial sums tending to , and by summability. Existence and uniqueness are part of the goal conclusion; no bound on the gradients or summability of the estimate error is assumed by the goal. A complete development needs reusable compact-product VI existence, Euclidean projection facts, matrix-product mixing for changing graphs, finite-dimensional norm estimates, and real-series convergence. Contributions proving these milestones and their intermediate lemmas are welcome.
The price of anarchy (POA) of a game measures how much selfish behaviour costs: it is the ratio between the largest cost of an equilibrium and the cost of an optimal outcome, for a nonnegative objective such as the sum of the players' costs. Since Koutsoupias and Papadimitriou (1999) and Roughgarden and Tardos (2002), POA bounds have been proved for routing, scheduling, facility location, auctions and many other models, mostly for pure Nash equilibria.
Pure Nash equilibria need not exist, are hard to compute in general, and are not what players running learning algorithms converge to. A bound that holds only at pure Nash equilibria therefore says little about realized play. Roughgarden's paper (J. ACM 62(5), 2015; conference version STOC 2009) observes that most known POA proofs follow one template, the smoothness argument, and proves that any bound obtained this way extends automatically to much broader equilibrium concepts. This mission formalizes the static half of that result: the extension to coarse correlated equilibria (Theorem 3.2) and to their approximate versions (Theorem 4.1).
Timeline:
A cost-minimization game has finitely many players . Player chooses a strategy from an arbitrary set ; an outcome is a vector , and player pays a real cost . Write for the outcome in which player switches to and the others stay put. The joint cost is , assumed nonnegative.
An outcome is a pure Nash equilibrium if for every and . For it is an -Nash equilibrium if .
A coarse correlated equilibrium is a probability distribution over outcomes with
and an -coarse correlated equilibrium satisfies the same with a factor on the right. Every pure Nash, mixed Nash and correlated equilibrium is a coarse correlated equilibrium, and coarse correlated equilibria are exactly the limits of play in which every player has vanishing external regret.
The game is -smooth if for every two outcomes
The robust price of anarchy is .
For every game with robust POA , every coarse correlated equilibrium and every outcome ,
Theorem 3.2 says that the robust POA of a game bounds the expected cost of every coarse correlated equilibrium, which contains every other equilibrium concept in the hierarchy. Combined with the companion result for no-regret sequences (Theorem 3.3, mission II of this series), it makes POA bounds meaningful for learning dynamics: whenever players use no-regret algorithms, their average cost is within the robust POA of optimal. For linear congestion games, which are -smooth, it yields the bound for all coarse correlated equilibria at once. Theorem 4.1 shows that the bounds degrade gracefully when the equilibrium condition holds only approximately, which covers equilibria computed to finite accuracy.
The results are proved in the paper; their proofs are short. No machine-checked version is known to exist. The mission's value is a reusable, platform-wide definition layer for cost-minimization games, smoothness, the robust POA and the equilibrium hierarchy, on which later results can be stated: the bicriteria bounds of §4.2, the tightness theorem for congestion games (mission III), and smoothness bounds for specific models such as auctions, routing and scheduling.
The mathematics is linear: it uses only linearity of expectation and one rearrangement. The difficulty lies in the encoding. The robust POA is an infimum over a set that may be empty (then on the page) and need not be attained. Passing from the fixed-pair bound to the infimum uses . Theorem 4.1's printed side condition is meaningless when and reverses its meaning when . Each of these must be handled so that the formal statement is neither false nor vacuous.
Players form a finite type with decidable equality, and strategy sets are arbitrary types with no finiteness assumed. Outcomes are dependent functions, and the deviation is Function.update s i s'ᵢ. Costs are real-valued, and are unconstrained reals except . Probability distributions are finitely supported weight functions that are nonnegative with total mass . Expectations are therefore finite sums with no integrability side conditions. This covers all finite games and all mixed and correlated equilibria of finite games, but not distributions with infinite support.
The robust POA is an extended-real (EReal) infimum over the smoothness pairs with , so it is when no such pair exists, and the goal compares the expected cost with in EReal. The goal carries two explicit hypotheses:
Without the second, a game with no smoothness pair and would be claimed to have expected cost at most (EReal sets ), which the page does not assert. A formalization in which the distribution may have total mass , or in which is an infimum over all pairs rather than over the smoothness pairs with , trivializes or falsifies the goal, and is ruled out by the definitions.
In Theorem 4.1 and the -Nash bound:
The -coarse correlated equilibrium is the extension of (15) that the paper says is "defined in the same way" as -Nash equilibria (p. 15). Remark 4.4 writes out the payoff analogue.
Claim (3)–(5) and the -Nash bound keep the paper's hypotheses and optimality of , although the inequalities hold without them. Example 4.2 is not posed: its printed bound should read .
Contributions welcome:
Nesterov’s accelerated gradient method is a discrete procedure for minimizing a smooth convex function. Its iterates use both a gradient step and a momentum term, so the position at the next step depends on recent motion as well as on the current gradient. Su, Boyd, and Candès study a continuous-time model of that behavior: a trajectory whose acceleration is driven by the negative gradient and opposed by a time-dependent damping term. The model is useful only if its prescribed starting point determines an actual trajectory. The first theorem of the paper supplies that guarantee for the damping coefficient . Su, Boyd, and Candès, 2015, Theorem 1.
The coefficient is undefined at the stated initial time . Standard results for differential equations with a continuous right-hand side at the initial time therefore cannot be applied directly. The existence and uniqueness claim is substantive: it makes the trajectory used in the paper’s later rate and restart theorems a defined mathematical object, including its behavior at the singular endpoint. The source proves the result; this mission asks for a machine-checked formalization of its statement and its supporting appendix lemmas.
Fix a dimension , a starting point , and a real-valued objective . For a constant , the paper’s class consists of functions that are convex, continuously differentiable, and have an -Lipschitz gradient:
The larger class is the union of these classes over positive . In particular, the objective need not be strongly convex and need not have a minimizer for this mission.
A solution is a position and its velocity , starting at and , that satisfy equation (3) at every positive time:
The trajectory is continuously differentiable through the initial endpoint, with a right derivative there, and twice continuously differentiable for . The paper also uses a smoothed equation indexed by , replacing with . Its solutions are denoted , and its velocity-growth quantity is
For local uniqueness, two solutions on are compared using . These quantities appear in the appendix lemmas and are represented by pointwise bounds in the formal statements.
The goal is Theorem 1, the well-posedness of equation (3). For every and every , it asserts both existence of a global trajectory with the regularity above and uniqueness on nonnegative time:
The milestone list follows the numbered statements in Appendix A. Lemma 16 controls the change in along a smoothed trajectory. Lemmas 15 and 17 bound on the initial smoothing interval and beyond it, with the explicit thresholds and . Lemma 18 states that the family of smoothed trajectories with is uniformly bounded and equicontinuous on . Lemma 14 gives existence for equation (3). Lemma 20 bounds the difference between gradients along two local solutions, and Lemma 19 gives uniqueness in a neighborhood of zero. The goal and milestones preserve the source’s domains, constants, and order of dependence.
Theorem 1 permits the rest of the paper to refer to “the” trajectory of equation (3) from a specified initial point. In particular, statements about its objective value, energy, and restarts need an actual trajectory, and uniqueness makes those statements independent of a choice of solution. The appendix estimates also provide reusable facts about this singular second-order equation: quantitative control of smoothed velocities and local agreement at the singular time.
The paper proves Theorem 1 and the seven listed lemmas on pp. 6 and 28–32. This mission does not claim a new analytical result. Its output would be checked Lean statements and, when solvers finish the proofs, a machine-checked development of the singular initial-value problem. The formal definitions are shared by all items in this mission; the lemmas can be reused in later formal work on accelerated gradient trajectories. No machine-checked proof of these particular statements is being claimed by the draft proposal.
The initial time is precisely where the damping has no finite value. Treating the problem as an ordinary initial-value problem at leaves the differential equation undefined there. Imposing the equation at after Lean’s total division would instead change it: Lean assigns a value to division by zero, while the paper imposes equation (3) only for . The demanded derivative at zero is one-sided, and control of the behavior as is part of the result.
The smoothed equations are regular at zero, but a statement about each smoothed trajectory does not by itself give a solution of the original singular equation. The appendix’s uniform bounds and equicontinuity are formulated on a common compact interval for a specified sequence of smoothing parameters. Uniqueness has a second boundary issue: local agreement near zero must be connected to ordinary uniqueness at positive time to obtain agreement for every .
The Lean space is , with its Euclidean norm; is arbitrary. The objective class includes convexity, regularity, a positive Lipschitz constant, and a globally Lipschitz gradient. A solution is encoded as a pair , so is witnessed by derivative assertions rather than by a total derivative operator. The initial conditions specify , , a right derivative of , and right continuity of . The differential equation and ordinary derivatives are required only at positive times. For the smoothed equation, is part of the solution predicate.
These choices rule out a vacuous solution predicate and prevent division by zero from defining a different equation. Lean functions are represented on all real times, but the source’s solution lives on ; uniqueness is therefore equality on that half-line. At negative times the formal representatives are unrestricted. The paper’s real suprema and are expressed as bounds on every member of their defining ranges, so an empty or unbounded real supremum cannot acquire a misleading default value. Every denominator in Lemmas 15 and 17 has the paper’s strict threshold in its hypotheses.
A full proof development needs ordinary differential equation existence and uniqueness at positive time, continuity and derivative facts at the right endpoint, and compactness of uniformly bounded equicontinuous families. The definitions of the objective class and solution predicates, the quantitative estimates, and the local uniqueness statement are welcome solver contributions. The target is the source theorem with its stated hypotheses and conclusion; a special objective, a weakened time interval, or a proof by an impossible hypothesis does not close it.
In online convex optimization, a learner makes a prediction before seeing the next loss. A standard regret guarantee often depends on a learning rate chosen using the size of the comparator that will be assessed later. That comparator is unknown during play. Chapter 13 of Orabona's textbook uses coin betting to obtain a bound that adapts to every comparator while the algorithm uses only its initial wealth and a bound on the observed subgradients. The coordinate-wise form allows the guarantee to reflect a comparator whose important coordinates differ greatly in size.
The motivating task is deterministic. An adversary may choose convex losses over successive rounds, and the performance measure compares the learner's cumulative loss with the loss of a single fixed vector. The algorithm is allowed to know the coordinate bound and its initial wealth parameter ; it does not know the final comparator or a suitable learning rate for it. The capstone is Theorem 13.9, p. 215, the chapter's coordinate-wise Krichevsky–Trofimov result.
There are rounds, numbered , in a space . In round the learner outputs , pays , and then receives a subgradient of the loss at . A subgradient supports the loss everywhere: for every . Each coordinate obeys . For a fixed comparator , regret is
The underlying KT bettor begins with wealth . Given coin outcomes , it wagers a fraction of its wealth before outcome arrives. Its signed wager is , and . The denominator is , including the first round, when the past sum and the wager are zero. Algorithm 13.1, p. 208 defines this update.
For optimization, Algorithm 13.3, p. 215 applies a separate KT update to every coordinate. With , the prediction is fixed by past gradients and past predictions:
This is the algorithm studied in the target theorem. A run includes the update and an admissible subgradient at each round; it is not an arbitrary sequence of predictions satisfying a bound after the fact.
The main target records both inequalities in Theorem 13.9. For every comparator ,
The milestone path consists of three statements drawn directly from the chapter: the gamma-potential one-step inequality (13.1), the continuous-coin wealth guarantee of Theorem 13.4, and the one-dimensional KT regret display in §13.2.1. The first controls the change in the betting potential, the second relates that potential to final wealth, and the third is the scalar guarantee used by the coordinate-wise theorem. All three retain the printed constants and the source's one-based indexing.
The first inequality charges each comparator coordinate according to its own magnitude. The second expresses the result using familiar and norms. Both apply to the same run without choosing a new algorithm for a new . At , the bound is , showing directly the cost of the initial-wealth choice. For a sparse or uneven comparator, the coordinate sum can be more informative than a bound that uses only the largest coordinate.
The mathematical results are proved in the cited textbook. This mission supplies Lean statements for those results; the theorem files are proof targets and do not yet contain machine-checked proofs. A completed development would connect the betting potential, the one-dimensional optimization reduction, and the coordinate aggregation through reusable lemmas. Its definition layer can also serve later formalizations of coin-betting algorithms with other wealth potentials.
The prediction uses a changing wager fraction determined by the previous outcomes. A direct fixed-fraction calculation does not describe that sequence of wagers. The chapter instead identifies a gamma-function potential that can be compared with the changing wealth at every round. For continuous coin outcomes, the potential must satisfy an inequality for every real , including interior values rather than only the binary endpoints.
The optimization guarantee adds another boundary: a lower bound on betting wealth must become an upper bound on regret for every real comparator. The desired expression has a logarithm, a square root, and the exact factor inside it. The coordinate-wise result must preserve the scalar constant in every coordinate and then justify the second inequality involving . These are the places where a weaker or altered constant would change the target.
Lean represents as functions Fin d → ℝ; its function norm is the sup norm, while the quantity is the explicit sum . The theorem assumes , , , and . These make the finite-dimensional setting nonempty and the printed quotients and logarithms operate on their intended domains. Time index zero is unused. All sums over rounds use .
Losses are real-valued and subdifferentiable on the whole space, as in Algorithm 13.3. The run records full-space subgradients selected at the learner's predictions and their coordinate bounds. This selected-gradient condition is sufficient for the printed regret inequalities; global boundedness of every possible subgradient is a stronger convention used in the one-dimensional prose. The gamma potential is a separate definition with Real.Gamma; its arguments are positive on the domains used by the wealth theorem. The bettor's wealth is a finite product of its exact per-round returns.
The formalization must keep the explicit update in the run predicate. Allowing to depend on the current , or replacing the update by a generic betting rule, would no longer state Algorithm 13.3's guarantee. Contributions are welcome on the gamma-potential inequality, the wealth bound, the one-dimensional regret bound, and the final coordinate aggregation. The supporting results should retain the chapter's constants and handle the first round and zero-valued coin outcomes.
A portfolio manager chooses fractions of current wealth to place in several stocks before seeing that day’s market gains. The gains need not follow a statistical model: a sequence may be selected adversarially, with some stocks losing all value on a given day. A useful benchmark is the best constantly rebalanced portfolio, which holds the same fractions each day but trades at the end of every round to restore them. Its fixed allocation is an active strategy, and it can grow even when buying and holding each individual stock does not. Chapter 10 of Orabona’s online learning text studies guarantees against this benchmark without imposing a positive lower bound or a finite upper bound on nonzero market gains.
The chapter presents a universal portfolio: an allocation determined by a prior distribution over all fixed portfolios and reweighted according to their wealth so far. The mission focuses on the uniform-prior part of Theorem 10.1. It asks for a worst-case logarithmic regret guarantee against every fixed comparator and every admissible market sequence. This is a deterministic guarantee; no distributional assumption about the market enters its statement.
There are stocks and rounds. In round , the market supplies a vector of nonnegative gains. A portfolio is , the simplex of vectors with nonnegative coordinates summing to one. If one unit is invested initially and the allocation stays fixed, its wealth after rounds is
A sequential strategy chooses before seeing , and has wealth . The quantity of interest is the difference between the logarithms of benchmark wealth and sequential wealth. A fixed portfolio can have zero wealth when all the stocks it holds have a zero gain on some day; its log wealth is then in the mathematical convention of the book.
Algorithm 10.1 begins with a prior on the simplex. Before round , it gives each fixed portfolio weight proportional to its wealth , and chooses the resulting mean allocation:
For this mission, is the uniform probability measure on the simplex. It is represented by Lebesgue measure in the first coordinates, scaled by ; the final coordinate is one minus their sum. This explicit density fixes what “uniform” means and prevents the prior from being chosen to suit a particular market sequence.
The goal is the uniform-prior case of Theorem 10.1. With the notation above, for every fixed portfolio of positive wealth,
The goal also asserts , so the algorithm’s logarithmic wealth is defined. The first inequality gives an exact finite-horizon combinatorial bound; the second displays its logarithmic dependence on for fixed . The book also states a Dirichlet prior bound in the same theorem. That companion branch is not among this proposal’s draft items; its gamma-function normalization and integral identities would require a separate audited definition layer. The fixed series title follows the chapter plan, while the goal and milestone list specify the precise scope delivered here.
The attack path records four source statements. Lemma 10.5 bounds a ratio of nonnegative sums by the largest component ratio. Lemma 10.6 reduces a universal portfolio’s wealth ratio to a maximum over sequences of single-stock choices. Theorem 10.4 bounds the size of a type class, the set of sequences with the same empirical fractions of symbols. Equation (10.5) computes the monomial integral under the uniform simplex prior. These statements are from the chapter’s proof of Theorem 10.1; the equation is referred to as an exercise in Problem 10.3.
The theorem ensures that the uniform-prior strategy keeps its log wealth within of the best constantly rebalanced portfolio, while making no bounded-gain assumption. In particular, a stock may have gain zero on one day or a very large gain on another. The guarantee is pathwise: it applies to the realized market vectors, regardless of how they were chosen. For a fixed number of stocks, dividing regret by therefore gives a vanishing average shortfall in log wealth.
The mathematical result is already proved in the cited text. This mission’s work is to give its exact algorithm, prior measure, combinatorial objects, and finite-horizon constants machine-checked statements and then proofs. The density-based prior, finite type classes, and simplex monomial integrals can also be reused in online aggregation and universal coding developments. The draft statements currently have Lean placeholders for proofs; a successful submission will still require solvers to close them.
Applying a generic online convex optimization bound to the loss runs into unbounded gradients when a chosen portfolio has small gain. A bound based on one global Lipschitz constant cannot cover the market sequences allowed here. The integral strategy creates a different obstacle: its denominator must be positive at every round, including histories with zero gains for many fixed portfolios. Its uniform prior is a measure on a -dimensional simplex embedded in , so ambient -dimensional volume would give it mass zero. A proof must work with the intrinsic coordinate measure and its normalization. The exact binomial coefficient also depends on counting all sequences of one type without losing the boundary cases where some symbol occurs zero times.
Lean represents a portfolio as a function Fin d → ℝ in Mathlib’s stdSimplex; a market is a one-based sequence of vectors of the same type. The coordinate chart maps into the simplex, and a scaled restricted Lebesgue measure is pushed forward to define the uniform prior. The chart’s measurability is proved in the definition file. Algorithm 10.1 is a componentwise ratio of real integrals, and the main theorem asserts positive realized wealth. All market vectors on rounds are nonnegative and nonzero. The parameter restrictions and make the dimension and printed denominators meaningful.
For Lemma 10.5, quotients use extended nonnegative reals, with when and as printed. Lemma 10.6 is stated for a generic prior concentrated on the simplex, with its ratios in extended nonnegative reals under the same conventions, and with the hypothesis that the normalizing integral of Algorithm 10.1 is positive in every round, which is what makes the algorithm's prediction defined. A comparator with zero wealth is omitted only from the real-log statement, corresponding to log wealth in the source. The prior cannot be replaced by an arbitrary point mass: the theorem names the chart-based uniform measure, and the prediction is the exact integral ratio. Contributions proving normalization, support, the integral identity, and the final regret bound are all within scope.
The Riemann hypothesis asks whether every nontrivial zero of the actual Riemann zeta function has real part one half. The Connes formalization has a certified implication from positivity of the Weil distribution to RH. That implication supplies a criterion; its positivity hypothesis still needs a proof. The Green realization formalization supplies an independently certified physical carrier, actual-zero columns and bounded synthesis operators. Their construction does not establish the arithmetic inequality.
This open problem isolates a finite-certificate formulation of that inequality. The goal is new research within the existing formal development, not a theorem asserted by the cited papers. It is an RH-equivalent target. A proof of the reductions below is already available; a proof of the target itself is not.
The relevant historical distinction is explicit: Riemann stated the zero-location hypothesis in 1859; Connes' 1999 paper relates trace-formula and positivity questions to the zeros; the present Lean development certifies the conditional positivity criterion and the Green realization. None of these citations is offered as an unconditional proof of the new arithmetic certificate bound.
Let be the subtype of complex numbers satisfying and . Multiplicities are the existing natural analytic multiplicities. Reflection is , and conjugation is . For each actual zero, let be its finite reflection/conjugation orbit, called its quartet. Repeated orbit elements are removed by the finite-set construction, so the term does not assert four distinct zeros.
At a positive support radius , the physical carrier is the existing closed Dirichlet energy-image completion on . Its energy convention is the integral of . Source lifts, Green columns and their pair normalization retain their published definitions. The original admissible tests are smooth compactly supported functions; the carrier is not defined from an arbitrary replacement zero family.
Write for the original positive column of an actual zero , with the original reflected-pair and multiplicity normalization. Their complete squared-norm sum is certified summable at each positive radius. For a finite set , is the published synthesis of exactly these positive columns into . Let be the original selected negative synthesis on the coefficient space for the unchanged quartet .
For a positive accuracy , define the already-published operators
and the selected coefficient correction
The positive regularization makes strictly positive, including dependent or repeated columns. Its ring inverse is certified to be a genuine inverse for positive .
The goal is
Here abbreviates the two strict inequalities in the Lean statement. The window is chosen before accuracy. The finite cutoff can depend on accuracy, but the selected negative quartet remains unchanged. The same accuracy occurs in the complete omitted tail and the correction operator.
The certified fixed-window theorem identifies all-accuracy finite certificates with the original Picard marker being at least half the identity. The certified cofinal quartet criterion identifies arbitrarily large such quartet windows with Mathlib's Riemann hypothesis. Their composition has also been checked independently in the native Lean environment against the exact goal statement.
These two reductions are the principal milestones, alongside the existing literature-form positivity implication. Shared definitions and supporting theorems remain reusable library nodes. Certification of a reduction is distinct from establishing the nonnegative correction demanded by the goal. The goal is currently unproved and carries no RH or desired-positivity hypothesis.
Finite tail cutoffs exist by summability, and regularized coefficient inverses exist by strict positivity. Those facts leave the sign of undetermined. An arithmetic representation of the full Weil operator alone also leaves that sign undetermined. The selected negative packet and the unselected negative background are different parts of the original signed operator; replacing one by the other changes the obligation.
The arithmetic transfer audit ZP-WEIL-MARKER-TRANSFER / RH-ZERO-PROV-2 records this distinction. Endpoint estimates or neutral-shell arguments contribute only when they supply the original lower bound with the required window and accuracy quantifiers. A bound at one boundary, an accuracy-dependent choice of window, or an estimate with a positive residual error floor does not supply the displayed target. No easier status is implied by its finite coefficient representation.
The proposal uses Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474, with the published original quartet and selected-correction definitions. A separate native audit uses the existing Lean 4.34.0 repository environment. Complex Hilbert inner products are conjugate-linear in the first argument. Operator nonnegativity uses the existing continuous-linear-map order. Infinite tails are unordered sums on the actual-zero complement.
No simple-zero assumption, independence of columns, unregularized Gram inverse, replacement carrier, changed coefficient metric or silently restricted zero family is permitted. Quartets include zeros on the critical line; an empty actual-zero subtype would make the universal target vacuous, exactly as specified by the existing actual-zero indexing. New auxiliary definitions belong in shared definition bundles, and reusable algebraic lemmas belong in the library. The existing Green milestone history and dependency graph are retained.
monocap-tech/provenance, RH-ZERO-PROV-2 arithmetic-transfer checkpoint, 2026. Its stated status is representation complete, lower-bound theorem open, RH not proved.The exact cofinal-quartet finite-certificate goal remains open. An independent Lean audit verifies its equivalence to Mathlib RiemannHypothesis by composing the two certified milestone reductions. The window is chosen before every positive regularization parameter; the selected actual-zero quartet is fixed, and the same parameter controls the full positive tail and selected correction. Tail summability and existence of inverses alone do not establish the required sign.
The foreign graph export ConnesRZ.weil_positivity_implies_RH matches the native ConnesRZClosed.weil_positivity_implies_RH: the older native ConnesRZ theorem takes explicitFormula as an input, discharged in Closed. The foreign record has a staged source qualification; it has not been edited.
Arithmetic transfer checkpoint: monocap-tech/provenance 178c83225b2300506ff622899d08ec3c987137d5, rh/checkpoints/RH_ZERO_PROV_2_EULER_WEIL_MARKER_TRANSFER_20260920.md, SHA256 0bb48b950f09220f7b2f193c16b45b15add0333906f919f8b50ca915f77a1a0d. Retained local Git bytes were verified; public availability is unverified. Critical-window location, the prescribed ordered-limit interface, and arithmetic endpoint/neutral-shell control remain open. RH is not established.
Helly's theorem says that a finite family of convex sets in has a common point whenever every of its members do. Two of its best-known strengthenings weaken the hypothesis in different directions. The colorful Helly theorem, due to Lovász and first published by Bárány (1982), distributes the sets into color classes and only asks that every colorful choice of one set per class intersects. The fractional Helly theorem of Katchalski and Liu (1979) only asks that a positive fraction of the -tuples intersect, and concludes that a positive fraction of the whole family has a common point. Bárány, Fodor, Montejano, Oliveros and Pór (2014) combined the two into a colorful fractional Helly theorem, which they used to prove colorful and fractional -theorems.
Timeline:
Work in with . A color class is a finite indexed family of convex subsets of ; repetitions are allowed. Given color classes , a colorful choice is a tuple with , selecting the sets . There are colorful choices.
For : if at least colorful choices satisfy , then for some color there is with
If every colorful choice satisfies , then for some color .
Colorful Helly specializes to Helly's theorem by taking all color classes equal, and the colorful fractional theorem specializes to the fractional Helly theorem in the same way. Both are standard inputs in the theory of intersection patterns: colorful and fractional -theorems, Helly-type results for families with extra structure, and bounds on transversal numbers. Mathlib contains Helly's theorem and Carathéodory's theorem but neither colorful statement; this mission adds both as reusable, machine-checked results.
Helly's theorem alone does not suffice: the hypothesis only controls colorful tuples, so subfamilies with two sets of the same color are never assumed to intersect. The arguments need an extremal object attached to each colorful intersection (classically a lexicographic minimum or a lowest point) and a Helly-type reduction showing that this object is determined by at most of the chosen sets. The sets are not assumed closed or bounded, so a reduction to compact sets is also required.
is EuclideanSpace ℝ (Fin d); the color classes are a dependent family indexed by Fin (d+1) and Fin (N i), and a colorful choice is a dependent function (i : Fin (d+1)) → Fin (N i). The number of intersecting colorful choices is the cardinality (Set.ncard) of a set of such functions. Empty color classes are allowed; they make the statements trivially true, since an intersection over an empty index set is the whole space. The fraction is explicit rather than existentially quantified. Proofs of the optimal fraction would be welcome as a stronger follow-up.
Prove equivalence between two WordRAM models: one with unsigned pointers, bit operations, and shifts; the other with signed pointers and branching on sign. Both support bounded-word arithmetic and multiplication.
For input and observable output bounded by words, transfer running time in either direction to
including input/output conversion, with one bound valid for every sufficiently large word width. We preserve halting and mapped memory as well.
A stochastic reaction network tracks the counts of chemical species as reactions occur. Different species and reaction rates may grow at different powers of a large system-size parameter. Kang and Kurtz's model-reduction paper uses these powers to identify candidate time scales and combinations of species that can remain bounded. Before a reduced model can be justified, the dominant reactions that increase a combination must be compared with those that decrease it. Condition 3.2 makes that comparison.
Checking the condition for every nonnegative linear combination is a large task even for a finite network: the weights range over a continuum, and changing a weight can change which reactions increase or decrease the combination. The paper's Lemma 3.4 relates this task to the directed graph of species. It says that combinations supported on different strongly connected components can be checked component by component. This mission formalizes that result and the claims in its proof that carry the reduction.
There are finitely many species and finitely many indexed reactions . Reaction consumes molecules of species and produces molecules of that species. The stoichiometric change is . Species has a nonnegative scaling exponent , and reaction has a real exponent . The effective reaction exponent is .
For a vector of nonnegative weights , the scalar is the change in its linear combination when reaction occurs. Write for reactions with positive change and for reactions with negative change. The balance equation equates the largest on these two sets. If that equation fails, the time-scale inequality permits a chosen exponent only when it is no larger than , the largest on the support of minus the largest on . Condition 3.2 is the disjunction of these two alternatives.
The species graph has an edge when one reaction consumes and produces . Its strongly connected components are the maximal sets of species that can reach one another by directed paths. A single species is a component when it shares no larger mutual-reachability class. A nonnegative vector supported in one such component is a component-level test vector.
The goal is Lemma 3.4, p. 15. Suppose , each is nonnegative and supported within one maximal strongly connected component, and distinct pieces belong to distinct components. For fixed , the lemma asserts all three implications:
The companion consequence on the same page quantifies over all nonnegative vectors: if any one of these properties holds for every vector supported in a strongly connected subgraph, then it holds for every vector. The milestones mirror the paper's proof: a chain of component pieces cannot revisit a piece; under Condition 3.2 the maximal positive exponent either satisfies the time-scale bound or is bounded by the maximal negative exponent; and the two uniform cases yield their respective alternatives.
Lemma 3.4 replaces a global family of tests with tests inside individual strongly connected components. In the paper this narrows the balance checks needed before the authors study separated time scales and reduced stochastic models. The uniform balance and uniform time-scale clauses matter separately: the first preserves equality of dominant positive and negative exponents, while the second preserves the same admissible across a sum of pieces. The general Condition 3.2 clause allows different pieces to satisfy different alternatives.
The mathematical result was proved in the 2010 arXiv preprint and published in 2013; it is not an open conjecture. This proposal supplies Lean statements and a reusable finite reaction-network vocabulary, with proofs left for solvers. The local sanity file checks the empty-maximum and zero-vector behavior without using sorry. The draft theorem files compile as statements, but their six proofs are not yet machine checked.
The obvious inequality for a sum says that a reaction increasing increases at least one piece. It does not say that the piece's dominant increasing reaction also increases the sum: contributions from other pieces can cancel it. Consequently, taking a maximum separately on each piece does not directly give the balance equation for the sum. The graph restriction is decisive because a sequence of compensating reactions would otherwise be able to cycle among pieces. The milestones isolate that no-repetition property and the two inequalities the paper obtains from it.
Species, reactions, and pieces are represented by Fin s, Fin r, and Fin m; these are zero-based versions of the paper's one-based indices. The stoichiometric coefficients are natural numbers, the changes and all scaling exponents are real, and . Following the standing restriction on p. 5, each reaction consumes at most two molecules. The paper's is computed from , , and , not supplied independently.
For a reaction set , uses WithBot ℝ, so the maximum of an empty set is , as the paper explicitly uses on p. 17. The support maximum in is an ordinary real maximum when relevant. The value is represented in EReal: when is empty, it is and the time-scale inequality holds for every real . Subtraction is performed in the reals before conversion to EReal. Thus zero vectors do not acquire a spurious bound from a default-valued maximum or extended-real subtraction.
An edge uses positive consumption and positive production in the same indexed reaction, matching the wording on pp. 4 and 15. Mutual reachability defines a component. Each piece is required to lie in one component, and different pieces in different components. These conditions prevent splitting a single component into separately balanced pieces, which would make the goal false. An empty family of pieces is permitted; its sum is zero. The definition file is useful for the other balance results in the paper, while the graph and component lemmas can support later work on reaction-network decomposition.
The proximal stochastic subgradient method is the workhorse of large-scale learning: to minimize a regularized population risk with , it samples a data point, takes a step against a sampled subgradient of , and applies the proximal map of the regularizer . Its sample complexity is classical for convex problems ( samples for function accuracy ) and for smooth nonconvex problems ( samples for gradient norm , Ghadimi–Lan 2013). For problems that are both nonsmooth and nonconvex, however, no complexity bound was known for any reasonably broad class before Davis–Drusvyatskiy 2019.
Many such problems — robust phase retrieval, nonlinear least squares with an loss, conditional value-at-risk minimization with smooth losses, covariance estimation — are weakly convex: they become convex after adding a quadratic . This mission formalizes the complexity guarantee of Davis and Drusvyatskiy for the proximal stochastic subgradient method on weakly convex problems.
Timeline. Nurminskii (1973) showed that for weakly convex and the stochastic subgradient method has limit points that are stationary, without a rate. Ghadimi and Lan (2013) proved the rate for smooth . Davis and Drusvyatskiy (arXiv 2018, SIAM J. Optim. 2019) proved the first rate for the proximal stochastic subgradient method under weak convexity, measured by the gradient of the Moreau envelope; this is Theorem 3.4 of their paper.
Work in with the Euclidean norm. Let be closed (its epigraph is closed) and convex, with nonempty domain , and let be -weakly convex: is convex. Set .
The subdifferential of a function at a point of its domain is the set of vectors with as ; it is empty off the domain. For the Moreau envelope and the proximal map are
Assumption A (stochastic subgradient oracle): on a probability space one can draw i.i.d. samples (A1); there are an open set and a measurable map with for all (A2); and for all (A3).
Algorithm 3.1 starts at and, for , samples and sets . It returns with drawn from with probability .
For and stepsizes ,
and with , ,
In the order the proof uses them: Lemma 2.1 (subdifferential characterization of weak convexity), the existence of with (§3.2), Lemma 3.2 ( is a proximal point of ), Lemma 3.3 (one-step contraction towards ), Lemma 2.2 (the envelope is with ), and the one-step descent estimate (3.14).
The result. A small certifies that is within of a point with and . Theorem 3.4 therefore gives a sample complexity of for reaching an -nearly stationary point, matching the smooth rate, for a method that is run in practice without modification. The underlying observation — the method is an approximate descent method on the Moreau envelope — is reused in the paper's model-based analysis (Theorem 4.3) and in subsequent work on stochastic nonsmooth nonconvex optimization.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A complete development produces reusable infrastructure: the Fréchet subdifferential of extended-valued functions, weak convexity and its subgradient characterization, Moreau envelopes of weakly convex functions and their differentiability, nonexpansiveness of convex proximal maps, and the bookkeeping of iterates driven by i.i.d. samples under a product measure.
The obvious argument — show that decreases in expectation — fails: neither nor need tend to zero, and the latter is discontinuous in . Progress must be measured on the Moreau envelope, which requires comparing the iterate with the proximal point of , not of . In Lean, the heaviest single ingredient is Lemma 2.2 (differentiability of the envelope of an extended-valued weakly convex function), and the direction of Lemma 2.1, which in the paper rests on Rockafellar–Wets' characterization of convexity by monotonicity of the subdifferential.
EuclideanSpace ℝ (Fin d). An extended-valued function is a pair (domain , real values on ); closedness is closedness of . The subdifferential is the published regular subgradient NonconvexSplitting.Shared.IsRegularSubgrad of the -extended lift.prox a z is a function constrained, for every , to return a minimizer over of ; this determines it uniquely.