Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Join-the-shortest-queue (JSQ) is the basic load-balancing rule for a system of parallel single-server queues: every arriving customer joins a queue of minimal length. It is optimal in several senses for homogeneous servers and is the reference policy against which cheaper rules (power-of- choices, join-the-idle-queue) are measured. In the Halfin–Whitt regime, where the arrival rate is with for a fixed , Eschenfeldt and Gamarnik (arXiv:1502.00999) proved that the suitably centred and scaled numbers of queues of length at least one and at least two converge, on finite time intervals, to a two-dimensional reflected diffusion. Braverman (arXiv:1801.05121) justified the interchange of limits (the stationary distributions of the -server chains converge to the stationary distribution of the diffusion). One ingredient of that result is that the diffusion is exponentially ergodic, so it has a unique stationary distribution that is approached at a geometric rate. This mission formalizes the analytic core of that ingredient: a Foster–Lyapunov drift condition for the diffusion's generator.
Timeline. Eschenfeldt and Gamarnik (2015) proved the process-level diffusion limit, the first analysis of JSQ in this regime. Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) showed that a class of load-balancing schemes shares the same diffusion limit. Braverman (arXiv 2018, v2 2019; Math. Oper. Res. 45(3), 2020) proved tightness of the scaled stationary distributions and exponential ergodicity of the limit, which together give the interchange of limits.
The state space is the closed quadrant . For write , , . On the boundary these are one-sided derivatives, and denotes the twice continuously differentiable functions in this sense.
The diffusion limit solves
with a standard Brownian motion and a nondecreasing regulator that increases only when . For with the reflection condition , its generator acts by
The construction of the Lyapunov function uses an auxiliary integer and the fluid operator
the generator of the deterministic fluid path , . A smoothed indicator (a piecewise cubic that rises from at to at ) and two levels define the PDEs
each with the reflection condition. Their solutions are written explicitly in terms of the fluid hitting times (through the Lambert W function) and , and the curves that split into regions .
For every there exist , , a compact set and with on , as in , and , such that
The constants are unspecified and depend only on ; the statement involves no .
By the criterion of Down, Meyn and Tweedie (Ann. Probab. 23, 1995, Theorem 5.2), a drift inequality of the form (5.2) with compact and implies that the diffusion is positive Harris recurrent and exponentially ergodic in the -norm (Theorem 3 and Corollary 1 of the paper). Together with tightness of the prelimit stationary distributions (mission 1 of this series), this gives convergence of the stationary distributions of the JSQ chains to that of the diffusion. That justifies approximating steady-state JSQ performance by the diffusion.
The construction itself is reusable. Solving the fluid-model PDE and exponentiating the solution is a general route from fluid stability to exponential ergodicity of a diffusion. This mission writes that route out for one reflected diffusion with explicit hitting-time formulas.
Status: the result is proved in the paper; no part of it has a machine-checked proof. Theorem 3 and Corollary 1 are not posed, because they rest on the cited Down–Meyn–Tweedie theory and on the existence of the reflected process, neither of which Mathlib has.
The reflecting boundary rules out the first candidates. The condition excludes exponentials of linear functions such as unless . The natural candidate from the fluid model, the exponential of the fluid time needed to reach a box, has a discontinuous integrand and is not in , so cannot be applied to it. The milestone functions , are given piecewise across the curves , and the lines , through implicitly defined hitting times. Three things are hard: regularity across these interfaces, the Lambert W asymptotics as , and second-derivative bounds that hold uniformly on the unbounded domain with the stated dependence on and .
ℝ × ℝ, and is Set.Iic 0 ×ˢ Set.Ici 0. Partials are fderivWithin ℝ f Ω in the coordinate directions, which are one-sided at boundary points. is ContDiffOn ℝ 2 f Ω.WithTop ℝ, with when no solution exists, and its real value is used only where it is finite. (the curve ) is the solution of a nonlinear system whose uniqueness is Lemma 5.Many procedures in high-dimensional statistics reduce to computing the probability that a normalized sum of independent random vectors falls into a set: simultaneous confidence intervals for many means, max-type tests, multiple testing with family-wise error control, and inference after model selection. When the dimension is comparable to or much larger than the sample size , these probabilities are approximated by those of a Gaussian vector with the same covariance, the high-dimensional central limit theorem. That Gaussian law is not available in practice, because its covariance matrix is unknown. The Gaussian multiplier bootstrap replaces it by a Gaussian vector built from the data, whose covariance is the sample covariance, and simulates from it.
Chernozhukov, Chetverikov and Kato, Central limit theorems and bootstrap in high dimensions (Ann. Probab. 45 (2017)), prove that this bootstrap is valid uniformly over hyperrectangles and over simple convex sets (sets sandwiched between a polytope with polynomially many facets and its small enlargement), with error depending on only through . This mission formalizes their abstract multiplier bootstrap theorem, Theorem 4.1.
Timeline:
Let and . Let be independent random vectors in with coordinates , centred () with . Let be independent Gaussian vectors with and set
The multiplier bootstrap: let be i.i.d. , independent of the data , let , and
Given the data, is Gaussian with covariance , while has covariance .
A hyperrectangle is a set with . For a finite set of unit vectors and thresholds , the polyhedron has the enlargement . For constants , a Borel set satisfies condition (C) if for some such polyhedron with facets; denotes this polyhedron and its normals. Condition (M.1′) with constant asks for every . Finally,
Let be a class of sets satisfying (C) and (M.1′). There is depending only on such that for every , on the event ,
The theorem is deterministic in the data: it holds at every realization on the event, and turning it into a rate requires only a bound on .
In the order of the proof (App. E.2, p. 2342):
Theorem 4.1 is the abstract step behind the paper's explicit multiplier bootstrap rates: Proposition 4.1 combines it with maximal inequalities that bound with high probability, and obtains, with probability at least , the rate for simple convex sets with sparse facet normals. In applications it justifies bootstrap critical values for max-type statistics and simultaneous confidence regions when . Remark 4.1, the hyperrectangle case, is the version most used in practice.
The results are proved on paper; none is formalized on the platform. A formal development produces machine-checked versions of the smooth-max sandwich, a Gaussian anti-concentration bound (Nazarov's inequality), a quantitative Gaussian comparison inequality and the bootstrap theorem itself. The comparison display and Lemma A.1 are proved in the paper only by citation ([20] and Klivans–O'Donnell–Servedio, Thm. 20), so formal proofs of them are new work rather than transcriptions.
The obvious route compares and through the Kolmogorov distance of their laws or through a total-variation bound between two Gaussians. Both depend polynomially on and fail when . The proof instead compares smooth functionals of the coordinatewise maximum, where the error depends on only through , and then converts back to probabilities of orthants with an anti-concentration inequality whose constant grows like . Both conversions must hold uniformly in the threshold , and the final bound for simple convex sets requires passing to the -dimensional vectors with , which is why appears. The comparison inequality for is the step with the least existing infrastructure: it is a Slepian–Stein interpolation between two Gaussian laws with explicit control of second derivatives of .
EuclideanSpace ℝ (Fin p); is Mathlib's multivariateGaussian 0 Σ. Independence is iIndepFun; 's law is fixed by P.map (Y i) = multivariateGaussian 0 (covMat P (X i)), and square integrability of each makes covMat positive semidefinite, so this is the genuine Gaussian law.mbLaw x is the push-forward of under , and the bound is asserted at every on the event, for the data . Since is independent of the data, this is a version of the conditional law; no conditional expectation appears.Infrastructure needed: multivariate Gaussian laws and their linear images, Gaussian integration by parts or Slepian interpolation, Nazarov's inequality, and properties of log-sum-exp. Lemma A.1, display (21) and the comparison display are reusable beyond this mission, for the high-dimensional CLT of the companion mission and for any max-type Gaussian approximation. Proofs of any milestone are welcome, as are proofs of the conditional Gaussianity identity from Mathlib's Gaussian API.
Many statistical procedures look at a large number of averages at once: simultaneous confidence intervals for means, multiple testing of hypotheses, the maximum of -statistics. Their calibration needs the joint law of a -dimensional normalized sum, and in modern applications is comparable to, or much larger than, the sample size . Classical multivariate central limit theorems with explicit error, such as Bentkus's bound over convex sets (Bentkus 2003), require to grow slowly with (roughly ), which rules out these applications.
Chernozhukov, Chetverikov and Kato showed that when the class of sets is restricted to hyperrectangles, the Gaussian approximation error depends on the dimension only through (Ann. Probab. 45 (2017)).
Timeline. In 2013 the same authors proved a Gaussian approximation for the maximum of a sum (sets of the form ) with rate (Ann. Statist. 41 (2013)). The 2017 paper extends this to all hyperrectangles, improves the rate to , and adds bootstrap results.
Let and . Let be independent random vectors in with coordinates , each centred () with . Let be independent centred Gaussian vectors with , the same covariance as . The normalized sums are
A hyperrectangle is a set with ; is the class of all of them. The quantity to bound is
The error is measured through the third-moment parameter and the truncated maximal moments
the same with , and . Here is the natural logarithm.
If for all , there are constants depending only on such that for every ,
The constants are left existential, as on the page: the goal asserts the shape of the bound, not particular values.
Under the moment conditions (M.1)–(M.2) and either an exponential (E.1) or a polynomial (E.2) moment bound with parameter ,
The result. Under the exponential moment condition (E.1), Proposition 2.1 makes the Gaussian approximation error tend to zero when , allowing much larger than . Under the polynomial moment condition (E.2), its second error term must also tend to zero. Theorem 2.1 is the probabilistic basis of the paper's multiplier and empirical bootstrap results for simultaneous inference (Chernozhukov, Chetverikov and Kato 2017).
Formalizing it. The result is proved on paper; no machine-checked version of this theorem was found in the platform catalog during this mission's prior-art search. A formal proof needs interpolation between and , Gaussian anti-concentration (Nazarov's inequality), and third-order Taylor estimates of smooth approximations of indicator functions. Nazarov's inequality is used in the paper by citation, so its formal proof is a separate milestone.
The obvious route, a Lindeberg replacement of each by after smoothing the indicator of a hyperrectangle coordinate by coordinate, loses a polynomial factor in : the derivatives of a product of smoothed one-dimensional indicators add up over coordinates, so the error grows like a power of rather than of . Any smoothing must also be paid for by the probability that the Gaussian vector falls in a thin neighbourhood of the boundary of a hyperrectangle, and a dimension-free bound on that probability is not available for general hyperrectangles; the anti-concentration bound is the best one can use. Finally, a direct comparison yields an inequality in which the quantity to be bounded appears on both sides, and the rate is obtained only after that inequality is solved; a one-shot estimate gives a worse power of . The truncation in handles coordinates too large for a third-order Taylor expansion, since no moment condition beyond third moments is assumed.
Vectors live in EuclideanSpace ℝ (Fin p) and the coordinate is X i ω j. The Gaussian comparison vectors satisfy P.map (Y i) = multivariateGaussian 0 (covMat P (X i)) with covMat P Z = (E[Z_j Z_k])_{j,k}, which is positive semidefinite, so this is the genuine ; the are independent. Hyperrectangle endpoints are extended reals used only in comparisons. Every theorem carries the standing assumptions , , independence, centring and finite second moments. Items that involve or add ; when a third moment is infinite the paper's bounds are vacuous, so this loses nothing. is defined by its formula for every real , because Theorem 2.1 evaluates it at , which may be below . Lemma 5.1 and Corollary 5.1 assume the 's independent of the 's, as the definition of does; Theorem 2.1 and Proposition 2.1 do not. A bound on a supremum is stated set by set.
Constants that the paper says depend only on (or on and ) are quantified after and before , , the probability space and every random vector; a constant chosen after , or the law would trivialize every statement. Upper bounds on expectations in hypotheses ((M.2), (E.1), (E.2)) and in Lemma C.1's conclusion are lower Lebesgue integrals, so a non-integrable function cannot make a hypothesis hold with a junk value of . Dropping the independence of the or using a wrong covariance would make the goal false.
A complete development needs: a multivariate Stein or Slepian interpolation, third-order Taylor expansion with remainder for functions on , Gaussian integration by parts, and Nazarov's inequality. The anti-concentration and smooth-max lemmas are reusable for any max-type Gaussian approximation, including the bootstrap results of the second mission of this series. Proofs of individual milestones, of Nazarov's inequality in particular, are welcome on their own.
Many scheduling decisions are not owned by a single decision maker. A machine shared by two departments, a production line serving two customers, or a computing resource shared by two users must process the jobs of two agents, each of which judges a schedule by its own criterion. Agnetis, Mirchandani, Pacciarelli and Pacifici introduced this model in Scheduling Problems with Two Competing Agents (Operations Research, 2004, doi:10.1287/opre.1030.0092), and it became the starting point of the literature on multi-agent scheduling (surveyed in Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer, 2014, doi:10.1007/978-3-642-41880-8).
When neither agent can impose its criterion on the other, the natural object to compute is the set of compromises that cannot be improved for one agent without hurting the other: the Pareto frontier. Section 11 of the paper asks how large that frontier can be for each pair of criteria it studies, because the size of the frontier decides whether it can be listed in polynomial time. This mission formalizes the answer for one agent minimizing its total completion time against the other agent's maximum cost.
Agent owns jobs and agent owns jobs , with . Every job has a positive processing time , is available at time , and is processed without interruption on a single machine that handles one job at a time. Since both criteria below are nondecreasing in completion times, a schedule is a sequence of all jobs processed in that order from time without idle time, and denotes the completion time of .
A schedule is nondominated if no schedule has and with at least one inequality strict. Its nondominated pair is . The constrained problem asks for a schedule with for every -job that minimizes among such schedules; such a schedule is optimal for the bound .
The -jobs of a schedule follow the SPT order when they appear by nondecreasing processing time, equal lengths in index order. A -job overtakes an -job when it moves from after it to before it.
The paper prints the bound . That bound is false: with one job per agent, unit processing times and , the schedules and give the two nondominated pairs and . The corrected bound is the one the printed argument supports.
A frontier of size at most means that the scheme the paper calls PP, which solves the constrained problem for a decreasing sequence of bounds, lists every nondominated pair with polynomially many calls to a polynomial algorithm (Theorem 5.5 of the paper). The contrast with the other criteria of §11 is the point: for two total-completion-time agents the paper exhibits an exponential frontier (Example 11.7). The bound therefore separates criteria whose compromises can be negotiated over an explicit list from those where they cannot.
Formalizing it adds three things. First, the printed statements need corrections: the bound is off by one, and Lemmas 11.4 and 11.5 are false when identical -jobs may be ordered differently in the two schedules. A machine-checked version fixes the exact hypotheses. Second, the monotonicity of overtakes (Lemma 11.5) is a reusable structural fact about parametric scheduling under a tightening constraint. Third, no part of this paper or of two-agent scheduling has been machine-checked before, to our knowledge; the published sequence model the mission builds on comes from the formalization of Moore's 1968 algorithm.
The obvious argument counts overtakes: as the bound decreases, each -job overtakes each -job at most once, so consecutive frontier points differ by at least one new overtake. The step that does not go through as printed is "at most once". Optimal schedules for a given bound are not unique, and two optimal schedules can disagree on the order of identical -jobs and on the position of a -job between them. Then an "overtake" can be undone between two bounds without any change in the objectives. The counting is valid only for a consistently chosen family of schedules, and turning the comparison of optimal schedules for two different bounds into a strict improvement needs an exchange argument with careful bookkeeping of which jobs shift. A second, smaller gap is the base case: the first schedule of the chain carries no overtake and must be counted separately.
Jobs are Fin nA ⊕ Fin nB, 0-based, and a schedule is a duplicate-free list of all jobs; completion times come from the published definition MooreLateJobs.Shared.completionTime (Moore 1968 series), referenced rather than redefined. Processing times are real and strictly positive, the paper's standing convention, which the exchange arguments use. The bound is real; the paper's integer is a special case. Feasibility for the bound is stated job by job. The maximum cost is a finite maximum and requires .
Explicit readings of the paper's phrases:
Set.encard of a set of real pairs, so the goal asserts finiteness as well as the bound; it is not a Set.ncard, which would be on an infinite set.Nothing in the statements is trivial by construction. The goal is about every instance with positive data, its hypotheses are satisfiable, and the counterexample to the printed bound is checked in Lean. The milestones' SPT hypotheses are met by some optimal schedule of every feasible instance, so they are not vacuous. Running times, including the polynomiality of PP and the choice of the decrement in Figure 4, are not formalized.
A complete development needs exchange lemmas for single-machine sequences (moving a job, swapping two adjacent jobs, and their effect on completion times), the existence of SPT-ordered optimal schedules, and a chain-counting argument for nested sets of overtakes. The exchange lemmas are reusable for any single-machine sequencing mission. Contributions of any of these, and of a proof of the corrected bound that avoids the scheme PP, are welcome.
Many constrained optimization problems in operations research have objective and constraint functions that are continuous but not differentiable: maxima of finitely many smooth functions, value functions of inner optimization problems, piecewise-linear costs. For such problems the classical Karush–Kuhn–Tucker theory does not apply directly, and algorithms need a nonsmooth replacement for the condition "the gradient of the Lagrangian vanishes". R. Mifflin's report Semismooth and semiconvex functions in constrained optimization (IIASA RR-76-21, 1976; SIAM J. Control Optim. 15(6), 1977) supplies one. It introduces a point-to-set map built from Clarke's generalized gradients and shows, in §5, that is necessary for optimality of locally Lipschitz problems and, for a class of semiconvex functions, also sufficient as soon as a strictly feasible point exists. The map goes back to Merrill's fixed-point work on differentiable and convex problems; Mifflin's own algorithm for semismooth problems converges to points satisfying , so the sufficiency result says when such points are actual minimizers.
This mission is the third of three on the report. Mission I treats pointwise maxima of compact families of smooth functions, mission II the chain rule for semismooth compositions.
Write for Euclidean space with inner product . For , a point and a direction , the generalized directional derivative is
and the generalized gradient is the set . When exists it is the directional derivative ; is quasidifferentiable at if exists and equals for every .
Let . is semiconvex at with respect to (Definition 2) if (a) is Lipschitz on a ball about , (b) is quasidifferentiable at , and (c) and imply . It is semiconvex on if this holds at every point of . Convex functions and differentiable pseudoconvex functions are semiconvex.
The problem of §5 is to minimize subject to , where . A point is feasible if and strictly feasible if ; is optimal if it is feasible and for every feasible . The map is
and is stationary if and . In Lean these are genGrad, HasDirDeriv, QuasidiffAt, SemiconvexAt/SemiconvexOn, IsFeasible, IsOptimal, Mmap and IsStationary in the namespace MifflinSemismooth.Optimality; is the published ClarkeGradients.Shared.genDirDeriv.
Suppose and are semiconvex on and . Then
The first alternative says the problem is infeasible, the last that it has no strictly feasible point. The theorem carries no constants and holds for any constraint function , not only a finite maximum.
The proof uses, in order: a point with minimizes a semiconvex over (p. 20); on the boundary , the condition yields , , with (p. 20); Proposition 1(b), (p. 3); Theorem 8, for semiconvex on a convex , implies (p. 19); and, if , for every feasible (p. 21).
Theorem 7 (p. 18): for locally Lipschitz , an optimal point is stationary. Theorem 6 (p. 17): for locally Lipschitz , is locally Lipschitz with , where ; semismoothness, semiconvexity and quasidifferentiability on pass from the to , and in the last two cases the inclusion is an equality at points of .
Theorems 7 and 9 together give a nonsmooth Karush–Kuhn–Tucker theory: for semiconvex problem functions with a strictly feasible point, stationarity in the sense of is equivalent to global optimality. For differentiable functions this recovers the sufficiency of the Fritz John conditions for pseudoconvex objectives and constraints (Mangasarian, Nonlinear Programming, Theorem 10.1.1); for convex functions it recovers the saddle-point characterization. Since Mifflin's algorithm produces stationary points, Theorem 9 is the certificate that turns its output into a global minimizer. Theorem 6 lets the constraint stand for a finite system .
The results are proved in the report. None of them, and neither the notion of semiconvexity nor the map , has a machine-checked proof on Prove2Me or in Mathlib as far as the platform search shows; Mathlib has no Clarke generalized gradient. The work is to formalize the known proofs, which also produces reusable facts about (nonemptiness, compactness, the max formula) and about semiconvex functions on convex sets.
The case analysis of Theorem 9 is short; the weight sits in its ingredients. Theorem 8 is the delicate step. Semiconvexity constrains only along directions where , so it says nothing directly about a direction along which does not increase; and a mean value inequality along the segment from to ignores quasidifferentiability and does not determine the sign of . Proposition 1(b) is an attainment statement for a sublinear function whose finiteness rests on the Lipschitz hypothesis, and it fails for the real-valued limsup without that hypothesis. The convex-combination step depends on and being nonempty and convex: the convex hull of a union of two sets need not consist of two-point combinations otherwise. Theorem 7 needs to be closed, which in the boundary case is a statement about the convex hull of two compact sets.
is EuclideanSpace ℝ (Fin n). is a real limsup and equals when the difference quotient is unbounded; every statement therefore has a Lipschitz hypothesis at the points where or is used, and semiconvexity includes "Lipschitz on a ball". is the paper's support-set definition, not the hull of gradient limits. is a relation (HasDirDeriv), never a function with a default value, so Definition 2(c) cannot hold vacuously. "Semiconvex on " means with respect to . "max" is IsGreatest, which asserts attainment. Lipschitz constants are nonnegative reals, which is equivalent to the page's positive constants.
The goal, Theorems 7, 8 and 9 are stated for an arbitrary constraint function ; the paper's is the special case maxConstraint hs with , and Theorem 6 is the bridge. Theorem 9's hypothesis is alone, without feasibility. Theorem 6(c) as printed asserts "for each "; that is false when (, , , ), so it is stated for . A formalization with the hull-of-limits , a junk-valued , a feasibility hypothesis added to Theorem 9, or semiconvexity with respect to a smaller set would prove a different and weaker theorem, and is ruled out.
A complete development needs the basic theory of the generalized gradient (Proposition 1(a), (b)), a Lebourg-type mean value theorem for case analysis along segments, and the finite-max rule. These are reusable beyond this mission, by missions I and II of the series in particular. Proofs of the milestones in any order are welcome, as are proofs of Proposition 1(a) as an auxiliary lemma.
Optimization models often build an objective from several intermediate quantities: constraints, penalties, and transformed measurements are evaluated first, then combined by an outer function. These intermediate and outer functions can be Lipschitz without being differentiable at the point of interest. Ordinary differentiation supplies no chain rule there. The generalized-gradient framework gives a set of possible first-order slopes, while semismoothness provides stronger directional behavior along sequences approaching the point. Mifflin's IIASA report asks whether this behavior survives such compositions and how the generalized gradient of the result relates to those of its ingredients.
The report first establishes basic properties of the generalized gradient in §2, including almost-everywhere differentiability and a nonsmooth mean value theorem. Section 4 then states a chain-rule inclusion as Theorem 4 and the semismooth composition result as Theorem 5. The report is dated December 1976; a journal version appeared in 1977. The mission cites theorem numbers and pages from the report version throughout. No claim about differences between the report and journal texts is needed here.
Work in finite-dimensional Euclidean spaces. Let , for , be component functions, and let be an outer function. Define the component map and the composite by
The functions are locally Lipschitz in the report's precise sense: on each bounded subset of their Euclidean domain they have a finite Lipschitz constant. For a scalar function , a point , and a direction , the generalized directional derivative is the joint upper limit of as and . Its associated generalized gradient is the support set
This is the definition used in Mifflin's report, not an identification assumed in advance with a hull of ordinary gradient limits. Proposition 1(c) supplies that identification under the paper's Lipschitz assumption. The ordinary one-sided directional derivative is the limit of for , when that limit exists.
Mifflin calls semismooth at if it is Lipschitz on a ball about and the scalar sequence has exactly one accumulation point whenever tends to zero, , and . The quantification is over every direction and every such sequence. This pointwise condition is Definition 1 of the report, and its link to one-sided directional derivatives is Lemma 2.
To state the chain rule, form the set
The same is used across all components. The sum is the action of the report's matrix on .
Theorem 4 asserts that is locally Lipschitz and that, at every point,
This is an inclusion, not a general equality. The report gives an example immediately after Theorem 4 in which the inclusion is strict: two identical absolute-value components cancel under an outer difference, while remains larger than .
The goal, Theorem 5, assumes the setting of Theorem 4. If each is semismooth at a selected and is semismooth at , then
The conclusion is pointwise. It does not assert semismoothness throughout from hypotheses at one point. The milestone list contains the chain rule and the source's stated support results: Proposition 2, Lemma 1, Proposition 1(c) and (d), Lemma 2, and the claims (4.2) and (4.11)–(4.12) from the proofs.
Theorem 5 permits composite nonsmooth objectives to be treated within the same semismooth class as their components. Theorem 4 gives a concrete set built from component generalized gradients that contains the composite's generalized gradient. Together, they let later statements about a composite use first-order information from its stated ingredients, subject to the inclusion's possible strictness. These are results proved in Mifflin's report, not open mathematical conjectures.
This mission drafts machine-checkable statements of those known results and their definition layer. The local Lean modules compile with proof placeholders; this staging does not supply machine-checked proofs of the theorems. A complete development would formalize the known arguments or another proof of the same statements. The reusable output would include the support-set generalized gradient, sequence-based semismoothness, the nonsmooth mean value result, and the chain-rule inclusion, all with their source assumptions exposed.
At a point where is differentiable, the component functions need not be differentiable, and the outer function need not be differentiable at . The ordinary smooth chain rule therefore cannot simply multiply ordinary gradients. The candidate is a convex set of combinations of generalized gradients; a single chosen combination does not in general describe all nearby limiting slopes. The report's strict-inclusion example also shows why replacing Theorem 4 by equality would be false. For semismoothness, the condition concerns every admissible sequence of generalized gradients near the point, so checking just one path or one gradient selection does not establish Theorem 5.
The Lean domain is EuclideanSpace ℝ (Fin n) and the outer domain is EuclideanSpace ℝ (Fin m). The report's norm is the Euclidean norm and its pairing is the real inner product. An index of type Fin m represents the components; is admitted, in which case the component space is a point and the composite is constant. A finite sum represents the column-matrix product. The generalized gradient is defined by all directional support inequalities, so Proposition 1(c) remains a theorem rather than becoming true by definition.
The generalized directional derivative is imported from the published definition matching the report's joint limit. Lean's real limsup has a default value for an unbounded quotient; Lipschitz hypotheses are carried wherever that operation is used. “Locally Lipschitz” is imported as Lipschitzness on every bounded subset, and the explicit constants of §2 use nonnegative reals, equivalent to the report's positive constants by enlarging them. The directional derivative is a relation asserting a limit, so no value is assigned when the limit fails. “Exactly one accumulation point” remains an existence-and-uniqueness assertion about cluster points. The report's means positive convergence to zero, as its proof of Lemma 2 says explicitly. These choices exclude a vacuous formulation that only asks about one convenient sequence or gives a default directional value.
The scope includes the two local definition files and the cited theorem statements, including both conclusions of Theorem 4 and Lemma 2. Proof contributions would need finite-dimensional Lipschitz and differentiability infrastructure, limiting-gradient compactness, convex hull and separation facts, and sequence convergence facts. Results about the alternative Qi–Sun vector-valued semismoothness notion are outside this mission's definition layer.
Mean field control studies the optimal control of a very large population of interacting agents through the limit in which the population is replaced by its distribution. The limit problem is a McKean–Vlasov (MKV) control problem: the dynamics and the cost of a representative agent depend on the law of its own state. Such problems arise in systemic risk, crowd motion, energy management and the planning of large distributed systems; the reference account is Carmona and Delarue, Probabilistic Theory of Mean Field Games with Applications I–II (Springer, 2018).
MKV control problems are rarely solvable in closed form, and grid-based numerical methods suffer from the dimension of the state. A practical alternative is to simulate a finite population on a time grid, parametrize the feedback control by a neural network, and minimize the simulated cost by stochastic gradient descent. Carmona and Laurière, Convergence analysis of machine learning algorithms for the numerical solution of mean field control and games: II — the finite horizon case (Ann. Appl. Probab. 32(6), 2022, doi:10.1214/21-AAP1715), quantify how close this computable proxy is to the true optimum. This mission formalizes the statement of their main result and of the propositions and lemmas its proof is built from.
Fix a horizon , a state dimension , a control dimension (controls take values in ), an initial law on , a drift , a volatility (not controlled), a running cost and a terminal cost ; ranges over , the probability measures with finite second moment, compared with the Wasserstein distance .
Problem 1 (the MKV problem). On a probability space carrying a -dimensional Wiener process and an independent , minimize over progressively measurable square-integrable controls
where is the law of .
Problem 3 (the -agent problem). agents with independent Wiener processes and i.i.d. initial states use a common feedback function ; the law is replaced by the empirical measure , and the cost is .
Problem 2 (the computable proxy). With and , the agents follow the Euler scheme
with i.i.d. Gaussian increments , and is the expected time-discretized cost. The feedback ranges over , the one-hidden-layer neural networks from to with hidden neurons and activation ; is -periodic, of class , with .
The standing assumptions (§2.2 and Appendix A of the paper) make affine in (A1), make differentiable in (in in the sense of the L-derivative) with Lipschitz derivatives (A2)–(A3), make strongly convex in (A4), and add the regularity (B1)–(B3), (C1)–(C3). Under them the reduced Hamiltonian has a minimizer , the Pontryagin forward–backward system has a solution with marginal flow , and for a regular decoupling field . The optimal feedback is .
for a constant depending only on the data and on , for all .
Lemma 18 (Lipschitz continuity of ), Proposition 10 (network approximation of a function and its first two -derivatives at rate on ), (C.2) (moment bounds uniform in ), Proposition 13 (stability of under feedbacks close on a ball), Lemma 19 (time regularity of the particle system) and Lemma 14 (strong error of the Euler scheme).
The theorem certifies the standard deep-learning approach to mean field control: the value computed by minimizing the simulated finite-population, discrete-time cost over networks is, up to an explicit error with separate rates for population size, network width and time step, no larger than the true MKV value. The rates also expose where the method loses: the term is a curse of dimensionality in the network step (Remark 11).
The result is proved in the paper (§3 and Appendices B–D); the proof of Proposition 7 is a modification of Carmona–Delarue, Vol. II, Theorem 6.17. None of it is formalized. A formal development would provide the first machine-checked bridge between a stochastic control problem of McKean–Vlasov type and a concrete learning architecture, and its intermediate results (moment and stability estimates for interacting particle systems, the strong error of an Euler scheme with constants independent of the number of particles, simultaneous approximation of a function and its derivatives by periodic networks) are reusable on their own.
Each step rests on research-level analysis. Proposition 7 needs the Pontryagin principle for McKean–Vlasov control, the propagation of chaos for the optimally controlled system, and the Fournier–Guillin rate for empirical measures, whose exponent and logarithmic correction at appear in the bound. Proposition 8 requires approximating the optimal feedback together with its first two derivatives in , because the time-discretization step needs regularity of the approximating network; standard universal approximation results give no control of derivatives, and the available simultaneous approximation results hold only for periodic functions, which forces a localization to a ball whose radius must be balanced against the approximation rate. Proposition 15 cannot be obtained from classical Euler estimates for a system of equations, whose constants grow with : the estimates must be done agent by agent through the empirical measure.
is Fin d → ℝ with the sup norm; every constant is existential, so all statements are norm-independent. Time is ℝ≥0 for processes. Solutions of (2.2) and (3.2) use the published Itô-process predicate Peng1990.SMP.IsItoProcess (for , with continuous paths and the natural filtration of the initial data and the noise); the backward equation of the Pontryagin system uses Peng1990.SMP.SolvesBSDE; is the published WassersteinDRO.Duality.wassersteinDistance. Problem 2 is law-level: the Euler scheme is a deterministic map of initial positions and increments, integrated against ; Lemma 14 couples it with the continuous system through the Brownian increments, as the paper does.
The hypotheses are bundled as Coeff ((A1)–(A4), (B1), (B3), (C1), with witnesses for every derivative; the L-derivative is the Fréchet derivative of the lift on ) and DecouplingField ((2.6), existence of a solution of (2.7) on some Problem-1 space, , (B2), (C2), (C3)). Disclosed readings: 's L-convexity is (A4) without and with right-hand side ; unique solvability of (2.7), uniqueness and Lipschitz continuity of are not assumed (the last is Lemma 18); Proposition 13 lets its constant depend on bounds for , as its proof does; Proposition 15 reads the first bound of (3.16) as . Infima are stated pointwise (), never as a real ⨅, and throughout. The hypothesis bundle is not vacuous: a sorry-free check exhibits the model , , , with , satisfying every assumption on any Problem-1 space. Junk values cannot trivialize the goal: the costs are Bochner integrals whose integrability follows from the assumptions, so a non-integrable cost would only make the claimed inequality harder, never vacuous.
Contributions are welcome at every level: proofs of the milestones, in particular the self-contained Lemmas 14 and 19, (C.2) and Proposition 13; infrastructure for the L-derivative, Itô's formula for the published Itô processes, empirical-measure convergence rates, and trigonometric approximation of periodic functions.
Carbon accounting assigns emissions from a shared supply-chain process to firms that can reduce them. If more than one firm can change the same emissions, charging each firm only a share may leave each with too little incentive to abate. Caro, Corbett, Tan and Zuidwijk study the conflict between avoiding double counting in an emissions ledger and inducing the effort a social planner would choose. Their working paper, published in Manufacturing & Service Operations Management in 2013, states an impossibility result for differentiable, increasing carbon-payment rules. It covers multiple firms, processes, and abatement actions, where a process can be influenced by several firms.
The question matters when a carbon footprint is used as a payment base rather than only as a report. A payment rule changes a firm's private incentive to exert costly effort. The rule may also include transfers between firms, so its incentive effect cannot be judged by looking at a single firm's allocated emissions alone. The paper asks what aggregate marginal payment is necessary if decentralized choices are to reproduce the social first best.
Timeline. Holmström (1982) showed for a team with one joint output and one-dimensional efforts that no budget-balanced sharing rule supports the efficient efforts as a Nash equilibrium (stated in the paper as Proposition 1, p. 11). Charging every team member the full social cost ("charging everything to everyone") is known to restore efficiency, as the paper recalls on p. 12. Caro, Corbett, Tan and Zuidwijk (2012 working paper, 2013 journal version) extend the impossibility to many processes, many abatement actions per firm and an explicit influence structure between firms and processes. They also characterize the linear rules that achieve the first best.
Let be a finite set of firms and a finite set of emission-producing processes. Firm chooses a vector of abatement efforts in , with . The full profile is . Firm 's profit before carbon payments is , concave and componentwise decreasing in its effort. Process 's footprint is , convex and componentwise decreasing in the collective effort, and nonnegative on the feasible box. The functions are differentiable, as assumed in the paper's model.
The influence matrix has entries in . An entry is one when the sum of the partial derivatives of with respect to firm 's actions is negative. The paper treats this matrix as independent of the effort profile. Joint carbon production means that a process has at least two influencing firms: for some , .
The societal cost per unit of footprint is . The social first best maximizes
over the effort box. The paper assumes that this solution is unique and that the effort bound is large enough for the relevant optimum to be interior. The first-best footprint is .
A carbon-based payment rule charges firm as a function of the observed footprint vector , rather than the unobserved effort profile. In the social-planner setting of equation (5), , where is its footprint allocation and the transfers balance: for . A Nash equilibrium is a feasible effort profile where no firm improves by changing its own entire effort vector while the other firms hold theirs fixed. At a footprint vector , the rule double-counts process when .
The goal is Proposition 2, evaluated at the first-best footprint:
The paper defines double counting existentially over footprint levels. Its Appendix A.1 proves the stronger assertion at , which is the target here. The rule remains of the form (5), with balanced internal transfers on the nonnegative footprint domain.
Two source statements form the milestone list. The necessary part of Lemma 7 gives equation (14): at an interior first best that is also a Nash equilibrium, the sum over processes of each footprint derivative times the gap between the firm's marginal payment and is zero, both with and without the influence indicator . Equation (18) says that if aggregate marginal payments do not exceed at , every individual process contribution to that sum is zero. The mission also drafts the sufficient part of Lemma 7 and Proposition 3, which characterizes the linear rules with : they implement precisely when .
Proposition 2 identifies a limit on footprint-based incentives under joint production. With more than one firm able to lower a process's emissions, a differentiable increasing rule that implements the first best cannot keep every aggregate marginal charge at or below the social carbon price. Balanced transfers among firms do not remove that requirement. Proposition 3 supplies a complementary characterization for linear payments, identifying which firms must bear the full marginal charge for the processes they influence. These are results proved in the paper, not open conjectures.
The formalization contributes a precise, reusable model of finite effort profiles, process footprints, unilateral deviations, and coordinate marginal payments. It also separates a global Nash best-response condition from first-order identities, so the necessary condition in Lemma 7 has mathematical content. The listed Lean theorems are draft statements with proof holes; they do not yet have machine-checked proofs. Completing them would formally verify the paper's stated claims under the declared model conventions.
The obstacle is the interaction between a shared footprint and unilateral decisions. A firm's payment derivative with respect to a process footprint is multiplied by that firm's own effect on the process, while the social objective prices the total footprint at . A condition on the sum of marginal payments alone does not specify the charge faced by each influential firm. With several actions and processes, the necessary condition is a sum over process contributions, so it cannot simply be read as a coordinatewise equality without further assumptions. These issues occur even though all effort and process index sets are finite.
Lean represents firms, each firm's action indices, and processes by finite types. Efforts and footprints are real-valued functions. The firm and collective effort boxes are closed coordinatewise intervals, with ; optimality and Nash equilibrium quantify over all feasible profiles or unilateral deviations. Coordinate partial derivatives use one-variable derivatives after replacing the corresponding coordinate. Payment rules are functions on real footprint vectors and “increasing” means componentwise nondecreasing.
The source's sign test for does not name an effort profile. The formalization pins it to every profile in the effort box, matching the paper's use of a fixed influence matrix. Interiority is required only of the named first best. The paper's “without loss of generality” nonempty row and column sums for are omitted because the results do not use them; the strict part of its cost monotonicity is likewise unused. Its participation condition (3) is outside the decentralized game (4) and is not added to Nash equilibrium. Equation (5) and transfer balance are imposed only for nonnegative footprint vectors, as printed. The effort bound and Proposition 3's matrix have distinct names.
The first best is a feasible global maximum, not a default-valued real supremum; Nash equilibrium tests full unilateral deviations, not stationarity. These choices rule out a vacuous first-best target and a first-order surrogate for the game. The supporting definitions of finite effort boxes, coordinate derivatives, social value, and Nash best response are useful beyond the final impossibility statement. Contributions that prove the source's necessary and sufficient conditions, the linear characterization, or the goal against these definitions are within scope.
The two-dimensional directed polymer is a random walk whose paths are reweighted by a random space-time environment. Its logarithmic partition function is a discrete counterpart of the height field of the two-dimensional Kardar–Parisi–Zhang equation. At the intermediate-disorder scale, the random weighting becomes weaker as the walk grows, yet its fluctuations remain visible. Caravenna, Sun and Zygouras prove that throughout the subcritical regime , spatial averages of the centred log-partition function converge to Gaussian fluctuations described by an additive stochastic heat equation (Theorem 1.6, p. 6).
The polymer formulation matters because it is a concrete finite-path model: each partition function is an average over finitely many nearest-neighbour walks, while its limit retains the effect of disorder at every scale. The same paper treats the continuum KPZ equation separately; this mission takes its stated polymer theorem as the target. Earlier work in dimension studied a different intermediate-disorder scaling and a Wiener-chaos limit (Alberts, Khanin and Quastel, 2014). The two-dimensional result concerns a distinct regime and a different limit.
Let be the simple symmetric random walk on . Starting at , it chooses each of its four nearest-neighbour steps with probability . Write , and let be an independent copy. Their expected overlap through time is
For a fixed , the disorder strength is . The environment consists of independent, identically distributed real random variables with mean zero, variance one and finite exponential moments at all sufficiently small positive arguments. Its logarithmic moment generating function is . The law also obeys the paper's concentration assumption (1.20): convex 1-Lipschitz functions of any finite collection of environment variables have stretched-exponential deviations from a median, measured with Euclidean distance (pp. 5–6).
For a length- walk from , sum over times , exponentiate, and average over paths. The result is the partition function . Where is finite, its centring gives . A restricted function samples disorder only from the space-time sites in . Section 2 uses an early window near the start and a late window to define , its remainder , and (pp. 7–9).
At macroscopic time and position , the fluctuation field is
The floor of a vector is componentwise. In the numerator, uses the disorder strength ; the field is divided by , exactly as in (1.23).
For every and smooth compactly supported test function , Theorem 1.6 asserts
The tested limit is centred Gaussian. Its variance is , where
The milestone list follows the paper's stated results: second-moment bounds (3.2)–(3.4), higher moments for some (3.12), a left-tail bound (Proposition 3.1) and the negative and logarithmic moments it yields (3.14)–(3.16), vanishing spatial averages for two error terms (Propositions 2.1–2.2), replacement by the late-window term (Proposition 2.3), and the Gaussian limit for that term (Proposition 2.4). These are the exact result labels used in Sections 2 and 3 (pp. 8–13).
The theorem identifies the fluctuation law of the logarithm of the polymer partition function for every strictly below the critical value . The coefficient records the disorder strength in the limiting covariance, and the time reflects the two-dimensional walk's covariance convention. Without the spatial averaging and normalization, the statement would concern a different observable; the theorem characterizes a field tested against compactly supported functions (Theorem 1.6 and Remark 1.7).
The result is proved in the cited paper. This mission asks for a machine-checked proof of that known result and its curated supporting statements. The reusable output includes a finite-path polymer model on , a precise restricted partition function, the disorder concentration assumption, and the Gaussian covariance functional. The published atomic polymer model already supplies the space-time cells, steps, walk positions and log moment generating function; this mission extends that common base to the centred, spatially shifted model of this paper.
Pointwise size does not identify the limiting spatial fluctuations. The early-window partition function captures much of at a fixed site, yet its averaged logarithm vanishes at the target scale. The small remainder cannot simply be discarded: after division by the early-window function, its late-time component carries the Gaussian limit. The paper separates these effects in Propositions 2.1–2.4 and needs moment and left-tail control to keep the logarithmic expression meaningful (Sections 2–4). A direct Taylor expansion of around its mean would lose this distinction.
Lean uses finite sequences of four-neighbour steps and the Euclidean norm on . Disorder is a family indexed by positive walk times and lattice sites; the time-zero row of its ambient type is unused. The full and restricted partition functions are finite walk averages. The concentration assumption quantifies over Euclidean 1-Lipschitz convex functions and their medians. The test class of Theorem 1.6 is ; the four Section 2 propositions use . Treating “smooth” as analytic would make compactly supported tests trivial, so the Lean statement uses the smooth differentiability order.
The target additive stochastic heat observable is represented by its Gaussian law and the kernel above; the random field itself is not formalized, and the statement does not need it. The kernel takes extended nonnegative values because it is infinite on the diagonal; the diagonal has zero area in the tested covariance integral. Moments and convergence use extended nonnegative integrals. The paper assumes exponential moments only near zero, so bounds whose printed form quantifies over every are stated for all sufficiently large , avoiding default values of the logarithmic moment generating function at early indices. The spatial sums have finite support because the test functions do. Replacing the Euclidean norm by the sup norm would change the early window (a square instead of a disc), the kernel and the class of 1-Lipschitz functions in (1.20), so all of these are Euclidean. The polymer propositions are stated for every window exponent below a threshold, as in (2.2), and the passage from the time-1 lattice averages of Propositions 2.1–2.4 to the general-time integral of Theorem 1.6 is part of the proof work, not of the statements. Contributions to the polymer moments, left-tail estimate, replacement propositions and Gaussian limit all feed the stated goal.
A retailer that decides which variants of a product to stock (its assortment) trades off the revenue each variant brings against the operational cost of carrying it. The classical model of this trade-off uses the multinomial logit (MNL) model of consumer choice: a consumer who does not like what the store offers simply buys nothing (van Ryzin & Mahajan 1999). In practice a consumer who does not like what the store offers can also go elsewhere. Cachon, Terwiesch and Xu (working paper, December 2002; published in MSOM 7(4), 2005) add this consumer search to the MNL model and ask how it changes the retailer's optimal assortment.
They study two search models. In the overlapping assortment model (§3.1), a consumer who searches pays a search cost and then finds a competitor carrying every variant, so search can only reveal variants the store does not carry. This mission formalizes the paper's Theorem 6 about that model: when search is cheap, the store's best response is to carry everything.
There are variants, , and an assortment is a subset ; write for the variants the store does not carry. A consumer's utility for variant is , where is the variant's expected net utility and the shocks are independent with the zero-mean Gumbel distribution function , with scale and Euler's constant. The no-purchase option is a "faux variant" with utility . Its preference is , and is the preference of not buying.
Without search, variant has the MNL demand (2), . Following Theorem 1, put and
the probability that every option the store offers, including not buying, has utility at most . The best utility outside the store, , has a density . A consumer whose best in-store utility is searches when the expected gain exceeds the cost,
and the search threshold is the solution of , equation (4). Theorem 3 gives the resulting demand,
When the store carries everything there is nothing to search for (p. 28: "If the retailer offers the full assortment, there will be no consumer search"), so .
Variant earns margin per unit and costs to carry, where is concave and increasing (economies of scale). The retailer's profit is
As printed, the second line of (13) writes where is meant; the definition uses the latter.
If the full assortment is profitable, , then there is a such that
The threshold depends on the data but is one number for all assortments .
Theorem 6 separates the overlapping model sharply from the no-search MNL model and from the paper's independent-assortment model. In those two models every variant in an optimal assortment must earn a strictly positive profit, because dropping a loss-making variant only shifts demand to the remaining ones. In the overlapping model the assortment also controls whether consumers leave: carrying an unprofitable variant can pay because it removes a reason to search. Theorem 6 is the extreme form of this effect, stating that the motive to prevent search can override the profitability of individual variants entirely (§4.3, p. 17).
The paper gives only a short sketch of the proof. The steps it asserts without proof are the existence and uniqueness of , its monotonicity and limits in , and the explicit density . This mission states each of them as a milestone. No machine-checked version of any of these results is known.
The search threshold is defined only implicitly, through an improper integral of the density of a maximum of Gumbel variables. Each property the theorem needs (that the equation has exactly one root, that the root moves monotonically with , and that it escapes to as ) has to be read off the integral. That means controlling on the whole real line: its convergence, its strict decrease, and its limits at .
The final comparison is not a direct consequence of either. A variant's profit tends to rather than to , so the conclusion depends on the sign of , and must be chosen uniformly over all assortments.
The shared model is the definition AssortSearch.FullAssort.Model, which builds on the published MNL share RetailVariety.Structure.share. Its conventions:
Fin n, numbered from 0; the paper's variant is index . The no-purchase option is not a variant: is a separate positive real.Real.eulerMascheroniConstant.Finset (Fin n), including , whose profit is .Several formalizations would make the goal trivial or empty, and each is excluded:
A complete development needs the integral calculus of the Gumbel tail ( and its derivative in ) and the product-measure computation of the law of a maximum of independent variables. Both are reusable beyond this paper, for instance in other search and extreme-value models. Contributions are welcome on any milestone, and on helper lemmas such as the continuity of and its limits at .
A graph is 3-colorable if its vertices can be colored with three colors so that adjacent vertices get different colors. Deciding 3-colorability is NP-complete in general, and one of the standard ways to map the boundary between easy and hard cases is to forbid an induced subgraph. For the path on vertices, 3-colorability of -free graphs was known to be polynomial (Randerath and Schiermeyer, 2004, reference [21] of the paper), and Randerath, Schiermeyer and Tewes asked in 2002 whether the same holds for .
Bonomo, Chudnovsky, Maceli, Schaudt, Stein and Zhong (Combinatorica, 2017) answered this question. Their Theorem 1 states that the list version, in which every vertex may only receive a color from a prescribed list , can be decided for -free graphs in time . The algorithm first reduces the instance to a polynomial number of configurations described by a seed, and then calls Lemma 11 (p. 14) on each configuration. Lemma 11 rests on one structural fact about -free graphs, Claim 13 (p. 16), which is the goal of this mission.
Timeline:
All graphs are finite and simple. For a set of vertices of a graph , is the set of vertices outside with a neighbor in , and . A graph is -free if it has no induced subgraph isomorphic to .
A palette assigns each vertex a list . A seed of is a nonempty set that induces a connected subgraph, is 2-dominating (every vertex is at distance at most from ), and satisfies for and for .
The Lemma 11 setting consists of a graph , a palette and a seed such that
For , is the set of with , and . For , is the set of for which is not complete to , and for the paper fixes non-adjacent , .
In the Lemma 11 setting, let , , and let , be non-adjacent. Then
Claim 13 says that the neighbor triples of the vertices of pairwise touch. This is what allows the proof of Lemma 11 (Claims 14 to 17) to refine the palette of all of simultaneously with only polynomially many guesses: without it, the vertices of could interact independently and the number of cases would be exponential. Claim 12 and display (1) are the general tools for building long induced paths through a seed, used throughout §3.1.
The paper's result is proved and published. None of it is formalized in a proof assistant as far as the platform's index shows. This mission produces a machine-checked version of the structural core of Lemma 11, and the definitions it needs (seeds, the Lemma 11 setting, the sets and ) are reusable for the rest of the paper's argument.
The proof of Claim 13 is short on paper, but it assembles an induced from three pieces: the path through given by Claim 12 and the two short paths and . Showing that the union is induced requires every non-adjacency between the pieces, and these come from different hypotheses: the stability of , the fact that has no neighbor in , the list structure of the vertices of next to , and part (c) of Claim 12. Claim 12 itself is an extremal argument (choose the neighbor closest to an end of a path), which in a formal setting requires explicit manipulation of paths as sequences of vertices: splitting, reversing and concatenating them while keeping them induced. The obvious approach of taking any shortest path through between two of the four vertices fails, because such a path can have interior vertices adjacent to the other two.
Graphs are SimpleGraph V on a finite type V with decidable equality; vertex sets are Finset V. The colors are 0,1,2 in Fin 3, and a palette is V → Finset (Fin 3). -freeness is the negation of Mathlib's induced containment IsIndContained of pathGraph 7; ordinary subgraph containment would be a different, much stronger condition. Connectedness uses Mathlib's Connected, which includes nonemptiness. An induced path is the published platform definition StrongPerfectGraph.Main.IsInducedPath (a nonempty list of distinct vertices in which two vertices are adjacent exactly when consecutive); its ends are the first and last list entries and its interior is the list with both ends removed.
The Lemma 11 setting is a structure Lemma11Hyp G L S bundling its hypotheses. Lemma 11's own conclusion, a decision procedure with running time , and the running time of Theorem 1 are not formalized, since there is no machine model. The paper's arbitrary choice of is replaced by quantification over every non-adjacent pair , , which is Claim 13 for every possible choice. The case is allowed.
One hypothesis is added to Claim 12: the four vertices are pairwise distinct, and the ends of the path are required to be distinct. The paper's proof and its use in Claim 13 take the four vertices distinct; without the assumption the claim can fail, and without a one-vertex path would satisfy it vacuously.
The following trivializing readings are excluded: dropping the overline in "anticomplete to " (which, together with milestone 3, would force to be isolated); a one-vertex path or repeated vertices in Claim 12; and subgraph instead of induced-subgraph containment for -freeness. The setting is satisfiable with : the 5-cycle with , , , , , satisfies every hypothesis, with .
Proofs of the milestones and the goal are welcome, as are general lemmas about induced paths as lists (subpaths, concatenation through a connected set) that would serve other graph-theory missions.
Twin-width is a graph parameter introduced by Bonnet, Kim, Thomassé and Watrigant in Twin-width I: Tractable FO Model Checking (J. ACM 69(1), Article 3, 2021; arXiv:2004.14789). Its main theorem says that first-order model checking is fixed-parameter tractable on every class of graphs of bounded twin-width, provided a witnessing contraction sequence is given. This turns every class shown to have bounded twin-width into a class on which a whole logic becomes algorithmically tractable, so the question "which natural classes have bounded twin-width?" has direct algorithmic content.
Section 4 of the paper answers that question for several classes. This mission covers the geometric part of Section 4: -dimensional grids, grids with diagonals, and unit -dimensional ball graphs with bounded clique number. Geometric intersection graphs are a standard source of hard instances in parameterized algorithms. Width parameters designed for dense graphs (rank-width, clique-width, boolean-width) are unbounded already on the planar grid, whereas twin-width stays bounded on grids of every fixed dimension and transfers from there to ball graphs.
All graphs are finite and simple. Two vertex sets of a graph are homogeneous if every pair is an edge or no pair is. For a partition of , the red degree of a part is the number of other parts not homogeneous to ; is a -partition if every red degree is at most . The graph has twin-width at most , , if there is a sequence of -partitions of that starts with the partition into singletons, ends with at most one part, and in which each partition arises from the previous one by merging two parts. This is the paper's partition form of its definition by contractions of trigraphs (graphs with black and red edges, §3).
For the all-red trigraph , in which every edge of is red, the paper's contraction rule never produces a black edge, and two parts are red-adjacent exactly when some edge of joins them. The red twin-width is defined as above with this adjacency.
For , the -dimensional -grid has vertex set , with iff . The grid with diagonals has the same vertices, with distinct iff , and is its all-red trigraph; is the all-red trigraph of .
Given centres for in a finite set , the unit ball graph joins distinct iff the closed unit balls around and meet, that is . Its clique number is the largest size of a set of pairwise adjacent vertices. A subgraph of is obtained by deleting vertices and edges.
For every , every subgraph of a unit -dimensional ball graph with clique number at most satisfies
A companion item, Theorem 4.1 (p. 3:13, graph case), states that adding one vertex joined to an arbitrary set at most changes twin-width from to .
The goal theorem places unit ball graphs of bounded clique number, in every fixed dimension, among the classes of bounded twin-width. Combined with the paper's main theorem, and with the paper's remark that a contraction sequence can be computed in polynomial time from a geometric representation, it gives fixed-parameter tractable first-order model checking on these graphs. The clique-number hypothesis is needed: unit disk graphs without a clique bound have unbounded twin-width (p. 3:16), as shown in Twin-width II. Theorem 4.3 and Lemma 4.4 are of independent use as twin-width bounds for grids, and the subgraph statements show that grids are an exception to the general fact that bounded twin-width is not preserved by taking (non-induced) subgraphs (p. 3:13).
All results here are proved in the paper. To our knowledge none of them, and no notion of twin-width with red degree, is machine-checked in Lean or Mathlib. The work is to formalize the paper's arguments: the parallel contraction of grid layers, the supercell contraction, and the geometric counting.
Twin-width is not monotone under subgraphs, so the obvious route, "a unit ball graph of bounded clique number is a subgraph of a grid-like graph, hence has bounded twin-width", fails as stated. The paper repairs it by working with all-red trigraphs throughout: for an all-red trigraph, removing edges can only remove red adjacencies, and this is why Theorem 4.3 is proved in its red form and Lemma 4.4 is stated for . A second difficulty is bookkeeping: the bound comes from contracting the layers of "in parallel" and tracking the red degree of every vertex at each step, and Lemma 4.4 is asserted "by the arguments of Theorem 4.3" without a separate proof, so its argument has to be reconstructed.
Lean represents twin-width by the predicates TwinWidthLE G d and RedTwinWidthLE H d on finite vertex types: an explicit sequence of Finpartitions of the vertex set from ⊥ (singletons) to at most one part, consecutive partitions differing by one merge of two distinct parts. Twin-width is never a number, so no infimum over an empty set enters. is Fin d → Fin n; centres live in EuclideanSpace ℝ (Fin d) with the Euclidean distance; balls are closed of radius , so centres at distance exactly are adjacent. is the natural-number ceiling of the real square root. "Clique number " is encoded as CliqueFree (k+1) (clique number at most ), which is the same theorem because the bound is monotone in ; subgraphs are a finite vertex set together with a graph on it.
The hypotheses , appear in Theorem 4.3, its red form, and the grid-subgraph statement, as on the page ("positive integers"). No other hypothesis is added; Lemma 4.4, the cell bound and the goal hold as stated also for or . The red-degree count uses "some edge joins the two parts", which is derived from the paper's contraction rule for trigraphs without black edges and is used only for all-red trigraphs; the twin-width of graphs counts non-homogeneous parts. This rules out the trivializing readings: a twin-width defined as an infimum that defaults to , a sequence allowed to jump to one part, homogeneity counted as adjacency for graphs, or a bound depending on the graph. The polynomial-time sentence of Theorem 4.5 is not formalized.
Reusable infrastructure: the partition-form twin-width predicates (shared with the other missions of this series), grids and grids with diagonals in coordinates, and unit ball graphs. Contributions are welcome on the general lemmas (induced subgraphs, red-to-black transfer, small explicit sequences) as well as on the grid theorems themselves.
Twin-width is a graph parameter introduced by Bonnet, Kim, Thomassé and Watrigant in Twin-width I: Tractable FO Model Checking (J. ACM 69(1), Article 3, 2021; arXiv:2004.14789). Its main algorithmic consequence is that first-order model checking is fixed-parameter tractable on graphs given with a contraction sequence of bounded width. A parameter of this kind is useful only if the classes it bounds are closed under the constructions that arise in practice. Many such constructions are first-order definable: the complement of a graph, its square (join vertices at distance at most two), the map graph of a planar map. Section 8 of the paper shows that twin-width is stable under every such construction: a first-order interpretation of a class of bounded twin-width has bounded twin-width. Bounded VC-dimension, by contrast, is not preserved (interval graphs have VC-dimension at most two but interpret every graph, p. 3:41).
The result has since become the basis of the "model-theoretic" view of twin-width: bounded twin-width classes are closed under first-order transductions (Theorem 8.1 of the paper), and later work identifies them, among ordered structures, with the monadically dependent classes (Twin-width IV, Bonnet, Giocanti, Ossona de Mendez, Simon, Thomassé and Toruńczyk).
Let be a finite simple graph on a vertex set .
Two vertex sets are homogeneous if all pairs in are edges or none is. For a partition of , the red graph has the parts as vertices, two distinct parts being adjacent when they are not homogeneous. is a -partition if has maximum degree at most . The graph has twin-width at most , , if there is a sequence of -partitions from the partition into singletons to a partition with at most one part, each obtained from the previous one by merging two parts (p. 3:32).
A prenex formula of depth with two free variables is
with a Boolean combination of atoms and , . The interpretation is the graph on in which distinct are adjacent iff . For a class , is the class of all induced subgraphs of the graphs , .
The proof works with morphism-trees. The complete tree has as nodes all tuples of vertices with , the parent of a tuple being its prefix. Two sibling nodes are equivalent in if an automorphism of the tree swaps them, preserving equalities and adjacencies among the entries of every tuple and the part of of every entry. A reduction deletes one of two equivalent siblings with its subtree, repeatedly; a reduct admits no further reduction. Two vertices are adjacent in when and are equivalent in some reduction of , and is the partition into the connected components of .
For every prenex formula and every there is such that
The bound depends on and only. No explicit function is asserted: the paper gives none (the proof goes through a tower-type bound on reducts).
Theorem 8.3 turns every first-order definable graph construction into a source of bounded-twin-width classes: squares and fixed powers of planar graphs, complements, map graphs (as transductions, via Theorem 8.1), -planar graphs and bounded-degree string graphs. Combined with the model-checking algorithm it gives FPT first-order model checking on all these classes, provided a contraction sequence is available. The theorem is also the first step of the model-theoretic characterisations of bounded twin-width in the later papers of the series.
The result is proved in the paper; no machine-checked proof of it, or of any twin-width bound, exists to our knowledge, and Mathlib has no notion of twin-width or of first-order interpretations of graphs. The mission asks for a formal proof of the graph case. The morphism-tree milestones are also the combinatorial core of the paper's linear-time model-checking algorithm (Theorems 7.5, 7.15), whose running-time statements are not part of this mission.
The obvious approach refines the -partitions of by the "type" of each vertex with respect to . The number of such types is not bounded: a vertex's behaviour depends on the whole graph through the quantifiers. The paper replaces types by the components of , defined through reductions of morphism-trees that respect . Two facts must then be shown, and neither is local in an obvious way. First, the number of components inside a part is bounded (Lemma 8.5); this needs the pruned shuffle, which assembles a reduction of the whole tree from reductions of the local trees , and the fact that it commutes with reductions (Lemma 7.12), where an automorphism of one local tree must be extended to the shuffle without breaking adjacency between non-homogeneous parts. Second, far-apart components are homogeneous in (Lemma 8.6), which needs the evaluation argument of Lemma 8.4 inside a reduction of the partitioned tree.
SimpleGraph V on a Fintype with decidable equality. Twin-width is the predicate TwinWidthLE G d in the paper's partition form (pp. 3:12, 3:32); trigraphs are not formalized, and twin-width is never an infimum, so no junk value of sInf can make a bound vacuous. Merge steps merge exactly two distinct parts, so a sequence cannot jump to one part.FirstOrder.Language.graph.Formula (Fin 2), evaluated in G.structure; variable 0 is , variable 1 is . Prenex is Mathlib's IsPrenex; quantifier depth qdepth is defined in the mission ( counts once).Set (List V)), the paper's identification of a node with its current path (p. 3:30), which is exact for reductions of complete trees. Equivalent siblings are distinct. Distances in are in , so disconnected parts are far apart. The sequence graph uses 0-based indices, hence the exponent . The pruned shuffle is defined by its characterisation (each component of the sequence graph of a tuple lies in the tree of its local root). Lemmas of §7.3 carry its standing assumption .Reusable beyond this mission: the partition form of twin-width, quantifier depth of first-order formulas, and the morphism-tree machinery (reductions, pruned shuffles), which formalizes the algorithmic core of first-order model checking on bounded twin-width. Contributions welcome: proofs of the §7 lemmas, of Lemma 8.4 by induction on the quantifier prefix, and the closure of twin-width under induced subgraphs.
Large systems of interacting diffusions — neurons, oscillators, agents in a network game, particles in a queueing or load-balancing model — are usually analysed through their mean-field limit: as the population grows, each particle interacts with the empirical law of the others, and the system is replaced by a single nonlinear (McKean–Vlasov) equation. The classical theory assumes that every particle interacts with every other one with the same strength. Real networks are heterogeneous and sparse: particle interacts with particle only through an edge of a random graph, and the number of neighbours of a particle is much smaller than the population size.
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) describe the heterogeneity by a graphon and prove laws of large numbers and rates of convergence for such systems. This mission is the fifth of a series formalizing that paper. Its subject is the paper's quantitative result for not-so-dense graphs: when the edges are sampled from a Lipschitz graphon and then thinned by a sparsity factor , the average mean-square distance between each particle and its graphon limit is of order for every .
Let with Lebesgue measure. A graphon is a measurable symmetric function . Fix a horizon and write with the norm .
One probability space carries, for every label , an initial state with law and a standard -dimensional Brownian motion , the whole family being independent. The limit system (4.2) is a continuum of diffusions, one per label:
The particles are independent but not identically distributed; their laws are coupled through the -integral.
The not-so-dense -particle system (4.1) uses the same initial states and Brownian motions at the labels :
The edges are percolated samples of (Condition 4.3): , independent for and independent of the noise. A particle has about neighbours, which is why the interaction is scaled by .
The standing hypotheses are Condition 4.1 — measurable with bounded second moments; bounded and Lipschitz; bounded, Lipschitz and invertible with bounded inverse; and — and Condition 2.3: on finitely many intervals covering , the map is Lipschitz in the Wasserstein distance , and is Lipschitz on every block .
Under Conditions 2.3, 4.1 and 4.3, for each there is with
The constant depends on and on the data, never on . The bound is on the average over particles, not on the maximum.
Theorem 4.2 gives an explicit rate for the convergence of a particle system on a sparse random graph to its graphon limit. Its companion, Theorem 4.1 (mission IV), proves the law of large numbers under weaker hypotheses but without a rate. The rate says that the effective sample size is , the typical degree, not : graphs with still approximate the graphon system as long as the degree grows. Results of this type justify replacing a large heterogeneous network by its graphon limit in control and game problems, such as graphon mean-field games, where the error of the replacement must be quantified.
The paper proves the theorem by hand; none of its results has a machine-checked proof. The formalization produces precise statements of the not-so-dense model, of the estimates of §7.1 that hold for any sparsity, and of the discretization bound, each usable on its own. The milestones (7.10) and (7.15) are the paper's key estimates for sparse interactions and are shared with mission IV.
The obvious approach is to compare each with by Gronwall's inequality, after bounding the difference of drifts. That step fails at the interaction term: the edge and the error are dependent, because the edge enters the dynamics of particle . A plain Cauchy–Schwarz bound loses a factor and gives nothing when . Estimates (7.10) and (7.15) quantify how weak this dependence is, and they are where the hypotheses that is invertible with bounded inverse and that are needed. The discretization term needs the Lipschitz regularity of the limit laws in the label (Theorem 2.1(b)), itself a fixed-point estimate on a space of measure-valued maps.
The Lean development uses Mathlib's unitInterval for , Fin d → ℝ with its sup norm for (all constants are existential, so the choice of norm does not matter), time ℝ≥0, and the path space as continuous maps on with the sup norm. Brownian motions, Itô integrals and Itô processes are those of the published Peng1990.SMP.Stochastic; Wasserstein distances are the published WassersteinDRO.Duality.wassersteinDistance, valued in . Particle is Lean's i : Fin n with label .
Committed conventions:
The solution predicates are not vacuous: the zero-coefficient system satisfies both, Condition 4.1 and Condition 4.3 are satisfiable, and every statement quantifies over solutions rather than assuming the conclusion. The constant is chosen after and before , so it cannot depend on , and the bound is the paper's average over , not a weaker or a stronger form. At both sides of every rate are .
The paper's proofs are in its §5 (Theorem 2.1), §7.1 (Lemma 7.1, (7.10), (7.15)) and §7.3 (Theorem 4.2). Stochastic analysis at that level — Burkholder–Davis–Gundy and Rosenthal inequalities, Girsanov's theorem for these SDEs, Gronwall arguments for measure-valued fixed points — is mostly absent from Mathlib, and contributions of such infrastructure are welcome, as are proofs of any milestone.
Join-the-shortest-queue (JSQ) is the load-balancing rule in which each arriving job is sent to a server with the fewest jobs. It is a baseline in the design of server farms and data centers, and in the many-server Halfin–Whitt regime, where the load per server approaches one at rate , it combines near-full utilization with vanishing waiting. Eschenfeldt and Gamarnik (arXiv:1502.00999, 2015) proved that the suitably scaled JSQ process converges, over bounded time intervals, to a two-dimensional reflected diffusion; Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) gave the form of the result that Braverman quotes as Theorem 1. Process-level convergence over bounded time intervals says nothing about the stationary distribution. To conclude that the stationary distributions converge as well, one needs tightness of the scaled stationary distributions, uniformly in the number of servers .
Braverman (arXiv:1801.05121, Math. Oper. Res. 45(3), 2020) supplied this, together with positive recurrence of the diffusion limit. This mission formalizes the first of the two main results, Theorem 2, and the chain of lemmas the paper uses to prove it.
There are identical servers, each with its own infinite buffer. Jobs arrive as a Poisson process of rate and service times are i.i.d. exponential with mean one. An arriving job joins a server with the fewest jobs, ties broken arbitrarily. The Halfin–Whitt regime is
For , is the number of servers with at least jobs. The process is a continuous-time Markov chain on
Its generator sends to at rate when , and to at rate . The fluid-scaled coordinates are , the negative of the fraction of idle servers, and for . The diffusion-scaled coordinates are . Expectations are taken under a stationary distribution of the chain.
The proof works with functions on and with the first-order operator
where is the partial derivative in , taken one-sided on .
For each there is a constant such that for all with and every stationary distribution,
The constant depends on only, not on , the stationary distribution, or .
with , vanishing second derivatives for , and explicit upper bounds of order above that level. 6. (3.18): . 7. Theorem 2, (2.2): the half of the goal.
Theorem 2 shows that in steady state the number of idle servers and the number of servers holding two or more jobs are on average, and the number of servers holding jobs is on average, uniformly in . Combined with the process-level limit and the positive recurrence of the limiting diffusion (Theorem 3, the companion mission), it yields Proposition 1: the diffusion-scaled stationary distribution converges to the stationary distribution of the diffusion. This justifies the diffusion as a steady-state approximation for JSQ.
The method is the generator-comparison or Stein's-method approach: a Lyapunov function solving a first-order PDE for the fluid model, with explicit bounds on its derivatives. It applies to other many-server systems, and the paper is an example of that approach on an infinite-dimensional chain whose diffusion limit is two-dimensional.
The result is proved in the paper; no machine-checked proof is known to exist. The work remaining is to formalize the known proof: the adjoint relation for a countable-state chain with bounded rates, the Taylor expansion of the generator, and the explicit analysis of through the fluid curves.
The obvious route is to bound in Lemma 2 directly. The paper notes that no good handle on these probabilities exists. The PDE route needs a solution whose second derivatives are bounded by . General results that give such bounds require a continuous fluid vector field, and the JSQ fluid model is discontinuous because of the reflection at . So is constructed explicitly from the fluid paths, and its derivatives must be bounded by hand through the implicitly defined and .
A second difficulty is dimensional: the chain is infinite-dimensional while the PDE is two-dimensional, so the remainder of Lemma 3 contains a term with that is controlled only by combining Lemma 2 with the monotonicity of .
ℕ → ℕ with 0-based indices: Lean q.1 i is the paper's , so the goal's "" is Lean index . Each state is bounded by , nonincreasing and eventually zero. The generator genQ is the displayed formula on p. 6.ℝ × ℝ. Partial derivatives are named functions asserted to be one-sided derivatives along coordinate lines (HasDerivWithinAt on Set.Iic 0 or Set.Ici 0). Weak second derivatives are a.e. derivatives of absolutely continuous functions, in integral form on compact intervals. A "solution" of the PDE whose derivatives are the junk values of a derivative operator is thereby excluded. The PDE needs genuine derivatives, and Lemma 7 is about the explicit of (4.14), not about an arbitrary function.WithTop ℝ, with as ⊤, so a missing solution is never read as . is an if cascade, and Lemma 7 states the agreement of its branches. is defined by the closed form (4.14), not through the fluid model (4.1).Contributions of reusable infrastructure are welcome: the adjoint relation for countable-state chains with bounded rates, and FTC/Taylor lemmas for absolutely continuous first derivatives.
Large networks are often modeled through a graphon, a measurable function that records how likely two labeled vertices are to interact. For interacting diffusions, this lets one ask whether a finite random network has a predictable population limit. Bayraktar, Chakraborty and Wu study that question for graphon weighted systems, including graphs obtained by independently retaining potential edges with a sparsity parameter . Their not-so-dense regime allows to decrease, provided the typical interaction scale diverges. Theorem 4.1 is the paper's law of large numbers for this regime; its two conclusions distinguish convergence of the population's empirical law from mean-square closeness of each particle to a coupled graphon limit. Bayraktar, Chakraborty and Wu, 2023.
The authors present three main convergence results: continuity of the continuum graphon system in Section 2, a dense-system law of large numbers in Section 3, and the percolated-system law of large numbers in Section 4. Section 7 establishes the latter. The graphon and cut-metric framework used here follows the graph-limit treatment cited by the paper. Bayraktar, Chakraborty and Wu, 2023; Lovász, 2012.
Let . A graphon is a symmetric measurable . The cut norm measures the largest absolute integral of over a measurable rectangle . A sequence of step graphons approaches when . The related operator norm measures the effect of on bounded measurable functions. Remark 2.1 says cut convergence implies convergence in this operator norm. Bayraktar, Chakraborty and Wu, 2023, Remark 2.1.
Fix a dimension and horizon . A label has an initial state and an independent -dimensional Brownian motion . The initial states are independent of each other and of the Brownian motions. The limiting graphon particle is a continuous path whose drift averages against the time- laws of all labels , and whose diffusion matrix is . The time- law at label is . The family of path laws is measurable in and has uniformly bounded second moments. Bayraktar, Chakraborty and Wu, 2023, (4.2).
For particles, label means , with . Each undirected edge weight is Bernoulli with mean ; diagonal weights are included. These edge variables are independent of the Brownian motions and initial states. The finite particle uses the same initial state and Brownian motion as . Its drift is the sum of divided by ; its diffusion is . The coefficients and are bounded and Lipschitz, and is invertible with uniformly bounded inverse. Initial laws have uniformly bounded second moments, , and . Bayraktar, Chakraborty and Wu, 2023, Conditions 4.1–4.2.
Let , , and . The main target, Theorem 4.1, first asserts convergence in probability in the weak topology on :
This uses Condition 2.2(a): on each of finitely many intervals covering , the initial law varies continuously in Wasserstein distance . If the graphon also satisfies Condition 2.2(b), its stated sectional continuity outside null sets, the theorem adds
The milestones record the paper's cut-to-operator observation, uniform coupling moments, the one-edge and two-edge estimates, the bound on the second interaction-error term, the quantitative coupling lemma, and the empirical law of large numbers for the independent limiting particles. The second displayed limit is conditional on 2.2(b); the first is not. Bayraktar, Chakraborty and Wu, 2023, Theorem 4.1.
The first conclusion identifies the population-level limit even when the sampled network has a decreasing edge-retention probability. It gives a deterministic law on path space, rather than only a limit at one time. The second conclusion is stronger: it compares each finite particle with the limiting particle built from the same initial state and Brownian motion, averaged over all labels. This comparison is available when the extra graphon continuity assumption holds. Bayraktar, Chakraborty and Wu, 2023, Theorem 4.1 and Remark 4.1.
The mathematical results were proved in the published paper. The present mission asks for machine-checked Lean proofs of its specified statements; the draft theorems themselves currently contain sorry. Reusable outputs would include the percolated-edge model, a path-law formulation of graphon diffusions, and estimates for random interactions that depend on the particle states they influence. The paper's proofs appear in Sections 5–7, with the sparse-system argument in Section 7. Bayraktar, Chakraborty and Wu, 2023.
The edge variables are independent of the driving noise, but a particle's state depends on its incident edges. Therefore an expression such as cannot be factored into the edge mean times the error moment. The same dependence affects pairs of edges in the squared interaction sum. Equations (7.10), (7.14), and (7.15) quantify the discrepancy. A second difficulty is that cut convergence controls integrals against fixed bounded tests, while the dynamics and their path laws supply tests that vary with the system. The paper's regularity conditions and quantitative estimates are needed to connect those forms of control. Bayraktar, Chakraborty and Wu, 2023, Sections 7.1–7.2.
Lean represents by Mathlib's unit interval, by Fin d → ℝ, and continuous paths by maps from into that vector space. The chosen vector and matrix norms are fixed sup-type norms; finite-dimensional norm equivalence preserves the limit statements and the estimates with existential constants. The horizon and dimension are explicitly positive. Particle index i : Fin n denotes the paper's st particle, and empirical laws use positive sizes to avoid division by zero. Wasserstein distances use extended nonnegative reals, while nonnegative expectations use lower integrals.
The noise lives on one probability space. The continuum equation uses the natural filtration of its own initial state and Brownian motion. The finite equation uses the natural filtration of its edge array, sampled initial states, and Brownian motions. A solution carries a measurable continuous-path law family in the paper's class ; this prevents a nonmeasurable pushforward or a default-zero integral from silently satisfying an equation. Edge symmetry, Bernoulli marginals, independence, and diagonal self-loops are explicit. The zero-coefficient system has a separate sorry-free Lean witness for both solution predicates, ruling out a vacuous solution concept.
The formalization uses the published Peng1990.SMP.Stochastic Itô interface and WassersteinDRO.Duality.wassersteinDistance definition. Contributions can prove the listed estimates, strengthen their reusable stochastic and measure-theoretic infrastructure, or connect this mission's local setting to the other graphon missions after their definitions are published. The auxiliary changed-measure particles of Section 7.1 are outside the initial milestone list. Bayraktar, Chakraborty and Wu, 2023, Sections 4 and 7.
The paper of Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (2016) has an algorithmic headline. This mission concerns one of its finite graph lemmas, Lemma 2.9. The lemma translates a condition phrased separately for every connected component into a condition on three vertex sets. A reader of graph decompositions encounters both forms: components express what remains connected after deleting vertices, while a small fixed number of parts gives a compact way to state constraints on a partition. Lemma 2.9 identifies exactly when the two forms agree for the half-balance threshold. The same result appears again in the paper as Lemma 6.2, where the authors use it in a later section.
The result does not require a tree decomposition or a treewidth hypothesis. It holds for every finite graph. That generality makes it a useful standalone target: the definitions of deletion, connected components, and the weighted three-partition can be reused wherever graph separators are studied. The mission follows the published SIAM article, with printed page 328 for the main lemma and pages 363–364 for its restatement and the supporting combinatorial observation.
Let be a finite simple graph with vertex set . Let and be subsets of its vertices. The deleted graph retains precisely the vertices outside and the edges joining them. Two remaining vertices are in the same connected component when a walk joins them without passing through any vertex of . Write for the vertex set of the component containing . This interpretation follows the paper's notation on page 320.
A balanced -separator is a set for which each component of contains at most half the vertices of :
The paper introduces this phrase on page 321. Here balance is a property of relative to ; it imposes no bound on the size of . The denominator counts all vertices of , including any that lie in .
A three-part partition of is a triple of pairwise disjoint sets whose union is . A part may be empty. Two parts have no edge between them if no edge of joins a vertex of one to a vertex of the other. Since the graph is undirected, checking the three unordered pairs of distinct parts covers the requirement for every .
The goal is the equivalence stated on page 328, also restated as Lemma 6.2 on page 363:
The equivalence is the target, including both directions. It applies even when or is empty. It does not include a bound on .
The main supporting result on page 363 says that nonnegative integers with total and can be divided into three classes, each with sum at most . The milestone list also records the paper's merge inequality and its assertion that a component cannot cross between parts having no edge between them. These are the specific claims used in the published discussion of Lemma 2.9.
Lemma 2.9 lets a componentwise balance condition be represented by three sets whose coverage, disjointness, edge separation, and cardinalities can be inspected directly. It gives an exact equivalence, so the three-part formulation loses no balanced separators and introduces none that fail the original definition. That is the mathematical content needed when a later argument represents a separator by a bounded number of regions rather than by a list of all its components. The result is already proved in the 2016 paper; the open work in this mission is a machine-checked formalization of that known result and its cited supporting claims.
Formalizing the equivalence also establishes reusable interfaces for vertex deletion and component membership in a finite simple graph. A future development can state a separator condition using IsBalancedSSep, or use the three-part conclusion without redefining what a component of means. The independent integer-partition lemma has uses whenever indivisible nonnegative weights, each no larger than half the total, must be grouped into three bounded classes. Nothing in that statement depends on graphs.
There may be arbitrarily many components of , although the conclusion permits only three parts. Simply assigning all components to one part can violate the half bound, while splitting a component between different parts may create forbidden edges. A component's weight is the number of its vertices in , and those weights can be uneven or zero. The theorem has to accommodate all such patterns without changing the threshold . In the converse direction, the absence of edges between the three parts must control entire walks, not only their first edge; ordinary connectivity in would allow a walk through and would describe the wrong components.
The Lean development uses SimpleGraph V with V : Type, [Fintype V], and [DecidableEq V]. Vertex sets are Finset V. The shared walk-based AvoidReach G X u v requires every vertex on a walk to lie outside , including both endpoints; avoidComp G X u collects the vertices reachable in this way. It is used only for when quantifying over components. This shared definition matches the paper's . The graph itself need not have decidable adjacency, since the statements concern propositions rather than computations.
Half bounds are written as or in natural-number arithmetic. This is equivalent to the paper's rational half bound and avoids any interpretation of natural-number division. The three parts may be empty, so is a genuine boundary case. The set may meet ; the right-hand denominator remains . The graph may have no vertices. There is no treewidth parameter or size condition on : adding one would change Lemma 2.9 and can make its reverse implication false. Nor may components be computed using connectivity in the original graph, where paths through deleted vertices could merge them.
The required infrastructure is finite graph walks, finite sets, cardinalities, sums over finite index types, and the three original claims in the milestone list. The graph-component definitions and the integer grouping theorem are reusable beyond this mission. Contributions that prove any milestone or the full equivalence under exactly these conventions are in scope.
Twin-width is a graph and matrix invariant introduced by Bonnet, Kim, Thomassé and Watrigant (J. ACM 69(1), Article 3, 2021). Classes of bounded twin-width include bounded tree-width and clique-width graphs, proper minor-closed classes, posets of bounded width, and permutations avoiding a fixed pattern; on all of them, first-order model checking is fixed-parameter tractable once a contraction sequence is given. The difficulty in applying this framework is to bound twin-width for a concrete class, because a contraction sequence is an intricate object.
Section 5 of the paper supplies the tool that makes such bounds routine: the Grid Minor Theorem for twin-width (Theorem 5.4). It reduces bounding twin-width to finding an order of the rows and columns of a matrix (for a graph, an order of its vertices) in which no large mixed minor appears. The paper then uses it for pattern-avoiding permutations, posets of bounded width and -minor free graphs (Section 6, Table 1). The argument is modelled on the proof of the Stanley–Wilf conjecture by Marcus and Tardos (JCTA 107, 2004) and on its use by Guillemot and Marx for permutation pattern matching (SODA 2014).
Timeline. Füredi and Hajnal (1992) conjectured a linear bound on the number of s in a -matrix avoiding a permutation pattern. Marcus and Tardos (2004) proved it, with constant , via -grid minors. Fox (arXiv:1310.8378) improved the constant to , and Cibulka and Kynčl (arXiv:1607.07491) to . Guillemot and Marx (2014) built from the grid structure a decomposition of permutations; Bonnet et al. (2020 preprint, 2021 journal) generalized it to arbitrary matrices over a finite alphabet, which is Theorem 5.4.
Let be an matrix with entries in a finite alphabet of size . For sets of rows and of columns, the zone is the submatrix on those rows and columns; it is constant if all its entries are equal.
A partition of is a pair of a partition of the rows and a partition of the columns. Its error value is the largest number, over all parts (respectively ), of parts of the other side forming a non-constant zone with it. A contraction sequence is a sequence of partitions starting from the finest one (all singletons), ending at the coarsest one (one row part, one column part), each obtained from the previous by merging two row parts or two column parts. has twin-width at most , , if some contraction sequence has error value at most throughout.
A division is a partition whose parts consist of consecutive indices. is -twin-ordered if it has a contraction sequence of error value at most consisting of divisions.
A zone is vertical if its rows are all equal, horizontal if its columns are all equal, and mixed otherwise. A -mixed minor is a division into row intervals and column intervals all of whose zones are mixed; is -mixed free if it has none. For -matrices, a -grid minor is such a division in which every zone contains a . Finally .
For :
$$M\ \text{-twin-ordered}\ \Longrightarrow\ M\ \text{-mixed free},
t\ge1,\ M\ \text{-mixed free}\ \Longrightarrow\ \operatorname{tww}(M)\le 4c_t,\alpha^{4c_t+2}.$$
The constant is the one the paper's proof produces; the paper's summary is not formalized.
Theorem 5.4 characterizes bounded twin-width of matrices, up to the order of rows and columns, by the exclusion of a mixed minor. Its second item is used in Section 6 of the same paper to show that -minor free graphs, posets of bounded width and pattern-avoiding permutations have bounded twin-width, and in later papers of the twin-width series as the standard route to twin-width upper bounds. Without it, each such bound needs its own explicit contraction sequence.
The result is proved in the paper; no machine-checked proof of it exists in Mathlib or on the platform. The mission produces a machine-checked statement and, once solved, a proof of the grid theorem with its explicit constant, a formal treatment of contraction sequences of matrices, and a statement of the Marcus–Tardos theorem with the Cibulka–Kynčl constant, which is itself absent from Mathlib.
The first item is comparatively short. The second item is where the work lies. The natural first idea — contract greedily as long as the error value stays below a bound depending on — does not work: the error value is not monotone under fusions, and nothing in the absence of a mixed minor directly prevents a greedy sequence from getting stuck with large error. Any proof has to identify a quantity that is monotone under fusion and is bounded by a density argument, and then turn a sequence controlled by that quantity into a contraction sequence of bounded error value; the paper's choices (mixed value, Lemmas 5.6 and 5.7) are the milestones. The density argument rests on the Marcus–Tardos theorem with an explicit single-exponential constant, a substantial combinatorial result in its own right and not available in Mathlib.
Matrices are Matrix (Fin n) (Fin m) A with [Fintype A], and is Fintype.card A. Partitions are Mathlib Finpartitions of univ; the finest is ⊥, and "coarsest" means at most one part. Twin-width is the partition form of p. 3:18, as a predicate MatTwinWidthLE M t with exactly one merge, of rows or of columns, per step; it is never an infimum over a possibly empty set. Divisions in minors are given by strictly increasing cut points , so all parts are non-empty. Vertical and horizontal mean "all rows (columns) of the zone agree". Grid minors use Bool entries. Since is not an integer, is a real power, and the bound is ; the mixed-value bound of Lemma 5.7 is .
Hypotheses added relative to the page: in Theorems 5.3, 5.4 and Lemma 5.7; in the second item of Theorem 5.4, in Theorem 5.3 and in Lemma 5.7, since for every non-empty matrix is vacuously -mixed free and the bound would be false; in the row-type count. Theorem 5.3 is stated with the explicit constant that the paper quotes and uses, not as a bare existence statement.
The statements are not trivializable by the usual routes: twin-width is not a junk infimum, a contraction sequence cannot jump to one part in a single step, the error value counts non-constant zones per part on both sides, minors range over divisions with non-empty interval parts rather than arbitrary partitions, and all bounds depend only on and , never on .
A complete development needs: finite partitions and their merges, divisions as interval partitions, the Marcus–Tardos theorem, and bookkeeping for sequences of partitions. The partition machinery and Theorem 5.3 are reusable beyond this mission (graph twin-width in the other missions of this series, pattern avoidance). Proofs of individual milestones, and of the Marcus–Tardos theorem from its original argument, are welcome.
Many scheduling situations involve more than one decision maker sharing a resource. Two departments of a firm may share a machine shop, two clients may share a contractor, or two users may share a processor, and each cares only about how its own jobs are served. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced a systematic study of such two-agent scheduling problems. Their framework has two questions. The constrained problem asks for the best schedule for one agent among those that keep the other agent's cost below a bound. The Pareto problem asks for the schedules whose cost pair cannot be improved for one agent without hurting the other. The paper settles the complexity of these questions for the standard scheduling objectives and gave rise to a large literature on multi-agent scheduling (see the survey by Perez-Gonzalez and Framinan, EJOR 235, 2014).
This mission covers §5.2 of the paper: agent minimizes the total completion time of its jobs, and agent requires that the maximum of its jobs' regular costs stay below a bound .
Agent owns jobs and agent owns jobs . Job has a processing time . All jobs are available at time and are processed one at a time, without interruption, on a single machine. Because every objective here is nondecreasing in the completion times, the machine is never left idle, and a schedule is simply a sequence of all jobs; the completion time of a job is the total processing time of that job and the jobs before it. Write and for the total processing times of the two agents.
Agent 's objective is the total completion time . Each -job has a nondecreasing cost function , and agent 's objective is the maximum cost
Given a bound , a schedule is feasible for the problem if for every -job, and optimal if it is feasible and minimizes among feasible schedules. The instance is feasible if a feasible schedule exists. A schedule is nondominated if no schedule is at least as good for both agents and strictly better for one.
The paper solves the problem with a backward rule (Figure 1). Fill the sequence from the end. With the total length of the jobs not yet placed, place last any unplaced -job with . If there is none, place last a longest unplaced -job. If neither exists, the instance is infeasible. The least-cost variant of §5.2.1 chooses, among the -jobs, one minimizing over all unplaced -jobs. A B-block of a schedule is a maximal run of consecutive -jobs.
On a feasible instance with , every schedule produced by the least-cost variant, under any tie-breaking, satisfies
The nondominance is the printed theorem; the optimality is how the paper introduces , and rests on Theorem 5.5.
Theorem 5.5 shows that the constrained problem with total completion time against a maximum cost is solvable by sorting, in contrast to its weighted version, which the same section shows NP-hard. Lemma 5.6 describes all optimal schedules: they agree on the completion times of the -jobs (up to permuting identical jobs) and on the B-blocks, and differ only inside each block. Theorem 5.7 turns this into a nondominated schedule. It is the building block for the Pareto problem of §11.2, where solving the constrained problem for a sequence of bounds enumerates the nondominated pairs.
The results are proved in the paper; none of them has a machine-checked proof that we know of. The mission formalizes the statements and asks for their proofs. The proof of Theorem 5.7 invokes "the very same proof of Lawler's algorithm (Lawler 1973) restricted to ", applied inside each B-block. Lawler's rule is a separate statement on the platform, LawlerPrec.MinMax.lawler_rule_optimal, currently open. A solver may prove it and adapt it, but the goal does not need it in that exact form.
The interchange arguments of Lemmas 5.3 and 5.4 are short. The obstacle is Lemma 5.6. Two optimal schedules can differ in which -job is placed at each step, and in the order of -jobs of equal length. The paper's argument compares the completion time of each -job across two optimal schedules and shows it cannot move earlier. That needs the fact that a -job finishing before an -job could not have been placed at that -job's completion time, which comes from applying Lemma 5.3 to a prefix of the schedule. Formalizing it requires restricting optimality to prefixes and sub-instances, which the bare sequence model does not provide. The tempting shortcut of proving Theorem 5.7 from Lawler's rule on the whole schedule fails, since the bound and agent 's objective change which jobs may be placed where; the reduction is only to one Lawler instance per block.
Jobs are Fin nA ⊕ Fin nB (0-based). A schedule is a duplicate-free list of all jobs, with completion times from the published sequence model MooreLateJobs.Shared.completionTime (Moore 1968 series), which this mission reuses. Processing times are real and strictly positive. Without positivity the second claim of Lemma 5.3 fails, because a zero-length -job can sit anywhere. Cost functions are real-valued and nondecreasing, and is real (the paper's integer is a special case). Feasibility is stated job by job; is a finite maximum and requires , which the goal assumes. Lemma 5.4 assumes , since "a longest -job" presupposes one.
The paper's loose phrases are read as follows:
The running times of Theorems 5.5 and 5.8 ( and ) are not formalized. Nor is the claim (3) inside the proof of Lemma 5.6.
A trivializing formalization is ruled out: feasibility of the instance is a hypothesis and not built into the rule, the rule constrains every position, and the goal asserts nondominance against all schedules.
Useful infrastructure includes interchange lemmas for the sequence model (moving one job to the end, swapping two jobs), restriction of a schedule to a prefix, and Lawler's rule for on a fixed time window. The interchange lemmas and the prefix restriction are reusable across the whole two-agent series.
Training a neural network means running a first-order method on a loss that is built from compositions of elementary operations, many of them nonsmooth: ReLU, max-pooling, absolute values, sorting, norms. The gradient the optimizer uses is not computed by hand. It is computed by automatic differentiation (autodiff), most often in its reverse mode, backpropagation, which applies the chain rule of calculus operation by operation. When every operation is smooth, the output is the gradient. When some are not, each nonsmooth operation is assigned some "derivative" at its kinks (for ReLU at , typically ), and the chain rule is applied anyway. The result is in general neither a gradient, nor a Clarke subgradient, nor an element of any classical subdifferential: the classical subdifferentials do not satisfy the chain rule that autodiff applies.
Bolte and Pauwels (TSE Working Paper 1044, 2019; Mathematical Programming, 2021) introduced conservative set-valued fields to give these outputs a meaning. A conservative field is a set-valued map whose circulation along every closed path vanishes, exactly as for a gradient field. It obeys a chain rule along absolutely continuous curves. This mission formalizes the paper's Theorem 8: forward-mode and reverse-mode automatic differentiation, run with conservative fields for the elementary operations, return a conservative field for the composed function. The companion mission of this series formalizes the paper's Theorem 1, that a conservative field equals the gradient of its potential almost everywhere.
Write for Euclidean space and for a set-valued map, assigning a subset to every point. A path is absolutely continuous, with derivative for almost every .
A conservative field (Definition 1) is a set-valued map with closed graph and nonempty compact values such that for every absolutely continuous loop () the circulation is Lebesgue integrable with integral . A function is a potential for , or is a conservative field for (Definition 2), if is conservative and for every absolutely continuous path from to . A map is a conservative mapping for (Definition 4) if, along every absolutely continuous curve , for almost every , for all .
An evaluation program (§5.1) has inputs and intermediate nodes . Node has a tuple of distinct earlier nodes and an elementary function . Algorithm 1 sets for and returns . Each comes with a conservative field (property (d)). Given a choice for every :
The autodiff fields are and , the sets of outputs of Algorithm 2 and Algorithm 3 over all choices at .
If every is a locally bounded conservative field for , then
"Conservative field for " is meant in full: closed graph, nonempty compact values, zero circulation and the potential identity.
Theorem 8 says what backpropagation computes on a nonsmooth program: an element of a conservative field of the function, a set that behaves like a gradient along curves. This is what lets the paper's later results apply to deep learning: stochastic subgradient methods driven by such outputs converge, for definable losses, to points that are critical for the conservative field. It is also the reason why spurious outputs of autodiff (a nonzero "derivative" of a function that is identically zero) are harmless: by the companion Theorem 1 they occur only on a Lebesgue null set.
The result is proved in the paper, and nothing here is open. To our knowledge none of it has been machine-checked: there is no formal account of conservative fields, and the existing formalizations of backpropagation treat smooth layered networks only. This mission produces a formal model of evaluation programs and of both autodiff modes, a formal chain-rule calculus for conservative mappings (Lemmas 2–5), and the theorem itself. Formalizing it exposed three points the printed text leaves to the reader: the overwriting update of Algorithm 3, the nonempty-values hypothesis missing from Lemma 2, and the local boundedness that Theorem 8 needs (see Formalization scope).
The obvious argument is "autodiff applies the chain rule, and conservative fields satisfy the chain rule". The chain rule along curves (Lemmas 3–5) only gives the derivative identity of Definition 4 for each element of . It does not give the set-valued properties of Definition 1. Passing back to a conservative field (Lemma 2) needs to have closed graph, nonempty compact values and local boundedness. These depend on how the sets vary with through the forward pass, and they fail without local boundedness of the . Lemma 2 relates an integral identity along every path to a pointwise almost-everywhere identity, and both directions involve the measure theory of absolutely continuous curves that Mathlib supports only in part. The equality of reverse and forward modes is linear algebra, but the two algorithms traverse the graph in opposite orders, and the printed reverse update is not the one the equality needs.
is EuclideanSpace ℝ (Fin n), and the conservative-field layer is polymorphic in the dimension: each lives on . A path is a function ℝ → ℝ^n that is AbsolutelyContinuousOnInterval on , with = deriv γ. Definitions 1–2 require the circulation to be interval-integrable, because Lean integrates a non-integrable function to . Definition 4 and the chain rule (5) assert HasDerivAt, not an equation for deriv, so they cannot hold by default at points of non-differentiability. Nodes are Fin q, numbered from . Parent tuples are duplicate-free lists of smaller nodes, and input nodes have none.
and range over all admissible choices. A single fixed choice would give a map that is not a conservative field in general, and the formal statement does not use one.
Deviations from the printed text, each recorded with its item:
Theorem numbers and pages are those of the TSE Working Paper 1044 (October 2019), the version this mission cites. The journal version is typeset differently.
The conservative-field definitions duplicate those of the companion mission and are meant to be merged with them. Contributions are welcome at every level: Lemma 2 and Lemmas 3–5 form a reusable nonsmooth chain-rule calculus, and the reverse-equals-forward identity is a standalone statement about backpropagation that holds for arbitrary weights.
Unconstrained minimization of a smooth nonconvex function is the core subproblem of most nonlinear optimization software. Methods that only drive the gradient to zero may stall at saddle points, so a second-order guarantee (approximately nonnegative curvature) is the natural target for nonconvex problems. Worst-case evaluation complexity, meaning the number of function and derivative evaluations needed to reach a prescribed accuracy, is the standard way to compare such methods.
Timeline:
This mission formalizes the second-order bound of Part II, Corollary 5.4.
Write and , and let be the Euclidean norm. At iterate , given a symmetric operator (an approximation of ) and a weight , the cubic model is
Algorithm ARC computes a step that decreases at least as much as the best step along (the Cauchy condition). It then forms the ratio . If it accepts the step, , and the iteration is successful; otherwise . Finally it updates : it may shrink after a very successful step () and grows by a factor in after an unsuccessful one. The parameters satisfy , and .
ARC(S) further requires
and the inner termination rule TC.s, with . In Corollary 5.4 each step is moreover a global minimizer of over a subspace spanned by the orthonormal columns of a matrix . The curvature measure is the leftmost eigenvalue
The assumptions are:
Let
For every , the successful iterations with number at most
Some iterate has , and if for all , then at most of the iterations are successful. When , every such satisfies
The constants are those printed in the paper.
The milestones follow the paper's proof:
The corollary gives an explicit, dimension-free bound of order on the number of iterations, and function evaluations, that a practical second-order method needs to reach approximate nonnegative curvature in its subspaces of minimization. The order is the one Nesterov and Polyak proved under much stronger requirements: exact Hessians and exact global minimization over . Taking and recovers their second-order guarantee. Corollary 5.5 of the paper combines this bound with the first-order bound of Corollary 5.3 into a joint first- and second-order complexity bound.
All results here are proved in the paper (some by citation of Part I). None has a machine-checked proof. A formal development would supply:
The neighbouring missions of this series formalize the first-order bounds (Corollaries 3.4 and 5.3).
The counting arguments are elementary once the per-iteration estimates are available. The substantial step is Lemma 4.1. Global minimality over a subspace must be turned into the identity (4.1), the inequality (4.2) and positive semidefiniteness of . First-order stationarity of the reduced model gives only (4.1); the semidefiniteness needs the global characterization of minimizers of a nonconvex cubic, which a local second-order condition does not provide. Lemma 5.1 needs a third-order Taylor remainder bound under a Lipschitz Hessian. A second point of care is the bookkeeping between and in Theorem 2.1, where the printed hypothesis is one index short (see below).
EuclideanSpace ℝ (Fin n). The gradient is Mathlib's gradient, the Hessian is fderiv ℝ (gradient f), and are self-adjoint continuous linear operators with the operator norm.Second-order methods for smooth nonconvex minimization are used in practice because they converge in far fewer iterations than gradient descent, yet for a long time their worst-case guarantee from an arbitrary starting point was no better than that of steepest descent. Nesterov and Polyak (Math. Program. 108, 2006) showed that adding a cubic term to Newton's quadratic model and minimizing that model globally at each step reaches a point with in iterations when the Hessian is Lipschitz, against for steepest descent. Their analysis needs the exact Hessian and an exact global minimizer of a nonconvex model, both of which are too expensive in large-scale computation.
Cartis, Gould and Toint built the Adaptive Regularisation with Cubics (ARC) framework for that setting: the Hessian may be replaced by an approximation , the regularisation weight is adapted without knowledge of a Lipschitz constant, and the step only approximately minimizes the model over a subspace (in practice a Krylov subspace generated by the Lanczos method). Part I (Math. Program. 127, 2011) proved convergence and fast local rates. Part II (Math. Program. 130, 2011), the source of this mission, proved that the practical variant ARC(S) keeps the worst-case bound. Later work showed that this order is sharp for the method (Cartis, Gould & Toint, SIAM J. Optim. 2010) and cannot be improved by any method using derivatives up to second order (Carmon, Duchi, Hinder & Sidford, Math. Program. 2020).
Let be twice continuously differentiable, with gradient , Hessian , and Euclidean norm . At iterate , with , a symmetric operator and a weight , the cubic model is
ARC (Algorithm 2.1) has parameters , and . At each iteration it:
Iterations with are successful. and are the successful and unsuccessful iterations .
ARC(S) (Algorithm 4.1) additionally requires each step to satisfy
The assumptions are:
With , , , , and , the corollary has three parts:
The milestones follow the proof:
The corollary shows that inexact subspace minimization and approximate Hessians cost nothing in worst-case order. The bound is the same count of iterations, function evaluations and gradient evaluations as for the exact cubic-regularised Newton method. It is the founding result of the evaluation-complexity theory of adaptive regularisation methods, and later results build on it: higher-order regularisation, constrained and stochastic variants, and the lower bounds showing that is optimal for second-order methods.
The result is proved on paper; to the knowledge of this mission it has no machine-checked proof. Formalizing it fixes the exact hypotheses: the standing assumption (2.6), the Lipschitz set in AF.4, and the off-by-one in Theorem 2.1. It also yields reusable Lean statements of the counting arguments (Theorems 2.1 and 2.2) shared by every trust-region and adaptive-regularisation complexity proof.
The first idea is to bound the model decrease by directly from . That fails: TC.s and the Taylor estimates bound the step length by the gradient at the next iterate, , not by . The count must therefore use , and turning it into a bound on the first with needs care at the last iteration. The constant combines four sources of error: the Hessian approximation, the Lipschitz Hessian, the bound on , and the inexact model gradient. The bound on itself (Lemma 5.1) needs a second-order Taylor estimate of along the step. Unsuccessful iterations do not decrease and are counted separately through the growth of .
The Lean development uses the following conventions:
EuclideanSpace ℝ (Fin n), is gradient f and is fderiv ℝ (gradient f);IsSelfAdjoint, and operator norms are Mathlib's;Hypotheses and quantifiers:
The constants are written out exactly as printed; replacing them with "there is a constant" would trivialize the goal and is excluded. Contributions are welcome:
EuclideanSpace;Both are reusable well beyond this mission.
Many stochastic dynamic programs in operations research, such as inventory control with partially observed demand or the pricing of American options, are too large to solve exactly. A heuristic policy gives a lower bound on the optimal expected reward; to judge whether it is good enough one needs an upper bound. Brown, Smith and Sun (Oper. Res. 2010) build such bounds by information relaxation: let the decision maker see more than she would in reality, and charge a penalty for using the extra information. The construction generalizes the martingale duality for optimal stopping of Haugh and Kogan (Oper. Res. 2004), Rogers (Math. Finance 2002) and Andersen and Broadie (Manage. Sci. 2004).
In applications, the analyst chooses both the relaxation and the penalty, trading the quality of the bound against the cost of computing it. Proposition 2.3 of the paper collects four properties that govern this choice. The first is the subject of this mission.
Uncertainty is a probability space , and decisions are made in periods . The natural filtration records what is known in each period, with . An action sequence is , chosen from feasible sets . Period rewards are -measurable random variables and the total reward is .
A policy is a map from outcomes to feasible action sequences. It is adapted to a filtration if the period- action is -measurable; denotes these policies. A filtration with for all is a relaxation of , written . A penalty is a function ; it is dual feasible if for every . For any relaxation and dual feasible , the dual bound
is at least the optimal value (weak duality, Lemma 2.1).
The paper's main source of penalties is Proposition 2.2. Given generating functions depending only on , set
Such a penalty has zero mean along every nonanticipative policy, and its dual bound is computed by the backward recursion (10), the Bellman recursion with rewards and conditional expectations given .
For filtrations and one common sequence of generating functions , let be the Proposition 2.2 penalty of . Then
With a common generating function, a looser relaxation gives a weaker bound.
Milestone 1 is on the goal's path; milestones 2–4 are the remaining parts of the same proposition.
Proposition 2.3(i) tells the analyst how to read a weak bound. If a cheap generating function (for instance , the zero penalty) gives a satisfactory bound under some relaxation, it will give a bound at least as tight under any less informative relaxation that still contains ; conversely, moving to a looser relaxation without improving the generating function can only weaken the bound. Part (ii) is a continuity statement: penalties close to the ideal penalty give bounds close to the optimal value. Part (iii) permits the subtracted conditional expectation to be computed under an intermediate filtration, which the paper uses when volatility is unobserved in its option-pricing example. Part (iv) is the justification for estimating penalties by nested simulation, as in the methods of Haugh–Kogan and Andersen–Broadie: unbiased estimates yield valid, if weaker, upper bounds.
The results are proved in the paper's electronic companion. To our knowledge none of them, nor the information-relaxation duality framework itself, has a machine-checked proof. Formalizing them requires a usable theory of policies adapted to a filtration, penalties evaluated along random action sequences, and backward recursions with conditional expectations, all of which are reusable for other duality results in stochastic dynamic programming.
The obvious argument for (12) compares the two suprema policy by policy: . This fails, because the two bounds use different penalties: for a fixed -adapted policy, and need not agree, so the larger policy set alone does not order the bounds. The penalty changes with the relaxation exactly so as to remove part of the value of the extra information, and the statement asserts that it never removes more than that information is worth. Even the representation (10) of a dual bound by a backward recursion is nontrivial: it requires near-optimal actions to be selected measurably in every period.
In Lean, the further difficulty is the composition of an action-indexed family of conditional expectations with a random action: , where each is only defined almost surely. Countability of the action set is what makes this composite well defined up to null sets.
Periods are Fin (T + 1); an action sequence is a function Fin (T + 1) → X for one countable action type X with the discrete σ-algebra (the disjoint union of the per-period action sets). Filtrations are Mathlib Filtrations of the ambient σ-algebra; a relaxation is 𝔽 ≤ 𝔾. Policies are maps Ω → (Fin (T + 1) → X) with values in the feasible set, adapted when each action is measurable for the corresponding σ-algebra. Conditional expectations are Mathlib's μ[f | m], so identities between them hold almost surely. Dual bounds are suprema in EReal over the adapted policy sets, so an infinite bound is represented and no junk value arises from an unbounded supremum.
Pinned regularity, beyond the paper's text: period rewards and generating functions are uniformly bounded (almost surely for the latter) and measurable, so that every expectation exists; in part (iv), the estimates are measurable and uniformly bounded. In part (ii), the difference of two dual bounds is taken in EReal, and the case where both bounds are (where the page's difference is undefined) is excluded.
The penalties of the goal are computed from by the formula of Proposition 2.2; stating the goal for arbitrary penalties with Proposition 2.2's properties would be a different and false claim. Likewise in part (iv) is constructed from and the estimates.
The definitions duplicate those of mission 1 of this series (the framework, the recursive model, the penalty construction); they are expected to be merged. Contributions of reusable lemmas about adapted policies over countable action sets and about backward recursions with conditional expectations are welcome.
Newton's method is the reference second-order method for unconstrained minimization of a smooth function . Near a nondegenerate local minimizer it converges quadratically, and in practice it often works well far from one. Its global behaviour on nonconvex functions is a different matter. The pure method may fail outright when the Hessian is singular or indefinite, and when every Hessian along the run is positive definite it is still not clear how fast the gradient goes to zero.
A natural question is how many iterations a method needs, in the worst case, to produce an iterate with . For steepest descent on functions with a Lipschitz gradient the answer is known to be at most (Nesterov 2004, p. 29). Cartis, Gould and Toint (SIAM J. Optim. 2010) showed that this bound is essentially sharp, and that Newton's method can be just as slow. A matching bound holds for cubic regularization (Nesterov–Polyak 2006; Cartis–Gould–Toint 2011), so the Newton example separates plain Newton from its regularized variants in the worst case.
This mission is the second of three on that paper. It covers the Newton example of §3.
Work in the Euclidean plane , with coordinates . For a twice continuously differentiable write for the gradient and for the Hessian, a symmetric linear operator on with operator norm .
At an iterate , Newton's method (in its simplest form) minimizes the quadratic model
The method is well defined when is positive definite. The model then has a unique global minimizer , characterized by , and the next iterate is (the unit Newton step). A run of the method from is a sequence satisfying these two conditions at every .
The paper aims at the standard assumptions under which globalized Newton methods are provably convergent:
AS.1 is twice continuously differentiable, bounded below, and has bounded and Lipschitz continuous second derivatives along each segment .
Fix and let , so that .
For every there exist and a run of Newton's method on from such that
The goal fixes no constant: the bounds on the Hessian and its Lipschitz modulus are existential. The paper's explicit constants appear in the milestones.
The milestones follow the paper's verification, in order:
The result. Under the standard assumptions for which globalized Newton methods are known to converge, Newton's method can need nearly iterations to reduce the gradient below , the same order as the worst case of steepest descent. Hence no worst-case complexity bound better than can be proved for Newton's method under those assumptions, for any . The identity makes the example robust (§6): every iteration is very successful in a trust-region framework, and the unit step is accepted by a linesearch, so the trust-region and linesearch globalizations of Newton's method are equally slow on it. The contrast with the bound for cubic regularization is what makes regularized Newton methods the better choice from the worst-case point of view.
Formalizing it. The result is proved on paper but has no machine-checked proof that we know of. A formalization has to make several things precise that the paper treats briefly: the smooth extension of the construction to negative coordinates, the gluing of infinitely many polynomial pieces, the passage from bounded third derivatives to Lipschitz continuity of the Hessian along the path, and the counting step from the gradient bound to the iteration count. The result is closed mathematically; the open work is the formal proof.
There is no difficulty in writing down the iterates: the paper prescribes , , and explicitly, and checking that they are consistent with Newton's method is algebra. The difficulty is to find one function on all of that takes these values, gradients and Hessians at the iterates and keeps the global properties: twice continuously differentiable everywhere, bounded below, bounded Hessian, Lipschitz Hessian along the path.
The first attempt fails at the Lipschitz requirement. The one-dimensional steepest-descent example of §2 with unit steplength already is a run of Newton's method, since its second derivative equals at every iterate, and its gradients decay at the required rate. But its third derivative grows linearly with (p. 5), so its second derivative is not Lipschitz continuous along the path, and AS.1 fails. The iterates of that example get closer together while the curvature must still return to at each of them. Any construction has to reconcile the slow decay of the gradient with a Lipschitz modulus of the Hessian along the path that does not grow with . A Lipschitz constant on the whole plane is neither claimed nor available for the paper's construction.
EuclideanSpace ℝ (Fin 2). The gradient is gradient f, the Hessian is fderiv ℝ (gradient f), and its norm is the operator norm. Components are x 0 and x 1.∃ x), with positive definiteness at every iterate. It is not a hypothesis, so the statement cannot hold vacuously. The Hessian in the Newton rule is the true Hessian of , not a free sequence of matrices.Bounded-confidence models describe a population of agents who repeatedly average their opinions with those of agents whose opinions are close to their own. They are used to study consensus and polarization in opinion formation, and in control as a primitive for decentralized rendezvous of mobile agents. Simulations of these models show a robust phenomenon: opinions converge to clusters, and the distances between clusters are typically close to twice the confidence radius rather than just above it. For finitely many agents this regularity has resisted proof.
V. D. Blondel, J. M. Hendrickx and J. N. Tsitsiklis (SIAM J. Control Optim. 48 (2010) 5214–5240) study a continuous-time version of the model in two forms: with discrete agents, and with a continuum of agents indexed by . For the continuum they prove that regular initial opinions converge to clusters whose separation obeys a lower bound depending on the cluster weights. To transfer such conclusions to finitely many agents one needs to know that the -agent model is close to the continuum model when is large. Section 4 of the paper proves this on every finite time horizon. This mission formalizes that result.
Discrete agents. There are agents with real opinions , . Agents and interact when . A solution of (2.1) is a continuous with
for all and all . The right-hand side is discontinuous when the interaction graph changes, so the integral form is used. A solution is proper if it is the unique solution from its initial value, its non-differentiability times have no accumulation point, and two agents that meet stay together.
Continuum agents. Agents are indexed by with Lebesgue measure. is the set of bounded measurable functions . For , is the set of nondecreasing with for ; such are regular. The interaction operator is
and a solution of (3.2) from is a measurable with every and for all and all .
The embedding. For , is the step function with on and . It distributes the agents over blocks of of length .
Let , the solution of (3.2) from , and for each let be a proper solution of (2.1) with nondecreasing and . Then for every and there is with
The statement fixes no rate in and no dependence of on ; it asserts only uniform convergence on bounded time intervals.
The theorem says that the continuum model is the large-population limit of the -agent model over any fixed time window. Combined with the paper's continuum convergence result (Theorem 6), it supports the paper's Conjecture 1 on intercluster distances for finitely many agents, and it is the first step of the paper's Proposition 5, which derives Conjecture 1 for random initial opinions from a stability conjecture for the continuum. It is a mean-field limit for a model whose interaction kernel is discontinuous, where standard Lipschitz mean-field arguments do not apply directly.
All four results and the goal are proved in the paper (with the time-scale correction described below). None of them has a machine-checked proof that this mission is aware of. The formalization contributes a checked continuous-dependence estimate for a discontinuous integral equation, a checked statement that the finite-agent dynamics embed in the continuum dynamics, and a precise record of the time normalization under which the two models agree.
The operator is not Lipschitz on : moving one opinion across the confidence threshold changes the interaction set discontinuously. The obvious Gronwall argument for continuous dependence therefore fails for two arbitrary solutions. It works only around a trajectory that stays in some , where few agents sit near the threshold, which is why the lower slope bound must hold at every time and not only at time . The perturbed trajectory, coming from agents, is a step function and is never regular, so the estimate must be one-sided in this sense.
A literal reading of the page also fails. The page writes , but for in block the continuum interaction equals times the discrete right-hand side of (2.1). With and , both models are linear; at the sup distance between and tends to . The discrete time must be rescaled by .
Namespace BHTOpinion.Approx. Agents of the discrete model are Fin n (0-based); the continuum index set is Set.Icc (0:ℝ) 1 with Lebesgue measure. Opinion functions are ℝ → ℝ, of which only the values on matter; trajectories are written x t α, time first, with time in ℝ and explicit guards. In 0-based form, on ; for the definition returns , and every statement assumes .
Explicit readings of the paper's phrases:
A trivializing formalization is ruled out: the hypotheses are satisfied by , the conclusion is not vacuous because is evaluated at only, and the perturbed initial values in Proposition 4 range over all of , not over regular functions.
Infrastructure needed: Gronwall's inequality for a sup-norm difference, measure-theoretic bookkeeping for on step functions, and a change of variables in interval integrals. The Lipschitz estimate on and the slope bound are reusable for any continuum bounded-confidence model. Contributions to any milestone are welcome; the embedding milestone is independent of the other three.