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?
Wasserstein distributionally robust optimization (DRO) replaces the empirical loss of a decision or model by its worst case over all distributions within a Wasserstein distance of the empirical distribution . It is used in operations research (newsvendor, portfolio and inventory problems) and in machine learning (robust classification and regression), and it is attractive because the worst-case loss is often a computable convex program (Mohajerin Esfahani and Kuhn 2018; Gao and Kleywegt 2023).
The practical question is how large must be for the robust loss to upper-bound the true, unknown loss with high probability. The classical answer goes through measure concentration of around in Wasserstein distance (Fournier and Guillin 2015), which forces in dimension : the curse of dimensionality. Rui Gao's paper (arXiv:2009.04382; Operations Research, 2023) shows that a radius of order suffices, independently of , under a transportation-information inequality and a complexity assumption on the loss class. This mission formalizes the paper's result for the 1-Wasserstein distance (Sec. 4.2, Theorem 2 and Corollary 4).
Let be a separable real Banach space with norm . is the set of Borel probability measures with . The 1-Wasserstein distance is
For a loss the Wasserstein regularizer is the gap between robust and nominal loss,
The Lipschitz norm is the best Lipschitz constant of .
The data are i.i.d. samples from , with empirical distribution . and refer to the product law. The distribution satisfies the transportation-information inequality if for every , where is relative entropy. It holds, for example, for every distribution with a sub-Gaussian norm.
The loss class satisfies Assumption 1(I) if for all , with . It satisfies Assumption 1(II) if is unbounded and each attains its Lipschitz norm at infinity, i.e. for some .
The Rademacher complexity of a class on the sample is , with i.i.d. uniform signs . Assumption 5 asks for a sub-root function that dominates the localized complexities:
Sub-root means non-negative, non-decreasing, non-constant, with non-increasing. Its positive fixed point is .
Set and . Under , Assumption 1 and Assumption 5, for , with probability at least ,
Corollary 4 justifies a radius of order whenever , which the paper verifies for kernel classes and other examples (Sec. 5). That rate is the one used in practice, and it was not covered by the concentration-based theory. Theorem 2 is a dimension-free generalization bound for Lipschitz-regularized learning in its own right. Lemma 1 links the two by identifying the 1-Wasserstein regularizer with Lipschitz regularization.
The results are proved in the paper. As far as known, none of them is machine-checked. A formalization would check the paper's peeling and fixed-point arguments, which turn out to need a corrected failure-probability count (see Formalization scope). It would also produce reusable Lean infrastructure: Rademacher complexity in the , no-absolute-value normalization, localized classes, sub-root functions, , and the Wasserstein regularizer on a Banach space.
The obvious route bounds and uses Kantorovich–Rubinstein duality. It fails because is of order , so no dimension-free radius comes out. A dimension-free bound must therefore hold uniformly over an infinite loss class without passing through the distance between and , and the bound must scale with each function's own Lipschitz norm rather than the class-wide constant . The statements also need measure-theoretic infrastructure that Mathlib lacks or has only partly: transport inequalities, Rademacher averages over classes, and suprema of uncountable families inside expectations.
RWPI.SqrtLasso.transportCost with cost . Expectations inside regularizers and complexities are extended integrals in (published ModelRiskOT.Duality.extIntegral). is the Bochner integral; it is the true expectation because a Lipschitz is integrable under . Relative entropy is Mathlib's klDiv.Lemma 5 (concentration on the product space under , used in Lemma 9's proof) belongs to the companion mission on variation-based concentration and is not restated here. Contributions are welcome at every level: sub-root fixed-point facts, symmetrization, the peeling lemma, and Lemma 1's two directions are independent entry points.
The source is arXiv:2009.04382; its printed page numbers equal the PDF's page numbers.
In distributed optimization, agents each hold a private function and must jointly solve
by exchanging vectors only with their current neighbours in a communication network. The setting covers distributed estimation and learning in sensor networks, formation control and power-system control, where no agent can see all the data and no central coordinator is available. Often the network changes over time: links appear and fail, and agents move.
The classical method, distributed gradient descent (DGD), mixes neighbours' iterates and takes a local gradient step. With a fixed step size it does not converge to the optimum, because at a consensual optimum the local gradients need not vanish; exact convergence requires diminishing steps and is then sublinear. Nedić, Olshevsky and Shi (arXiv:1607.03218, SIAM J. Optim. 2017) introduced DIGing, which adds a second variable that tracks the network-wide average gradient, and proved that it converges R-linearly (geometrically) to the exact optimum with a fixed step size, over time-varying undirected graphs, with an explicit rate.
An matrix is stored by its rows; row is agent 's copy , and is the Frobenius norm. Write and (the consensus violation). The stacked gradient has rows .
Objectives. Each is differentiable with -Lipschitz gradient, (Assumption 4), and satisfies with , at least one (Assumption 5). Put , and . Then has a unique minimizer .
Network. At time the agents communicate over an undirected graph and mix with a matrix . Let and . Assumption 1 requires: when and ; every is doubly stochastic; and for some positive integer , .
DIGing (Algorithm 1) with step size : and
Let . For every step size there is with
where is the explicit rate
The proof runs a small gain argument in the ergodic norm around the cycle , where and are the gradient differences. The milestones are the paper's own lemmas: Lemma 2 (the -step consensus contraction); Lemmas 5, 6, 7 and 9 (the four arrows); Lemma 8 (an error bound for inexact gradient descent, used by Lemma 9); Theorem 3 (the small gain theorem); Lemma 4 (a bounded ergodic norm gives an R-linear rate).
The existence and uniqueness of (p. 9); Corollary 11, the polynomial-in- rate under the concrete graph and weight Assumptions 2–3; and Proposition 1, the optimality conditions behind the algorithm.
Theorem 10 gives geometric convergence of a fixed-step method to the exact optimum over networks that may be disconnected at every instant, provided they are jointly well mixed over windows of steps. Its rate is explicit in , , , and , and Corollary 11 turns it into an iteration count polynomial in . Gradient tracking of this kind has since become a standard building block of decentralized optimization and learning algorithms, and the small-gain analysis in the ergodic norm is reused for other methods with time-varying or directed communication; the companion mission in this series treats Push-DIGing over directed graphs with the same machinery.
The result is proved in the paper. As far as is known it has not been machine-checked. A formalization provides checked versions of the paper's reusable components: the small gain theorem in the ergodic norm, the error bound for inexact gradient descent on a sum of strongly convex functions, and the consensus contraction for products of doubly stochastic matrices. It also pins down the conventions the paper leaves implicit, such as the sign of the mixing weights and the endpoint of the step-size interval.
DIGing does not decrease any obvious quantity monotonically: the distance to the optimum can grow while the gradient tracker is still far from consensus, and over a time-varying graph a single mixing step need not contract at all; only products of matrices do. A one-step Lyapunov argument therefore fails. The paper's way around this is to bound each quantity of the cycle by the previous one in the ergodic norm, with gains that depend on , and to choose and so that the product of the four gains is below one. The algebra of that choice, which produces the two-regime formula for , is delicate: the constraints , and the gain condition (37) pull in opposite directions. Lemma 8 needs a careful one-step analysis of gradient descent with perturbed gradient evaluations.
A stacked matrix is Fin n → EuclideanSpace ℝ (Fin p); , , , and the ergodic norm (6) are defined in DIGing.Undir.Common; , (the operator norm on Euclidean ), , Assumptions 1–3, DIGing, and the rate are in DIGing.Undir.Setting. The constants are parameters. is given as the least upper bound of , and the optimum by its optimality. Agents and iterations are indexed from . Roots are Real.rpow.
Two hypotheses differ from the printed text, both disclosed in the item notes. Doubly stochastic includes nonnegative entries (Mathlib's doublyStochastic); the paper uses the term in this sense, and Lemma 6 is false for signed matrices with unit row and column sums. The right endpoint , printed as included, is excluded: there the rate formula gives . Corollary 11 assumes , the paper's standing range (p. 4).
The goal assumes nothing about the arrows, the gains, the auxiliary parameters or the ergodic norm of the iterates; its only rate hypothesis is , and its conclusion includes , so a bounded-sequence reading is ruled out.
A complete development needs: products and the spectral norm of doubly stochastic matrices; the ergodic norm and its monotonicity in ; basic smooth strongly convex analysis (existence of the minimizer, , co-coercivity); and real-power algebra for the choice of . The small gain theorem, Lemma 8 and Lemma 2 are reusable beyond this mission, and are shared with the Push-DIGing mission of this series. Corollary 11's proof additionally uses a bound from the consensus literature; formalizing it is a welcome separate contribution. Proofs of any milestone, and alternative arguments for the arrows, are welcome.
Wasserstein distributionally robust optimization (Wasserstein DRO) replaces the expected loss under an empirical distribution by the worst-case expected loss over all distributions within a Wasserstein distance of it. It is used in operations research, statistics and machine learning to guard decisions and predictors against the gap between the sample and the population. The statistical question it raises is how large must be for the robust loss to bound the true loss with high probability. Classical answers go through the concentration of the empirical measure in Wasserstein distance, which forces in dimension : the curse of dimensionality.
Gao (arXiv:2009.04382; Operations Research, 2023) shows that a radius of order suffices, independently of the dimension. The first ingredient, and the subject of this mission, is a new concentration inequality for the empirical mean of a single loss function, whose rate is governed by the Wasserstein regularizer itself.
Let be a separable Banach space with norm and let . is the set of Borel probability measures with , and the Wasserstein distance of order is
the infimum over couplings of and . For a loss , a nominal distribution and a radius , the Wasserstein regularizer is the excess of the robust loss over the nominal loss,
The data are i.i.d. samples from an unknown ; is their joint law and is the empirical loss. A distribution satisfies the transportation-information inequality if
with the relative entropy. holds for every distribution with a Gaussian moment , and (Talagrand's inequality) is implied by a log-Sobolev inequality.
The rate function is built from
If with and satisfies , then for every
and for every , with probability at least ,
Theorem 1 says that the large-deviation rate of the empirical loss is the inverse of the Wasserstein regularizer, and that the regularizer at radius is a valid high-probability correction of the empirical loss. Neither involves the dimension of or the complexity of a covering of it. The paper builds its covering-number and local-Rademacher guarantees for Wasserstein DRO (Sections 4.1–4.2, the subject of two companion missions) on this single-function result, and Corollary 1 recovers, for , the Lipschitz-norm bound known from transportation inequalities while sharpening it for .
The results are proved in the paper; none is formalized. A complete development would give a machine-checked tensorization of transportation-information inequalities on Banach spaces and a Marton–Herbst-type concentration argument, both of which are used well beyond DRO.
The proof combines three ingredients that Mathlib does not yet connect. Tensorization (Lemma 4) needs disintegration of a measure on and the chain rule for relative entropy, together with a gluing of couplings and Hölder's inequality for the dimension constant. Lemma 5 combines with Kantorovich duality for the cost and the entropy of an exponential tilt, then optimizes a Young-inequality split over two parameters for , and extends from bounded to -growth by monotone truncation. Proposition 1 rests on the strong duality (1) of Gao and Kleywegt, an external result, and on the first-order optimality condition of a convex perspective function. A naive approach that bounds the deviation by fails: that distance decays like , which is exactly the curse the theorem avoids.
The source is arXiv:2009.04382; its printed page numbers equal the PDF's. The Lean development lives in the namespace WassFSG.Conc and uses these conventions:
klDiv.A formalization that reads an infinite through a real coercion would turn the tail bound into the trivial bound ; the conventions above rule this out. Likewise a regularizer whose supremum ranged only over measures supported on the sample, or a condition over a restricted class of , would be a different statement.
Contributions welcome: Lemma 4 and Corollary 1 are independent entry points; a proof of the duality (1) under the paper's growth condition would be reusable by every Wasserstein DRO mission.
In a stochastic linear–quadratic (LQ) optimal control problem a controller steers a linear stochastic differential equation and pays a quadratic cost. When the cost weights are allowed to be indefinite — as in mean–variance portfolio selection, where the control weight is zero — the problem can still be well posed, and two different notions of solution appear. An open-loop optimal control is a process chosen for one given initial pair . A closed-loop optimal strategy is a feedback law that is optimal for every initial state at once. A closed-loop optimal strategy yields an open-loop optimal control for each initial state; the converse is the question.
Timeline. Chen, Li and Zhou (1998, doi:10.1137/S0363012996310478) started the theory of indefinite stochastic LQ control. Ait Rami, Moore and Zhou (2002, doi:10.1137/S0363012900371083) introduced the generalized Riccati equation with a Moore–Penrose pseudoinverse and stated that, for Problem (SLQ) with continuous coefficients and , a continuous open-loop optimal control exists at every initial pair if and only if the Riccati equation has a solution satisfying a range condition and a sign condition. Sun and Yong (2014, doi:10.1137/140953642) characterized closed-loop solvability by regular solutions of that Riccati equation. Sun, Li and Yong (2016, doi:10.1137/15M103532X) showed by two explicit examples that the 2002 equivalence fails in both directions, and that open-loop solvability is strictly weaker than closed-loop solvability. This mission formalizes those examples.
Let be a standard one-dimensional Brownian motion on a probability space and its augmented natural filtration. For and a control in the space of -progressively measurable -valued processes with , the state equation is
and the cost is the expectation of plus the time integral of a quadratic form in with weights and linear terms . Problem (SLQ) is the case , with cost and value function .
The Riccati equation (4.6) is
where is the Moore–Penrose pseudoinverse. A solution is regular if (4.7) a.e., (4.8) , and (4.9) a.e.
Example 7.1 is Problem (SLQ) with , , :
that is, , , , , , .
For every ,
while , and for every the problem is not closed-loop solvable on .
For and , the Riccati equation (7.12) has the unique solution , which satisfies (4.7) and (4.9), yet no open-loop optimal control exists at , .
The result. Example 7.1 refutes the necessity half of the Ait Rami–Moore–Zhou criterion: a continuous open-loop optimal control exists at every initial pair, but the Riccati equation has no regular solution. Example 7.2 refutes the sufficiency half. Together they show that the Riccati equation with conditions (4.7) and (4.9) characterizes neither notion, and that open-loop solvability is strictly weaker than closed-loop solvability; Example 7.1 also exhibits a finite value function that is discontinuous in time. These facts are why the paper develops separate characterizations of open-loop solvability (through the regularized Riccati solutions ) instead of the Riccati equation itself.
Formalizing it. The examples are proved in the paper by appeal to its Theorems 5.3 and 6.2 and to Theorem 4.3 from Sun–Yong (2014). Nothing in this chain is machine-checked anywhere. A formal proof of the goal must verify the explicit optimal control against the canonical stochastic state equation, compute the value function, and rule out every closed-loop strategy; it can use Theorem 4.3 (posed here as a milestone) or a direct argument. The definitions built here (the stochastic LQ problem, the pseudoinverse Riccati equation, regularity) are shared with the other missions of this series.
Open-loop optimality looks immediate because , but it requires showing that the state driven by hits at time , which means identifying the solution of the stochastic state equation for this control. The value at requires the degenerate interval to be handled inside the same SDE framework. The hard part is the negative claim: it quantifies over all feedback pairs with , and must show that no such pair drives every initial state to at time . The paper reduces this to Theorem 4.3, whose proof (in Sun–Yong 2014) is a substantial piece of stochastic LQ theory; checking that fails the range condition is the easy end of that chain.
Time is , vectors are Fin k → ℝ, inner products are dot products, and . The Brownian motion is the published Peng1990.SMP.IsStdBrownian, the filtration the published augmented filtration, the SDE solution concept the published Peng1990.SMP.SolvesSDE, and the pseudoinverse the published HarmonicGames.Decomposition.pinv.
Proving only that violates (4.7) does not settle the goal: the goal is about solvability of the control problem itself, and "not closed-loop solvable on any " is stated for every , not as the failure on some interval.
Contributions are welcome on any milestone, on the well-posedness of linear SDEs in this framework, and on the pseudoinverse identities (Penrose equations, the pseudoinverse of a scaled symmetric matrix) that the Riccati computations need.
In decentralized optimization, agents connected by a communication network jointly minimize a sum of private functions without a central coordinator: each agent sees only its own and talks only to its neighbours. Applications include sensor networks, distributed estimation, multi-agent control and learning over data spread across machines. The simplest method in this setting is decentralized gradient descent (DGD), in which every agent averages its neighbours' iterates and then takes a local gradient step. DGD and its relatives were analysed by Nedić and Ozdaglar (IEEE TAC 2009) and many later papers, almost always under the assumption that the (sub)gradients are bounded.
K. Yuan, Q. Ling and W. Yin (arXiv:1310.7063v3; SIAM J. Optim. 26(3), 2016) removed that assumption for DGD with a fixed stepsize. They showed that a stepsize bound depending on the spectrum of the mixing matrix keeps the gradients bounded, that the agents stay within of their mean, and that for convex smooth the objective error of the mean decreases at rate until it reaches a neighbourhood of size . This mission formalizes that last result, Theorem 2 of the paper, together with the lemmas its proof rests on.
Consider agents on a connected undirected graph . Agent holds a function , and the agents solve
with solution set , assumed nonempty.
A mixing matrix is symmetric and doubly stochastic, and only if or and are neighbours. Its eigenvalues are , and
Assumption 1 (p. 4): (a) each is convex, bounded below, and differentiable with an -Lipschitz gradient, ; (b) the network is connected and is symmetric, doubly stochastic, with .
DGD with stepsize , started from , is
Stacked vectors carry the Euclidean norm. Write , , , , , , , and
The paper reads DGD as unit-step gradient descent on the Lyapunov function
For a minimizer of and a solution , set
Let and . Then
and, for , if for every , then
The paper prints these as and . The constants are the ones its proof fixes: the recursion with (milestone below) and the threshold condition "", under which the error term absorbs half of the quadratic decrease. That gives , and " increases at " with this constant gives .
Theorem 2 is the convex, non-strongly-convex case of the paper's analysis. It says that DGD with a constant stepsize behaves like centralized gradient descent, with rate , until it reaches a floor of size . The floor shrinks with the stepsize and grows as the spectral gap of the network closes, which makes the trade-off between speed, accuracy and network connectivity explicit. The result is proved without bounded gradients; the boundedness comes out of the stepsize condition through the Lyapunov function. It is the baseline that exact methods such as EXTRA (Shi et al. 2015) were designed to improve on.
The paper's proof is complete in its main lines but informal in places: the rate is stated with , the constant is written with a -dependent , and the minimizer of is asserted to exist on grounds that do not suffice. To our knowledge no part of this analysis (DGD, mixing matrices with spectral bounds, the Lyapunov reformulation) has been machine-checked. A formal proof fixes the constants, records the needed hypotheses, and supplies decentralized-optimization infrastructure that Mathlib lacks.
The obvious approach treats the mean as gradient descent on with the exact gradient , which fails: by (15) the mean moves along , the average of gradients taken at different points. Controlling needs the consensus bound of Lemma 1, which in turn needs the gradients to be bounded, and no assumption bounds them. They are bounded only because DGD is unit-step gradient descent on and the stepsize condition makes that descent monotone (Theorem 1). Lemma 1 also needs the operator-norm identity for a symmetric doubly stochastic , a spectral fact about sorted eigenvalues. Finally, the recursion in needs a bound on that is uniform in , which comes from Fejér monotonicity of the iterates with respect to a minimizer of , not from anything about .
is EuclideanSpace ℝ (Fin p) and stacked vectors are PiLp 2 (fun _ : Fin n => ℝᵖ), so every stacked norm (, , ) is Euclidean on , not the sup norm. Gradients are Mathlib's gradient. DGD is a recursively defined sequence started at , not an arbitrary sequence with a property. and come from the eigenvalues of the symmetric sorted with multiplicity (eigenvalues₀). is , and is a supremum over the finite index set, i.e. a maximum.
Conventions and additions, each disclosed in the item statements:
Trivializing formalizations are ruled out. The iterates are the DGD recursion itself. The threshold in the rate is required at every earlier step, not only at step . does not depend on . The constants and are explicit, not an existential placed before the data. A sorry-free instance (, , constant ) shows that the goal's hypotheses can all hold together.
A complete development needs: the operator norm of via the spectral theorem, the descent lemma and co-coercivity for -smooth convex functions on Euclidean space, for -smooth functions bounded below, and Fejér monotonicity of gradient descent. These are reusable well beyond this mission. Contributions to any milestone are welcome; Lemmas 1–2 and (15) do not use convexity.
Liouville quantum gravity (LQG) equips a planar domain with a random area measure and a random boundary length measure . Both are built from an instance of the Gaussian free field (GFF). The Schramm–Loewner evolution is the conformally invariant random curve that describes interfaces in critical planar models. Sheffield's paper (arXiv:1012.4797, Ann. Probab. 44 (2016)) shows that the two are linked by a conformal welding. Zipping up a free boundary GFF by a reverse Loewner flow glues two boundary arcs of equal quantum length, and the glued seam is an curve.
This "quantum zipper" is the starting point of the mating-of-trees programme (Duplantier–Miller–Sheffield, arXiv:1409.7055). It is also the mechanism behind the conjectured, and partly proved, scaling limits of random planar maps decorated by statistical-physics models.
Timeline:
, and the free boundary Green's function is . Fix and put and .
which by Theorem 1.2 has the law of modulo additive constants.
as a vague limit. The area measure is the analogous limit with circle averages and exponent .
Almost surely, for every on and the two real points that maps to ,
The statement is scale free: it does not depend on the additive constant of .
Theorem 1.3 says that reverse SLE zipping is a welding by quantum length. Combined with the removability of for , it gives Theorem 1.4: the field determines the curve . The same equality of boundary lengths on the two sides of an SLE is the defining property of the quantum-zipper and mating-of-trees constructions, which build random surfaces by welding wedges together.
All results here are proved in the paper, and none has a machine-checked proof. The proofs are partly sketches: Proposition 5.5 ends with a limiting estimate, and the zero–one step of Theorem 1.8 is delegated to [DMS14a, Lemma 8.2]. A formal development would therefore check the most cited welding argument in random conformal geometry. The definitions it needs (arc averages of a GFF, , quantum wedges, conditionally Gaussian fields) are reusable for any LQG statement.
The obvious argument tries to compare the left and right boundary measures directly, ball by ball along the curve. It fails because the two measures depend on the field near the curve in the same way (5.1): nothing local distinguishes them, and nothing local forces them to agree. The paper instead builds a stationary picture (Lemma 5.6, Proposition 5.5, Figure 1.7). It shows that the curve splits a -wedge into two independent -wedges, and it uses the ergodic theorem with scale invariance to force the ratio of the two lengths to be a constant , which symmetry makes equal to . The last step transfers the result from the wedge to the field of Theorem 1.3 by absolute continuity. Every step uses Gaussian conditioning on random conformal images of the field, which current libraries lack.
Conventions committed to in Lean:
IsBrownianReal. Flows are pathwise ODE solutions, with no stochastic integrals.OAI.SLEExactGauge.IsOrdinaryChordalSLE.Disclosed readings of the text:
Contributions are welcome on any of the following:
A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. It covers constrained convex minimization (with ), saddle-point problems, Nash equilibria of convex games and complementarity problems, which is why projection methods for it are a standard topic in optimization and numerical analysis.
The classical methods for a monotone, -Lipschitz field (Korpelevich's extragradient method, Tseng's forward–backward–forward method, the subgradient extragradient method of Censor, Gibali and Reich) use a constant step or a backtracking search for one. Yu. Malitsky's paper (arXiv:1502.04968v1; SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) introduces the projected reflected gradient method, which needs one projection and one evaluation of per iteration. Its constant-step version requires , and so requires knowing , which is rarely available in practice (§4, p. 8). Section 4 removes that requirement: Algorithm 4.2 chooses its step from local information only and corrects it when a computable test fails. This mission formalizes the paper's convergence theorem for that algorithm, Theorem 4.4.
Let be a real Hilbert space with inner product , nonempty, closed and convex, and . Write for the metric projection onto . The variational inequality (1.1) asks for with
and denotes its solution set. The standing conditions (p. 1) are (C1) ; (C2) is monotone, ; (C3) is -Lipschitz, , with .
Algorithm 4.2 (pp. 8–9) has parameters , and a cap , and adopts the convention . It starts from with , , and . For it uses the step rule
forms the trial values , , , and evaluates a test quantity built from these. If the trial is accepted. Otherwise, in step (4.i) () the step is replaced by some satisfying (4.2), and in step (4.ii) () the reflection is replaced by for some satisfying (4.3), with a step satisfying (4.4); is then recomputed. The values kept after iteration are the corrected ones. A sequence produced this way is a run of Algorithm 4.2. The Lipschitz constant appears nowhere in the algorithm.
Under (C1)–(C3), for every run of Algorithm 4.2 there is with
where is weak convergence in .
In the order the proof uses them:
The supporting lemmas 2.2 (Minty), 2.3 (Opial) and 2.7 are included as plain items, together with a statement that runs exist from every .
The result shows that the projected reflected gradient method keeps its weak convergence guarantee when the step is chosen adaptively, without knowledge of , at a cost of at most two projections per iteration (one in most iterations, per the experiments of §5). Adaptive step rules of this kind, based on the local ratio , recur in later work on reflected and golden-ratio methods for variational inequalities (e.g. Malitsky 2020, arXiv:1803.08832), so a formal treatment of the run predicate and its energy inequality is reusable beyond this paper.
The theorem is proved in the paper; it has no machine-checked proof that this mission knows of. The work here is to formalize the definitions of Algorithm 4.2, its well-definedness, the energy inequality and the closing weak-limit argument in a general Hilbert space. The proof as printed has a gap, described under Difficulty; a formal proof would either close it or show that the statement needs an extra hypothesis.
Lemma 4.3 is the bookkeeping core. It has five cases depending on how compares with and on the sign of a norm expression. In the case where the reflection is changed, the previous iterate must be reinterpreted as the projection of a point on a segment (via Lemma 2.4) before the estimate of the constant-step method applies.
The closing argument needs the step sizes to stay away from zero, so that the limit can be taken in the optimality inequality for the iterates. The paper asserts that is a lower bound of , "from Lemma 4.2" (p. 12). The proof of Lemma 4.2 shows only that the step rule is at least , and that only under . In step (4.ii) the algorithm allows any satisfying (4.3) and any , so an admissible run can take arbitrarily small at such steps. The step regrows by the factor at later steps, but the printed proof does not control this. The obvious first attempt, citing a uniform lower bound , does not work as stated.
All objects live in one definitions item. is a general real Hilbert space, never . The projection is a nearest point chosen by choice, with a junk value when none exists. Every theorem that uses it assumes closed and convex together with a nonemptiness source, so the junk branch is never reached. Weak convergence is for all . (C3) uses a real constant . The convention is encoded by omitting the ratio term from the minimum when its denominator is zero, never by Lean's .
A run is a relation: the corrections , range over all admissible values, and nothing selects the largest. The stopping rule of step 3 is not encoded. A run whose residual vanishes continues as a constant sequence through the branch . Indices are used only for , and is a separate parameter.
The goal assumes exactly (C1)–(C3), , and . It assumes neither nor any lower bound on . Adding such a bound would assume the unproved step of the paper's argument. The milestone on carries and as explicit, disclosed hypotheses. Lemma 4.3 and (4.10) are stated without (C1) and (C3), which their proofs do not use. A formalization that concluded norm convergence, specialized to finite dimension, or fixed one particular choice of corrections would be a different theorem.
The development needs the existence and characterization of the metric projection onto a closed convex set, Minty's lemma, Opial's inequality and weak sequential compactness of bounded sets in Hilbert space. These pieces are reusable for other projection methods. Contributions toward any milestone are welcome, as is a resolution of the lower-bound question for .
Many problems in statistics and machine learning minimize a finite sum: an average of smooth convex losses, one per data point, often plus a strongly convex regularizer. The full gradient method costs component gradients per iteration and converges at rate , or linearly when the objective is strongly convex (Nesterov, 2004). The stochastic gradient method costs one component gradient per iteration, but its rates are sublinear, and , and these are optimal for algorithms that only see unbiased gradient estimates (Nemirovski et al., 2009).
The stochastic average gradient (SAG) method of Le Roux, Schmidt and Bach exploits the finiteness of the sum: it keeps the last gradient computed for every component and steps along their average. It was the first method with the iteration cost of the stochastic gradient method and the rates of the full gradient method.
Timeline.
Let , , and
Write for the gradient of and . The standing assumptions are: each is convex and differentiable; each gradient is Lipschitz with constant , ; and some minimizes . Put . The function is -strongly convex if is convex.
A state is : a table of vectors in and an iterate . One SAG step with index and step size replaces by and then sets
with the refreshed table. The indices are independent and uniform on ; is the state after steps, and is the average iterate. Expectations are over the indices only; the data are fixed. The table starts either at or at the centered gradients .
With and every ,
and, if is -strongly convex with ,
where for and for the centered table. All four combinations are stated, with the paper's constants.
The proof of Appendix B builds a Lyapunov function
with and , and fixes constants (App. B.5). The milestones follow it: the expectation identity of Lemma 1 and the inverse of Lemma 2; inequalities (12) and (13); the B.3 bound of by a quadratic in and ; the verification of Constraints 1–9 for the B.5 constants; the one-step decrease and the domination (B.7); the linear, summed and averaged rates in terms of ; and the initial values of for the two tables (B.8).
The result. Theorem 1 shows that one component gradient per iteration suffices for the convergence rates of the full gradient method on finite sums. In the strongly convex case the rate is, for large relative to , better per pass through the data than the full gradient method's. The result started the line of variance-reduced methods (SVRG, SAGA, and their accelerated and proximal variants), which are now standard for empirical risk minimization. The convex-case rate holds without strong convexity and from either initialization.
Formalizing it. The rates are proved on paper, but the proof leans on a large symbolic computation: Table B.3 has dozens of terms, and the verification that the chosen constants satisfy the constraints (B.6) was done with computer algebra and an off-paper script for . A machine-checked proof removes that dependency. The appendix also contains slips: a parametric step of B.4 that fails for , a wrong coefficient in B.8.2's intermediate identity, and a missing argument for . A formal proof settles which claims are right as stated. No formal proof of Theorem 1 is known to be recorded in a proof assistant library.
The method is not a stochastic gradient method in disguise: the step is a biased estimate of , because the table holds stale gradients. The standard argument, a one-step contraction of in expectation, fails, since the bias depends on the whole table. The analysis must track the joint state through a Lyapunov function with several free parameters, find constants for which its expected decrease is negative uniformly in and , and show that it dominates . Each of these steps reduces to sign conditions on rational functions of and that hold for all , not just for a few values.
is EuclideanSpace ℝ (Fin p), and the components are indexed by Fin n. The gradients are an explicit map f', tied to f by HasGradientAt at every point. and are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg. The expectation over i.i.d. uniform indices is the uniform average over all index sequences (SAGA.Convex.expectIdx). A conditional expectation given is the average over the next index from an arbitrary current state. The SAG step refreshes the table at the current iterate before the iterate moves. The average iterate includes and excludes .
The standing assumptions are exactly those of §3: , , each convex and differentiable with -Lipschitz gradient, and a minimizer of . Strong convexity is assumed only where the paper assumes it, in the shifted-convexity form of §3, with in Theorem 1 and in Appendix B. Hypotheses added to milestones, each one used by the paper without stating it, are wherever the B.5 constants appear (p. 43: "We will assume "), in the constraint verification (B.6), and the sign conditions , , , in the B.3 bound. The goal covers .
The goal is stated directly about expectIdx of along the SAG iterates from the two initial tables. It does not mention the Lyapunov function, its constants, or one-step averages, so it cannot be discharged by unfolding a definition. Junk values of Lean division are excluded by , and .
A complete development needs the expectation identity of Lemma 1 for block quadratic forms, smoothness and co-coercivity inequalities for convex functions with Lipschitz gradients, Jensen's inequality for finite uniform averages, and exact rational inequalities in and . The first two are reusable for other variance-reduced methods (SAGA, SVRG, IAG). Proofs of any milestone, of the case, and alternative proofs of the constraint verification are all welcome.
Networks of identical dynamical systems coupled along a directed graph model power grids, sensor and robot swarms, neural populations and coupled oscillators. A basic control question is how to steer every node of such a network onto a prescribed reference trajectory by acting directly on only a few nodes. This is pinning control: feedback is injected at a small set of pinned vertices, and the coupling has to carry the reference signal to the rest of the network.
For undirected or strongly connected networks, criteria for pinning synchronization go back to Wang and Chen (2002) and Chen, Liu and Lu (2007), and the first mission of this series treats the strongly connected case of Yu, Chen, Lü and Kurths (2013). Many networks of interest are not strongly connected: information flows down a hierarchy of groups, and the minimal requirement for the reference to reach every node is that the network, with the reference added as a virtual leader, contains a directed spanning tree rooted at the leader. Section 4 of that paper gives a criterion for this general case that splits into one condition per strongly connected component. This mission formalizes that criterion, Theorem 4.5, with the lemmas its proof uses and three corollaries.
There are vertices with states . The coupling configuration matrix has for , where records a connection from vertex to vertex , and zero row sums, . Given a function , a coupling strength , an inner coupling matrix and pinning gains (vertex is pinned when ), the controlled network is
where the reference solves . The network is globally synchronized when for every vertex and every pair of solutions.
The nonlinearity is controlled by Assumption 1: there is a matrix with for all and . Throughout §4 the paper also assumes that and commute, that is positive definite, and puts .
The vertices split into strongly connected components . In the Frobenius normal form the components are ordered so that no edge goes from a later component to an earlier one, which makes block lower triangular. For each component the mission uses three matrices:
In Lean, component membership is a map blk : Fin N → Fin M, and Fin M carries the Frobenius order.
If, for every component ,
then the controlled network with a directed spanning tree is globally synchronized.
Theorem 4.5 replaces a single matrix inequality for the whole network with inequalities, one of the size of each component. In practice the test runs component by component down the Frobenius order: decide which components need pinning, choose gains for each one separately, and get synchronization of the whole network. Corollary 4.7 makes this explicit in terms of the outer in-degrees: a component with no incoming edges from earlier components has to be pinned (Remark 4), while a component that receives enough weight from upstream needs no control. These conditions underlie the pinning scheme algorithm of §5 of the paper.
On the formal side, as far as a search of the platform and of Mathlib shows, none of these results is machine-checked. Mathlib has the positive semidefinite Schur complement and irreducible nonnegative matrices, but not the strict Schur complement, block-diagonal Lyapunov scaling, or Lyapunov arguments for networked ODEs with Kronecker-structured couplings. The mission produces, beyond the paper's theorem:
The obvious argument is to take one Lyapunov function weighted by a positive left null vector of the whole coupling matrix, as in the strongly connected case. Here it fails: the coupling matrix of a network that is not strongly connected has no positive left null vector, and condition (4.8) is local to each component. The central step is the passage from blockwise to global negative definiteness (Lemma 4.4). Condition (4.8) says nothing about the off-diagonal blocks that couple a component to earlier ones, and a block lower-triangular matrix whose symmetrized diagonal blocks are negative definite need not have a negative definite symmetric part; the component weights have to be found so that those couplings are dominated, which is a quantitative statement about Schur complements. Turning the resulting matrix inequality into convergence of the trajectories then needs a differential inequality on , a Kronecker-product definiteness argument with , and the commutation of and to reach the θ bound.
States are Fin n → ℝ and matrices are indexed by Fin N, Fin n, or the subtype of one component's vertices. Solutions are functions on ℝ that satisfy their ODE on through HasDerivWithinAt … (Set.Ici 0). "For any initial conditions" means for every pair of solutions ; existence of solutions is not claimed. Convergence is componentwise, which agrees with every norm on . "Positive definite" is Mathlib's Matrix.PosDef, which includes symmetry, and is (-X).PosDef. is the least Rayleigh bound, IsLamMax, never a supremum of a possibly empty set.
The vertices are not permuted into Frobenius form. The hypotheses say instead that:
The weights are tied to the paper's object by . The standing assumptions of p. 1402 (Assumption 1, , , ) are hypotheses of every goal-level statement. The goal does not assume the weights , the bound (4.10), or definiteness of a whole-network matrix; it assumes only (4.8) on each component, so it cannot be trivialized by assuming its own conclusion. For the hypothesis cannot be met, so that degenerate dimension is excluded.
The pages contain three misprints. (4.10) has "" in its third line and "" in its last; the last line, with a single , is formalized. Corollary 4.9 ranges "" where the component range is meant.
A complete development needs a Gronwall-type decay lemma on , the strict Schur complement, definiteness of Kronecker products, and the square root of a positive definite matrix commuting with matrices that commute with it. Each of these is reusable well beyond this mission, and contributions to any of them are welcome, as are proofs of the milestones in any order.
In decentralized consensus optimization a connected network of agents cooperatively solves
where agent privately knows the convex function and may exchange information only with its neighbours. The model covers distributed estimation in sensor networks, decentralized learning over data that cannot be pooled, and multi-agent control and power systems, where a central coordinator is unavailable or undesirable.
The standard first-order method is decentralized gradient descent (DGD) of Nedić and Ozdaglar (2009): every agent averages its neighbours' iterates with weights from a mixing matrix and takes a local gradient step. With a fixed step size, DGD does not converge to a minimizer of (1.1) but to a neighbourhood of one whose size scales with the step size (Yuan, Ling and Yin, arXiv:1310.7063); exact convergence needs diminishing steps and is then slow. Shi, Ling, Wu and Yin (arXiv:1404.6264, SIAM J. Optim. 2015) introduced EXTRA, a decentralized method with the same per-iteration cost as DGD that converges exactly with a fixed step size. This mission formalizes its convergence and sublinear rate for convex objectives with Lipschitz gradients (§3.1–3.2 of the paper).
Agent holds a local copy of the variable. The stacked variable has as its -th row, , and has as its -th row. For a symmetric , , and is the Frobenius norm.
Mixing matrices (Assumption 1). On a connected graph with vertex set , the matrices vanish off the edges and the diagonal, are symmetric, satisfy and , and obey and . The recommended choice is .
Objectives (Assumptions 2–3). Each is convex and differentiable with -Lipschitz gradient, and (1.1) has a minimizer.
EXTRA (Algorithm 1). Fix a step size and any . Set and, for ,
Analysis objects. is the symmetric positive semidefinite square root, , and . A pair is optimal if for some and
By Lemma 3.1 these are exactly the pairs whose is consensual with every row solving (1.1).
Under Assumptions 1–3 and , as ,
and the same running-average and running-best rates hold for the optimality residuals (violation of first-order optimality) and (violation of consensus). The statement involves only the iterates: no optimal pair, constant or summability hypothesis appears in it.
For every optimal and every ,
and converges to an optimal .
In attack order: Proposition 2.2 (spectral consequences of Assumption 1), Proposition 2.1 (consensus plus zero total gradient implies optimality), Lemma 3.1 (optimality conditions), (3.5) and Lemma 3.2 (the error recursion), the co-coercivity inequality (3.10), the descent inequality (3.17), Theorem 3.3, Proposition 3.4 (rates of summable sequences), the summability bound (3.19), the residual decomposition (3.20) and the constant of p. 14.
Theorem 3.3 is what distinguishes EXTRA from DGD: a fixed step size, independent of the network size and as large as for , reaches the exact minimizer. Theorem 3.5 quantifies this with rates on quantities each agent can relate to its own state, the progress between iterates and the two optimality residuals. The analysis, which writes a two-step gradient recursion as a contraction in a -norm on the pair , was reused by later exact decentralized methods, such as the proximal-gradient extension PG-EXTRA, so its formal statement is reusable beyond this one algorithm.
The results are proved in the paper. No machine-checked proof of them is known at the time of writing, and Mathlib has no decentralized optimization. The mission's output is a formal, self-contained statement of the EXTRA model and its convergence theory, with each step of the published proof isolated as a milestone. Alternative proofs of the convergence clause of Theorem 3.3 (the paper defers it to the standard analysis of contraction methods, citing B. He, Math. Programming 66, 1994) are welcome.
The obvious attempt treats EXTRA as gradient descent on some function, and fails: the iteration is not a gradient step for any function of alone, because the correction carries the whole history. The quantity that decreases is a distance on the lifted pair in the -norm, not any natural quantity of alone. Whether the progress is monotone is left open in the paper (p. 14), which is why the rates are stated for running averages and running minima rather than for the last iterate. Passing from the progress to the optimality residuals requires a spectral comparison of the quadratic forms of and , which rests on the null-space part of Assumption 1. In Lean, the convergence clause of Theorem 3.3 needs a Fejér-type argument in a non-Euclidean, matrix-weighted norm on .
Rows are EuclideanSpace ℝ (Fin p) and a stacked variable is a function Fin n → EuclideanSpace ℝ (Fin p). The Lean norm on such functions is the sup norm and is never used: the Frobenius inner product is an explicit sum frob, and is the quadratic form mnormSq M x . Matrices act row-wise through mix. is a parameter characterised as the smallest real eigenvalue. is a parameter with , and , which determines it uniquely. Running minima range over , the indices of the sums; and are Mathlib's Landau relations along atTop.
Committed conventions and added hypotheses:
A trivializing formalization is ruled out: the goal assumes neither convergence, nor summability, nor an optimal pair, and its hypotheses are satisfiable (two agents, , , ).
A complete development needs basic linear algebra of symmetric positive semidefinite matrices acting on (null spaces, ranges, comparison of quadratic forms), co-coercivity of gradients of convex -smooth functions (the Baillon–Haddad theorem), and summable-sequence asymptotics. The last two are reusable beyond this mission. Proofs of any milestone, and of general lemmas on matrix-weighted norms of stacked variables, are welcome.
The stochastic block model is the basic random-graph model of a network with communities. It serves as a test bed for clustering algorithms in statistics, machine learning and theoretical computer science. In its sparse two-community form, each vertex has a constant expected degree, and the question is how much of the hidden partition a graph reveals. Using the cavity method of statistical physics, Decelle, Krzakala, Moore and Zdeborová (arXiv:1109.3041, 2011) conjectured a sharp threshold: one can label the vertices better than chance when the signal-to-noise ratio exceeds one, and not otherwise.
Timeline:
Fix and let be the number of vertices. In every vertex receives, independently and uniformly, a label . Then each unordered pair is an edge independently, with probability if and otherwise. Write
for the average degree and the signal strength; may be negative.
An estimator receives only the graph and outputs a labelling, possibly at random. Its overlap with the planted labelling is , with an absolute value because the two communities carry no names. A uniformly random guess has overlap of order .
The proof works with paths in the complete graph: consecutive vertices distinct. A path is non-backtracking if and self-avoiding if all its vertices are distinct. With and , the path sums and add over the non-backtracking, respectively self-avoiding, paths of length from to . An -tangle is a connected subgraph of diameter at most that contains two cycles.
For fixed with there are an estimator and an with
The goal fixes neither nor the algorithm, so it is the weakest form of the conjecture.
Together with the impossibility result for , Theorem 2.1 establishes as the detection threshold of the sparse two-community block model, a threshold first predicted by statistical physics. It equals the Kesten–Stigum bound for reconstruction on the Poisson Galton–Watson tree with the Ising channel, which locally describes the model. The non-backtracking and self-avoiding path statistics behind it led to the later spectral analyses of the non-backtracking matrix and to the multi-community theory.
The theorem is proved on paper. As far as is known, none of its ingredients is machine-checked: no formal statement of the block model, of path-count moments in sparse random graphs, or of tangle-freeness exists in Mathlib. The mission produces a faithful statement of the threshold theorem together with the first-moment, second-moment and combinatorial estimates the proof rests on. These can be attacked independently.
The obvious approach estimates by the sign of the number of length- paths between and , with . Its mean is right: it is of order . Its variance is not under control. With probability about a clique of size appears near and , and on that event the number of paths is so large that the expectation is dominated by a rare configuration. A plain second-moment argument therefore fails. The rare dense structures (tangles) must be excluded by conditioning, and the non-backtracking count must be compared with the self-avoiding one, whose moments can be computed. Even then, the second moment determines only with probability bounded away from . Turning many weakly correlated pairwise estimates into a globally correlated labelling is a separate step close to the threshold, where is barely above one.
Everything is a finite sum. Vertices are Fin n, graphs SimpleGraph (Fin n), labellings Fin n → Bool. The joint law of is written as an explicit weight. Conditioning on the labels of a vertex set is a weighted average with positive denominator . An estimator is a map from graphs to PMFs on labellings, so it never sees and may be randomized. Its success probability is the probability that the overlap, with absolute value, is at least , for an fixed before .
Asymptotic notation follows §1.3 of the paper. is for an explicit chosen before the vertices, sets and labellings it is uniform over. "Sets of size " in a hypothesis means: for every , all sets of size at most . Assumption 2.7 ( and ) and the preamble of Theorem 2.8 (, the choice of , ) are shared definitions, so the four displays of Theorem 2.8 cannot drift apart. Non-asymptotic statements assume , which is Definition 1.1's .
Three printed slips are corrected and disclosed. Theorem 2.8 (2) carries the square that the proof's display (17) gives. Theorem 2.8 (4) uses , since may be negative. Lemma 4.7 assumes distinct endpoints, as all its uses do.
The labelled branching tree of Lemma 3.7 is encoded by its generation counts: the numbers of and labelled vertices at depth form a two-type Poisson chain on , which has the same law by Poisson thinning and superposition. Lemma 3.7 assumes , the standing assumption of its section, and is stated for all sufficiently large , the range its proof covers.
The statements rule out the trivial readings: the estimator cannot see , the overlap carries its absolute value, does not depend on , antecedent bounds are universally quantified, and the model's weights are genuine probabilities for all large .
Reusable infrastructure includes the finite-sum stochastic block model, path edge-type counts, and tangle-freeness. The weights of independent-edge random graphs and the Poisson Galton–Watson tree with the Ising broadcast are also of independent use. Contributions are welcome on any milestone, on infrastructure lemmas such as normalisation of the model's weights and independence of distinct edges given the labels, and on the steps of §3 that connect Theorem 2.8 to the goal.
Many problems in machine learning and statistics minimize an average of component losses, : one term per training example, per data shard, or per block of a decomposed objective. Incremental methods such as SAG, SVRG, SAGA, SDCA and their accelerated variants touch one component at a time, so the natural measure of their work is the number of component queries. When every component is -smooth and -strongly convex, accelerated incremental methods reach accuracy after on the order of queries, while treating as one function and running accelerated gradient descent costs component queries.
Woodworth and Srebro ask how far this can go when the oracle is as strong as possible: for a requested component it returns the value, the gradient, and an exact proximal point, the minimizer of . A proximal step solves a whole optimization problem for that component, so it is not obvious that oracle-complexity lower bounds for gradient methods survive. Their Theorem 4 shows that for deterministic algorithms they do: the full factor is unavoidable (Woodworth and Srebro, 2016, Theorem 4, p. 6). Randomization is what separates this from the upper bounds of accelerated incremental methods, which the paper treats separately.
Timeline. Nemirovski and Yudin (1983) and Nesterov (2004) gave the lower bound for one smooth strongly convex function under span-restricted methods. Agarwal and Bottou (2015) gave finite-sum lower bounds for deterministic methods with gradient access. Lan and Zhou (2018) proved bounds for randomized incremental gradient methods. Woodworth and Srebro (NeurIPS 2016; revised arXiv v3, 2019) handled arbitrary deterministic and randomized algorithms with a gradient-and-prox oracle and no span assumption.
Write with the Euclidean inner product and norm . A finite-sum objective is with components . A component is -smooth if it is differentiable and its gradient is -Lipschitz, and -strongly convex if for all .
A query names a component , a point , and a parameter . The oracle answers with , , and . A deterministic algorithm chooses each query as a function of the answers it has received so far. The quantity bounded from below is the number of queries before some query point satisfies , where minimizes .
The proof works with directions , chosen orthonormal, and indicators with , and the components (at )
With and these define the quantities in the milestones (App. B.4, pp. 16–17).
Let . There are absolute constants such that for every , with , and there is a dimension with the following property. For every deterministic algorithm there are -smooth, -strongly convex on and an exact oracle for them, with a minimizer of and , such that every query point with satisfies
The constants are left unspecified, as in the paper's and .
At , , the proof establishes, in order: the closed form of with the factor ; the minimizer with ; the ratio bound for points orthogonal to ; the exponential bound once ; the choice of that makes the ratio at least ; and the final count (pp. 17–18).
The theorem shows that an exact component prox does not buy a better dependence on the condition number for deterministic methods: the best deterministic method is, up to constants, accelerated gradient descent on itself. Combined with the paper's randomized lower bounds and known upper bounds, it pins down the gap between deterministic and randomized incremental methods at a factor of about . It also tells designers of distributed and incremental solvers that a prox subroutine per component cannot replace randomization.
The result is proved on paper. To our knowledge it has no machine-checked proof. This mission formalizes the complete deterministic argument: the closed-form algebra of the quadratic construction, the geometric decay of its error along the chain, the counting of rounds, and, as the main work, the adversary that keeps the oracle's answers consistent with an algorithm that has not yet found the later directions. Each algebraic step is checked separately, so its constants are verified individually.
The argument from function values and gradients is standard for span-restricted methods. It does not cover this setting, for two reasons. First, the algorithm is arbitrary and deterministic: its query points need not lie in the span of earlier gradients, so the directions must be chosen adaptively, orthogonal to every query made so far. The hard instance therefore depends on the algorithm, and the oracle must be shown to answer every query consistently with one fixed set of components, chosen at the end. Second, the prox answer is the minimizer of a global problem. The proof must show that, while a component has not been queried in round , the prox of the truncated component coincides with the prox of the final one. The paper asserts this step for the strongly convex construction ("a fact which follows directly from the previous proof"). A solver has to carry it out for the extra term.
The algebraic steps are also delicate in their constants: the boundary equation at holds only with , and the final count uses and to keep the logarithm and the floor away from their degenerate values.
Points live in EuclideanSpace ℝ (Fin d). Components are indexed by Fin m (from 0); is written lam. A deterministic algorithm is a function from the list of previous responses to the next query, and an oracle is a fixed function from queries to responses (value, gradient, prox). Query n is the paper's -st. Prox points are a predicate (IsProx), not a choice function, and queries carry . Smoothness is a global gradient that is -Lipschitz, and strong convexity is Mathlib's StrongConvexOn, which for differentiable functions is equivalent to the gradient inequality above. The minimum is an explicit minimizer, never a real infimum. is natural-number division.
Choices that strengthen or pin the page's statement, each disclosed in the items:
The goal mentions none of the proof's objects (, , rounds, , , , , ), so it cannot be made trivial by fixing the construction. Its conclusion requires a genuine minimizer with , so the claim cannot hold for degenerate components.
Needed infrastructure: quadratic forms over orthonormal families, gradients and prox points of quadratics plus , and an adaptive Gram–Schmidt adversary. The model of algorithms and oracles is shared with the companion missions on Theorems 1 and 3 and can be reused for other oracle-complexity lower bounds. Proofs of individual milestones, of the consistency step, and of the scaling from to general are all welcome.
Nonlinear filtering asks for the conditional law of an unobserved Markov process given noisy partial observations of it. It is the computational core of data assimilation in weather forecasting, oceanography and geophysics, of target tracking, and of inference in large networked systems. The standard numerical method, the particle filter, replaces the conditional law by a cloud of weighted samples. Its error is well understood in fixed dimension, but in practice it degrades exponentially in the dimension of the state: the number of particles needed for a fixed accuracy grows exponentially with the number of variables. This phenomenon, the curse of dimensionality of particle filters, has been documented empirically and analysed by Bickel, Li and Bengtsson and by Snyder et al. (Bickel–Li–Bengtsson 2008; Snyder et al. 2008), and it is a main obstacle to their use in high-dimensional data assimilation.
Rebeschini and van Handel (arXiv:1301.6585v2, Ann. Appl. Probab. 25(5), 2015) gave the first rigorous proof that a local variant of the particle filter, the block particle filter, has an approximation error that does not depend on the model dimension, for models with local interactions above a mixing threshold. The result is the standard theoretical reference for localization in sequential Monte Carlo.
Let be a finite graph with graph distance , and fix a neighbourhood size . The -neighbourhood of a vertex is , and the -inner boundary of is . Each vertex carries a Polish state space with a reference measure , and an observation space ; write and .
The hidden process is a Markov chain on with transition density with respect to , where each depends on only through (locality). The observation has density given . For a fixed observation sequence, the filter is the recursion
where applies the transition kernel and reweights by and renormalizes (the Bayes formula).
A partition of into blocks defines the blocking operator , which replaces a measure by the product of its block marginals. The block particle filter with particles is
where replaces a measure by the empirical measure of i.i.d. samples from it. The local quantities are , , and . The error is measured locally:
where is the class of measurable functions depending only on the coordinates in .
There is depending only on such that, if , , and , then for all , , , ,
with depending only on . The goal states the constants existentially, as the paper does, so that it survives any improvement of them.
The proof splits the error through the block filter :
Theorems 4.14 and 4.23 together give Theorem 2.1 by the triangle inequality.
The theorem shows that the error of a local particle filter can be controlled by quantities that are local in the graph: neither the assumptions nor the bound depend on the time horizon or on . On a square lattice, choosing blocks of side length of order balances the two terms and gives a local error, at most locations, that tends to zero as uniformly in time and in the lattice size (the paper's Corollary 2.5, which is not part of this mission): the number of particles needed for a given local accuracy does not grow with the dimension. The result identifies decay of correlations of the filter, established through the Dobrushin comparison theorem, as the mechanism that makes localization work, and it underlies later work on local particle filters and their spatial bias.
The result is proved on paper. No part of it is formalized, and the formal library has no nonlinear filter, no particle filter and no Dobrushin comparison theorem. The mission produces machine-checked statements of the main theorem and of the intermediate results of its proof, with explicit constants for the two halves; proofs of any milestone, or of the goal from Theorems 4.14 and 4.23, are the remaining work.
The obvious argument fails in two places. First, the standard particle filter error bound is uniform in time only through filter stability, and its constants are exponential in the dimension, because the reweighting step compares likelihoods over all of at once. Localizing the sampling (blocking) removes this, but introduces a bias at block boundaries that must not accumulate over time. Controlling that bias requires showing that the filter has decay of correlations uniformly in time, which is a statement about conditional distributions of a high-dimensional measure, not about its marginals. Second, the sampling error must be propagated through the block filter dynamics in a norm strong enough to compose: the weak norm does not contract under the block filter, which is why the paper measures one-step errors in total variation after one further step of dynamics.
The Lean development is in the namespace LocalPF.Block. Committed conventions:
Added or changed hypotheses, each disclosed in the item: strict positivity and integrability of in Theorem 4.14 and Proposition 4.17 (the paper assumes no bounds on there; without them the Bayes formula is undefined); explicit bounds in Lemma 4.2, whose clause is stated for Giry-measurable random probability measures; in Theorem 4.23, excluding only the case where the paper's bound is ; Lemma 4.19 and Proposition 4.22 are stated for every deterministic probability measure in place of the random previous estimate, which is stronger.
The statement admits no trivializing reading: the constants of Theorem 2.1 are quantified before the graph and the model, so they cannot depend on ; the goal and Theorem 4.23 assert that the particle-array law is a probability measure, so a zero law cannot make the expectation vanish; test functions are measurable and bounded, so the integrals are not junk values; excludes division by ; and the correction step's normalizer is positive and finite under the stated hypotheses.
Needed infrastructure: product measures over finite index sets and their marginals, the Giry monad and measurability of the maps it composes, conditional distributions on products of Polish spaces, and matrix Neumann series. The Dobrushin comparison theorem and the V-statistic bound (Lemma 4.20) are reusable beyond filtering. Proofs of any milestone are welcome, and so are formal statements of the remaining results of §4 (Propositions 4.4, 4.8, 4.9, Corollary 4.13).
Many problems in machine learning and statistics minimize an average of convex losses, one per data point or per block of data. Incremental methods such as SAG, SVRG, SAGA, SDCA, Finito and Katyusha exploit this finite-sum structure: each step touches one component instead of the whole average, and for smooth components the best of them reach accuracy with far fewer component evaluations than full-gradient methods. A natural question is how much of this improvement is possible at all, and whether access to stronger per-component information, such as a proximal step, could do better still.
B. Woodworth and N. Srebro, Tight Complexity Bounds for Optimizing Composite Objectives (NeurIPS 2016, arXiv:1605.08003), answer this with lower bounds on the number of component-oracle calls. Their oracle returns, for a requested component, its value, its gradient, and its exact proximal point. Earlier lower bounds covered only gradient access to smooth, strongly convex sums: Agarwal and Bottou (arXiv:1410.0723) for deterministic algorithms, and Lan (arXiv:1507.02000) for randomized algorithms that sample components from a fixed distribution and keep their iterates in the span of the gradients received (p. 2–3 of the paper). Woodworth and Srebro allow any algorithm, any sequence of gradient and prox queries, and iterates anywhere in , in all four combinations of Lipschitz or smooth components and bounded or strongly convex objectives. This mission formalizes the deterministic bound for smooth, not strongly convex components on a bounded domain (Theorem 3 of the paper).
Fix integers and , and write with the Euclidean inner product and norm . The domain is the ball . Given functions , the objective is
A component is -smooth on if it is differentiable and its gradient is -Lipschitz on : for . Each is also required to be convex on .
A query is a triple of a component index, a point and a parameter . The oracle answers it exactly with
A deterministic algorithm chooses its first query, and then each next query as a function of the ordered list of answers received so far. Running against an oracle produces a sequence of query points .
There are absolute constants such that for every and there is a dimension with the following property. For every deterministic algorithm there are convex, -smooth components on the -ball, an exact oracle for them, and a minimizer of over the ball, such that
In words: oracle calls are needed before any queried point is strictly -suboptimal. The constants are left unspecified, as in the paper's and .
The proof (Appendix B.3) builds the components adaptively from orthonormal directions and indicators . The milestones are the claims it states on the way:
The result. Running accelerated gradient descent on , with all component gradients computed at each step, finds an -suboptimal point with oracle calls (§2 and Table 1 of the paper). Theorem 3 shows that this is optimal among deterministic algorithms, up to a constant factor: neither incremental access to single components nor an exact prox oracle improves the order of the deterministic complexity. Randomized algorithms need only between and calls (Table 1, with the suboptimality of the point ), so Theorem 3 also measures the benefit of randomization in incremental methods such as accelerated SVRG: a factor of order in the dominant term.
Formalizing it. The theorem is proved in the paper; it has no machine-checked proof. A formal proof needs the adaptive adversary argument in full: the construction of directions orthogonal to all earlier queries, the consistency of answers given by partial functions, and the explicit linear-algebra of the tridiagonal quadratic. The paper's final count is false for some parameters (for even and ), and the large- construction needs a dimension of order that the stated bound does not allow when ; a complete formal proof settles both points.
The algorithm is arbitrary and adaptive, and it sees exact prox points, which in principle reveal far more about a component than a gradient. The construction must therefore be chosen after the algorithm, round by round, so that every answer the algorithm has received is consistent with the final functions, yet reveals at most one new direction per round. The naive argument, "the algorithm only explores the span of previous gradients", is not available: the algorithm is not restricted to linear spans, and its queries can lie anywhere. Instead, each new direction must be made orthogonal to every point queried so far, and one must show that the partial function used to answer a query has the same gradient and the same constrained prox as the final function at that point (Lemmas 4–5). The constrained prox over the ball is not covered by the paper's unconstrained computation and needs its own argument.
The space is EuclideanSpace ℝ (Fin d). Components are indexed by Fin m (0-based). A query is a structure carrying a component, a point and a parameter with a proof of ; the prox answer is described by the published minimizer predicate BoydADMM.Prox.IsProx, not by a choice function. A deterministic algorithm is a function from the list of earlier answers to the next query, and the oracle is a fixed function of the query, required to be exact on every query. The minimum is an explicit attained minimizer over the ball, never a real infimum.
Committed conventions, each disclosed in the item statements:
A trivializing formalization is ruled out: the goal mentions none of , , rounds, , or , so it cannot be discharged by assumptions about the construction, and the oracle must answer every query exactly.
A full development needs: the adversary construction (orthonormal vectors orthogonal to a finite set of earlier queries), smoothness of the quadratic hard functions (a Hessian bound ), existence of constrained prox points, and the arithmetic of the counts. The tridiagonal linear algebra of milestones 2–3 is reusable for other lower-bound constructions in the style of Nesterov's. Proofs of individual milestones, alternative constructions and a corrected explicit constant are all welcome.
Many operational decisions are made after observing covariates that carry information about the uncertainty: a retailer sets inventory after seeing weather and calendar features that predict demand, a grid operator commits generation after seeing a load forecast. The decision problem is a conditional stochastic program: choose to minimize , where is the uncertain quantity, the covariates and their observed value. The conditional distribution of given is unknown; only joint data are available (Bertsimas and Kallus, 2020).
Kannan, Bayraksan and Luedtke (arXiv:2207.13554) proposed fitting a regression model and adding its empirical residuals to the point prediction at , producing scenarios for a sample average approximation (the ER-SAA). With few data, any such sample average is optimistically biased: the optimal value underestimates the true cost of the chosen decision. Distributionally robust optimization (DRO) over a Wasserstein ball corrects this bias in the covariate-free case, where Mohajerin Esfahani and Kuhn (2018) showed that a suitably sized ball turns the DRO optimal value into an upper confidence bound on the out-of-sample cost. The paper formalized here (Kannan, Bayraksan and Luedtke, 2023) extends that guarantee to the residuals-based setting. Its main result, Theorem 7, is this mission's goal.
Let , and give and the Euclidean norm . The model is
with regression function and zero-mean errors independent of . The conditional distribution is then the law of . Let be a cost and a nonempty compact feasible set. The true objective is .
A known nonempty closed convex set range of is given, with orthogonal projection (the nearest-point map). The data are covariates and errors , with responses for . A regression estimate built from the data has empirical residuals . Two empirical distributions are compared: the true empirical distribution , which needs , and the estimated empirical distribution , which is computable:
Their scenarios differ by , the prediction error at plus the estimation error at .
For the -Wasserstein distance is , with the infimum over couplings of and . The ER-DRO problem (8) with radius is
with optimal solution .
The radius (10) combines two allowances:
The radius is . Its second term inverts Lemma 2 at level .
Under Assumptions 1 and 2 at , , i.i.d. errors, Lemma 2's bound with constants and , the ER-DRO problem with radius satisfies
Theorem 7 gives the ER-DRO optimal value a meaning a decision maker can use. The computed number bounds the true expected cost of the computed decision, with confidence , for every finite . The scenarios are built from an estimated regression function, not from samples of the conditional distribution. The price is an enlarged radius: the covariate-free radius plus a term for the regression error. The same radius drives the paper's asymptotic optimality and rate results (Theorems 9–11).
The theorem is proved in the paper. No part of it is formalized. The covariate-free analogue, Theorem 3.5 of Mohajerin Esfahani and Kuhn, is formalized and proved on the platform (WassDDRO.Consistency.theorem_3_5). This mission adds three things:
The obvious argument copies the covariate-free proof: treat as an empirical distribution of and apply a concentration inequality. This fails. The scenarios are not samples from , and they are not independent: all of them share the data-dependent estimate . No concentration inequality applies to directly. The regression error has to be separated from the sampling error, and each controlled by its own hypothesis, at a fixed covariate .
On the formal side, Lemma 3 needs the triangle inequality for between arbitrary probability measures, which needs a gluing construction. Mathlib does not have it, and on the platform it is an open statement. Lemma 4 needs Minkowski's inequality for a normalized finite power mean. The probabilistic steps act on events whose measurability is not assumed.
Conventions:
EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, and .The integrability hypothesis on is necessary: without it the true law would not be counted in the worst case and the certificate would be vacuous. Centring the ball at instead of would trivialize the mission by removing the regression error, and is excluded.
Needed infrastructure, reusable beyond this mission: the gluing lemma and triangle inequality for ; Wasserstein bounds between empirical measures with matched atoms; nonexpansiveness of the metric projection onto a closed convex set. The general Wasserstein objects are the published WassersteinDRO.Duality definitions. Proofs of any milestone are welcome, as is a proof of Theorem 7 from the milestones.
Many optimization problems minimize the average of component losses: one loss per observation, machine, or term in an objective. When an algorithm can inspect one component at a time, the number of component queries is a useful measure of work. A component oracle can provide more than a value or subgradient: a proximal point summarizes a global minimization involving that component. Woodworth and Srebro ask whether this stronger access reduces the worst-case number of queries for nonsmooth finite sums. Their deterministic lower bound answers the question in the regime of convex Lipschitz components on a bounded Euclidean ball (Woodworth and Srebro, 2016, Theorem 1).
The paper studies deterministic and randomized algorithms separately. This mission concerns the deterministic claim in Section 4.1 and its Appendix B.1 proof. The result is relevant to algorithms that alternate among components and use both local subgradient information and component prox computations. The exact oracle matters: a lower bound for an approximate or restricted oracle would not settle the claim made for the stronger one in this paper (Woodworth and Srebro, 2016, pp. 1, 4–5).
Let and let be convex functions. Their finite-sum objective is , minimized over the closed Euclidean ball for . Each component is -Lipschitz on when for points in that ball. The paper's notation paragraph prints in this definition; the two-point condition is the intended reading (p. 3).
A query chooses a component index , a point , and . The component oracle returns the value , a subgradient of at , and a point minimizing over . The subgradient is global: its defining inequality holds against every point in . A deterministic algorithm chooses its next query from the ordered responses to its previous queries. The oracle is exact and makes a fixed response choice for each query. The paper allows algorithms without a span restriction and defines a round by how many distinct components have been queried, not by how many total queries have occurred (pp. 1, 4–5).
For the appendix milestones, are orthonormal directions and records whether component was missed in round . The hard components and their truncations are the explicit absolute-value sums in equations (6) and (7). These objects support the lower-bound analysis; they do not restrict the theorem's quantified algorithm or hard instance (pp. 5, 11–12).
There are absolute constants such that, for every , , and , some dimension defeats every deterministic algorithm: for that algorithm there are convex -Lipschitz components and a valid oracle whose first query points all obey
where minimizes on . This is the paper's conclusion. The constants are absolute, and the dimension bound expresses its clause (Theorem 1, p. 5).
Appendix B.1 supplies five milestones: the formula and attained minimum of the average hard function, its error gap for a point orthogonal to an unrevealed direction, the query-count inequality, and Lemmas 2 and 3 on subgradient and proximal-response consistency. The first three are quantitative claims for the normalized construction; the last two say that answers derived from a truncated component can remain valid for the final component (pp. 11–13).
The theorem puts a worst-case limit on deterministic methods that can ask for a component prox point as well as a subgradient. Its factor of says that access to individual components does not remove the cost of discovering information spread across the finite sum. The paper compares this lower bound with its deterministic upper bounds, making the query rate tight up to constants in this regime (Woodworth and Srebro, 2016, Table 1 and Theorem 1).
The mathematical result is proved in the paper; this mission asks for a machine-checked proof of its faithful formal statement. The model of exact component queries, deterministic response histories, and constrained proximal minimizers can also support related oracle-complexity developments. None of the new theorem items in this proposal has a machine-checked proof yet. The already published global subgradient definition is reused as a reference.
The theorem concerns every deterministic algorithm, including one whose future queries depend on all responses so far. A single hard function fixed without regard to that interaction does not capture the adversarial information limit established by the paper. The proof must also show that each answer exposed during the interaction is genuinely a value, subgradient, and constrained prox point for one completed family of component functions. Lemma 2 handles the subgradient requirement, while Lemma 3 handles the more global proximal requirement. The latter is delicate because equation (3) minimizes over the ball, whereas the appendix displays an unconstrained calculation (pp. 11–13).
The printed formula in equation (6) can have Lipschitz constant greater than one, contrary to a sentence on page 11. This affects an explicit constant in the proof, though the theorem's rate survives rescaling. A verified development must establish a valid uniform Lipschitz bound and carry its normalization into the final constants (Appendix B.1, p. 11).
Vectors are EuclideanSpace ℝ (Fin d) with its Euclidean inner product and norm. Components use Fin m, a zero-based encoding of the paper's . Query number zero is the first query; a bound on represents the number of queries made through query . The proximal operation is a predicate describing all minimizers over ; each legal query has . The oracle is memoryless and exact for every query, even when its point lies outside . Candidate points in the goal are the algorithm's query points. The dimension is chosen before the algorithm, as the appendix construction permits. The finite average is an explicit sum and is an explicit feasible minimizer, avoiding a default-valued real infimum.
The milestones use , orthonormal directions, binary indicators, and where the average is involved. Their normalization is . Natural-number division represents , and a finite interval starting at one prevents the term from underflowing. The goal quantifies over every deterministic algorithm and demands a valid oracle and an attained minimum; the hard directions, indicators, rounds, and truncations occur only in supporting statements. This rules out a fixed easy instance or an oracle allowed to return arbitrary answers.
The development needs Mathlib's Euclidean-space, convexity, finite-sum, and orthonormal-family libraries and the published global-subgradient definition. Contributions that establish the five milestones, a uniform Lipschitz bound for the hard functions, or the algorithm-dependent construction are within scope. The other deterministic smooth regimes and the randomized results have separate problems and are outside this mission.
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.
Polynomial optimization asks for the global minimum of a polynomial over a set cut out by polynomial equations and inequalities. It contains nonconvex quadratic programming, max-cut, and many problems from control and engineering. Lasserre's hierarchy (Lasserre 2001) replaces this problem by a sequence of semidefinite programs whose optimal values increase towards the true minimum . Under the archimedean condition, Putinar's Positivstellensatz (Putinar 1993) gives asymptotic convergence .
In computations the hierarchy usually reaches exactly at a small order (Henrion and Lasserre), while the theory guaranteed only the limit. Known failures of finite convergence were special constructions, for example the Motzkin polynomial on the unit ball. Nie (2014) resolves this gap: finite convergence holds whenever the classical optimality conditions of nonlinear programming hold at every global minimizer.
Timeline. Lasserre (2001) introduces the hierarchy and proves under archimedeanness. Laurent (2007) and Nie (2013) prove finite convergence when has finitely many complex, respectively real, solutions. Marshall (2006, 2009) introduces the boundary hessian condition and proves that it yields a representation of in the quadratic module. Nie (arXiv 2012, Math. Program. 2014) shows that the classical optimality conditions imply the boundary hessian condition, and derives finite convergence.
Fix polynomials , , and the problem
with feasible set and minimum value . Put . A polynomial is SOS if it is a sum of squares of polynomials. For the truncated ideal and the truncated quadratic module are
and . The order- relaxation is s.t. , with optimal value . The archimedean condition asks that for some and some . The hierarchy has finite convergence if for some .
At a point with active set :
The boundary hessian condition (BHC) at asks for local parameters of the variety near such that for and is locally . In these parameters the linear part of must be with all , and its quadratic part on must be positive definite.
If the archimedean condition holds and CQC, SCC and SOSC hold at every global minimizer of the problem, then
The goal fixes no order and no rate; it asserts exactly the paper's finite convergence.
The theorem turns an algebraic question (does a degree-bounded certificate of exist uniformly in ?) into conditions checkable by linear algebra at the minimizers. Combined with the paper's second main result, that these conditions hold off a proper Zariski-closed set of input data, it shows that finite convergence of Lasserre's hierarchy is generic under archimedeanness. This is the theoretical explanation for the finite convergence observed in practice, and it underlies later work on flat truncation and the detection of optimality in moment relaxations.
Formalizing it produces the first machine-checked statements of Lasserre's hierarchy, truncated quadratic modules and the boundary hessian condition on the platform. The paper's own argument (Theorem 3.1 and the -argument) is short. Two cited results it rests on, Marshall's Theorem 9.5.3 and the Real Nullstellensatz, are proved in the literature but, as far as is known, have no formal proof in Mathlib or elsewhere. The result itself is proved (Nie 2014); none of it is formalized.
The obvious route is Putinar's Positivstellensatz applied to . It gives a certificate for each , but its degree grows as , so it yields only . Finite convergence needs a certificate whose degree is bounded uniformly in , which is a statement about itself, a polynomial that vanishes on and is therefore not strictly positive. Putinar's theorem says nothing there. Marshall's theorem supplies the missing representation under the boundary hessian condition, and its proof uses local real-analytic geometry at the zeros of , together with real algebra of quadratic modules.
Theorem 3.1 asks for a smooth local parametrization of whose first coordinates are prescribed constraint functions, and for control of the Taylor coefficients of in those parameters; Mathlib has the analytic ingredients but no such constructions for real varieties. The Real Nullstellensatz depends on the theory of real fields and real ideals. Neither cited result is available in Mathlib.
Polynomials are MvPolynomial (Fin n) ℝ, points are Fin n → ℝ, and the paper's indices are Fin m; or is allowed. Gradients and Hessians come from formal partial derivatives. SOS is Mathlib's IsSumSq. is a supremum in EReal (it is when the relaxation is infeasible). is a real number that is the least value of on , which excludes only . The archimedean condition is the truncated form of p. 2, equivalent to §2.2's. is Mathlib's vanishingIdeal. The multipliers of SCC and SOSC are the ones that satisfy (1.3)–(1.4). The boundary hessian condition is encoded with a parametrization of near that is an immersion and a homeomorphism onto its image, together with nonsingularity of in the real-algebraic sense ( polynomials vanishing on with independent gradients at ); Marshall's analytic parameters give the same condition, because both requirements are invariant under a change of parameters that fixes .
Several encodings would make the statements trivial or false, and the formalization excludes them. Degree bounds are per term, on each and each (including ), never on the sum. is never a real sSup, which would be on an infeasible relaxation. CQC is linear independence of an indexed family, not of a set, so repeated gradients are dependent. The boundary hessian condition is not defined through the chart of the proof of Theorem 3.1. Finite convergence is , not .
A complete development needs: truncated quadratic modules and their monotonicity; univariate SOS criteria; the Real Nullstellensatz; Marshall's representation theorem; and local parametrizations of real varieties at nonsingular points (Theorem 3.1). The definitions of the hierarchy and of the optimality conditions are reusable for any work on moment-SOS relaxations. Proofs of any milestone are welcome, as are proofs of the cited results under weaker hypotheses.
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.
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.
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.
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.