Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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.
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.
Many Markov processes that arise as solutions of stochastic partial differential equations, stochastic delay equations, or other infinite-dimensional models are not strong Feller: their transition probabilities from two nearby starting points can be mutually singular. For such processes convergence to equilibrium cannot hold in total variation, and the classical Harris theorem (a Lyapunov function plus a minorization on a small set) does not apply. Hairer, Mattingly and Scheutzow ([23], 2011) replaced total variation by a coupling distance built from a suitable distance-like function , and proved a weak Harris theorem: contraction of on the whole space, -smallness of the level sets of a Lyapunov function, and the Lyapunov drift together give a unique invariant measure and a rate of convergence. Butkovsky ([6], 2014) extended it to subgeometric rates, and Kulik's monograph ([25], 2017) gives a systematic account.
The remaining difficulty is to verify the contraction hypothesis for a concrete model. Butkovsky, Kulik and Scheutzow (arXiv:1806.00395, Ann. Appl. Probab. 2020) show that it suffices to build a generalized coupling: a pair of processes whose first component has the correct law, whose second component is only close in law to the process started at the other point, and whose components approach each other. Their abstract theorem of §2 is the input to the paper's applications to stochastic functional differential equations and to the 2D Navier–Stokes, Euler-type and Boussinesq SPDEs of §4.
Let be a Polish space with Borel -field , and let be a Markov transition function: Markov kernels with and the Chapman–Kolmogorov identity. Write . The semigroup is Feller if maps bounded continuous functions to continuous functions.
A distance-like function is symmetric, lower semicontinuous and vanishes exactly on the diagonal. A premetric is lower semicontinuous and vanishes exactly on the diagonal, but need not be symmetric. For probability measures , is the set of couplings and
is the total variation distance.
A measurable satisfies the Lyapunov condition if, for a concave differentiable increasing to infinity with and a constant ,
Put for .
Assumption A asks for a non-increasing with , a locally bounded , and for every a pair of processes with ,
Assumption B1 for a set and : for every there is a set with and . Assumption B2 is a generalized-coupling version of B1 on a set . The paper's auxiliary distance is .
Assume is Feller, satisfies the Lyapunov condition, , Assumption A holds, and there is such that B1 holds for every level set and . Then has a unique invariant probability measure , and for every there are with
The constants are existential, so the goal survives any improvement of them.
In the exponential case , hypothesis B1 on all level sets may be replaced by B2 on the single level set ; the same bound then holds and is exponential in .
In attack order: is distance-like (2.6); the coupling lemma, the gluing lemma and the reimbursement bound used inside the proof of Theorem 2.3(i); Theorem 2.3(i) (contractivity of under A) and (ii) (-smallness under B1); the remark after Definition 2.2 that contractivity and smallness give (2.3)–(2.4); the non-expansion step of the proof of Theorem 2.5; Proposition 2.1 (cited weak Harris theorem); and, for the companion, Theorem 2.3(iii), Proposition 2.2 (cited) and Theorem 2.6.
Theorem 2.5 turns the verification of the weak Harris theorem into two checks that can be carried out model by model: construct a controlled process that is close in law to the true one (Assumption A), and check a support condition on level sets (B1). It covers subexponential rates, given by the function of the Lyapunov drift, and the Wasserstein distance it controls metrizes weak convergence. Theorem 2.6 is the abstract result behind the exponential ergodicity statements for SPDEs in §4 of the paper.
The results are proved in the paper; none of them, nor the weak Harris theorems of [6] and [23] they rely on, has a machine-checked proof. Mathlib has Markov kernels, their composition and invariant measures, but no coupling distances for lower semicontinuous costs, no maximal coupling or gluing lemma on Polish spaces, and no weak Harris theorem. Propositions 2.1 and 2.2 are cited by the paper, not proved there; formalizing them is part of the mission.
The obvious route to contraction is a true coupling of and whose components meet or approach. For processes without the strong Feller property, such a coupling is generally not available explicitly; the generalized coupling only gives the second marginal up to a total variation error. Turning the error-in-law bound into a statement about needs a maximal coupling of two laws on a Polish space and a gluing of two couplings along a common marginal, both of which rest on disintegration of measures. The cited Proposition 2.1 is itself a substantial result: existence of an invariant measure needs tightness from the Lyapunov drift and the Feller property, and the subexponential rate needs a careful interpolation between the drift and the contraction.
The state space is any type with MetricSpace, CompleteSpace, SeparableSpace and the Borel σ-algebra; is dist. Time is ℝ≥0 and is a map ℝ≥0 → Kernel E E with Markov kernels, , Chapman–Kolmogorov, and measurability of , which the time integral in (2.2) presupposes. Expectations, and are lower Lebesgue integrals in , and (2.2) is stated without subtraction (), which is equivalent. A pair of processes is represented by its joint law on path space; is read through the one-dimensional marginals , a weaker hypothesis. Total variation is the published MarkovChainCLT.tvDist, without a factor 2. "Unique invariant measure" means unique among probability measures, with invariance for every . is encoded by quantifying over every with ; such a exists and is unique under the Lyapunov condition. In Proposition 2.1 condition 2 is stated as , which is Proposition 2.1 for the equivalent complete metric and is the form the proof of Theorem 2.5 uses.
No statement relies on a junk value: no Bochner integral of a possibly non-integrable function, no real-valued infimum over a possibly empty or unbounded set, no Measure.map along a non-measurable map, no default-valued inverse of (which would make the bound read ), and "invariant" is never used without "probability".
A complete development needs: Kantorovich-type coupling distances for lower semicontinuous costs, maximal couplings and gluing on Polish spaces, the transfer of -bounds through Markov kernels, and the weak Harris theorem with subexponential rates. All of these are reusable well beyond this mission. Contributions to any milestone, including the cited Propositions 2.1 and 2.2, are welcome.
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.
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.
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.
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.
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.A probability distribution on the real line is self-decomposable (of class L) if its characteristic function satisfies for every , with again a characteristic function. Equivalently, a random variable can be written as with a copy of independent of . Class L consists exactly of the limit laws of normalized sums of independent summands, and its members are infinitely divisible, absolutely continuous (when nondegenerate) and unimodal.
None of this transfers to counting variables: apart from , no random variable on satisfies , because leaves the lattice. Steutel and van Harn (Memorandum COSOR 78-07, 1978; Ann. Probab. 7 (1979) 893–899) replaced scalar multiplication by binomial thinning, which keeps the variable integer valued. The resulting notion of discrete self-decomposability later became the basis of integer-valued autoregressive (INAR) time-series models (Al-Osh and Alzaid, 1987).
Timeline:
A distribution on is a sequence with ; its probability generating function (p.g.f.) is . The generating function of a sequence is written .
The -thinning of a variable with p.g.f. is with independent Bernoulli() variables ; its p.g.f. is . A distribution with p.g.f. is discrete self-decomposable (Definition 2.1) if for every
with a p.g.f.; in variables, .
A distribution is infinitely divisible if for every its p.g.f. is the -th power of a p.g.f. When , its canonical sequence is the unique solution of
Throughout §2 the paper assumes .
For a distribution with :
for some and some p.g.f. of a distribution with , the pair being unique; and
Theorem 2.2 reduces discrete self-decomposability, a condition quantified over all and over unknown factors , to a single monotonicity condition on the sequence computed recursively from . It is the entry point of the rest of the paper: combined with Theorem 2.3 it gives unimodality of every discrete self-decomposable distribution (Corollary 2.4), and §3 shows that discrete stable distributions are discrete self-decomposable. In time-series modelling it identifies the marginals that a stationary INAR(1) process can have for every .
The result has been proved since 1979; to our knowledge none of it is formalized in any proof assistant, and Mathlib has neither probability generating functions on nor infinite divisibility. The mission produces a machine-checked version of the canonical form together with the compound-Poisson characterization of infinite divisibility on (Lemma 1.2), which the paper only cites.
The forward direction is not a consequence of (2.1) for any single : one factorization constrains very little, and the information sits in the whole family of factors , , which are not given explicitly. Turning that family into a statement about needs a passage to a limit of p.g.f.'s, and the fact that such a limit is again a p.g.f. (the continuity theorem for p.g.f.'s, Feller vol. 1, p. 280) is not in Mathlib. The paper does not prove Lemma 1.2 either; it cites Feller and Steutel. For the converse, nonnegativity of the canonical sequence is not enough: the obvious attempt to show that has nonnegative coefficients fails for infinitely divisible in general, and the monotonicity of is exactly what is needed. Finally, every identity is stated between real functions on , and passing to identities between coefficients requires the uniqueness of power-series coefficients on a real interval.
p : ℕ → ℝ with ∀ n, 0 ≤ p n and HasSum p 1; the p.g.f. is the real function pgf p z = ∑' n, p n * z ^ n. All identities between p.g.f.'s are required for real (or for (1.4), (2.4), (2.6), (2.7)), not for complex ; p.g.f.'s agreeing on have equal coefficients, so this is equivalent. is Lean's deriv of pgf p.Reusable beyond this mission: the p.g.f. and infinite-divisibility vocabulary, Lemma 1.2 (compound Poisson characterization), and Lemma 1.1. A continuity theorem for p.g.f.'s on , and the uniqueness of power-series coefficients from values on , are welcome as independent contributions.
Most stochastic dynamic programs that arise in operations research are too large to solve exactly. In practice one computes a heuristic policy and estimates its expected reward by simulation, which gives a lower bound on the optimal value. To know whether the heuristic is good enough one also needs an upper bound. Brown, Smith and Sun (Oper. Res. 2010) give a general way to produce such bounds: relax the requirement that decisions use only the information available when they are made, and charge a penalty for using the extra information.
The idea grew out of option pricing. Rogers (Math. Finance 2002) and Haugh and Kogan (Oper. Res. 2004) bounded the price of an American option from above by letting the holder see the whole future and subtracting a martingale; Andersen and Broadie (Manag. Sci. 2004) built such martingales from approximate exercise policies. Brown, Smith and Sun (2010) extended this to general finite-horizon dynamic programs, to arbitrary penalties, and to imperfect information relaxations in which the decision maker learns some, but not all, of the future. The paper illustrates the framework on an adaptive inventory problem and on pricing American options under stochastic volatility and interest rates.
Uncertainty is a probability space . Time is . The natural filtration describes what the decision maker knows at the start of each period, with . An action sequence is , and is the set of feasible sequences. A policy chooses a sequence for each outcome; it is adapted to a filtration if each action is -measurable. The adapted policies form ; the measurable policies form . The total reward is , and the primal problem (1) is
A filtration is a relaxation of if for all ; the perfect-information relaxation has . A penalty is a function ; it is dual feasible, , if for every . The dual bound of is .
In recursive form, the feasible actions in period form a set , each is -measurable and depends on , and the value functions are and
Given generating functions depending on , Proposition 2.2 builds the penalty
The ideal penalty is this penalty for .
For every relaxation of , and
a primal-optimal also attains the right side; and under perfect information almost surely.
Theorems 2.1 and 2.3 say that information-relaxation duality has no gap: the optimal value of a dynamic program can be computed, in principle, as a minimum over penalties of a problem in which the decision maker sees more. Theorem 2.3 adds that the gap is closed by one explicit penalty, built from the value functions, simultaneously for every relaxation. This is the justification for the practical recipe of the paper and of the literature that followed: choose generating functions that approximate the true value functions, and the resulting dual bound approaches the optimum. Under perfect information, part 4 of the goal says the ideal penalty removes all randomness from the penalized reward of an optimal policy.
The paper defers its proofs to an electronic companion; none of these results has a machine-checked proof. This mission produces a checked version of the duality layer for general finite-horizon dynamic programs on a filtered probability space, with conditional expectations as in Mathlib. Weak duality, strong duality and complementary slackness are stated for arbitrary feasible sets and rewards and are reusable for any information-relaxation argument; the recursive statements give a verified link between the Bellman recursion and the primal problem.
The duality statements of §2.2 are elementary once expectations exist; the work is in §2.1 and §2.3. The claim that is the optimal value of (1) needs two facts that the paper asserts without proof: that the supremum in (2) is -measurable, and that near-optimal actions can be selected measurably, so that a nonanticipative policy comes within of even when the suprema are not attained. Neither holds for general action spaces without measurable-selection arguments, which is why this mission fixes a countable action set. A second difficulty is the evaluation of action-indexed conditional expectations at a random action: conditions , where each is only defined up to null sets, one for each . The induction must also carry these almost-sure identities through suprema over actions.
The Lean development lives in the namespace InfoRelax.IdealPenalty. Periods are Fin (T + 1); actions take values in one type X (the disjoint union of the per-period action sets); filtrations are Mathlib Filtrations of the ambient -algebra; conditional expectation is condExp. Primal values, dual bounds and dual values are in EReal, taken over the adapted-policy sets, so that no supremum or infimum silently returns . Penalties in are required to be integrable along every measurable policy, and the reward is assumed integrable along every policy in the general statements: without this, a Bochner integral of a non-integrable function is and the statements become vacuous. The value functions (2), the dual value functions (10), the penalty of Proposition 2.2 and are definitions computed from the data, never variables constrained by hypotheses.
The recursive statements fix a countable action set with the discrete -algebra, bounded period rewards, and generating functions bounded almost everywhere. Identities between value functions are almost sure. The general results (Lemma 2.1, Theorems 2.1–2.2, Proposition 2.1) assume none of this. The optional identity (5), which exchanges a supremum over policies with an expectation of a pathwise supremum, is not formalized: for a general dual feasible penalty the pathwise supremum need not be integrable.
Contributions welcome: the measurable-selection lemma for countable action sets, the tower-property argument for action-indexed conditional expectations evaluated at adapted policies, and proofs of the milestones in any order.
Worst-case iteration counts are the standard way to compare unconstrained optimization methods on nonconvex problems. For finding an approximate first-order critical point, a point with , steepest descent needs at most iterations on functions with a Lipschitz gradient. The cubic regularization of Newton's method needs at most iterations on functions with a Lipschitz Hessian. This bound was proved by Nesterov and Polyak (2006) for exact global model minimization (doi:10.1007/s10107-006-0706-8). Cartis, Gould and Toint (2009a, 2011) extended it to the adaptive variant ARC with approximate model minimization (doi:10.1007/s10107-009-0286-5).
An upper bound alone leaves open whether a better analysis could lower it. Cartis, Gould and Toint (SIAM J. Optim. 20(6), 2010, doi:10.1137/090774100) settle this for three methods by explicit one- and two-dimensional examples. This mission formalizes the third: the bound for ARC is sharp up to an arbitrarily small loss in the exponent.
Timeline:
Let be twice continuously differentiable, and write , . At an iterate , with a regularization weight , the cubic model (1.3) is
One iteration of the Adaptive Regularization with Cubics (ARC) algorithm, in the variant considered here, proceeds as follows.
The parameters satisfy and . In Lean the model is SlowConvergence.ARC.model, the ratio rho, and a run is the predicate IsARCRun f γ₁ γ₂ η₁ η₂ x s σ.
The paper fixes and sets . It then prescribes iterates , with , and function values (5.3). At the iterates it prescribes gradients , Hessians and weights (5.4).
For every there are a function and a run of ARC on it from , , with the following properties:
The goal fixes no Lipschitz constant or Hessian bound; it asserts the existence of the example, which is the paper's claim.
The example shows that the upper bound of Nesterov–Polyak and Cartis–Gould–Toint cannot be improved to for any , even in one dimension and with exact global model minimization. It also shows that adaptive weights do not help: the run is valid for every choice of the algorithm's parameters. Together with the paper's other two examples, it separates the worst-case orders of steepest descent and Newton's method () from that of ARC (). The paper ends by asking whether is optimal among all second-order methods. That question was answered later by Carmon, Duchi, Hinder and Sidford (2020) for a broad algorithm class.
The paper's argument is a construction checked by hand plus a plot of the first sixteen intervals. No machine-checked version of this lower bound is known to exist. A formal proof would certify every interpolation identity, the uniform third-derivative bound and the gluing into a globally function. The upper bounds of Nesterov and Polyak are separate statements on the platform (CubicNewton.Nonconvex.*) and are not proved there.
Checking the algebra at the iterates is routine; the difficulty is the function. The piecewise quintic must be twice continuously differentiable across infinitely many knots. Its second derivative must be Lipschitz with one constant on the whole line, although the intervals shrink like . This requires a third-derivative bound that does not grow with . The obvious first idea is to interpolate values and slopes with cubics; it fails, because the second derivative must vanish at both ends of every interval to match . A further step is that the knots go to only because , which is where enters. Finally, must be extended to without losing boundedness below or the global Lipschitz bound.
f : ℝ → ℝ, = deriv f, = deriv (deriv f), for the norm. The model uses the true second derivative of the same , not a free approximation . The step is a global minimizer of the model; uniqueness is not required.Data (iterates, values, gradients, the model built from them) and Pieces (the quintics , ). Proofs of the polynomial identities and of gluing infinitely many polynomial pieces into a function with a global Lipschitz second derivative are reusable for the paper's other two examples. Proofs of the milestones, of the gluing lemma, and of the goal are all welcome.CubicNewton.Shared.cubicModel and IsCubicStep are the same model and step in with ; they are not imported here.Matrix completion asks for a low-rank matrix from a small random subset of its entries. It models collaborative filtering (recommendation systems), sensor-network localisation, and structure from motion. In practice the revealed entries are corrupted by noise, and the most widely used estimator is nuclear-norm regularized least squares: fit the observed entries in squared error while penalizing the sum of singular values. The estimator is a convex program, so it is solved reliably by proximal and singular-value-thresholding methods, and it needs no knowledge of the rank.
Its statistical accuracy was not understood. In the noiseless case, convex relaxation recovers the matrix exactly from nearly the information-theoretic minimum number of samples (Candès–Recht 2009, Candès–Tao 2010, Gross 2011). With noise, the available bounds for the plain convex program (Candès–Plan 2010) give under random noise. That can be a factor of order above the oracle lower bound, and the numerical performance of the program is far better. Sharper rates were known only for modified estimators: Negahban–Wainwright 2012 add a spikiness constraint, Koltchinskii–Lounici–Tsybakov 2011 use a different estimator. In 2019, Chen, Chi, Fan, Ma and Yan (arXiv:1902.07698; SIAM J. Optim. 30(4), 2020, doi:10.1137/19M1290000) showed that the unmodified convex program attains near-optimal error in the Frobenius, entrywise and spectral norms simultaneously. Their argument goes through nonconvex gradient descent. This mission formalizes that theorem.
The unknown matrix is of rank , with singular value decomposition . The columns of are orthonormal, and with , and condition number . Write for the largest Euclidean norm of a row of . is -incoherent if and (Definition 1). Incoherence says that the energy of is not concentrated on a few rows or columns.
Under Assumption 1, each index enters the observed set independently with probability . One observes for , where the are i.i.d., zero-mean, and have sub-Gaussian norm . Let keep the entries indexed by and zero the rest. The convex estimator is any minimizer of
where is the nuclear norm, is the spectral norm and is the largest absolute entry.
Suppose and . Then with probability , every minimizer of (3) satisfies
Every best rank- approximation is within of in Frobenius norm, and satisfies the same three bounds.
satisfies under Conditions 1–2. 2. Probabilistic layer: Lemma 3 (Condition 1(a)), Lemma 19, Lemmas 7 and 8, and Lemma 4. Lemma 4 gives Conditions 1(b) and 2 uniformly over an neighbourhood of the truth. 3. Algorithmic layer: Lemma 5, the error bounds and the small-gradient iterate of gradient descent started at the truth, and (31), its consequence for .
The bounds of Theorem 2 match the minimax lower bounds up to logarithmic factors when and are bounded. This holds in all three norms and for noise of any size below a threshold. The theorem also shows that the convex solution is nearly of rank . Neither statement requires modifying the estimator, so practitioners running standard solvers get the guarantee as is. The entrywise bound (11b) shows an implicit regularization: the convex program spreads its error over all entries without being told to.
The theorem has a complete published proof. What this mission adds is a machine-checked version, which has value of its own here. The proof chains about twenty lemmas, including a leave-one-out analysis of gradient descent with polynomially many iterations. Its constants are hidden behind "" at nearly every step. The formal development fixes the quantifier order of every such constant. It also records the hypotheses the proof uses without stating them, such as the independence of the sampling pattern from the noise. No part of this paper has been formalized before. The deterministic layer (Lemmas 20, 2, Claims 2–3) applies to any Burer–Monteiro factorization of a nuclear-norm problem, not only to this one.
The obvious approach is to analyse the convex program directly through a dual certificate, as in the noiseless theory. With noise there is no exact recovery, and the certificate approach loses a factor polynomial in . The difficulty is to transfer statistical bounds from a point one can control, the nonconvex iterate, to a point one cannot construct, the convex minimizer. The two are compared through an approximate first-order condition. That comparison is useful only if injectivity and concentration hold uniformly over all factor pairs near the truth, because the iterates depend on and on the noise. A fixed-tangent-space injectivity bound, the usual tool, does not suffice. The entrywise control of the iterates requires leave-one-out sequences, and those sequences make up most of the appendix.
Matrices are Matrix (Fin n) (Fin n) ℝ and factors Matrix (Fin n) (Fin r) ℝ, using the published matrix_completion_basic, _svd and _tangent definitions (nuclear norm, SVD data, , , spectral, Frobenius and entrywise norms). comes with an explicit SVD with positive singular values, so its rank is exactly . Definition 1 is MatrixCompletion.A0. The sub-Gaussian bound is the moment form of [Ver12, Definition 5.7] above, not Mathlib's MGF form. The randomness lives on an arbitrary probability space. The sampling indicators and the noise entries are each mutually independent, and the two families are independent of each other. This last independence is an added hypothesis, which the paper's proofs use. "With probability " is stated as an outer-measure bound on the failure event. Every unnamed constant ("", "sufficiently large ", "sufficiently small ") is an existential placed before and all data, together with an . Explicit constants of the paper are kept: the exponents and , , , , , , , the factors in (31), the in (12), and in Lemma 2.
The goal keeps the randomness in the statement. A version with fixed and that assumes Conditions 1–2 or the conclusions of Lemma 5 would be Lemma 2 plus (31), not Theorem 2, and is not acceptable as a proof of the goal. The goal quantifies over every minimizer of (3) and every best rank- approximation. Excluded: Theorem 1 (the corollary), the noise condition of Remark 4, approximate minimizers (Remark 6), Lemmas 1 and 6, and the internal lemmas of the leave-one-out analysis (App. D), which solvers may add as supporting theorems. The development needs nuclear-norm subgradients, Weyl's inequality, matrix Bernstein and spectral-norm bounds for sparse random matrices. These are reusable well beyond this mission, and contributions of them are welcome. Theorem and equation numbers are those of the authors' preprint (Sep. 2019, arXiv:1902.07698) and may differ in the SIAM typesetting.
In multi-agent scheduling, several decision makers share one processing resource, and each one cares only about the completion of its own jobs. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) set up the two-agent version of this problem and classified its complexity for most combinations of classical objectives. Typical settings are a manufacturing cell that serves an internal and an external customer, or two departments that negotiate access to a shared machine. Most of the paper treats a single machine. Its §10 asks what happens when the shared resource is a small shop: two machines that every job must visit.
The answer is that even the simplest two-machine case is hard. In the classical single-agent setting, the two-machine flow shop makespan problem is solved by Johnson's rule (Johnson 1954) and the two-machine open shop makespan problem by Gonzalez and Sahni (1976), both in polynomial time. As soon as two agents each want their own jobs finished early, both problems become NP-hard.
There are two agents, A and B. Agent A owns jobs and agent B owns jobs . Every job consists of one operation on machine and one on machine , and is the processing time of job on machine . A schedule gives every operation a start time. It is feasible when no operation starts before time , each machine processes at most one operation at a time, and the two operations of one job do not overlap in time. Processing is nonpreemptive.
The makespan of agent , , is the latest completion time of an operation of one of its jobs. The recognition problem asks, for given thresholds , whether some feasible flow shop schedule has and . The problem is the same question for the open shop.
PARTITION (Problem 9.1 of the paper) asks whether a finite list of nonnegative integers can be split into two parts of equal sum , where .
with polynomial-time many-one reducibility between binary-coded languages. This is how the paper proves " is NP-hard" (Theorem 10.1, p. 238) and " is NP-hard" (Theorem 10.2, p. 239).
For Theorem 10.1, with , the paper builds the instance with A-jobs of times , one B-job of times , and thresholds , . The milestones are:
For Theorem 10.2 the instance has A-jobs of time on both machines, one B-job of time on both machines, and thresholds , . The milestones are:
The two theorems mark the boundary of tractability of §10. The single-agent problems and are polynomial. Giving the second agent a single job and a deadline is already enough to make the problems NP-hard, so no extension of Johnson's rule or of the Gonzalez–Sahni algorithm solves the two-agent versions unless P = NP. The paper also observes that any other combination of the objectives it considers is NP-hard in these shops.
The theorems are proved in the paper by short reductions. As far as we know none of them is machine-checked. This mission produces checked statements of both reductions on a general two-machine shop model with real start times. It also corrects the flow shop equivalence, which as printed does not hold for odd .
The hard direction of each equivalence goes from a feasible schedule to a partition. A schedule is a set of real start times, not a permutation. Nothing forces the jobs into a fixed order or rules out idle time. The proof has to extract a combinatorial split from interval packing: which A-jobs fit into the gap before the B-job on one machine and which fit into the gap after it. The sum of lengths of pairwise disjoint intervals inside a window must be bounded by the window's length.
In the flow shop the gap after the B-job has length , which is not . Integrality of the A-lengths is what closes the gap, and it only works when is an integer. In the open shop, the same argument has to cover both orders of the B-job's operations. Both reductions output rational data, so the goal also needs a scaling to integer data and a polynomial-time bound on the code map.
Fin (n_A + n_B), the A-jobs first. Start times are real numbers, and idle time and different job orders on the two machines are allowed. Flow shop feasibility is the published JohnsonFlowShop.TwoStage.IsFeasible from the Johnson (1954) series. Open shop feasibility is the definition IsOpenFeasible of this mission: no machine overlap between distinct jobs, and no time overlap between the two operations of a job. "" is stated as "every operation of every -job ends by ", so no maximum over a possibly empty set is taken.ProjSchedTW.Complexity.partitionLang (nonnegative sizes, zero allowed), and reducibility is CookPvsNP.PolyReducible. Both come from published definitions of the Neumann–Schwindt–Zimmermann and Cook series. NP-membership is not formalized.encNats, and a scaling lemma for shop schedules are reusable beyond this mission.Many objective functions in engineering design, Chebyshev approximation and game-theoretic planning are extremal-valued: they are the pointwise maximum or minimum of a family of smooth functions, . Such a function is typically not differentiable at points where two or more members of the family are active, so gradient methods do not apply directly. In 1976 R. Mifflin introduced the class of semismooth functions to identify which nondifferentiable functions can be minimized by bundle-type and line-search methods whose convergence relies only on generalized gradients (Mifflin, IIASA RR-76-21; journal version SIAM J. Control Optim. 15 (1977), doi:10.1137/0315061). For that class to be useful it must contain the functions that actually occur in practice. §3 of the report shows that it contains min–max objectives, which is the content of this mission.
Background: F. H. Clarke defined the generalized gradient of a locally Lipschitz function and computed it for max functions (Clarke, Trans. AMS 205 (1975), Theorem 2.1). A. Feuer's Columbia dissertation (1974) proved the formulas of Theorem 1 below under stronger assumptions and a result close to semismoothness, from which Mifflin's proof of Theorem 2 is adapted (report, Remark, p. 8). Mifflin's notion of semismoothness was later extended to vector-valued maps by Qi and Sun (1993), where it became the standard hypothesis for superlinear convergence of nonsmooth Newton methods.
Let carry the Euclidean inner product and norm , and let . is Lipschitz on a set if for all . Clarke's generalized directional derivative is
and the generalized gradient is . When exists it is the directional derivative ; is quasidifferentiable at if exists and equals for all .
is semismooth at (Definition 1) if it is Lipschitz on a ball about and, for each and all sequences , with , and , the real sequence has exactly one accumulation point. is semiconvex at with respect to (Definition 2) if it is Lipschitz on a ball about , quasidifferentiable at , and , imply .
In §3, is open, is a topological space, is sequentially compact, , and satisfies either (d) on or (d′) on . The active set is , and is the generalized gradient of at . Hypotheses (a)–(c) ask that be continuous on , Lipschitz in uniformly in , and that be upper semicontinuous on ; (e) and (e′) ask that exist and equal , respectively .
If (a) holds, has the max form (d) or the min form (d′), is differentiable on for each , and is continuous and bounded on , then
in the max form, and in the min form.
Theorem 2 places every min–max objective with continuously differentiable data inside the class on which Mifflin's descent algorithms, and the bundle methods that followed them, are proved to converge. Theorem 1 is the generalized-gradient form of Danskin's theorem, the standard tool for computing subgradients of max functions. Theorem 3 shows that semiconvexity, unlike pseudoconvexity, survives pointwise maximization, which is what the sufficient optimality results of §5 of the report need.
All of these results are proved in the report and in the literature since 1977; none is open. As far as is known, none of them has a machine-checked proof. Mathlib has Fréchet derivatives and convex analysis but no Clarke generalized gradient calculus, no semismoothness and no Danskin-type theorem. A formalization produces those pieces as reusable infrastructure, and checks the report's statements under exactly stated hypotheses. One printed claim already needs a correction (see Formalization scope).
Lipschitz continuity of and the inequality follow from Theorem 1 and the upper semicontinuity of . The difficulty is the matching lower bound: semismoothness asks that the slopes along an arbitrary sequence , with arbitrary , not accumulate strictly below . A generalized gradient of at is only a convex combination of gradients of the active functions at , and the active set can change discontinuously along the sequence. Upper semicontinuity of alone does not prevent this; the function (p. 6) is Lipschitz and has an upper semicontinuous but is not semismooth at . The argument has to use the continuity of jointly in and the compactness of . Theorem 1 itself needs a mean value theorem for Lipschitz functions and a compactness argument over the active set, neither of which is in Mathlib in this form.
is EuclideanSpace ℝ (Fin n). is the published ClarkeGradients.Shared.genDirDeriv, a real limsup; every statement assumes the Lipschitz hypothesis of the page at the points where or is used, so that this limsup is the true value. is the support-set definition of the page, not Clarke's convex hull of gradient limits; the two coincide by Proposition 1(c), which is not assumed. is a relation (HasDirDeriv), so "" means "exists and is nonnegative". "Exactly one accumulation point" is a unique cluster point, not convergence. "" is read as "positive and tending to ", as the report reads it in the proof of Lemma 2. "max" and "min" are attained extrema (IsGreatest, IsLeast), never suprema with default values.
is a given function constrained by (d) or (d′), not a supremum; this rules out the trivializing formalization in which is defined as ⨆ u ∈ U, f x u and takes the default value for an empty or unbounded family. (d) and (d′) force . The page's "for each either (d) and (e) or (d′) and (e′)" is read as one form on all of , as the proof of Theorem 2 treats it, and Theorem 1 is stated as two items. Hypothesis (c) is the sequential accumulation-point form in which Proposition 1(d) glosses upper semicontinuity.
The goal does not assume (b), (c), (e), (e′) or convexity of ; the report derives the first four from smoothness. The report claims (b) on all of , which fails for non-convex open (a bounded gradient gives a uniform Lipschitz constant only on convex sets). The corresponding milestone states (b) on balls contained in , which is all the proof needs.
The development needs Clarke's calculus for Lipschitz functions on (Propositions 1 and 2, a Lebourg mean value theorem), a Danskin-type theorem, and the regularity of functions. These are reusable well beyond this mission; a companion mission of the series covers Propositions 1(c), 2 and the chain rule. Contributions are welcome on any milestone, including alternative proofs of Theorem 1.
Retailers decide which product variants to stock, and most assortment-planning tools model consumer choice with the multinomial logit (MNL) model: a consumer who does not find an acceptable variant simply leaves without buying. Cachon, Terwiesch and Xu (Retail Assortment Planning in the Presence of Consumer Search, working paper of December 2002; published in MSOM 7(4), 2005, doi:10.1287/msom.1050.0088) point out that consumers also search: a consumer who likes what the store offers may still walk out to look elsewhere, and that is more likely when the assortment is narrow.
In practice a retailer does not know consumer preferences; it estimates them from sales data and re-plans. This mission formalizes §5.1 of the paper, which asks what happens when a retailer runs this estimate-and-replan loop with the traditional no-search MNL model while consumers actually search. The loop can settle at a heuristic equilibrium in the sense of Cachon and Kok (2002), and the question is how that equilibrium compares with the truly optimal assortment.
There are product variants, labelled from most to least popular, with preferences , and a no-purchase option ("variant 0") with preference . An assortment of depth is the set . Variant has margin , with whenever (monotone margins, p. 6), and carrying it at demand incurs an operational cost , where is concave and increasing on (demand is normalised to one consumer).
True demand: the independent assortment model. With a constant (Theorem 1 of the paper: ) and , the probability that a consumer searches is , and variant has demand
The no-purchase demand is , and the true profit is .
Estimates. Observing for , the retailer fits the MNL model, normalised by : for , and for variants not carried it reuses the estimates from an initial depth test with the full assortment. The no-search model fed with preferences predicts the shares and the profit .
Heuristic equilibrium. A depth is a heuristic equilibrium when maximises over : the assortment is optimal for the estimated preferences, and the estimates are those observed under the assortment. An optimal depth maximises the true profit over .
If is a heuristic equilibrium and is an optimal depth such that every deeper depth is strictly worse ( for ), then
Theorem 8 says that a retailer who ignores consumer search and plans iteratively from its own sales data can only err on the side of a too-narrow assortment, never a too-deep one. The bias is structural: Theorem 7 shows that the estimates get every product variant's relative preference right but misjudge the no-purchase option in a direction fixed by the depth. The result thus separates the part of the MNL model that survives consumer search (IIA among products) from the part that does not (IIA with respect to the no-purchase option).
The results are proved in the paper, by short arguments, but some steps are only asserted: the non-negativity of variant profits at the equilibrium is attributed to "the previous section", and the overlapping assortment model is dismissed with "the similar process". No machine-checked proof of these results is known. A formalization makes explicit the hypotheses the paper leaves implicit (, and a strict-deeper condition on in place of the presumed uniqueness of the optimum), and delivers a reusable formal model of MNL estimation under search.
Each step is elementary, and the difficulty lies in keeping two profit functions apart and carrying the right inequalities between them. The tempting shortcut, "the estimates are correct, so the no-search optimum is the true optimum", fails: the estimates are correct only up to the no-purchase preference , which depends on , and that single number shifts every predicted share. The proof of Theorem 7 must reduce the comparison of and to the monotonicity of the function . The step from no-purchase demand to profit needs every predicted variant profit to be non-negative, which requires the monotone labelling of preferences and margins together with concavity of and ; the paper asserts it without proof.
Fin n, 0-based: the paper's variant is index . Depths are natural numbers, and depth is the published RetailVariety.Structure.popularSet n x; the MNL share is the published RetailVariety.Structure.share.Fin n; its preference and estimate are separate reals.Trivializing formalizations are ruled out: the estimates are not the true preferences (in particular , which would force ); is not an arbitrary maximiser but one with all deeper depths strictly worse; , where nothing is observed, is excluded rather than given junk estimates; and nothing is claimed for the overlapping model.
Contributions welcome: proofs of the milestones, in particular Theorem 7 and the positivity step, and a formal treatment of the overlapping model with its additional hypotheses.
A retailer deciding which variants of a product to stock trades off two effects. A deeper assortment captures consumers whose favourite variant would otherwise be missing, but it splits demand among more variants, each of which then carries its operational costs (shelf space, handling, inventory) at a smaller, less efficient scale. Van Ryzin and Mahajan (Management Science 1999) showed that under multinomial-logit (MNL) demand the optimal assortment consists of the most popular variants, which reduces the search over assortments to candidates.
Cachon, Terwiesch and Xu (working paper, 2002; published in MSOM 2005) add consumer search: a consumer who finds nothing good enough in the store may leave to look elsewhere, and a deeper assortment makes that less likely. In their independent-assortment model the search threshold does not depend on the store's assortment, but the fraction of consumers who stay does. This mission formalizes their Theorem 5: even with this extra dependence, the profit change from adding a variant is quasi-convex in that variant's preference.
There are variants. Variant has a preference and the no-purchase option has preference (in the paper , with the net utility and the Gumbel scale). For an assortment the MNL purchase probability without search is
A consumer searches when her best alternative in the store, including no purchase, falls below a threshold . With Euler's constant and , this happens with probability , and by the paper's Theorem 1 the independent-assortment demand is
Each variant sold earns a margin , and stocking a variant with demand costs , where the cost function is concave and increasing on (economies of scale). Variant 's profit is . Write .
Fix and a variant , and treat 's preference as a variable. Let be variant 's profit in ; its demand carries the factor , not . The cannibalization loss and the profit change are
Quasi-convexity of says that a variant is worth adding, if at all, at an extreme of its popularity. The paper uses it to conclude that, as without search, the optimal assortment under independent-assortment search lies among the popular assortments, the sets of the most preferred variants. This reduces assortment optimization to candidates. The paper also shows that the conclusion fails in its overlapping-assortment model, so the independent-assortment case marks where this structural result survives the addition of search.
The result is proved in the paper; none of it has a machine-checked proof. The paper's proof contains gaps that a formalization must close: several sign and monotonicity facts are asserted without proof ("It can be shown", "by a similar argument as in Theorem 4"), display (8) is printed without a factor , and the step from (10) to (11) rests on an inequality asserted without the full expression. A complete formal proof of Theorem 5 therefore also fixes the argument.
The no-search analogue (Theorem 4) is easy: the numerator of is increasing, so changes sign at most once. Here the search factor depends on , and the derivative splits as with , , nondecreasing and nonincreasing, but neither nor is monotone. So the argument used for Theorem 4 no longer applies, and when and the derivative cannot be written as a positive factor times a monotone one. The proof needs a separate second-order argument at critical points in that case. Showing only that has at most one zero is also not enough: it must change sign from negative to positive.
Fin n (0-based); the no-purchase option is a separate real v0 > 0, not an element of Fin n. All preferences are positive. The MNL probability is the published RetailVariety.Structure.share, referenced, not redefined.deriv c. The value is unconstrained; .Function.update v j x on insert j S, with . Quasi-convexity is Mathlib's QuasiconvexOn ℝ (Set.Ici 0).Graph coloring asks whether vertices can be assigned colors so that adjacent vertices receive different colors. Restricting the graphs by forbidden induced paths can expose structure that is absent from general graphs. Bonomo, Chudnovsky, Maceli, Schaudt, Stein and Zhong study list three-coloring when the graph has no induced path on seven vertices, building on earlier work on coloring graphs with shorter forbidden induced paths. Their paper proves an algorithmic result, but its treatment also uses a purely graph-theoretic statement: a connected -free graph has a small connected set that reaches every vertex within two steps, unless the graph contains a four-vertex clique. This mission isolates that statement as Corollary 5 of the paper.
The structural input to the corollary is a theorem of Camby and Schaudt about connected dominating sets in -free graphs, quoted as Theorem 4 in the coloring paper. That result applies to every allowed path length , rather than only to the seven-vertex case. It is a milestone here in the precise form printed in the source article. The Camby–Schaudt paper develops connected domination as a characterization of graphs without long induced paths.
A simple graph has a vertex set and an undirected edge relation with no loops. The graphs in this mission are finite. The path has vertices and consecutive vertices adjacent. A graph is -free when it has no induced subgraph isomorphic to : the graph may contain a path with vertices as a non-induced subgraph if extra edges join vertices of that path. This distinction matters throughout the source paper.
For a vertex set , its open neighborhood consists of vertices outside with a neighbor in . Write . The set is dominating when , so each vertex lies in or has an edge to . It is 2-dominating when , meaning each vertex is at graph distance at most two from some vertex of . A dominating or 2-dominating set is connected when the subgraph induced by is connected. In this mission, connectedness includes nonemptiness, as in the paper's use of such sets.
A clique of size four is a set of four pairwise adjacent vertices. The notation below asserts the existence of such a set. Since all edges between those four vertices are present, it is also an induced complete subgraph. The notation means there is a graph isomorphism from the induced graph on to that path.
For a finite, connected, -free graph , the goal is
The four-vertex clique is a genuine alternative in the claim; the mission does not assume its absence. The result is the first, structural sentence of Corollary 5. Its following sentence gives a running time for finding the set or clique and is outside this mission.
For every , the cited theorem asserts that each finite connected -free graph has a connected dominating set for which
The other milestones are statements identified in the proof of Corollary 5: a connected -free graph is complete, domination inside a dominating set yields 2-domination in the original graph, and the three non-leaf vertices work when the induced dominating graph is a . These are listed in the paper's order of use, with the quoted theorem also available as a separate target.
Corollary 5 gives a bounded set of vertices from which the rest of a connected -free graph can be reached in two steps, except when a is present. Its bound is the concrete number three, independent of graph size. In the coloring paper this supplies a small structural seed for later restrictions on vertex palettes. A formal statement of the corollary makes that finite structural claim available independently of any coloring algorithm.
Theorem 4 has broader reuse: it links forbidden induced paths to connected dominating sets for general . The remaining milestones isolate the graph facts needed to connect this general result to the seven-vertex corollary. The article and the cited theorem provide mathematical proofs; these Lean declarations are open theorem statements, with machine-checked proofs still to be supplied. This mission therefore asks for formal proofs of known graph-theoretic results, not for a new resolution of an open mathematical problem.
The difficult step is finding a connected dominating set whose induced graph has the much stronger path restriction in Theorem 4. Ordinary domination by itself does not impose that restriction, and replacing induced-path exclusion with exclusion of all paths would change the class of graphs. The later cases require careful handling of connectedness and the passage from domination within to distance-two domination in . These issues are mathematical as well as formal: an empty set or a merely preconnected induced graph would erase the intended content.
Lean represents as SimpleGraph V with a finite vertex type. Vertex sets are Finset V; is Mathlib's pathGraph t; -freeness is the absence of an induced copy using IsIndContained. The definitions of , , domination and 2-domination are shared within P7ThreeColor.Seed. A connected induced graph uses Connected, which requires at least one vertex. Four-clique existence is ¬ G.CliqueFree 4. The only added standing convention is finiteness, implicit in the source's graph algorithm and finite cardinalities. No extra colorability or clique-free hypothesis is attached to the goal.
The running-time claim in the second sentence of Corollary 5 and the paper's headline Theorem 1 are not formalized because this mission has no machine model. A statement that merely postulates a small set as a hypothesis, or substitutes ordinary domination for 2-domination, would miss the result. Contributions are welcome for proofs of the goal and milestones, reusable facts about induced paths and connected domination, and auxiliary Mathlib lemmas needed to cross between graph isomorphisms, induced subgraphs and finite sets.
Classical mean field theory describes exchangeable diffusions, each interacting with the empirical average of all the others. As the particles become independent copies of a McKean–Vlasov process (propagation of chaos). Many systems of interest are not exchangeable. Particles sit at the vertices of a network and interact only with their neighbours, as in models of opinion dynamics, epidemics on contact networks, synchronisation of oscillators and systemic risk in financial networks. When the network is dense and its adjacency structure converges, the natural limit object is a graphon, a symmetric measurable function that encodes the limiting edge density between "positions" (Lovász, Large Networks and Graph Limits, 2012).
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) develop a law of large numbers for such systems. This mission formalizes their second main result, Theorem 3.1. Under cut-metric convergence of the interaction kernels, the empirical measure of the -particle system converges in probability to the averaged law of a continuum graphon particle system. Related work includes Bhamidi, Budhiraja and Wu (Stochastic Process. Appl., 2019) on weakly interacting particles on inhomogeneous random graphs, Coppini, Dietert and Giacomin (Stoch. Dyn., 2020) on Erdős–Rényi graphs, and Bet, Coppini and Nardi (arXiv:2006.07670) on oscillators on dense random graphs.
Write with Lebesgue measure and fix a horizon . Let with the uniform norm . On one probability space take independent initial states with laws and independent -dimensional Brownian motions , for all . The graphon particle system (2.1) for a graphon and Lipschitz coefficients is the continuum of nonlinear diffusions
where is the law of . Write for the path law of and for the averaged law.
The -particle system (3.1) places particle at label , starts it at , drives it by , and weights its interaction with particle by :
The weights come from a step graphon , constant on the squares of the -grid. Either , or are independent Bernoulli variables for , independent of the noise (Condition 3.1). The kernels converge in the cut norm . Two further norms appear: the operator norm , and the Wasserstein-2 distance on .
Assume the initial laws are measurable in with a uniform -moment and are Lipschitz (Condition 2.1). Assume is -continuous on each interval of a finite cover of (Condition 2.2(a)), and that Condition 3.1 holds with in the cut metric. Then
If, in addition, is continuous at for a.e. at each interior point of the cover (Condition 2.2(b)), then
In order: Remark 2.1, where cut-norm convergence implies operator-norm convergence; Theorem 2.1(a), continuity of in ; the weak-LLN bound (6.4); the discretization bound (6.11); Lemma 6.1,
Lemma 6.2, a law of large numbers for the continuum particles ; the approximation of by continuous graphons; the continuity (6.12) of in the graphon, in a corrected qualitative form; the empirical coupling bound for ; and (6.14).
Theorem 3.1 shows that the averaged graphon law is the correct macroscopic description of a dense heterogeneous particle system. This holds for deterministic weights and for Erdős–Rényi-type random weights, and the graphon may be discontinuous. It is the foundation for graphon mean field games and for control of large networked systems, where replaces the intractable -particle law. Under the regularity Condition 2.2(b) the convergence holds in , particle by particle, along the natural coupling.
The result is proved in the paper (§6.1–§6.2). Nothing in it is formalized. A formal proof would produce reusable infrastructure: graphons, the cut and operator norms, Lusin approximation of graphons, Wasserstein distances between empirical measures, and laws of large numbers for random probability measures on path space. It also needs pathwise stability estimates for SDE systems built on Itô integrals, which goes well beyond what Mathlib has today.
The particles are neither exchangeable nor identically distributed. The classical propagation-of-chaos argument compares each particle with an i.i.d. copy of one McKean–Vlasov process, and it does not apply here. Each must be compared with its own limit , and the error has two sources: the random or discretized weights , and the replacement of by . Cut-metric convergence controls only through integrals against bounded test functions. The interaction term, however, integrates the unbounded function against varying laws . When is merely measurable, the map need not be continuous, and the error of replacing by the average over the labels need not vanish. The direct estimate therefore fails for (3.3) without Condition 2.2(b), and this is the case the goal must cover.
The setting file GraphonMF.DenseLLN.Setting fixes these conventions:
Fin d → ℝ with the sup norm. All statements are invariant under this choice: constants are existential and the other conclusions are limits.Peng1990.SMP.IsItoProcess. The filtrations are the uncompleted natural filtrations and .WassersteinDRO.Duality.wassersteinDistance with values in .Two encodings would trivialize the targets, and both are ruled out. A pointwise or almost-sure reading of (3.3), or convergence of for a single test function, is not the claim. Choosing the constants of Lemma 6.1 and (6.11) after the sequence would make them nearly empty, so they are chosen before it. A sorry-free check confirms that the solution predicates are satisfiable: with the constant paths solve both systems.
Solvers will need several pieces of library work: the inequality , BDG-type moment bounds for the Itô integrals of Peng's library, Gronwall estimates, Lusin's theorem on , and the metrization of weak convergence on (Lévy–Prokhorov). Contributions to any of these are welcome independently of the goal. The paper's proofs are in its §5 (Theorem 2.1) and §6.1–§6.2 (Lemmas 6.1, 6.2 and Theorem 3.1).
Taxi fleets, ride-hailing services and dial-a-ride systems assign incoming customer requests to vehicles under time constraints. Bertsimas, Jaillet and Martin (Online Vehicle Routing: The Edge of Optimization in Large-Scale Applications, Operations Research 67(1), 2019) model the online taxi routing problem, a special case of the online dial-a-ride problem with time windows in which a vehicle serves one customer at a time. They show that mixed-integer optimization over a sparsified graph can dispatch thousands of New York City taxis in real time. The offline problem, in which all requests are known in advance, is the building block of their online algorithms, and its structure determines which offline methods are fast.
The structural fact this mission formalizes is the paper's Theorem 1. When every customer has a fixed pick-up time, the mixed-integer formulation of the offline problem is integral: its linear relaxation has only binary extreme points. So the problem is a linear program in disguise, which the paper uses for its maxflow heuristic.
The source is the authors' accepted manuscript (March 2018, 46 pages); every page and display number below refers to that manuscript, not to the typeset article.
Let be a finite set of customers and a finite set of taxis. Customer has a pick-up time window , and taxi becomes available at time . For customers , the number is the travel time from serving to picking up , and is the profit earned when is served right after . The numbers and are the travel time and profit when is the first customer of taxi .
The graph has the customers and taxis as nodes. Between customers there is an arc exactly when
Taxi nodes have outgoing arcs only. Throughout the paper is assumed acyclic (§2.1, p. 7).
The mixed-integer formulation (5)–(14) (pp. 11–12) has binary variables (customer is picked up right after ), ( is the first customer of taxi ) and ( is served), and continuous pick-up times . It maximizes subject to the flow constraints
the binary constraints (9)–(11), and the time constraints
Constraints (13) and (14) are strengthened Big-M constraints: with , (13) reads .
The LP relaxation replaces (9)–(11) by . A formulation is integral when every extreme point of its LP relaxation has .
If for every customer (and is acyclic, the standing assumption), then
Three further statements from the same pages are included as plain theorems. The first is the paragraph after Theorem 1: a solution with fixed times is feasible for the formulation with windows. The other two are the conditions (3) and (4) of §2.1, which exclude 2-cycles and all cycles of .
Theorem 1 turns a mixed-integer program into a linear program when the time windows shrink to points. The fixed-time problem can then be solved by the simplex method or by a max-flow algorithm. By the paragraph after the theorem, any choice of times inside the windows then gives a feasible solution of the original problem. This is the maxflow heuristic, and the paper reports it to be near-optimal when windows are small. The theorem also locates the source of the integrality gap: the time constraints (12)–(14), not the flow structure.
The result is proved on the page, briefly. No machine-checked version exists. Formalizing it means making the page's "equivalent to a formulation in which variable is removed" precise. The extreme points of the relaxation in -space must correspond to those of a flow polytope in -space. The integrality of that flow polytope must then be proved, which the page settles by appeal to max-flow.
The reduction to the flow system is elementary linear arithmetic. The substance is milestone 3. The system (6)–(8) is not literally in the standard form of a network-flow problem: it mixes an equation defining with inequalities, has unit upper bounds, and allows arbitrary arc sets, including cycles and loops . Neither the integrality theorem for standard-form network flows nor total unimodularity can be applied without first exhibiting a network and checking that the polytope corresponds to its flow polytope. Mathlib has the definition of total unimodularity but not the Hoffman–Kruskal theorem.
The page's phrase "the formulations are equivalent" also hides a step: the goal speaks of extreme points in -space, while the flow system lives in -space, and the two notions of extreme point have to be related explicitly.
Set.extremePoints ℝ.Two trivializing readings are ruled out. "Integral" is the extreme-point property of the relaxation, not the existence of an integral optimum for a given objective, and not the integrality of the mixed-integer feasible set, which holds by definition. Integrality is never demanded of the continuous times .
A complete development needs an integrality theorem for flow polytopes with integer bounds, which Mathlib does not have. Such a result is reusable well beyond this mission. Contributions of general network-flow integrality lemmas are welcome.
In a congestion game, several users choose facilities and each facility becomes more costly as more users choose it. Such games model settings in which each participant chooses a route or collection of resources for personal use while the resulting load is shared. A pure Nash equilibrium is a stable choice of routes: no single participant can lower their own cost by switching. Stability alone gives no assurance that the resulting allocation serves the group well. The price of anarchy compares the social cost of an equilibrium with the best social cost attainable by coordinated choices.
Christodoulou and Koutsoupias studied finite congestion games with linear latency functions and several notions of social cost. For the maximum cost borne by any player, their STOC 2005 paper gives both an upper bound valid for all such games and a family of instances showing that its square-root dependence on the number of players has the right order. This mission formalizes those two claims together. The maximum criterion matters when a single heavily delayed user is significant even if the total cost of the population is moderate.
Let be the number of players and let be a finite set of facilities. Player has a finite collection of available pure strategies, each a subset of . A profile chooses one strategy for every player. For a facility , its load is the number of players whose chosen strategy contains . The latency of at load is . Player pays the sum of the latencies on the facilities they chose:
A profile is a pure Nash equilibrium if no player can decrease this cost by replacing their own strategy while the others keep theirs. The paper calls latencies linear when with ; these are affine functions in standard terminology. The paper displays many calculations for the special case and states the general nonnegative affine convention in its model section. The maximum social cost is ; the total cost is . The paper's average social cost is .
For a game with at least one pure Nash equilibrium and a positive optimal maximum cost, the maximum-cost pure price of anarchy is the largest equilibrium value of divided by the smallest feasible value. The Lean targets use inequalities against every feasible comparison profile rather than dividing by an optimum. This form continues to say something when an optimum has cost zero, and finite strategy sets ensure an optimum exists whenever the profile space is nonempty.
For every , every finite game with nonnegative affine latencies, every pure Nash equilibrium , and every feasible profile , Theorem 5's proof yields
This states a numerical version of the paper's theorem without an unspecified constant. Taking to minimize gives the corresponding price-of-anarchy bound. The bound is about asymmetric games: players may have different strategy sets, and no symmetry assumption is present.
For every integer , let . Theorem 6 provides an identity-latency congestion game with players and facilities, a pure Nash profile , and an optimal profile for which
Every feasible profile in the instance has maximum cost at least . Thus the ratio is , and . The proof's explicit instance has positive comparison cost, so the lower bound cannot be satisfied by a zero-cost game. The source also says such behavior occurs in network congestion games and sketches a network realization in Figure 2; this mission's formal lower target is the finite congestion-game construction.
Together these results identify the order of growth of the worst pure equilibrium maximum cost relative to an optimum: it can grow with the population, yet for linear latencies it grows no faster than a constant times . The upper statement applies to any feasible comparison profile, so it can also be used when a convenient benchmark is known without solving the entire optimization problem. The lower family prevents replacing the square-root dependence by a bound independent of for this class of games.
The results are proved in the 2005 paper; the mission is to give them machine-checked Lean proofs in a common finite-game representation. The development also supplies reusable definitions of congestion games, loads, pure cost equilibria, and maximum social cost, together with the total-cost estimate of Theorem 1 and the intermediate bounds appearing in Theorem 5. The current draft contains statements with sorry placeholders, not completed proofs.
A bound on total player cost does not directly control the cost of the most expensive player sharply enough. An individual player can use several facilities whose loads interact, and bounding each load separately loses the dependence required for the square-root result. Affine coefficients add another issue: the proof printed for identity latencies writes a cardinality where the general statement needs a coefficient-weighted quantity. The lower example has an indexing discrepancy in the printed alternative strategies, so the intended Nash profile must be checked against the costs on every permitted deviation.
Players are represented by Fin N; facilities by an arbitrary finite type in upper bounds and by a type with elements in the lower family. A profile is a function from players to finite facility sets, with feasibility stated separately. Latencies are real-valued on natural-number loads. The IsLinear predicate requires explicit nonnegative affine coefficients. Pure Nash uses a cost inequality; it is the negative-payoff version of a standard finite game's payoff equilibrium. MAX requires at least one player, and all upper-bound targets therefore require . The lower family begins at , where is positive.
The source's number is written as in Lean to keep natural-number subtraction inside its valid range. The two expressions agree for . In the source's one-based indexing, the proposed alternative strategy uses a ceiling index. The printed denominator makes some alternative facilities carry users and breaks the Nash assertion; denominator agrees with Figure 2's short-route users per layer and gives the stated costs. This correction is recorded with the lower theorem. No normalization of coefficients or artificially restricted strategy class is assumed. Contributions to the finite-game definitions, Theorem 1, the player-cost bounds, and the explicit lower instance are all in scope.
Approximate message passing (AMP) is an iterative method for large systems with random matrices. At each step, every coordinate receives a weighted combination of nonlinear messages from all other coordinates, together with a correction for dependence created by earlier steps. For symmetric random matrices, the correction makes a simple description of the high-dimensional iterates possible: a finite collection of covariance matrices predicts their limiting distributions. Bayati, Lelarge and Montanari prove this state evolution statement for polynomial AMP on a broad class of independent sub-Gaussian matrix entries, rather than only Gaussian entries (paper, §§1.2–1.3). It gives a precise distributional account of an algorithm whose coordinates are coupled at every iteration.
The paper has three distinct headline results. Its Theorem 3 compares AMP moments under two matrix laws with equal entry variances, and its Theorem 2 concerns projected cross-polytopes. This mission targets Theorem 4, which identifies the limit of empirical averages of AMP iterates with a Gaussian expectation. The companion missions address the other results; the statements here use their own copy of the paper's AMP model because draft definitions cannot yet be imported across proposals (paper, pp. 5, 8–9).
For each size , let be a random symmetric matrix with zero diagonal. Its entries above the diagonal are independent, centered, and sub-Gaussian at scale . Each coordinate carries a polynomial map at iteration and an initial vector . Their coefficients have degree at most and a uniform bound . The AMP orbit is
The second sum is the Onsager memory term; it is absent at . Here is the Jacobian, so its product with the preceding -vector is another -vector. The initial vectors obey an exponential bound on their squared Euclidean norms. These assumptions form the paper's -regularity condition (Definitions 2–4, pp. 6–7).
A converging sequence has a fixed finite set of classes . Coordinate belongs to for one class , whose proportion approaches . A symmetric nonnegative matrix specifies entry variances: if and , then . Independent labels have class-dependent laws , each a finite mixture of Gaussian laws that may be degenerate. The polynomial maps have the common form for (Definition 5, pp. 8–9).
The empirical second moments of converge in probability to a prescribed positive semidefinite matrix . For , state evolution defines
where is independent of . The index in the first formula and in the second are essential (equations (1.9)–(1.11), p. 9).
For a nonnegative multi-index and a coordinate sequence eventually in class , Proposition 4 identifies the Gaussian limit of each moment. Proposition 5 says the variance of the class-average monomial tends to zero:
The diagonal two-time identity (4.4) is another milestone: has four blocks, each equal to . These are the paper's stated intermediate targets (pp. 15, 30, 32).
For , class , and every locally Lipschitz function with for some , prove convergence in probability:
The target covers polynomial-growth test functions, including functions beyond monomials. The expectation on the right is under the product law of the Gaussian state and the independent class label (Theorem 4, p. 9).
The theorem assigns a computable asymptotic distribution to each class of AMP coordinates at every fixed positive iteration time. It can be used to evaluate empirical observables without tracking the full coupled -dimensional random trajectory. The class weights and variance profile permit heterogeneous coordinates, while the sub-Gaussian assumption covers more matrix laws than a Gaussian-only statement (paper, Introduction and Theorem 4).
The paper proves this result. The mission's Lean statements are compilation-checked targets, with proofs still to be formalized. A completed development would establish the measure-theoretic meaning of the covariance recursion and its Gaussian expectations, as well as the moment and concentration claims needed for the empirical limit. The polynomial representation, random-matrix regularity predicate, and Gaussian transport are reusable for other AMP results from the same paper.
The matrix is reused at every AMP iteration, so a new coordinate is correlated with earlier coordinates and with the matrix entries that produced them. A direct independent-summand argument for its Gaussian limit is unavailable. The memory term is tuned to this dependence, and any formal proof must account for its exact Jacobian and squared-entry form. Passing from individual moments to empirical averages also requires control of correlations between different coordinates. The target allows locally Lipschitz functions with polynomial growth, so convergence for a fixed monomial alone does not finish the job (paper, §4.7).
Vectors in are functions Fin q → ℝ; squared Euclidean norms are explicit sums of coordinate squares. Polynomials use bounded real coefficient arrays as in (4.10), with an explicit Jacobian. Fin N uses zero-based indices. The orbit stores the current and preceding iterates and omits the memory term at . A single probability space carries all sizes; matrix entries, labels, coefficients, and initial vectors have explicit measurability and independence conditions.
The paper's displayed sub-Gaussian formula conflicts with its stated scale, so the model uses the scale required by its moment estimates and imposes the moment-generating bound for all real arguments. Its initial exponential bound is read almost surely at every size, which ensures the expectations used by the paper are well-defined. Label-dependent polynomial coefficients are measurable. The full label vector is independent of the matrix and initial vectors; this makes explicit the independence needed for Theorem 4's Gaussian-label product law. Independence of the induced polynomial coefficients alone would not imply it when ignores part of a label. The initial covariance limit is entrywise convergence in probability; finite-dimensional equivalence makes this the same matrix convergence. Class averages divide by the class cardinality, even though that expression has Lean's default value at an empty class for a small . Positive limiting class fractions make those finite exceptions irrelevant.
Gaussian laws live on Mathlib's Euclidean space and are transported to coordinate vectors. Theorems explicitly assert positive semidefiniteness or integrability where a non-PSD covariance, non-integrable expectation, or non-square-integrable variance could otherwise give a default value. The source's in (1.12) is read as , its summation index, and its final covariance as . The Gaussian covariance is computed by the recursion above; it is not defined from the proposed limit. Contributions establishing moment bounds, covariance positivity, Gaussian integrability, the three milestones, or the full Theorem 4 are within scope.
Markov chain Monte Carlo methods approximate a target probability measure by the law after steps of a Markov chain. A quantitative guarantee for such a method is a bound on the distance between the law after steps and the target, or between the laws of two copies of the chain started from different initial distributions. A standard route to such bounds is contractivity in a Kantorovich (Wasserstein) distance: if one step of the chain contracts the distance between any two initial laws by a factor , the laws converge geometrically.
For many chains of practical interest, including Hamiltonian Monte Carlo with a numerical integrator, contractivity can only be proved on a bounded region of the state space. Outside it, the integrator may be unstable, or the coupling used to prove contraction may fail. Bou-Rabee, Eberle and Zimmer (arXiv:1805.00452, Ann. Appl. Probab. 30(3), 2020) isolate a general principle that turns such local contractivity into a global distance bound. It requires two Lyapunov functions: one controls how quickly the chain can leave the region of contraction, and one controls the distance once it has left. The principle is their Theorem 2.11. It is stated for an arbitrary Markov kernel on a complete separable metric space, and they apply it to adjusted numerical HMC (their Theorem 2.12).
Let be a complete separable metric space with Borel -algebra , and let be a Markov transition kernel on . For a probability measure , the law after steps is , where and . For a non-negative function , .
A coupling of probability measures on is a probability measure on with marginals and ; is the set of couplings. The Kantorovich distance is
Assumption 2.3 asks for a constant and measurable functions such that:
Finally,
Under Assumption 2.3, for every and all probability measures on ,
The constants are those of the paper and are not weakened. Each quantity may be infinite, and the bound is read in .
The result. Theorem 2.11 separates two tasks that are usually entangled in convergence proofs for Markov chains on unbounded spaces. One is a contraction estimate that only has to hold on a sublevel set . The other is a pair of drift conditions that control excursions out of that set. The second term of (42) is made small by choosing large, and the first by choosing large. In the paper this gives bounds to the invariant measure for adjusted numerical HMC (Theorem 2.12), whose contraction (Theorems 2.4 and 2.7) is only established on a ball. The theorem uses nothing about HMC and applies to any chain with a locally contractive coupling and the two Lyapunov conditions. Examples are other discretized diffusions and Metropolis-adjusted samplers.
Formalizing it. The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization requires constructing a Markovian coupling on a general measurable space and working with a generalized, -valued supermartingale stopped at an exit time. It also needs the Markov property with respect to the joint filtration of a coupled pair. Both pieces are reusable in coupling arguments for Markov chains in general.
Contraction on gives no control once either copy leaves that set, and the exit time is random and may be infinite. The bound therefore has to be split at . On the contraction accumulates, which requires optional stopping for a supermartingale that need not be integrable, because may be . On the distance at time has to be bounded by quantities at the random time . This requires the Markov property of each copy with respect to the filtration of the pair: the event depends on both copies. A Markov property of each copy in its own filtration does not suffice. Finally, at the exit time has to be controlled by its initial integral, which is a second stopped supermartingale built from (C1).
MetricSpace with its Borel -algebra, complete and separable; is dist. is a Markov kernel (Kernel S S with IsMarkovKernel), and is the bind of with the -fold composition of .ℝ≥0∞). No Bochner integral appears, so a non-integrable quantity can never be replaced by a junk . In particular, is allowed, as on the page.MongeKantorovichYao.transferencePlans.Supermartingale requires integrability, which the page does not assume. The exit time is -valued, and when the chain never leaves.A complete development needs Ionescu-Tulcea's construction of a Markov chain on a general measurable space (ProbabilityTheory.Kernel.traj in Mathlib), the measurability of the coupling kernel , and optional stopping for -valued supermartingales stopped at an exit time. Contributions are welcome on the milestones individually. The optional-stopping and joint-Markov-property lemmas are reusable beyond this mission.