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?
An associahedron is a polytope whose vertices represent triangulations of a convex polygon and whose edges represent flips between triangulations. The same combinatorial polytope can be realized in different vector spaces with different facet directions. This matters when a construction uses the geometry of the realization, rather than only its face lattice: a linear change of coordinates can preserve its normal fan, while a general combinatorial relabelling need not. Ceballos, Santos and Ziegler compare three constructions and use parallel facets to distinguish them.
Two of those constructions form large families. Hohlweg–Lange choose a word of signs; Santos chooses a triangulation as a seed. Both yield associahedra, and both include the Chapoton–Fomin–Zelevinsky (CFZ) realization. The paper proves that CFZ is their only shared normal-isomorphism class. Its Theorem 6.1 is the target here; the result was announced as Theorem 1.1 in the introduction. Source, pp. 4 and 28.
Fix and a convex polygon with cyclically ordered vertices. A diagonal joins two nonadjacent vertices. Two diagonals cross when their endpoints alternate around the boundary. A triangulation is a maximal collection of pairwise noncrossing diagonals. Every triangulation has diagonals, and replacing one diagonal with the other diagonal of the quadrilateral it borders is a flip. The faces of an associahedron correspond to noncrossing sets of diagonals, while its vertices correspond to triangulations. Source, pp. 5 and 18–19.
A normal fan records the outward normal directions of all faces of a polytope and the cones they span. Two complete fans are linearly isomorphic when a real linear equivalence sends every cone of the first to a cone of the second. Polytopes are normally isomorphic when their normal fans are linearly isomorphic. This is Definition 2.1 of the paper; the comparison is geometric because it requires a linear map. Source, p. 5.
For the Hohlweg–Lange family, choose a sign word and extend it to on the labels . The negative labels, in increasing order, form one boundary chain; the positive labels, in decreasing order, form the other. For a diagonal with endpoint labels , let contain the labels strictly below it. Form by replacing with and with if those labels occur in . The characteristic vector of , considered modulo the all-ones vector, gives its facet normal. Source, pp. 14–16, Definition 4.1.
For the Santos family, choose a seed triangulation and use one basis vector for each seed diagonal . The normal assigned to a diagonal is when . Otherwise it is the sum of over seed diagonals crossing . The cones spanned by compatible diagonal vectors give the fan. The distinguished snake seed joins alternating polygon positions ; this seed gives the CFZ fan. Source, pp. 13 and 18–19.
Let and be the two normal fans, and let be the fixed snake. If is a triangulation, the target says
and it also asserts that . Together these are the uniqueness and existence parts of Theorem 6.1. The result covers dimensions zero and one as well as higher dimensions; Lemma 2.2 uses only for its second sentence, the uniqueness of the inducing symmetry. Source, pp. 6, 16 and 28–29.
The milestone list follows the paper's stated intermediate results: polygon symmetries of the associahedron, the parallel-facet pairs in each family, and the three properties of triangles in the seed that force the snake. Proposition 4.4 supplies the alternating-sign realization used for existence. The parallel-pair targets retain the source's exact count of pairs, through their characterization by the seed flips or the labelled quadrilaterals. Source, pp. 6, 16–17, 23 and 28–29.
Theorem 6.1 gives a complete answer to a comparison question that face-lattice data alone cannot settle: every member of either family has the same associahedral combinatorics, but almost no cross-family pair has linearly equivalent normal fans. It identifies the exceptional class without fixing coordinates for either construction. The characterization of parallel facets also gives a concrete invariant for later comparisons among associahedron realizations. Source, pp. 23 and 27–28.
The paper proves the result mathematically. A complete Lean development would add machine-checked definitions of the two ray systems and a proof of the classification, including the geometric step that a linear fan isomorphism induces a compatible correspondence of facet rays. The polygon triangulation and crossing definitions are already available as a published reusable component; proofs about fans and the two constructions are the remaining work.
An isomorphism of abstract face lattices gives too little information: it exists between all associahedra of the same dimension. The useful comparison must control a linear map on the actual normal vectors. The first obstacle is proving that such a map preserves the rays and therefore preserves which facets are parallel. Then the two explicit descriptions of parallel pairs must be reconciled, and the resulting sign restriction on a triangulation must force alternating turns of its dual path. Showing only that the dual tree is a path is insufficient; path triangulations can make consecutive turns on the same side. Source, pp. 17, 23 and 28–29.
Vertices are Fin (n+3) in counterclockwise positions, with zero-based indexing; Hohlweg–Lange signs apply to labels carried by those positions. Diagonals are unordered pairs. The imported Chvátal triangulation definition gives boundary edges, crossings, maximal noncrossing sets, and their triangles. A cone is the nonnegative span of the vectors assigned to a noncrossing set. The type I vectors are represented in using quotient coordinates ; type II vectors are functions on the seed diagonals. Hohlweg–Lange Proposition 4.3, cited in the paper, identifies the maximal cones of the type I normal fan with triangulations. Source, pp. 15–16.
Normal isomorphism uses a real linear equivalence, dihedral symmetry uses only rotations and reflections of the polygon, and the snake is the explicit alternating triangulation. The cones use the actual facet vectors. These commitments exclude a mere bijection of index sets, an arbitrary permutation of vertices, and a path triangulation with nonalternating turns. The condition appears only where the page has it, in the second sentence of Lemma 2.2 (uniqueness of the inducing symmetry); facet-normal comparisons quantify only over diagonals, exactly the facets represented in the paper. Reusable contributions include combinatorial flip lemmas, linear independence of triangulation rays, and general results about linear maps of simplicial fans.
Firms increasingly account for, and offset, the greenhouse-gas emissions of their entire supply chain, not only their own operations. Emissions in a supply chain are often jointly produced: the footprint of one process (transport, packaging, a molten-bulk delivery) depends on the abatement efforts of several firms at once. When each firm is charged for "its" emissions, the question is how to allocate the footprint of a jointly produced process so that every firm has the right incentive to abate.
Caro, Corbett, Tan and Zuidwijk (working paper, 2012; published in Manufacturing & Service Operations Management 15(4), 2013) model this as a moral-hazard problem in teams. Their §4 shows that a social planner who wants the first-best efforts must, under joint production, double-count emissions: the marginal payments across firms for one process exceed the carbon price. This mission formalizes §5, which looks at a different institutional arrangement observed in practice. One firm, the carbon leader (the paper's example is the cosmetics company Natura), voluntarily pays for all supply-chain emissions at a carbon price and compensates the other firms to induce abatement.
Timeline. Holmström (1982) showed that a budget-balanced sharing rule cannot implement efficient efforts in a team. Strausz (1999) showed that sequential moves can restore efficiency. Battaglini (2006) studied joint production with multidimensional output. Caro et al. (2012) placed the carbon leader in this line: a Stackelberg leader whose commitment plays the role of Strausz's sequential structure.
There are finite sets of firms and processes . Firm chooses efforts , one for each of its abatement actions, and the effort profile lies in the box . Firm earns profit , which is differentiable, concave and componentwise decreasing: effort is costly. Process emits , which is differentiable, convex and componentwise decreasing on the box. The influence matrix has if firm influences process , that is, if , and otherwise.
The first best at carbon price maximizes the social value over the box. At the societal cost its maximizer is , assumed unique.
The carbon leader is a firm , written L in Lean. Every other firm has a reservation profit . The signed transfer is recorded as a payment by firm ; a negative value means compensation from the leader. The leader faces two problems.
Let be optimal for and define, for ,
Then is feasible for , its value equals , and every feasible solution of has value at most :
If , each is supermodular and each is submodular, then componentwise.
The result. Proposition 5 says that, when efforts are unobservable, a carbon leader that can commit loses nothing compared with contracting on efforts. A linear rule, the form footprint accounting already takes in practice, achieves the benchmark. The rule charges each firm the full price on every footprint it influences, so emissions are double-counted internally, yet the supply chain as a whole pays for carbon once. This is how the paper reconciles its §4 impossibility (a planner must double-count) with a footprint-balanced scheme: the leader moves first and is excluded from the incentive constraints. Lemma 6 then says that a leader paying a price below the societal cost induces weakly less effort than the first best.
Formalizing it. Both results are proved in the paper. As far as the platform's catalog shows, neither is machine-checked anywhere. The proof of Proposition 5 combines a reduction of a bilevel problem with a first-order argument for concave games on a box. The appendix compresses these into three sentences, one of which contains a misprint ("since f is concave" for convex). Formalizing it makes the leader–follower conventions explicit: the leader's tie-breaking choice of follower efforts, and the unilateral deviation in (11).
The paper calls a constrained version of , but their feasible sets are not literally nested: 's payments are functions of the emission vector and 's of a firm's own effort. Establishing the common upper bound therefore requires care with the two payment domains and the participation constraint (10).
The incentive compatibility of (12) is the substantive step. It is a global best-response claim on a closed effort box, while the appendix states only a first-order identity at an interior point. The influence indicator also has to agree with every action-level derivative, rather than only their sum. For Lemma 6, the optimum at price need not be unique.
e : (n : ι) → act n → ℝ, and a unilateral deviation is Function.update.deriv along one coordinate. Every theorem that uses one assumes differentiability.sSup. is the objective at an optimal pair.Rule (12) is a function of the emission vector only, and the deviation in (11) moves only firm 's efforts. A formalization in which payments may depend on efforts, or in which a deviation also moves the leader, would make the goal trivial and is ruled out. A sorry-free instance with two firms checks that every hypothesis of the goal can be satisfied. Supermodularity reuses the published Supermodularity.Monotonicity.SupermodularOn. All other definitions live in CarbonDoubleCount.Leader.Setting.
Proofs of the milestones, or alternative routes such as a Lagrangian argument for incentive compatibility, are welcome. A general lemma that a concave differentiable function on a box is maximized at an interior stationary point would be reusable beyond this mission.
Many graph classes are defined by excluding a fixed graph as a minor. A minor can be formed by deleting vertices, deleting edges, and contracting edges. Planar graphs, for example, exclude as a minor. Édouard Bonnet, Eun Jung Kim, Stéphan Thomassé, and Rémi Watrigant proved that every class excluding a fixed clique minor has bounded twin-width, a graph parameter that controls how much adjacency information is lost while vertices are successively combined. Their result connects a classical graph-minor restriction with the contraction parameter used in their first-order model-checking framework. The explicit bound is very large, but it establishes that the width depends only on the excluded clique size, rather than on the graph's number of vertices. Bonnet et al., Twin-width I, Theorem 6.3.
Let be a finite simple graph. A partition of its vertices is a collection of nonempty, disjoint parts covering all vertices. Two distinct parts are homogeneous if every vertex pair across them is adjacent, or every such pair is nonadjacent. Otherwise the pair of parts is marked red. A -partition has at most red neighbours at every part. A contraction sequence begins with singleton parts, merges two parts at each step, and finishes with at most one part. The statement says that such a sequence exists with every intermediate partition a -partition. This partition formulation is equivalent to the paper's original description in terms of trigraph contractions. Bonnet et al., pp. 3:11–3:12, 3:32.
Write for the complete graph on vertices. The graph is -minor free when cannot be obtained from by the minor operations above. The Lean statement uses a branch-set formulation: a minor model consists of disjoint, nonempty, connected vertex sets, with a connecting edge for each edge of the minor. Bonnet et al., p. 3:9.
An ordering of the vertices gives a Boolean adjacency matrix , with entry at an edge and otherwise. A division cuts its rows and columns into nonempty consecutive intervals. A zone is mixed if it is neither constant down its columns nor constant across its rows. A -mixed minor is a division with row intervals and column intervals in which every zone is mixed; a -grid minor requires a in every zone. A matrix is -mixed free or -grid free if the corresponding minor does not exist. A mixed Boolean zone always contains a , so grid freeness implies mixed freeness. Bonnet et al., pp. 3:18–3:19.
The order used in the proof is a depth-first search (DFS). A discovery order lists the vertices; at each time the active vertex is the lastly discovered vertex that still has an undiscovered neighbour, and the next vertex is a neighbour of the active vertex, which becomes its parent in the DFS tree . The Lex-DFS breaks ties: among the connected components of the undiscovered vertices that meet the active vertex's neighbourhood, it enters one whose word (the vector recording which discovered vertices have a neighbour in the component) is lexicographically largest. The proof also uses minimal subtrees of : the union of the tree paths between the vertices of a set. Bonnet et al., pp. 3:26–3:27.
The main target is the explicit excluded-clique-minor bound. With
the goal says
The in follows the value defined and used in the proof of Theorem 6.3 on p. 3:26; the printed theorem statement has . The formal target uses the proof-supported bound and records the printed statement verbatim in its provenance. It does not assert the paper's asymptotic triple-exponential notation as a separate theorem. Bonnet et al., pp. 3:26–3:29.
The milestones follow the proof in order:
The Helly theorem is a reference to an existing open platform statement rather than a duplicate draft. Bonnet et al., pp. 3:22–3:29.
The theorem supplies a uniform contraction-width bound for every fixed excluded clique minor. In particular, the paper applies it to planar graphs through exclusion of . Its numerical value is far from small; the article remarks that the planar specialization has billions of digits. Without the result, excluding a clique minor alone would not yield the particular twin-width certificate required for those applications. Bonnet et al., p. 3:29.
The mathematical result is proved in the cited paper. This mission asks for machine-checked statements and, eventually, proofs of its graph and matrix claims. The reusable output includes a precise partition model of graph twin-width, interval-division models of mixed and grid minors, and a graph statement that converts a mixed-free adjacency order into a contraction-width bound. No machine-checked proof of these new target items is claimed here.
A dense pattern of nonzero matrix zones does not directly give a graph minor. A matrix zone merely contains an edge somewhere between two vertex blocks. Those blocks need not induce connected subgraphs, and contracting them as if they were connected would use operations unavailable to graph minors. The proof also needs a vertex order with strong enough structure to control how the relevant connected sets overlap. These are the points that separate the grid-free milestone from a direct application of the matrix grid theorem. Bonnet et al., pp. 3:26–3:29.
The conversion from a mixed-free adjacency matrix to graph twin-width has a second issue: matrix twin-width permits separate row and column contractions, while a graph contraction merges one vertex partition and must keep the two matrix axes synchronized. Theorem 5.8 addresses the graph case. The milestone uses the explicit constant that the paper applies at the end of Theorem 6.3, while the printed Theorem 5.8 states an asymptotic bound. Bonnet et al., pp. 3:22–3:23, 3:29.
Graphs are finite simple graphs, and twin-width and the number of division parts are natural numbers. The real constants and are compared with natural-number twin-width through ; the explicit value is positive. Vertex orders are equivalences with . Matrix divisions use strictly increasing cut points, so every part is a nonempty consecutive interval. The adjacency matrix has a zero diagonal because simple graphs have no loops. The graph-minor predicate and the subtree representation come from existing published definitions with the same conventions; graph twin-width and the matrix objects are local draft definitions shared across this mission. Bonnet et al., pp. 3:9, 3:12, 3:17–3:19.
The grid-free milestone holds for every Lex-DFS order, as in the paper, and the existence of such an order is a separate milestone. Lemmas 6.4–6.6 are stated in the proof's context: a DFS, and vertices , and blocks with exactly the order and adjacency properties the page uses. Lemma 6.5 is posed for every block except the last. As printed it also covers the last block , and for that block it can fail. A five-vertex example satisfies every hypothesis of the lemma and violates the printed conclusion; it is checked in Lean in the sanity file, and the formal item records the change. The theorem's bound is uniform over all finite graphs on the excluded-minor hypothesis. A twin-width definition using an unrestricted real infimum, a sequence that skips directly to one part, red degree counted over homogeneous pairs, or a grid minor over arbitrary noninterval partitions would change the claim. Components and empty graphs use the endpoint conventions stated above. The hypothesis in the graph conversion milestone rules out the degenerate zero-division case.
Contributions toward the core grid-free order claim, the symmetric contraction bridge, the component theorem, and the reusable minor and division lemmas are within scope. The running-time claims elsewhere in the paper and the pointer construction and the two -minor constructions inside the proof of Theorem 6.3 are not separate milestones: they are unnumbered and their statements need the pointers. They remain part of the grid-free milestone.
Join-the-shortest-queue (JSQ) is the basic load-balancing rule for a system of parallel single-server queues: every arriving customer joins a queue of minimal length. It is optimal in several senses for homogeneous servers and is the reference policy against which cheaper rules (power-of- choices, join-the-idle-queue) are measured. In the Halfin–Whitt regime, where the arrival rate is with for a fixed , Eschenfeldt and Gamarnik (arXiv:1502.00999) proved that the suitably centred and scaled numbers of queues of length at least one and at least two converge, on finite time intervals, to a two-dimensional reflected diffusion. Braverman (arXiv:1801.05121) justified the interchange of limits (the stationary distributions of the -server chains converge to the stationary distribution of the diffusion). One ingredient of that result is that the diffusion is exponentially ergodic, so it has a unique stationary distribution that is approached at a geometric rate. This mission formalizes the analytic core of that ingredient: a Foster–Lyapunov drift condition for the diffusion's generator.
Timeline. Eschenfeldt and Gamarnik (2015) proved the process-level diffusion limit, the first analysis of JSQ in this regime. Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) showed that a class of load-balancing schemes shares the same diffusion limit. Braverman (arXiv 2018, v2 2019; Math. Oper. Res. 45(3), 2020) proved tightness of the scaled stationary distributions and exponential ergodicity of the limit, which together give the interchange of limits.
The state space is the closed quadrant . For write , , . On the boundary these are one-sided derivatives, and denotes the twice continuously differentiable functions in this sense.
The diffusion limit solves
with a standard Brownian motion and a nondecreasing regulator that increases only when . For with the reflection condition , its generator acts by
The construction of the Lyapunov function uses an auxiliary integer and the fluid operator
the generator of the deterministic fluid path , . A smoothed indicator (a piecewise cubic that rises from at to at ) and two levels define the PDEs
each with the reflection condition. Their solutions are written explicitly in terms of the fluid hitting times (through the Lambert W function) and , and the curves that split into regions .
For every there exist , , a compact set and with on , as in , and , such that
The constants are unspecified and depend only on ; the statement involves no .
By the criterion of Down, Meyn and Tweedie (Ann. Probab. 23, 1995, Theorem 5.2), a drift inequality of the form (5.2) with compact and implies that the diffusion is positive Harris recurrent and exponentially ergodic in the -norm (Theorem 3 and Corollary 1 of the paper). Together with tightness of the prelimit stationary distributions (mission 1 of this series), this gives convergence of the stationary distributions of the JSQ chains to that of the diffusion. That justifies approximating steady-state JSQ performance by the diffusion.
The construction itself is reusable. Solving the fluid-model PDE and exponentiating the solution is a general route from fluid stability to exponential ergodicity of a diffusion. This mission writes that route out for one reflected diffusion with explicit hitting-time formulas.
Status: the result is proved in the paper; no part of it has a machine-checked proof. Theorem 3 and Corollary 1 are not posed, because they rest on the cited Down–Meyn–Tweedie theory and on the existence of the reflected process, neither of which Mathlib has.
The reflecting boundary rules out the first candidates. The condition excludes exponentials of linear functions such as unless . The natural candidate from the fluid model, the exponential of the fluid time needed to reach a box, has a discontinuous integrand and is not in , so cannot be applied to it. The milestone functions , are given piecewise across the curves , and the lines , through implicitly defined hitting times. Three things are hard: regularity across these interfaces, the Lambert W asymptotics as , and second-derivative bounds that hold uniformly on the unbounded domain with the stated dependence on and .
ℝ × ℝ, and is Set.Iic 0 ×ˢ Set.Ici 0. Partials are fderivWithin ℝ f Ω in the coordinate directions, which are one-sided at boundary points. is ContDiffOn ℝ 2 f Ω.WithTop ℝ, with when no solution exists, and its real value is used only where it is finite. (the curve ) is the solution of a nonlinear system whose uniqueness is Lemma 5.Mean field control studies the optimal control of a very large population of interacting agents through the limit in which the population is replaced by its distribution. The limit problem is a McKean–Vlasov (MKV) control problem: the dynamics and the cost of a representative agent depend on the law of its own state. Such problems arise in systemic risk, crowd motion, energy management and the planning of large distributed systems; the reference account is Carmona and Delarue, Probabilistic Theory of Mean Field Games with Applications I–II (Springer, 2018).
MKV control problems are rarely solvable in closed form, and grid-based numerical methods suffer from the dimension of the state. A practical alternative is to simulate a finite population on a time grid, parametrize the feedback control by a neural network, and minimize the simulated cost by stochastic gradient descent. Carmona and Laurière, Convergence analysis of machine learning algorithms for the numerical solution of mean field control and games: II — the finite horizon case (Ann. Appl. Probab. 32(6), 2022, doi:10.1214/21-AAP1715), quantify how close this computable proxy is to the true optimum. This mission formalizes the statement of their main result and of the propositions and lemmas its proof is built from.
Fix a horizon , a state dimension , a control dimension (controls take values in ), an initial law on , a drift , a volatility (not controlled), a running cost and a terminal cost ; ranges over , the probability measures with finite second moment, compared with the Wasserstein distance .
Problem 1 (the MKV problem). On a probability space carrying a -dimensional Wiener process and an independent , minimize over progressively measurable square-integrable controls
where is the law of .
Problem 3 (the -agent problem). agents with independent Wiener processes and i.i.d. initial states use a common feedback function ; the law is replaced by the empirical measure , and the cost is .
Problem 2 (the computable proxy). With and , the agents follow the Euler scheme
with i.i.d. Gaussian increments , and is the expected time-discretized cost. The feedback ranges over , the one-hidden-layer neural networks from to with hidden neurons and activation ; is -periodic, of class , with .
The standing assumptions (§2.2 and Appendix A of the paper) make affine in (A1), make differentiable in (in in the sense of the L-derivative) with Lipschitz derivatives (A2)–(A3), make strongly convex in (A4), and add the regularity (B1)–(B3), (C1)–(C3). Under them the reduced Hamiltonian has a minimizer , the Pontryagin forward–backward system has a solution with marginal flow , and for a regular decoupling field . The optimal feedback is .
for a constant depending only on the data and on , for all .
Lemma 18 (Lipschitz continuity of ), Proposition 10 (network approximation of a function and its first two -derivatives at rate on ), (C.2) (moment bounds uniform in ), Proposition 13 (stability of under feedbacks close on a ball), Lemma 19 (time regularity of the particle system) and Lemma 14 (strong error of the Euler scheme).
The theorem certifies the standard deep-learning approach to mean field control: the value computed by minimizing the simulated finite-population, discrete-time cost over networks is, up to an explicit error with separate rates for population size, network width and time step, no larger than the true MKV value. The rates also expose where the method loses: the term is a curse of dimensionality in the network step (Remark 11).
The result is proved in the paper (§3 and Appendices B–D); the proof of Proposition 7 is a modification of Carmona–Delarue, Vol. II, Theorem 6.17. None of it is formalized. A formal development would provide the first machine-checked bridge between a stochastic control problem of McKean–Vlasov type and a concrete learning architecture, and its intermediate results (moment and stability estimates for interacting particle systems, the strong error of an Euler scheme with constants independent of the number of particles, simultaneous approximation of a function and its derivatives by periodic networks) are reusable on their own.
Each step rests on research-level analysis. Proposition 7 needs the Pontryagin principle for McKean–Vlasov control, the propagation of chaos for the optimally controlled system, and the Fournier–Guillin rate for empirical measures, whose exponent and logarithmic correction at appear in the bound. Proposition 8 requires approximating the optimal feedback together with its first two derivatives in , because the time-discretization step needs regularity of the approximating network; standard universal approximation results give no control of derivatives, and the available simultaneous approximation results hold only for periodic functions, which forces a localization to a ball whose radius must be balanced against the approximation rate. Proposition 15 cannot be obtained from classical Euler estimates for a system of equations, whose constants grow with : the estimates must be done agent by agent through the empirical measure.
is Fin d → ℝ with the sup norm; every constant is existential, so all statements are norm-independent. Time is ℝ≥0 for processes. Solutions of (2.2) and (3.2) use the published Itô-process predicate Peng1990.SMP.IsItoProcess (for , with continuous paths and the natural filtration of the initial data and the noise); the backward equation of the Pontryagin system uses Peng1990.SMP.SolvesBSDE; is the published WassersteinDRO.Duality.wassersteinDistance. Problem 2 is law-level: the Euler scheme is a deterministic map of initial positions and increments, integrated against ; Lemma 14 couples it with the continuous system through the Brownian increments, as the paper does.
The hypotheses are bundled as Coeff ((A1)–(A4), (B1), (B3), (C1), with witnesses for every derivative; the L-derivative is the Fréchet derivative of the lift on ) and DecouplingField ((2.6), existence of a solution of (2.7) on some Problem-1 space, , (B2), (C2), (C3)). Disclosed readings: 's L-convexity is (A4) without and with right-hand side ; unique solvability of (2.7), uniqueness and Lipschitz continuity of are not assumed (the last is Lemma 18); Proposition 13 lets its constant depend on bounds for , as its proof does; Proposition 15 reads the first bound of (3.16) as . Infima are stated pointwise (), never as a real ⨅, and throughout. The hypothesis bundle is not vacuous: a sorry-free check exhibits the model , , , with , satisfying every assumption on any Problem-1 space. Junk values cannot trivialize the goal: the costs are Bochner integrals whose integrability follows from the assumptions, so a non-integrable cost would only make the claimed inequality harder, never vacuous.
Contributions are welcome at every level: proofs of the milestones, in particular the self-contained Lemmas 14 and 19, (C.2) and Proposition 13; infrastructure for the L-derivative, Itô's formula for the published Itô processes, empirical-measure convergence rates, and trigonometric approximation of periodic functions.
The two-dimensional directed polymer is a random walk whose paths are reweighted by a random space-time environment. Its logarithmic partition function is a discrete counterpart of the height field of the two-dimensional Kardar–Parisi–Zhang equation. At the intermediate-disorder scale, the random weighting becomes weaker as the walk grows, yet its fluctuations remain visible. Caravenna, Sun and Zygouras prove that throughout the subcritical regime , spatial averages of the centred log-partition function converge to Gaussian fluctuations described by an additive stochastic heat equation (Theorem 1.6, p. 6).
The polymer formulation matters because it is a concrete finite-path model: each partition function is an average over finitely many nearest-neighbour walks, while its limit retains the effect of disorder at every scale. The same paper treats the continuum KPZ equation separately; this mission takes its stated polymer theorem as the target. Earlier work in dimension studied a different intermediate-disorder scaling and a Wiener-chaos limit (Alberts, Khanin and Quastel, 2014). The two-dimensional result concerns a distinct regime and a different limit.
Let be the simple symmetric random walk on . Starting at , it chooses each of its four nearest-neighbour steps with probability . Write , and let be an independent copy. Their expected overlap through time is
For a fixed , the disorder strength is . The environment consists of independent, identically distributed real random variables with mean zero, variance one and finite exponential moments at all sufficiently small positive arguments. Its logarithmic moment generating function is . The law also obeys the paper's concentration assumption (1.20): convex 1-Lipschitz functions of any finite collection of environment variables have stretched-exponential deviations from a median, measured with Euclidean distance (pp. 5–6).
For a length- walk from , sum over times , exponentiate, and average over paths. The result is the partition function . Where is finite, its centring gives . A restricted function samples disorder only from the space-time sites in . Section 2 uses an early window near the start and a late window to define , its remainder , and (pp. 7–9).
At macroscopic time and position , the fluctuation field is
The floor of a vector is componentwise. In the numerator, uses the disorder strength ; the field is divided by , exactly as in (1.23).
For every and smooth compactly supported test function , Theorem 1.6 asserts
The tested limit is centred Gaussian. Its variance is , where
The milestone list follows the paper's stated results: second-moment bounds (3.2)–(3.4), higher moments for some (3.12), a left-tail bound (Proposition 3.1) and the negative and logarithmic moments it yields (3.14)–(3.16), vanishing spatial averages for two error terms (Propositions 2.1–2.2), replacement by the late-window term (Proposition 2.3), and the Gaussian limit for that term (Proposition 2.4). These are the exact result labels used in Sections 2 and 3 (pp. 8–13).
The theorem identifies the fluctuation law of the logarithm of the polymer partition function for every strictly below the critical value . The coefficient records the disorder strength in the limiting covariance, and the time reflects the two-dimensional walk's covariance convention. Without the spatial averaging and normalization, the statement would concern a different observable; the theorem characterizes a field tested against compactly supported functions (Theorem 1.6 and Remark 1.7).
The result is proved in the cited paper. This mission asks for a machine-checked proof of that known result and its curated supporting statements. The reusable output includes a finite-path polymer model on , a precise restricted partition function, the disorder concentration assumption, and the Gaussian covariance functional. The published atomic polymer model already supplies the space-time cells, steps, walk positions and log moment generating function; this mission extends that common base to the centred, spatially shifted model of this paper.
Pointwise size does not identify the limiting spatial fluctuations. The early-window partition function captures much of at a fixed site, yet its averaged logarithm vanishes at the target scale. The small remainder cannot simply be discarded: after division by the early-window function, its late-time component carries the Gaussian limit. The paper separates these effects in Propositions 2.1–2.4 and needs moment and left-tail control to keep the logarithmic expression meaningful (Sections 2–4). A direct Taylor expansion of around its mean would lose this distinction.
Lean uses finite sequences of four-neighbour steps and the Euclidean norm on . Disorder is a family indexed by positive walk times and lattice sites; the time-zero row of its ambient type is unused. The full and restricted partition functions are finite walk averages. The concentration assumption quantifies over Euclidean 1-Lipschitz convex functions and their medians. The test class of Theorem 1.6 is ; the four Section 2 propositions use . Treating “smooth” as analytic would make compactly supported tests trivial, so the Lean statement uses the smooth differentiability order.
The target additive stochastic heat observable is represented by its Gaussian law and the kernel above; the random field itself is not formalized, and the statement does not need it. The kernel takes extended nonnegative values because it is infinite on the diagonal; the diagonal has zero area in the tested covariance integral. Moments and convergence use extended nonnegative integrals. The paper assumes exponential moments only near zero, so bounds whose printed form quantifies over every are stated for all sufficiently large , avoiding default values of the logarithmic moment generating function at early indices. The spatial sums have finite support because the test functions do. Replacing the Euclidean norm by the sup norm would change the early window (a square instead of a disc), the kernel and the class of 1-Lipschitz functions in (1.20), so all of these are Euclidean. The polymer propositions are stated for every window exponent below a threshold, as in (2.2), and the passage from the time-1 lattice averages of Propositions 2.1–2.4 to the general-time integral of Theorem 1.6 is part of the proof work, not of the statements. Contributions to the polymer moments, left-tail estimate, replacement propositions and Gaussian limit all feed the stated goal.
A retailer that decides which variants of a product to stock (its assortment) trades off the revenue each variant brings against the operational cost of carrying it. The classical model of this trade-off uses the multinomial logit (MNL) model of consumer choice: a consumer who does not like what the store offers simply buys nothing (van Ryzin & Mahajan 1999). In practice a consumer who does not like what the store offers can also go elsewhere. Cachon, Terwiesch and Xu (working paper, December 2002; published in MSOM 7(4), 2005) add this consumer search to the MNL model and ask how it changes the retailer's optimal assortment.
They study two search models. In the overlapping assortment model (§3.1), a consumer who searches pays a search cost and then finds a competitor carrying every variant, so search can only reveal variants the store does not carry. This mission formalizes the paper's Theorem 6 about that model: when search is cheap, the store's best response is to carry everything.
There are variants, , and an assortment is a subset ; write for the variants the store does not carry. A consumer's utility for variant is , where is the variant's expected net utility and the shocks are independent with the zero-mean Gumbel distribution function , with scale and Euler's constant. The no-purchase option is a "faux variant" with utility . Its preference is , and is the preference of not buying.
Without search, variant has the MNL demand (2), . Following Theorem 1, put and
the probability that every option the store offers, including not buying, has utility at most . The best utility outside the store, , has a density . A consumer whose best in-store utility is searches when the expected gain exceeds the cost,
and the search threshold is the solution of , equation (4). Theorem 3 gives the resulting demand,
When the store carries everything there is nothing to search for (p. 28: "If the retailer offers the full assortment, there will be no consumer search"), so .
Variant earns margin per unit and costs to carry, where is concave and increasing (economies of scale). The retailer's profit is
As printed, the second line of (13) writes where is meant; the definition uses the latter.
If the full assortment is profitable, , then there is a such that
The threshold depends on the data but is one number for all assortments .
Theorem 6 separates the overlapping model sharply from the no-search MNL model and from the paper's independent-assortment model. In those two models every variant in an optimal assortment must earn a strictly positive profit, because dropping a loss-making variant only shifts demand to the remaining ones. In the overlapping model the assortment also controls whether consumers leave: carrying an unprofitable variant can pay because it removes a reason to search. Theorem 6 is the extreme form of this effect, stating that the motive to prevent search can override the profitability of individual variants entirely (§4.3, p. 17).
The paper gives only a short sketch of the proof. The steps it asserts without proof are the existence and uniqueness of , its monotonicity and limits in , and the explicit density . This mission states each of them as a milestone. No machine-checked version of any of these results is known.
The search threshold is defined only implicitly, through an improper integral of the density of a maximum of Gumbel variables. Each property the theorem needs (that the equation has exactly one root, that the root moves monotonically with , and that it escapes to as ) has to be read off the integral. That means controlling on the whole real line: its convergence, its strict decrease, and its limits at .
The final comparison is not a direct consequence of either. A variant's profit tends to rather than to , so the conclusion depends on the sign of , and must be chosen uniformly over all assortments.
The shared model is the definition AssortSearch.FullAssort.Model, which builds on the published MNL share RetailVariety.Structure.share. Its conventions:
Fin n, numbered from 0; the paper's variant is index . The no-purchase option is not a variant: is a separate positive real.Real.eulerMascheroniConstant.Finset (Fin n), including , whose profit is .Several formalizations would make the goal trivial or empty, and each is excluded:
A complete development needs the integral calculus of the Gumbel tail ( and its derivative in ) and the product-measure computation of the law of a maximum of independent variables. Both are reusable beyond this paper, for instance in other search and extreme-value models. Contributions are welcome on any milestone, and on helper lemmas such as the continuity of and its limits at .
Twin-width is a graph parameter introduced by Bonnet, Kim, Thomassé and Watrigant in Twin-width I: Tractable FO Model Checking (J. ACM 69(1), Article 3, 2021; arXiv:2004.14789). Its main algorithmic consequence is that first-order model checking is fixed-parameter tractable on graphs given with a contraction sequence of bounded width. A parameter of this kind is useful only if the classes it bounds are closed under the constructions that arise in practice. Many such constructions are first-order definable: the complement of a graph, its square (join vertices at distance at most two), the map graph of a planar map. Section 8 of the paper shows that twin-width is stable under every such construction: a first-order interpretation of a class of bounded twin-width has bounded twin-width. Bounded VC-dimension, by contrast, is not preserved (interval graphs have VC-dimension at most two but interpret every graph, p. 3:41).
The result has since become the basis of the "model-theoretic" view of twin-width: bounded twin-width classes are closed under first-order transductions (Theorem 8.1 of the paper), and later work identifies them, among ordered structures, with the monadically dependent classes (Twin-width IV, Bonnet, Giocanti, Ossona de Mendez, Simon, Thomassé and Toruńczyk).
Let be a finite simple graph on a vertex set .
Two vertex sets are homogeneous if all pairs in are edges or none is. For a partition of , the red graph has the parts as vertices, two distinct parts being adjacent when they are not homogeneous. is a -partition if has maximum degree at most . The graph has twin-width at most , , if there is a sequence of -partitions from the partition into singletons to a partition with at most one part, each obtained from the previous one by merging two parts (p. 3:32).
A prenex formula of depth with two free variables is
with a Boolean combination of atoms and , . The interpretation is the graph on in which distinct are adjacent iff . For a class , is the class of all induced subgraphs of the graphs , .
The proof works with morphism-trees. The complete tree has as nodes all tuples of vertices with , the parent of a tuple being its prefix. Two sibling nodes are equivalent in if an automorphism of the tree swaps them, preserving equalities and adjacencies among the entries of every tuple and the part of of every entry. A reduction deletes one of two equivalent siblings with its subtree, repeatedly; a reduct admits no further reduction. Two vertices are adjacent in when and are equivalent in some reduction of , and is the partition into the connected components of .
For every prenex formula and every there is such that
The bound depends on and only. No explicit function is asserted: the paper gives none (the proof goes through a tower-type bound on reducts).
Theorem 8.3 turns every first-order definable graph construction into a source of bounded-twin-width classes: squares and fixed powers of planar graphs, complements, map graphs (as transductions, via Theorem 8.1), -planar graphs and bounded-degree string graphs. Combined with the model-checking algorithm it gives FPT first-order model checking on all these classes, provided a contraction sequence is available. The theorem is also the first step of the model-theoretic characterisations of bounded twin-width in the later papers of the series.
The result is proved in the paper; no machine-checked proof of it, or of any twin-width bound, exists to our knowledge, and Mathlib has no notion of twin-width or of first-order interpretations of graphs. The mission asks for a formal proof of the graph case. The morphism-tree milestones are also the combinatorial core of the paper's linear-time model-checking algorithm (Theorems 7.5, 7.15), whose running-time statements are not part of this mission.
The obvious approach refines the -partitions of by the "type" of each vertex with respect to . The number of such types is not bounded: a vertex's behaviour depends on the whole graph through the quantifiers. The paper replaces types by the components of , defined through reductions of morphism-trees that respect . Two facts must then be shown, and neither is local in an obvious way. First, the number of components inside a part is bounded (Lemma 8.5); this needs the pruned shuffle, which assembles a reduction of the whole tree from reductions of the local trees , and the fact that it commutes with reductions (Lemma 7.12), where an automorphism of one local tree must be extended to the shuffle without breaking adjacency between non-homogeneous parts. Second, far-apart components are homogeneous in (Lemma 8.6), which needs the evaluation argument of Lemma 8.4 inside a reduction of the partitioned tree.
SimpleGraph V on a Fintype with decidable equality. Twin-width is the predicate TwinWidthLE G d in the paper's partition form (pp. 3:12, 3:32); trigraphs are not formalized, and twin-width is never an infimum, so no junk value of sInf can make a bound vacuous. Merge steps merge exactly two distinct parts, so a sequence cannot jump to one part.FirstOrder.Language.graph.Formula (Fin 2), evaluated in G.structure; variable 0 is , variable 1 is . Prenex is Mathlib's IsPrenex; quantifier depth qdepth is defined in the mission ( counts once).Set (List V)), the paper's identification of a node with its current path (p. 3:30), which is exact for reductions of complete trees. Equivalent siblings are distinct. Distances in are in , so disconnected parts are far apart. The sequence graph uses 0-based indices, hence the exponent . The pruned shuffle is defined by its characterisation (each component of the sequence graph of a tuple lies in the tree of its local root). Lemmas of §7.3 carry its standing assumption .Reusable beyond this mission: the partition form of twin-width, quantifier depth of first-order formulas, and the morphism-tree machinery (reductions, pruned shuffles), which formalizes the algorithmic core of first-order model checking on bounded twin-width. Contributions welcome: proofs of the §7 lemmas, of Lemma 8.4 by induction on the quantifier prefix, and the closure of twin-width under induced subgraphs.
Large systems of interacting diffusions — neurons, oscillators, agents in a network game, particles in a queueing or load-balancing model — are usually analysed through their mean-field limit: as the population grows, each particle interacts with the empirical law of the others, and the system is replaced by a single nonlinear (McKean–Vlasov) equation. The classical theory assumes that every particle interacts with every other one with the same strength. Real networks are heterogeneous and sparse: particle interacts with particle only through an edge of a random graph, and the number of neighbours of a particle is much smaller than the population size.
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) describe the heterogeneity by a graphon and prove laws of large numbers and rates of convergence for such systems. This mission is the fifth of a series formalizing that paper. Its subject is the paper's quantitative result for not-so-dense graphs: when the edges are sampled from a Lipschitz graphon and then thinned by a sparsity factor , the average mean-square distance between each particle and its graphon limit is of order for every .
Let with Lebesgue measure. A graphon is a measurable symmetric function . Fix a horizon and write with the norm .
One probability space carries, for every label , an initial state with law and a standard -dimensional Brownian motion , the whole family being independent. The limit system (4.2) is a continuum of diffusions, one per label:
The particles are independent but not identically distributed; their laws are coupled through the -integral.
The not-so-dense -particle system (4.1) uses the same initial states and Brownian motions at the labels :
The edges are percolated samples of (Condition 4.3): , independent for and independent of the noise. A particle has about neighbours, which is why the interaction is scaled by .
The standing hypotheses are Condition 4.1 — measurable with bounded second moments; bounded and Lipschitz; bounded, Lipschitz and invertible with bounded inverse; and — and Condition 2.3: on finitely many intervals covering , the map is Lipschitz in the Wasserstein distance , and is Lipschitz on every block .
Under Conditions 2.3, 4.1 and 4.3, for each there is with
The constant depends on and on the data, never on . The bound is on the average over particles, not on the maximum.
Theorem 4.2 gives an explicit rate for the convergence of a particle system on a sparse random graph to its graphon limit. Its companion, Theorem 4.1 (mission IV), proves the law of large numbers under weaker hypotheses but without a rate. The rate says that the effective sample size is , the typical degree, not : graphs with still approximate the graphon system as long as the degree grows. Results of this type justify replacing a large heterogeneous network by its graphon limit in control and game problems, such as graphon mean-field games, where the error of the replacement must be quantified.
The paper proves the theorem by hand; none of its results has a machine-checked proof. The formalization produces precise statements of the not-so-dense model, of the estimates of §7.1 that hold for any sparsity, and of the discretization bound, each usable on its own. The milestones (7.10) and (7.15) are the paper's key estimates for sparse interactions and are shared with mission IV.
The obvious approach is to compare each with by Gronwall's inequality, after bounding the difference of drifts. That step fails at the interaction term: the edge and the error are dependent, because the edge enters the dynamics of particle . A plain Cauchy–Schwarz bound loses a factor and gives nothing when . Estimates (7.10) and (7.15) quantify how weak this dependence is, and they are where the hypotheses that is invertible with bounded inverse and that are needed. The discretization term needs the Lipschitz regularity of the limit laws in the label (Theorem 2.1(b)), itself a fixed-point estimate on a space of measure-valued maps.
The Lean development uses Mathlib's unitInterval for , Fin d → ℝ with its sup norm for (all constants are existential, so the choice of norm does not matter), time ℝ≥0, and the path space as continuous maps on with the sup norm. Brownian motions, Itô integrals and Itô processes are those of the published Peng1990.SMP.Stochastic; Wasserstein distances are the published WassersteinDRO.Duality.wassersteinDistance, valued in . Particle is Lean's i : Fin n with label .
Committed conventions:
The solution predicates are not vacuous: the zero-coefficient system satisfies both, Condition 4.1 and Condition 4.3 are satisfiable, and every statement quantifies over solutions rather than assuming the conclusion. The constant is chosen after and before , so it cannot depend on , and the bound is the paper's average over , not a weaker or a stronger form. At both sides of every rate are .
The paper's proofs are in its §5 (Theorem 2.1), §7.1 (Lemma 7.1, (7.10), (7.15)) and §7.3 (Theorem 4.2). Stochastic analysis at that level — Burkholder–Davis–Gundy and Rosenthal inequalities, Girsanov's theorem for these SDEs, Gronwall arguments for measure-valued fixed points — is mostly absent from Mathlib, and contributions of such infrastructure are welcome, as are proofs of any milestone.
Join-the-shortest-queue (JSQ) is the load-balancing rule in which each arriving job is sent to a server with the fewest jobs. It is a baseline in the design of server farms and data centers, and in the many-server Halfin–Whitt regime, where the load per server approaches one at rate , it combines near-full utilization with vanishing waiting. Eschenfeldt and Gamarnik (arXiv:1502.00999, 2015) proved that the suitably scaled JSQ process converges, over bounded time intervals, to a two-dimensional reflected diffusion; Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) gave the form of the result that Braverman quotes as Theorem 1. Process-level convergence over bounded time intervals says nothing about the stationary distribution. To conclude that the stationary distributions converge as well, one needs tightness of the scaled stationary distributions, uniformly in the number of servers .
Braverman (arXiv:1801.05121, Math. Oper. Res. 45(3), 2020) supplied this, together with positive recurrence of the diffusion limit. This mission formalizes the first of the two main results, Theorem 2, and the chain of lemmas the paper uses to prove it.
There are identical servers, each with its own infinite buffer. Jobs arrive as a Poisson process of rate and service times are i.i.d. exponential with mean one. An arriving job joins a server with the fewest jobs, ties broken arbitrarily. The Halfin–Whitt regime is
For , is the number of servers with at least jobs. The process is a continuous-time Markov chain on
Its generator sends to at rate when , and to at rate . The fluid-scaled coordinates are , the negative of the fraction of idle servers, and for . The diffusion-scaled coordinates are . Expectations are taken under a stationary distribution of the chain.
The proof works with functions on and with the first-order operator
where is the partial derivative in , taken one-sided on .
For each there is a constant such that for all with and every stationary distribution,
The constant depends on only, not on , the stationary distribution, or .
with , vanishing second derivatives for , and explicit upper bounds of order above that level. 6. (3.18): . 7. Theorem 2, (2.2): the half of the goal.
Theorem 2 shows that in steady state the number of idle servers and the number of servers holding two or more jobs are on average, and the number of servers holding jobs is on average, uniformly in . Combined with the process-level limit and the positive recurrence of the limiting diffusion (Theorem 3, the companion mission), it yields Proposition 1: the diffusion-scaled stationary distribution converges to the stationary distribution of the diffusion. This justifies the diffusion as a steady-state approximation for JSQ.
The method is the generator-comparison or Stein's-method approach: a Lyapunov function solving a first-order PDE for the fluid model, with explicit bounds on its derivatives. It applies to other many-server systems, and the paper is an example of that approach on an infinite-dimensional chain whose diffusion limit is two-dimensional.
The result is proved in the paper; no machine-checked proof is known to exist. The work remaining is to formalize the known proof: the adjoint relation for a countable-state chain with bounded rates, the Taylor expansion of the generator, and the explicit analysis of through the fluid curves.
The obvious route is to bound in Lemma 2 directly. The paper notes that no good handle on these probabilities exists. The PDE route needs a solution whose second derivatives are bounded by . General results that give such bounds require a continuous fluid vector field, and the JSQ fluid model is discontinuous because of the reflection at . So is constructed explicitly from the fluid paths, and its derivatives must be bounded by hand through the implicitly defined and .
A second difficulty is dimensional: the chain is infinite-dimensional while the PDE is two-dimensional, so the remainder of Lemma 3 contains a term with that is controlled only by combining Lemma 2 with the monotonicity of .
ℕ → ℕ with 0-based indices: Lean q.1 i is the paper's , so the goal's "" is Lean index . Each state is bounded by , nonincreasing and eventually zero. The generator genQ is the displayed formula on p. 6.ℝ × ℝ. Partial derivatives are named functions asserted to be one-sided derivatives along coordinate lines (HasDerivWithinAt on Set.Iic 0 or Set.Ici 0). Weak second derivatives are a.e. derivatives of absolutely continuous functions, in integral form on compact intervals. A "solution" of the PDE whose derivatives are the junk values of a derivative operator is thereby excluded. The PDE needs genuine derivatives, and Lemma 7 is about the explicit of (4.14), not about an arbitrary function.WithTop ℝ, with as ⊤, so a missing solution is never read as . is an if cascade, and Lemma 7 states the agreement of its branches. is defined by the closed form (4.14), not through the fluid model (4.1).Contributions of reusable infrastructure are welcome: the adjoint relation for countable-state chains with bounded rates, and FTC/Taylor lemmas for absolutely continuous first derivatives.
Training a neural network means running a first-order method on a loss that is built from compositions of elementary operations, many of them nonsmooth: ReLU, max-pooling, absolute values, sorting, norms. The gradient the optimizer uses is not computed by hand. It is computed by automatic differentiation (autodiff), most often in its reverse mode, backpropagation, which applies the chain rule of calculus operation by operation. When every operation is smooth, the output is the gradient. When some are not, each nonsmooth operation is assigned some "derivative" at its kinks (for ReLU at , typically ), and the chain rule is applied anyway. The result is in general neither a gradient, nor a Clarke subgradient, nor an element of any classical subdifferential: the classical subdifferentials do not satisfy the chain rule that autodiff applies.
Bolte and Pauwels (TSE Working Paper 1044, 2019; Mathematical Programming, 2021) introduced conservative set-valued fields to give these outputs a meaning. A conservative field is a set-valued map whose circulation along every closed path vanishes, exactly as for a gradient field. It obeys a chain rule along absolutely continuous curves. This mission formalizes the paper's Theorem 8: forward-mode and reverse-mode automatic differentiation, run with conservative fields for the elementary operations, return a conservative field for the composed function. The companion mission of this series formalizes the paper's Theorem 1, that a conservative field equals the gradient of its potential almost everywhere.
Write for Euclidean space and for a set-valued map, assigning a subset to every point. A path is absolutely continuous, with derivative for almost every .
A conservative field (Definition 1) is a set-valued map with closed graph and nonempty compact values such that for every absolutely continuous loop () the circulation is Lebesgue integrable with integral . A function is a potential for , or is a conservative field for (Definition 2), if is conservative and for every absolutely continuous path from to . A map is a conservative mapping for (Definition 4) if, along every absolutely continuous curve , for almost every , for all .
An evaluation program (§5.1) has inputs and intermediate nodes . Node has a tuple of distinct earlier nodes and an elementary function . Algorithm 1 sets for and returns . Each comes with a conservative field (property (d)). Given a choice for every :
The autodiff fields are and , the sets of outputs of Algorithm 2 and Algorithm 3 over all choices at .
If every is a locally bounded conservative field for , then
"Conservative field for " is meant in full: closed graph, nonempty compact values, zero circulation and the potential identity.
Theorem 8 says what backpropagation computes on a nonsmooth program: an element of a conservative field of the function, a set that behaves like a gradient along curves. This is what lets the paper's later results apply to deep learning: stochastic subgradient methods driven by such outputs converge, for definable losses, to points that are critical for the conservative field. It is also the reason why spurious outputs of autodiff (a nonzero "derivative" of a function that is identically zero) are harmless: by the companion Theorem 1 they occur only on a Lebesgue null set.
The result is proved in the paper, and nothing here is open. To our knowledge none of it has been machine-checked: there is no formal account of conservative fields, and the existing formalizations of backpropagation treat smooth layered networks only. This mission produces a formal model of evaluation programs and of both autodiff modes, a formal chain-rule calculus for conservative mappings (Lemmas 2–5), and the theorem itself. Formalizing it exposed three points the printed text leaves to the reader: the overwriting update of Algorithm 3, the nonempty-values hypothesis missing from Lemma 2, and the local boundedness that Theorem 8 needs (see Formalization scope).
The obvious argument is "autodiff applies the chain rule, and conservative fields satisfy the chain rule". The chain rule along curves (Lemmas 3–5) only gives the derivative identity of Definition 4 for each element of . It does not give the set-valued properties of Definition 1. Passing back to a conservative field (Lemma 2) needs to have closed graph, nonempty compact values and local boundedness. These depend on how the sets vary with through the forward pass, and they fail without local boundedness of the . Lemma 2 relates an integral identity along every path to a pointwise almost-everywhere identity, and both directions involve the measure theory of absolutely continuous curves that Mathlib supports only in part. The equality of reverse and forward modes is linear algebra, but the two algorithms traverse the graph in opposite orders, and the printed reverse update is not the one the equality needs.
is EuclideanSpace ℝ (Fin n), and the conservative-field layer is polymorphic in the dimension: each lives on . A path is a function ℝ → ℝ^n that is AbsolutelyContinuousOnInterval on , with = deriv γ. Definitions 1–2 require the circulation to be interval-integrable, because Lean integrates a non-integrable function to . Definition 4 and the chain rule (5) assert HasDerivAt, not an equation for deriv, so they cannot hold by default at points of non-differentiability. Nodes are Fin q, numbered from . Parent tuples are duplicate-free lists of smaller nodes, and input nodes have none.
and range over all admissible choices. A single fixed choice would give a map that is not a conservative field in general, and the formal statement does not use one.
Deviations from the printed text, each recorded with its item:
Theorem numbers and pages are those of the TSE Working Paper 1044 (October 2019), the version this mission cites. The journal version is typeset differently.
The conservative-field definitions duplicate those of the companion mission and are meant to be merged with them. Contributions are welcome at every level: Lemma 2 and Lemmas 3–5 form a reusable nonsmooth chain-rule calculus, and the reverse-equals-forward identity is a standalone statement about backpropagation that holds for arbitrary weights.
Bounded-confidence models describe a population of agents who repeatedly average their opinions with those of agents whose opinions are close to their own. They are used to study consensus and polarization in opinion formation, and in control as a primitive for decentralized rendezvous of mobile agents. Simulations of these models show a robust phenomenon: opinions converge to clusters, and the distances between clusters are typically close to twice the confidence radius rather than just above it. For finitely many agents this regularity has resisted proof.
V. D. Blondel, J. M. Hendrickx and J. N. Tsitsiklis (SIAM J. Control Optim. 48 (2010) 5214–5240) study a continuous-time version of the model in two forms: with discrete agents, and with a continuum of agents indexed by . For the continuum they prove that regular initial opinions converge to clusters whose separation obeys a lower bound depending on the cluster weights. To transfer such conclusions to finitely many agents one needs to know that the -agent model is close to the continuum model when is large. Section 4 of the paper proves this on every finite time horizon. This mission formalizes that result.
Discrete agents. There are agents with real opinions , . Agents and interact when . A solution of (2.1) is a continuous with
for all and all . The right-hand side is discontinuous when the interaction graph changes, so the integral form is used. A solution is proper if it is the unique solution from its initial value, its non-differentiability times have no accumulation point, and two agents that meet stay together.
Continuum agents. Agents are indexed by with Lebesgue measure. is the set of bounded measurable functions . For , is the set of nondecreasing with for ; such are regular. The interaction operator is
and a solution of (3.2) from is a measurable with every and for all and all .
The embedding. For , is the step function with on and . It distributes the agents over blocks of of length .
Let , the solution of (3.2) from , and for each let be a proper solution of (2.1) with nondecreasing and . Then for every and there is with
The statement fixes no rate in and no dependence of on ; it asserts only uniform convergence on bounded time intervals.
The theorem says that the continuum model is the large-population limit of the -agent model over any fixed time window. Combined with the paper's continuum convergence result (Theorem 6), it supports the paper's Conjecture 1 on intercluster distances for finitely many agents, and it is the first step of the paper's Proposition 5, which derives Conjecture 1 for random initial opinions from a stability conjecture for the continuum. It is a mean-field limit for a model whose interaction kernel is discontinuous, where standard Lipschitz mean-field arguments do not apply directly.
All four results and the goal are proved in the paper (with the time-scale correction described below). None of them has a machine-checked proof that this mission is aware of. The formalization contributes a checked continuous-dependence estimate for a discontinuous integral equation, a checked statement that the finite-agent dynamics embed in the continuum dynamics, and a precise record of the time normalization under which the two models agree.
The operator is not Lipschitz on : moving one opinion across the confidence threshold changes the interaction set discontinuously. The obvious Gronwall argument for continuous dependence therefore fails for two arbitrary solutions. It works only around a trajectory that stays in some , where few agents sit near the threshold, which is why the lower slope bound must hold at every time and not only at time . The perturbed trajectory, coming from agents, is a step function and is never regular, so the estimate must be one-sided in this sense.
A literal reading of the page also fails. The page writes , but for in block the continuum interaction equals times the discrete right-hand side of (2.1). With and , both models are linear; at the sup distance between and tends to . The discrete time must be rescaled by .
Namespace BHTOpinion.Approx. Agents of the discrete model are Fin n (0-based); the continuum index set is Set.Icc (0:ℝ) 1 with Lebesgue measure. Opinion functions are ℝ → ℝ, of which only the values on matter; trajectories are written x t α, time first, with time in ℝ and explicit guards. In 0-based form, on ; for the definition returns , and every statement assumes .
Explicit readings of the paper's phrases:
A trivializing formalization is ruled out: the hypotheses are satisfied by , the conclusion is not vacuous because is evaluated at only, and the perturbed initial values in Proposition 4 range over all of , not over regular functions.
Infrastructure needed: Gronwall's inequality for a sup-norm difference, measure-theoretic bookkeeping for on step functions, and a change of variables in interval integrals. The Lipschitz estimate on and the slope bound are reusable for any continuum bounded-confidence model. Contributions to any milestone are welcome; the embedding milestone is independent of the other three.
In many production and service settings a single resource is shared by several parties, each judging the outcome only by how its own work is treated. Multi-agent scheduling studies this situation. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model in which two agents, A and B, each own a set of jobs and each minimize their own objective. Their paper treats two questions: the constrained problem, minimizing A's objective subject to a bound on B's, and the Pareto problem, describing every schedule that cannot be improved for one agent without hurting the other.
For the Pareto problem the first quantity of interest is the number of distinct trade-offs, because the natural way to compute the whole front is to solve the constrained problem repeatedly with a decreasing bound (the paper's scheme PP, Figure 4, p. 239). Enumeration of this kind is polynomial exactly when the number of nondominated pairs is polynomially bounded. This mission formalizes the paper's bound for the case where both agents minimize a maximum of regular cost functions (§11.1, pp. 239–240).
Agent A owns the jobs and agent B owns , with . Every job has a processing time . All jobs are available at time . A schedule is an ordering of all jobs; the machine processes them in that order from time without idle time, so the completion time of a job is the sum of the processing times of the jobs up to and including it.
Each A-job carries a cost function and each B-job a cost function , all nondecreasing (regular). The agents' objectives are the maximum costs
This covers the makespan and maximum lateness of each agent as special cases.
A schedule is nondominated if no schedule satisfies and with at least one inequality strict. The pair of a nondominated schedule is a nondominated pair, and the schedule corresponds to that pair. Write for the set of nondominated pairs. Different nondominated schedules can share a pair; the problem asks for , with one schedule per pair. Job precedes job in if comes before in the ordering.
The paper prints the bound . It is off by one: with , unit processing times and , the schedules AB and BA give the two nondominated pairs and . The goal states , the bound the printed argument supports once the first schedule is counted.
The bound places among the two-agent problems whose Pareto front has polynomially many points. Combined with the polynomial algorithm for the constrained problem (Theorem 4.1 of the same paper), it means the full front can be listed with polynomially many constrained solves. The structural content is an order statement: as the bound on agent B tightens along the front, B-jobs overtake A-jobs and never fall back, so each of the (A-job, B-job) pairs changes order at most once. The same question for other pairs of objectives is the subject of later work on multi-agent scheduling, collected in the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal (Springer 2014).
The result is published but, to our knowledge, has no machine-checked proof. Formalizing it also fixes the printed off-by-one error in the statement. The overtaking lemmas are of independent use for other pairs of regular min-max objectives.
The obvious argument walks along the front and charges each step to one (A-job, B-job) pair that changes order. Two things must be secured. First, the charged pair must change order in a consistent direction; schedules corresponding to a pair are not unique, and nothing forces two arbitrary representatives of different pairs to agree on the order of the jobs they do not charge. Lemma 11.2 asserts that representatives can be chosen so that no B-job falls back behind an A-job, and establishing it requires control over every job pair simultaneously, not one at a time as in Lemma 11.1. Second, a step must change at least one order. The tempting proof looks at a B-job attaining and argues that the jobs it overtakes include an A-job; this fails for an arbitrary choice of that B-job, since another B-job with a flatter cost function can be the one that moves. Finally, the count of reversals bounds the number of steps, not the number of pairs; the first pair has to be added.
Jobs are Fin nA ⊕ Fin nB (Sum.inl h is , Sum.inr k is , 0-based). A schedule is a duplicate-free list containing every job, and completion times are prefix sums of processing times; this is the published sequence model MooreLateJobs.Shared.completionTime (Moore 1968), reused as a reference item. Processing times are real and nonnegative; costs are real-valued and Monotone; so that both maxima exist. Nondominance compares against all schedules of all jobs. Precedence compares first positions in the list.
The count is over pairs, , measured with Set.encard, so finiteness is part of the goal. Counting nondominated schedules instead would be a different and false statement: permuting jobs inside a block often leaves both maxima unchanged. The printed bound is replaced by and the reason is given in the goal's statement; stating a larger bound "to be safe" or the printed one would make the mission either weaker than the paper's argument or false. The scheme PP and the choice of in it are not formalized; they are the paper's computation device, not part of the theorem. In the exchange claim the paper's σ and σ̃ are schedules of consecutive pairs; the milestone states it for any two nondominated schedules with the two strict inequalities, which includes that case. Running times are not formalized.
A complete development needs elementary facts about completion times when one job is moved within a sequence, the simultaneous statement of Lemma 11.2, and a counting argument along the front. Contributions of reusable lemmas about job moves in the sequence model are welcome.
Firms that change prices over time face customers who remember past prices. A large empirical literature in marketing documents reference price effects: demand depends not only on the current price but on how that price compares with a price the customer expects, and losses (prices above the reference) weigh more than gains of the same size, the loss aversion of prospect theory (Tversky and Kahneman 1991; Kalyanaram and Winer 1995). Most dynamic pricing models with reference effects form the reference price by exponential smoothing of past prices (Popescu and Wu 2007; Kopalle, Rao and Assunção 1996; Fibich, Gavious and Lowengart 2003).
Psychology suggests a different memory process. Under the peak-end rule (Kahneman et al. 1993), people evaluate a past sequence of experiences mainly by its most extreme and its most recent episode. Nasiry and Popescu (INSEAD Working Paper 2009/20/DS/TOM; published in Operations Research 59(6), 2011) build a dynamic pricing model in which the reference price is a weighted average of the lowest price seen so far and the last price, and characterize the firm's optimal long-run and transient pricing. This mission formalizes the core of that analysis: the steady states (Section 3.1) and the convergence of optimal price paths (Section 3.2).
A firm sets a price in the price set in every period . The base demand is non-negative, bounded, continuous and decreasing on , with , and the base profit is non-monotone and strictly concave (Assumption 1). With sensitivities to surcharges and discounts, demand at price and reference price is
and the short-term profit is . It equals of the two smooth profits .
Given an initial minimum price and last price , the minimum price evolves as and the peak-end reference price is
With discount factor , the firm's value function is
An optimal price path is a price sequence in attaining ; a steady state is a state , , from which the constant path is optimal.
Two thresholds organize the answer. Let and be the roots in of
so that , and let , , . For , let be the root of
For every initial state with in , an optimal price path exists, and every optimal price path is monotone and converges:
The limit depends only on the initial minimum price.
In attack order: monotonicity of (Lemma 1); the identity and supermodularity of (Lemma 2); the upper bounds by smooth problems with one-dimensional state (Lemma 3); the unique steady state of each smooth problem (Lemma 4); two families of steady states (Lemma 5); the full set of steady states
(Proposition 1); Claims 1–4 and the invariance of the regions (Proposition 2: when , and when ); and Claim 5 (for the price eventually falls to or below).
The result gives a complete description of optimal pricing under peak-end anchoring with loss-averse consumers. A continuum of steady states exists, and the one reached is set by the remembered minimum price alone. A firm facing a low minimum price raises prices toward ; with an intermediate minimum it settles exactly at that minimum; with a high minimum it cuts prices down to and then holds them there. Optimal paths are monotone, so the model predicts no cyclical discounting under loss aversion. The comparison with Popescu and Wu (2007) in Section 3.3 of the paper and the robustness results of later sections (heterogeneous markets, non-linear reference effects) build on these statements.
The paper's results are proved on paper; none is formalized. The mission produces a machine-checked model of a non-smooth, two-dimensional dynamic program defined directly as a supremum over price sequences, the reduction of its steady states to smooth one-dimensional bounds, and the convergence theorem.
Both the per-period profit (through the kink at ) and the state transition (through ) are non-smooth, so neither the Euler equation nor standard concavity arguments for the value function apply directly. The Bellman objective need not be concave in the price, and the value function is not differentiable on the diagonal . Supermodularity of yields monotone optimal policies only within a region where the minimum price stays fixed, and showing that the state never leaves its initial region (Proposition 2) is itself a comparison of optimal paths against steady states. Existence of an optimal path is needed in its own right, because the value function is a supremum over an infinite-dimensional set.
All declarations live in PeakEndPricing.Convergence. Conventions fixed in Lean:
minPrice m0 q n is and refPrice at index is the reference price faced by .tsums, never "a solution of the Bellman equation". On the domain of the theorems all series converge and the families are bounded, so the junk values of ⨆ and ∑' are not reached.A goal stated without the existence of an optimal path would hold vacuously if no path attained ; existence is therefore part of the goal. Contributions are welcome on general infrastructure that is reusable beyond this mission: existence of optimal paths for discounted problems over compact action sets, the principle of optimality for sequence formulations, and Topkis-type monotonicity of optimal paths for supermodular objectives.
A vendor holding a finite stock of a product must set prices over time without knowing how many customers will come. Each price does two things: it earns revenue now, and through the sales it generates it reveals information about demand that improves future prices. This tension between earning and learning is central in revenue management with demand uncertainty, in retail markdown pricing, and in online selling. Optimal Bayesian policies for such problems are characterized by a Hamilton–Jacobi–Bellman equation that has no closed-form solution, so practice relies on heuristics, and the question is which heuristics come with guarantees.
Farias and Van Roy introduced decay balancing and proved that, for exponentially distributed reservation prices and a Gamma prior on the arrival rate, it earns at least one third of the optimal expected discounted revenue, uniformly over all problem parameters (V. F. Farias, B. Van Roy, Dynamic Pricing with a Prior on Market Response, Operations Research 58(1):16–29, 2010, doi:10.1287/opre.1090.0729). They describe it as the first heuristic for problems of this type with a uniform performance guarantee. This mission formalizes that guarantee and the chain of results leading to it. The source is the authors' manuscript of January 20, 2009 (MIT DSpace); its printed page numbers coincide with the PDF page numbers, and all theorem and page numbers below refer to it.
Customers arrive according to a Poisson process with rate . Each has an independent reservation price with density and tail ; a customer facing price buys one unit if it is available and is at most his reservation price, and otherwise leaves. The hazard rate is . Assumption 1 (p. 5) asks that be differentiable with support and that be non-decreasing. The exponential law with mean has .
The vendor starts with units and a Gamma prior on with shape and rate (density , mean ). After sales the posterior is Gamma with and , so the state is . A policy sets the price; the expected discounted revenue at rate is
the supremum over all measurable non-negative policies. With known, the same problem has value . Assumption 2 (p. 9) asks that be differentiable in .
Decay balancing uses the approximation , , and posts the price solving the balance equation (5), p. 13,
The optimal price solves the same equation with in place of . The constant
measures the cost of uncertainty for a prior of shape .
For exponential reservation prices with mean , every , , , :
In attack order:
Theorem 2 gives a guarantee that depends only on the coefficient of variation of the prior. Theorem 3 removes even that dependence for exponential reservation prices: whatever the inventory, prior, discount rate and price scale, decay balancing loses at most a factor of three. The analysis also yields reusable facts about Bayesian pricing: knowing the rate helps (), the decay-balance characterization of optimal prices, and comparison with a vendor who does not learn.
All results are proved in the source, using Dynkin's formula, an HJB verification argument (Appendix E) and a coupling of sales processes. None of them is machine-checked. The mission asks for a formal development of the known proofs.
The obvious route to Theorem 3 would chain Theorem 2 at the initial state. That fails because blows up as , so for a diffuse prior Theorem 2 gives no constant bound. The paper instead compares the two systems only up to the first sale, after which the shape parameter is at least . This needs two things: a coupling in which the optimal system never sells first, and Lemma 12, which bounds the value of one extra unit without a decreasing-returns property in (none is known). Lemma 12 itself rests on a numerical inequality involving the Lambert function.
At the foundational level, neither Mathlib nor the platform has a counting process whose intensity is a random rate times a state-feedback price. Defining and faithfully is part of the mission.
Reusable pieces are the Gamma–Poisson sales process in the b-clock, the incomplete Gamma function, and the known-rate pricing problem. Proofs of any milestone, of the p. 6 revenue identity, and of Assumptions 1–2 for the exponential law are welcome.
Related platform work in other models: Gallego–van Ryzin known-demand pricing (GVRPricing), Talluri–van Ryzin (RevenueManagement), Bitran–Caldentey (PricingRM.DetHeuristic), and the Bayesian bounds of Satia–Lave (SatiaLave.Bayes).
Many large optimization problems arising in networked control, smart grids, distributed estimation and resource allocation have a separable objective with coupled affine constraints: agents each own a variable and a private cost , and only a linear constraint ties them together. Distributed algorithms for such problems let each agent solve a small local problem and exchange only a few aggregated quantities. For convex problems the standard method is the alternating direction method of multipliers (ADMM), which converges at a linear rate; for nonconvex problems ADMM can diverge (Houska, Frasch and Diehl give a two-variable example in §2 of their paper).
Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton method), which combines the decoupled augmented-Lagrangian subproblems of ADMM with a coupled equality-constrained quadratic program borrowed from sequential quadratic programming (SQP). Their local convergence analysis (§7) rests on one stability result for the decoupled subproblems, Lemma 3, which this mission formalizes. Similar statements are classical for augmented Lagrangian methods: Bertsekas analyzes minimizers of augmented Lagrangians under perturbation of the multiplier (Constrained Optimization and Lagrange Multiplier Methods, 1982, Prop. 4.2.3), and Nocedal and Wright give a related analysis (Numerical Optimization, 2nd ed., 2006, Thm. 17.6).
Problem (1.1). Given , , () and ,
All and are twice continuously differentiable (the paper's standing assumption in §3). The multiplier of the coupling constraint is , that of is .
A KKT point is feasible, satisfies for every , and has with . It is regular if
The decoupled subproblems. In step 1 of ALADIN, given the current primal and dual iterates , a penalty and positive semidefinite scaling matrices , agent solves
with . These problems are nonconvex in general and are solved to local optimality.
Let be a local minimizer of (1.1) with a regular KKT point, and let satisfy
Then for every sufficiently small ball of radius around the origin of there are constants such that for all with the problems (3.2) have local minimizers , unique in , with
The constants are not specified: the goal asserts only the shape of the estimate, not values of .
Lemma 3 is the bridge between ALADIN and the local theory of SQP. Once the decoupled minimizers are known to exist, to be locally unique, and to stay within a linear distance of , the full-step variant of ALADIN behaves locally like an inexact SQP method, and the paper derives its local quadratic convergence estimates (with exact Hessians and a suitably large ) from this. Without the lemma the local subproblems could jump between distant local minimizers of a nonconvex objective, and no local rate could be claimed.
The result is proved in the paper, in a short paragraph that delegates the main step to the regularity of the KKT point. No machine-checked version of this lemma, of the sensitivity theory of parametric nonlinear programs it rests on, or of ALADIN exists, as far as a search of the Prove2Me catalogue and Mathlib shows. Formalizing it means supplying the argument the paper leaves implicit: a parametric local-minimizer theorem for inequality-constrained problems under LICQ, strict complementarity and a second-order condition.
The obvious argument applies the implicit function theorem to the stationarity condition of (3.2), . That works only without inequality constraints. With constraints, the local minimizer satisfies a KKT system involving the multipliers and complementarity, which is not a smooth equation; one has to fix the active set, use strict complementarity to show that it does not change nearby, and use LICQ of the active constraints to make the reduced KKT matrix invertible. The second difficulty is uniqueness: the implicit function theorem gives a unique KKT point near , but the lemma claims uniqueness among local minimizers within a ball in the primal variable alone, so the multipliers of any nearby local minimizer must be shown to lie near . Third, the hypothesis is the positive definiteness of on all of , not only on the critical cone; the subproblems inherit their second-order condition from it rather than from the SOSC of (1.1).
Vectors are Fin n → ℝ with Mathlib's sup norm, blocks are indexed by Fin N, matrices are Mathlib Matrix over Fin index types, and Fin m → ℝ. Gradients and Hessians enter through Fréchet derivatives (fderiv), with written fderiv ℝ (fderiv ℝ g) z d d. LICQ is stated as linear independence of the active gradients in . The "sufficiently small open set " is read as every ball of radius in the sup norm of , with allowed to depend on but not on ; is read through the -component, . Local minimizers are local minimizers on the feasible set and are required to be feasible. The hypotheses and come from the paper's standing assumptions (§3 and Algorithm 2, step 1).
A trivializing formalization is ruled out: the goal keeps all four conclusions (local minimality, membership in the -ball, uniqueness in that same ball, and the bound), since the bound alone is satisfied by ; and it quantifies over every small ball rather than asserting the result for one neighbourhood. The hypotheses are satisfiable: a sorry-free check with , , , , , , is in the development.
Needed infrastructure: a parametric implicit-function argument for KKT systems with a fixed active set, persistence of LICQ and of strict complementarity under perturbation, and second-order sufficiency for inequality-constrained problems. These pieces are reusable well beyond this mission, for any sensitivity or local-convergence analysis of nonlinear programs (SQP, augmented Lagrangian, interior-point methods). Proofs of any milestone, alternative routes (for instance via Robinson's strong regularity), and general lemmas on second-order sufficient conditions are welcome.
Betweenness centrality measures how much of the communication in a network passes through a node. Freeman's original measure (Freeman 1977) counts the fraction of shortest paths between each pair of nodes that pass through it, and Brandes' algorithm (Brandes 2001) made it computable on large graphs. Variants replace shortest paths by maximum flows (Freeman, Borgatti and White 1991), random walks (Newman 2005) or load-splitting rules (Goh, Kahng and Kim 2001), and group variants measure the traffic that passes through a set of nodes (Everett and Borgatti 1999).
Dolev, Elovici and Puzis (technical report 2009, J. ACM 2010) define routing betweenness centrality (RBC): given the actual routing scheme of a communication network and its traffic matrix, the RBC of a node is the expected number of packets that pass through it. Each of the measures above is a special choice of routing scheme. The application is the placement of traffic monitors: the RBC of an ordered sequence of monitors is the expected number of packets sampled by all of them in order, which measures, for example, redundant inspection along a path.
Let be a finite set of nodes. A routing scheme assigns to every source , current node , next node and target a number , the probability that forwards to a packet with source address and target address . Routing decisions are independent. The scheme is assumed to be
A route from to is a sequence of nodes from to whose every hop has positive forwarding probability; its probability is the product of the hop probabilities. For nodes and a sequence :
A traffic matrix gives the number of packets sent from to , and sampling rates give the fraction of passing packets a monitor at samples. The target dependency is , and the RBC of the sequence of distinct nodes is
For a source-oblivious scheme and a sequence of distinct nodes, ,
The right side is the value returned by the paper's Algorithm 6. The identity contains no running time and no constant: it states the exact equality the algorithm relies on.
The goal reduces the RBC of a sequence of monitors to arithmetic on precomputed single-node quantities, instead of a pass over the routing graph of every source–target pair. This is what makes repeated evaluation of candidate monitor sequences, as in greedy or search-based placement, affordable on large networks. Eqs. (1) and (9) are the recursions behind the paper's algorithms for the RBC of single nodes; Eq. (9) replaces the loop over all source–target pairs by a loop over targets.
The paper's proof of Lemma 1 is an argument about conditional probabilities of informally described events. A formalization fixes what "the probability that a packet passes through " means, as a sum over a finite set of routes, and checks the factorization against that definition, including the corner cases the prose passes over: sequences with repeated nodes, a first node equal to the source or to the target, and the source in the sum over all sources. No machine-checked version of these identities is known.
Dependency chaining is a Markov property: after the packet reaches , its future does not depend on its past. The obvious argument splits every route through into a prefix ending at and a suffix starting there. Two points need care. First, the suffix must be a route of a packet with source , which is where source-obliviousness enters; for source-dependent routing the lemma is false. Second, the prefix probabilities must sum to while the suffix probabilities sum to one, which requires that no packet is lost: this is where totality of the forwarding probabilities and loop-freeness (every walk reaches the target in at most steps) are needed. The passage from Lemma 1 to the goal then requires the sum over all sources, including , where Lemma 1 does not apply.
Nodes form a type V with [Fintype V] [DecidableEq V]; probabilities, traffic and sampling rates are real numbers; sequences are Lean lists, indexed from . Routes are repetition-free lists, and every dependency is a finite sum over them; no infinite sums, suprema or measure theory are used. The definitions file bundles the standing assumptions in IsRoutingScheme and source-obliviousness in IsSourceOblivious.
The paper's probabilities are informal. The following readings are explicit:
Defining by the recursion (3) or the product (16), the target sequence dependency by (17), or the sequence RBC as the sum over targets of the chained product would make the goal true by definition; every dependency here is a sum of route probabilities, and the RBC of a sequence is the double sum of Eq. (4).
The running-time claims of the paper are out of scope. Lemma 2 of the paper (p. 17) is false as printed for a nonempty monitor set and is not posed. Contributions welcome: proofs of the milestones, a general lemma that the total route probability from any node is one under a total loop-free scheme (reusable for absorbing Markov chains on finite DAGs), and the prefix–suffix decomposition of routes.
Bounded-confidence opinion dynamics model a population in which each agent repeatedly moves its opinion towards the opinions of those agents whose views lie within a fixed distance of its own. Introduced in discrete time by Krause (1997) and studied as the Hegselmann–Krause model, these systems are a standard test case for multi-agent coordination with state-dependent communication: who talks to whom depends on the current state, so the interaction graph changes over time and the linear consensus theory does not apply. Simulations show that opinions settle into clusters that are further apart than the confidence radius, and that the distances between clusters are larger than the radius would force. Explaining those distances is a long-standing question in the area (Lorenz 2007).
Blondel, Hendrickx and Tsitsiklis (SIAM J. Control Optim. 2010) study the continuous-time version, first for finitely many agents and then for a continuum of agents. The continuum model is the limit of a large population and captures the intercluster distances observed in simulations. This mission formalizes the continuum part of the paper, Section 3: well-posedness for regular initial opinions, convergence to clusters, and the intercluster distance bound of Theorem 6.
Agents are indexed by with Lebesgue measure. An opinion function gives the opinion of agent . Write for the bounded measurable opinion functions and for the nondecreasing bounded ones. For , is the set of whose increase rate is at least for all , and the set with rate at most . A function is regular if it lies in for some ; the uniform profile is regular.
Two agents are connected when their opinions differ by less than . The interaction operator is
Given an initial condition , a solution of (3.2) is a measurable , , with each and
The differential form (3.1) is .
is the set of nondecreasing whose distinct values are pairwise more than apart; the set of nondecreasing whose values, for almost every pair of agents, are equal or at least apart. A fixed point is an for which (3.2) started at has the unique solution . A cluster of is a value held by a set of agents of positive measure , its weight.
For a regular , a solution of (3.2), and almost everywhere: any two distinct clusters of satisfy
and agrees almost everywhere with a member of that is a fixed point.
Theorem 6 turns the qualitative picture "opinions freeze into clusters at least one unit apart", which already follows from Theorem 5, into a quantitative statement depending on the cluster weights: two clusters of equal weight are at least apart, and a light cluster can sit closer to a heavy one. This matches the intercluster distances observed in simulations of large populations and yields Corollary 1 of the paper, a necessary condition for the stability of an equilibrium in the sense. Theorem 4 is of independent interest: the right-hand side of (3.1) is discontinuous in the state, a two-valued initial profile admits two different solutions, and well-posedness holds only under the slope bounds.
The results are proved in the paper. Nothing in this mission has a machine-checked proof yet. Formalizing it means building a small theory of integral equations with a state-dependent, discontinuous kernel on -type spaces of opinion profiles: a contraction argument on short intervals, its continuation, monotone convergence of partial integrals, and an a.e. limit argument with Fatou's lemma and Fubini.
The obvious route to Theorem 4, Picard–Lindelöf, fails: is not Lipschitz on , because a small perturbation of opinions can switch the connection indicator on a set of positive measure. Lemma 1 restores the Lipschitz property only at functions with a positive increase rate, so existence and uniqueness require a contraction on a carefully chosen set of profiles together with a proof that the dynamics keep the increase rate positive (Lemma 2), and a continuation argument whose step size shrinks as the lower slope decays. For Theorem 6, convergence alone gives only ; the extra term comes from agents trapped between two clusters, whose existence relies on the continuity in of every , which the a.e. limit does not have.
Opinion functions are ℝ → ℝ, and only their values on Set.Icc 0 1 matter; a trajectory is x : ℝ → ℝ → ℝ with x t α , time real with . Lebesgue measure on is volume.restrict (Set.Icc 0 1), and uses its product measure. The slope conditions are written multiplied out for . Explicit readings of the paper's phrases:
Tendsto … atTop (𝓝 l) to a real limit; "except possibly for a countable set": a countable exceptional set; "a.e.": almost everywhere for Lebesgue measure on .A trivializing formalization is ruled out: clusters are distinct with positive weight, regularity requires a positive lower slope, the solution predicate forbids the junk value of a non-integrable time integral, and is checked to be regular, so no hypothesis is vacuous.
The development needs an integral-equation solution theory for a discontinuous kernel, the Banach fixed point theorem (Mathlib ContractingWith), Grönwall-type estimates, countability of discontinuities of monotone functions, Fatou's lemma and Fubini. Lemmas 1 and 2 and the lower bound in Theorem 4 are reused by the companion mission on the discrete-to-continuum approximation (Theorem 7). Contributions are welcome on every milestone, and in particular on the slope estimates, which are self-contained.
Many problems in statistical learning, signal processing and distributed optimization minimize a sum of a large number of convex components over a convex set: a data-fit term per sample plus a regularizer or constraint per sample. When is large, a method that processes one component per iteration is often far cheaper per step than one that evaluates the whole sum. Incremental methods do exactly this. The incremental subgradient method of Nedić and Bertsekas (SIAM J. Optim., 2001) takes a subgradient step on one component at a time; the incremental proximal method replaces some of these steps by proximal steps, which are more stable and are cheap when a component has a closed-form proximal map (an term, an indicator of a simple set).
Bertsekas, Incremental Proximal Methods for Large Scale Convex Optimization (Report LIDS-P-2847, MIT, 2010, revised 2011; Math. Program. 129 (2011), doi:10.1007/s10107-011-0472-0), combines the two: each component is split as , with a proximal step on and a subgradient step on , followed by a projection. The paper analyzes two ways of choosing the component at each iteration, a fixed cyclic order and a randomized order. This mission covers the randomized order (§4 of the paper); its companion mission covers the cyclic order.
Let be a nonempty closed convex set and let , , be convex. The problem is
with optimal value , possibly , and optimal set , possibly empty. is the Euclidean projection on and a subgradient of at .
At iteration a component index is drawn and, with stepsize , one of three updates is applied:
The implicit equations are proximal steps: in (42), minimizes over . The randomized order means that is uniformly distributed over and independent of the past history (Assumptions 3(a), 4(a)). The growth conditions (Assumptions 3(b), 4(b)) ask for a constant bounding, with probability 1 and for every component , the norms of the subgradients used by the step that would be taken if were , and the decrease of , along that step by times its length.
If and , then
and if in addition and , then with probability 1 the iterates converge to some (which may depend on the sample path).
Proposition 9 says that a randomized incremental method with a diminishing stepsize solves the problem exactly, almost surely, under conditions that do not require differentiability, bounded level sets, or strong convexity. Propositions 7 and 8 quantify the constant-stepsize regime: the error bound is , smaller by a factor of than the worst case of the cyclic order (Proposition 4 of the paper). This is the paper's argument for randomization, and the same comparison recurs in the later literature on stochastic and incremental methods.
The results are proved in the paper. As far as known, none of them is machine-checked: Mathlib has conditional expectation, filtrations and Doob's martingale convergence theorem, but not the Robbins–Siegmund almost-supermartingale theorem in the form used here, and no incremental or stochastic proximal method has a formal convergence proof on the platform. The mission produces a formal model of a randomized algorithm with implicit (proximal) steps, a formal Robbins–Siegmund special case, and a complete a.s. convergence proof that other stochastic-approximation formalizations can reuse.
The deterministic estimate behind (58) is the one of the cyclic analysis with the sampled component in place of the cyclic one. The new difficulty is the conditioning step: needs the step that would be taken for each component to be a function of the past, and to be independent of it, and both must be stated so that the conditional expectation is that of an integrable function. The obvious route from (59) to part 2 of the goal fails: (59) gives, for each , an event of probability 1, and is in general uncountable, so the events cannot be intersected directly. Part 1 must also handle , where no point of is available.
EuclideanSpace ℝ (Fin n); components are indexed by Fin m (), with .EReal, so is represented and the and statements are in EReal.A formalization in which the would-be steps may depend on , or in which is only assumed uniform, would let a step pick its component adversarially; the measurability and independence hypotheses rule this out, and none of the hypotheses is unsatisfiable (a sorry-free instance with is checked locally).
Needed infrastructure: the Robbins–Siegmund special case (Proposition 2), conditional expectation of a function of an independent uniform index and a past-measurable quantity, and existence of a countable dense subset of a closed set in . The supermartingale theorem and the conditioning lemma are reusable beyond this mission. Proofs of the milestones, of the goal, and of reusable lemmas about projections and proximal steps are welcome.
Bounded-confidence opinion dynamics model a population in which each individual revises an opinion, represented by a real number, by looking only at opinions close to its own. The best-known example is the discrete-time model of Krause (1997), also called the Hegselmann–Krause model, in which every agent moves to the average of the opinions within distance 1 of its own. Such models are studied in the social sciences as models of consensus formation and polarization, and in control theory as prototypes of multiagent systems with state-dependent interaction topology: the communication graph is not given in advance but is determined by the state itself, which is what rendezvous algorithms for mobile robots and flocking models share (Lorenz 2007; Olfati-Saber, Fax, Murray 2007).
Blondel, Hendrickx and Tsitsiklis (SIAM J. Control Optim. 48 (2010)) study the continuous-time, symmetric counterpart of Krause's model. Each opinion is continuously attracted by every other opinion differing from it by less than 1, with an intensity proportional to the difference. Simulations show convergence to clusters, groups of agents sharing a common value, with distinct clusters at distance at least 1 and typically close to 2. This mission formalizes the first of the paper's results: convergence to clusters at least 1 apart for finitely many agents.
Timeline.
There are agents, labelled . Agent holds a real opinion at each time , and is a continuous function of time. Agent is a neighbour of agent at time when ; the inequality is strict, and every agent is its own neighbour. The intended dynamics are
The right-hand side jumps whenever a pair of opinions crosses distance 1, so (1.1) usually has no differentiable solution. The model is therefore the integral equation
Solutions of (2.1) need not be unique. The two-agent initial condition is a fixed point, but the agents can also start attracting each other immediately. An initial condition is proper if (a) (2.1) has exactly one solution with ; (b) the set of times at which is not differentiable is at most countable and has no accumulation point; and (c) agents that meet stay together: implies for all . That solution is then a proper solution.
The set of equilibria is
The average opinion is , and is the sum of squared differences from it.
Every proper solution of (2.1) converges to a limit in :
that is, all limits exist and two agents with different limits end at distance at least 1.
The result. Theorem 2 establishes the clustering behaviour seen in simulations for every proper solution. The paper's Theorem 1 states that almost every initial condition is proper, so the conclusion covers almost every initial condition. The lower bound 1 on the distance between clusters is the baseline that the paper's continuum analysis improves to . Average preservation and the decrease of (Proposition 1) are the structural facts that the continuum model also has.
Formalization. Theorem 2 is proved in the paper; no machine-checked version exists on Prove2Me or, as far as is known, elsewhere. The mission produces a Lean definition of solutions of a discontinuous integral equation with a state-dependent neighbour graph, and a convergence proof for it. The remaining work is to formalize the known argument, from the integral equation to the existence and location of the limit.
The obvious approach treats (1.1) as an ODE and differentiates along trajectories. That fails because the right-hand side is discontinuous in the state. A solution is only an integral solution, it may fail to be differentiable, and derivative identities such as (2.3) hold only outside an exceptional set of times. Every step from a derivative sign to a monotonicity or limit statement therefore has to go through the integral equation, not the differential one. A second obstacle is that pairs of agents at distance exactly 1 sit on the discontinuity of the interaction rule. This is where uniqueness fails (footnote 3 of the paper) and why conditions (a)–(c) are hypotheses. A decreasing Lyapunov function alone does not give convergence of the trajectory to a single point, so Proposition 1 does not by itself settle Theorem 2.
Agents are Fin n. Time is ℝ, and only values at enter. A trajectory is x : ℝ → Fin n → ℝ. A solution of (2.1) is continuous on and satisfies (2.1) for every and every , with the neighbour set Finset.univ.filter (fun j => |x τ i - x τ j| < 1). The integrand is also required to be interval-integrable on ; for a continuous trajectory this always holds. Explicit readings of the paper's phrases:
Tendsto x atTop (𝓝 xstar) in Fin n → ℝ, with real time;The paper's sortedness convention ("we assume … that the components of proper initial conditions are sorted") is a hypothesis only of the partial-sum milestone. Theorem 2 is stated for every proper solution. A formalization that dropped condition (a), restricted solutions to sorted, differentiable or eventually constant trajectories, or replaced (2.1) by the differential equation would prove a different, and in parts trivial, statement. These are excluded.
The work needs interval integrals and the fundamental theorem of calculus for integrands with jumps, monotonicity from almost-everywhere derivative signs, and bounded monotone convergence. The definition of solutions of (2.1) and the equilibrium set is reusable for the stability results of the same paper (Theorem 3), which are not part of this mission. Contributions are welcome at every milestone, as are alternative convergence proofs, such as the paper's reference [9], that avoid symmetry.
A finite-sum optimization problem asks for one vector that performs well across many component objectives. In empirical risk minimization, each component can represent the loss from one data point. A full gradient uses every component, whereas a stochastic gradient uses one component and can be much cheaper per step. The latter carries sampling noise, so a method must control that noise while moving toward the optimum. Allen-Zhu's Katyusha paper gives a direct accelerated stochastic method for this setting. Its strongly convex result, Theorem 2.1, bounds the expected objective error of a specified algorithm after a specified number of epochs.
The problem is relevant when the number of terms is large enough that a full gradient at every iteration is costly, but individual component gradients and proximal steps remain practical. Katyusha combines a periodically refreshed full gradient with individual component gradients. The paper's result concerns the actual returned snapshot of Algorithm 1, Option I, whose weighted averaging rule matters to the claim. Formalizing a generic noisy gradient method would leave the paper's central algorithmic guarantee unstated.
Let be differentiable functions, with . Their finite-sum objective is . A real-valued regularizer gives the composite objective
Each is convex and smooth: its gradient is Lipschitz in the Euclidean norm. The regularizer is strongly convex, with , in the paper's convention that the quadratic term has coefficient . The comparison point minimizes the full objective .
Algorithm 1 starts from and keeps three vectors: a snapshot , a proximal sequence , and another proximal sequence . In each epoch it computes . At a current point , it samples uniformly from and forms the gradient estimator
The algorithm then makes two proximal updates using and . Its next snapshot is a weighted average of the new values, with weights for . The iterates and persist between epochs. In the theorem's run the epoch length is , and , , and . The output after epochs is .
For every starting point and minimizer of , the target is the paper's two-case expected bound:
The expectation is over every independent uniform index sampled by the run. The two regimes meet at the threshold where the algorithm's minimum defining changes branch. The milestone list follows Lemmas 2.3–2.7 and the displayed one-epoch inequalities of Section 2.2. It includes the variance bound, the proximal estimates, and the two regime-specific epoch estimates that feed the final theorem.
The theorem gives an accelerated linear reduction of the expected composite-objective error under the paper's strong convexity assumptions. It identifies how the rate depends on component count , smoothness , strong convexity , and epoch count . The author also translates the result into an iteration-complexity statement and uses it as a basis for later reductions and generalizations in the paper. The objective-error theorem is the stable mathematical claim formalized here; the complexity paraphrase is outside this mission's Lean goal.
Allen-Zhu proved Theorem 2.1 in the paper. The Lean declarations in this proposal are targets with proof placeholders, not machine-checked proofs of Katyusha's convergence. Completing them would produce a checked account of the exact algorithm, its finite probability space, and the conditional inequalities for an epoch. The finite-sum and proximal-point definitions reused here are already published in the SAGA formalization; Katyusha's weighted snapshot and coupling statements require their own development.
The estimator is unbiased, but that fact alone does not give the claimed acceleration. Its variance depends on the snapshot and current point, and a direct descent estimate retains a variance penalty. The bound in Lemma 2.4 expresses that penalty through a smooth convex gap which can have either sign before it is combined with other terms. The two proximal sequences and the snapshot therefore have to be accounted for together. Across an epoch, the iterates are averaged with nonuniform weights, while and themselves are carried into the next epoch. Replacing the snapshot with the final value or with a uniform average changes the algorithm and the theorem.
The two rate cases also reflect different parameter values. When , is determined by a square root; above that threshold it is fixed at . A proof of only one branch would omit part of the source result. Treating the sampled indices as a single arbitrary path would ask for a false pathwise guarantee, whereas stating the result for a favorable path would lose the expectation bound.
Vectors are EuclideanSpace ℝ (Fin d) and component indices are Fin n, translating the paper's one-based to a zero-based finite type. The goal fixes as Algorithm 1 does; the conditional one-epoch statements admit any positive . The number of epochs can be zero, in which case the output is the initial snapshot. The objective is real-valued. Thus may be nondifferentiable but does not include extended-valued indicator functions. The component gradient fields are required to be the actual gradients of their functions, and the comparison point minimizes , not merely .
A proximal map is an explicit argument constrained, for every , to minimize the proximal objective of the given . The run computes the paper's two proximal updates with that map. The expectation is the finite uniform average over all sequences, equivalent to independent uniform samples. It never quantifies over a convenient sequence. These links prevent a vacuous or unrelated encoding of the method.
The paper writes both rates using . Its Section 2.2 bounds yield the concrete coefficient in the square-root regime and in the regime; these are the expressions in the Lean goal. For Case 1 the rate is represented by division by , a positive denominator. For Case 2 it is . The statement retains both conclusions at their stated boundary. The one-step lemmas average only a fresh sampled index with the current state fixed, and the epoch statements average the current epoch's indices.
The development needs finite sums and finite expectations, Euclidean smooth and strong convexity facts, proximal minimizer inequalities, and algebra of the weighted snapshot. The finite-sum objective, averaged gradient, proximal-point predicate, and finite index expectation are shared definitions; the Katyusha run, progress value, potential, and epoch inequalities are specific to this algorithm. Contributions proving the milestone statements, establishing existence and uniqueness of the proximal map under these assumptions, or improving reusable proximal and finite-expectation lemmas are within scope.
Reflected backward stochastic differential equations describe processes that must remain above a prescribed obstacle. El Karoui, Kapoudjian, Pardoux, Peng and Quenez connect that probabilistic construction to a parabolic partial differential equation with an obstacle in their 1997 paper. A representation by a stochastic process is useful only if the associated differential equation identifies a definite function. The comparison result in Theorem 8.6 supplies that identification: within a specified growth class, two viscosity solutions cannot disagree. This mission isolates that deterministic uniqueness statement. The companion existence and stochastic representation result is Theorem 8.5 of the same paper.
Fix a terminal time and a spatial dimension . At time and point , the drift is a vector and the diffusion coefficient is a matrix. Both are continuous and Lipschitz in uniformly over . A continuous terminal payoff has at most polynomial growth. The continuous generator depends on a scalar value and a vector ; it has polynomial growth at and is Lipschitz in . The continuous obstacle has a polynomial upper bound and satisfies .
Write . The associated second order spatial operator is . The obstacle problem asks for a function whose terminal value is and whose interior value obeys
A parabolic superjet or subjet at an interior point is a triple of a time slope, spatial slope and symmetric second order matrix that bounds the function locally above or below by the associated quadratic expansion, up to . These jets let a continuous function satisfy the differential inequality without having ordinary derivatives. A viscosity subsolution uses superjets and a terminal upper bound; a viscosity supersolution uses subjets and a terminal lower bound. A viscosity solution satisfies both definitions.
The goal is the paper's Theorem 8.6. Under the coefficient assumptions above and condition (27), every pair of continuous viscosity solutions with polynomial growth agrees on the entire closed time strip:
Condition (27) gives a continuous modulus for the change in between bounded spatial points, with argument and . The quantifiers include every radius , every bounded scalar argument, and every gradient vector . The milestone is Lemma 8.7, which controls the location and separation of the maximizers of the paper's doubled-variable function .
The theorem shows that the obstacle PDE has at most one solution in the natural class allowed by polynomially growing coefficients and payoffs. Together with Theorem 8.5, which identifies the reflected backward SDE value as a viscosity solution, and the growth estimate at the end of Section 8, it yields the paper's probabilistic representation of the unique solution. Theorem 8.6 alone asserts uniqueness, so it makes no existence claim.
The formal development provides reusable interfaces for parabolic jets, viscosity inequalities, the obstacle operator and uniform polynomial growth on a finite time strip. Those interfaces can serve other comparison theorems and other parabolic obstacle problems. The mathematical result is proved in the 1997 article; this mission asks for a Lean proof of its deterministic uniqueness statement. The proposal declares the theorem with a proof placeholder and includes the comparison lemma as an intermediate target.
The first obstruction is that the candidate solutions need only be continuous. Subtracting their PDE expressions directly would assume derivatives they may not possess. The paper instead uses viscosity jets, and its comparison argument invokes the theorem of sums from Crandall, Ishii and Lions' viscosity-solutions guide. The generator's spatial modulus must control a gradient argument that grows as the two spatial points approach each other. Lemma 8.7 provides the necessary separation limit for the maximizers. The argument also treats a polynomial growth class on all of , so a comparison confined to one fixed bounded ball would not establish the stated result.
Lean uses nonnegative real time and functions on represented by Fin d → ℝ. The terminal time and dimension are positive. Bounds with existential constants use the finite-dimensional sup norm, which is equivalent to the Euclidean norm in the paper. The displayed quadratic form, and are written by coordinate sums, so their signs, factor , and matrix order are exact. The obstacle is bounded only above in the data assumptions, exactly as condition (22) states. Condition (27) is imposed only on uniqueness, not folded into the definition of viscosity solution.
Jets are taken at through a one-sided little- bound in the relative neighborhood of the interior strip. The terminal equality comes from the two terminal inequalities; the viscosity tests impose no separate condition at . The printed text calls “symmetric nonnegative matrices,” but the proof of Theorem 8.6 uses arbitrary symmetric matrices produced by the theorem of sums. The formal definition therefore uses all symmetric matrices and records this correction for review.
The mission permits every continuous solution of polynomial growth. It does not restrict candidates to smooth, bounded or stochastic-representation functions. The companion reflected SDE construction, penalization limit and existence theorem are outside this mission's goal; the general stochastic interface Peng1990.SMP.Stochastic is listed as series context but is not imported by the deterministic statements. Useful contributions include the comparison proof, the lemma on doubled-variable maximizers, and reusable lemmas about jet transformations and the matrix trace inequality.
Classical mean-field theory describes diffusions that interact symmetrically, each feeling the empirical average of all the others, and shows that as every particle behaves like an independent copy of a single McKean–Vlasov process. Many systems of interest are not symmetric: neurons, agents in a financial network, or oscillators interact through a graph, and particles in different parts of the graph feel different neighbourhoods. A graphon is the limit object of dense graph sequences (Lovász, Large Networks and Graph Limits, AMS 2012), and it is the natural way to describe the interaction structure of such systems in the limit.
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) study a continuum of diffusions indexed by labels whose interaction is weighted by a graphon, and prove laws of large numbers and rates of convergence for -particle systems on graphs sampled from the graphon. This mission targets their uniform rate of convergence for weights sampled from a Lipschitz graphon (Theorem 3.2).
Write with Lebesgue measure. Fix a horizon and let with .
On one probability space, are i.i.d. -dimensional Brownian motions and are independent initial states with laws , independent of the Brownian motions. Given a graphon and coefficients , the graphon particle system (2.1) is
with . The particles are independent but not identically distributed, and their laws are coupled through the -integral.
The -particle system (3.1) uses the same randomness at the labels :
so particle and the continuum particle at share their initial state and Brownian motion.
The hypotheses are:
Under Conditions 2.1, 2.3 and 3.2 there is such that
The result. Theorem 3.2 gives a quantitative propagation of chaos for heterogeneous interactions: with weights sampled from a blockwise Lipschitz graphon, every particle of the finite system, not just an average particle, is within in root-mean-square path distance of the continuum particle with the same label. The rate matches the classical mean-field rate (e.g. Sznitman 1991), so heterogeneity of the interaction costs nothing in the exponent. The same estimate covers the deterministic weighted graph and the random graph sampled from (in the annealed sense), and it is the dense counterpart of Theorem 4.2 for percolated graphs.
Formalizing it. The result is proved in the paper (§6.3); it has no machine-checked proof. A formal development would produce a reusable account of graphon particle systems and their finite- approximations: graphon-weighted McKean–Vlasov drifts, couplings through shared noise, and the decomposition of the interaction error into a Lipschitz feedback term, a law-of-large-numbers term and a Riemann-sum discretization term.
The obvious approach is to compare with directly and close a Gronwall inequality. The difficulty is that the comparison involves the empirical, graph-weighted average of the other particles, which is neither the graphon average nor an average of independent terms. Three different errors must be controlled simultaneously and uniformly in : the feedback of all particles' errors into particle , the fluctuation of a sum of independent but non-identically distributed terms whose weights may themselves be random, and the error of replacing an integral over labels by a sum over the grid . The last needs regularity of the law in the label , which is itself a theorem about the graphon system (Theorem 2.1(b)) and fails at block boundaries of , where only the small number of boundary cells saves the rate. Averaging over , as in the law of large numbers of Theorem 3.1, is not enough: the goal bounds the maximum.
Fin d → ℝ with the sup norm; matrices are measured entrywise. All statements are norm-invariant because every constant is existential. Particle is Lean's i : Fin n with label ; time is ℝ≥0; is Mathlib's unitInterval.Peng1990.SMP.Stochastic definitions; an SDE with random initial value is stated as an Itô process for . Each continuum particle uses the natural filtration of ; the -particle system uses the natural filtration of the weights, initial states and Brownian motions at the labels.WassersteinDRO.Duality.wassersteinDistance 2, valued in ; expectations of nonnegative quantities are lower Lebesgue integrals.Policy gradient methods optimize a parameterized policy by gradient descent on its expected total cost. They are a staple of reinforcement learning and of simulation-based optimization in operations research, but the objective is nonconvex in the policy parameters, and the standard theory guarantees convergence only to a stationary point. J. Bhandari and D. Russo (arXiv:1906.01786v3, Operations Research, 2024, DOI 10.1287/opre.2021.0014) identify structural conditions under which every stationary point is globally optimal.
Their first result (Theorem 1) requires the policy class to be closed under policy improvement. That excludes many classes used in practice, where it is known only that some member of the class is optimal: base-stock policies in finite-horizon inventory control are the standard example (Bertsekas, Dynamic Programming and Optimal Control, 1995). For stationary policy classes, containing an optimal policy is not enough: the paper's Example 1 has a policy class that contains the optimal policy, and policy gradient still gets stuck in a bad local minimum. Theorem 3 shows that for finite-horizon problems with a non-stationary policy class (separate parameters for each period), containing an optimal policy suffices, together with a single-period regularity condition imposed only at the optimal cost-to-go. This mission formalizes Theorem 3.
A Markov decision process consists of a state space , nonempty feasible action sets , a bounded measurable cost , a transition kernel , a discount factor and an initial distribution . A policy is a measurable map with ; is the set of all of them. The cost-to-go is , the loss is , and the discounted state-occupancy measure is . An optimal policy has pointwise for all ; . With the Bellman operator , the weighted policy-iteration objective is
A parameterized policy class is for a convex , and . A point is stationary for if is differentiable at and for all .
The finite-horizon structure (Condition 3) embeds a time-inhomogeneous problem in this discounted formulation: the states split into stages ; from a state in , , every feasible action leads to ; and is a costless absorbing state. The parameter is a concatenation , the parameter set is a product , and on the action depends only on . The stage objectives are .
Condition 4 asks that for every , the problem has no suboptimal stationary points. Assumption 3 asks that for every . Condition 0 asks that the policy-iteration objective be continuously differentiable in the parameters.
Under Conditions 0, 3 and 4 and Assumption 3, if is an optimal policy for some , then every stationary point of on satisfies
Theorem 3 covers finite-horizon dynamic programs in which a structured class of time-varying policies is known to contain an optimal policy, but is not closed under policy improvement: the paper's Example 8, multi-period inventory control with base-stock policies, is the motivating case. Policy gradient on such a class has no suboptimal stationary points, so any method that finds a stationary point finds a globally optimal policy, optimal among all policies and not only within the class. Condition 4 involves only the Bellman objective of the optimal cost-to-go , which often has regularity (for instance convexity) that the cost-to-go of an arbitrary policy lacks.
The result is proved in the paper. To our knowledge no part of it, nor the policy gradient theorem for deterministic policies on general state spaces, has a machine-checked proof. Formalizing it requires a measure-theoretic treatment of occupancy measures, the stage-wise decomposition of the weighted policy-iteration objective, and the backward induction of App. D.2.
The obvious approach reasons stage by stage directly on , but couples the stages: changing changes the distribution of states visited after stage . The paper's argument instead passes through the policy gradient theorem, which turns stationarity of into stationarity of single-period problems weighted by the occupancy measure of the current policy. These single-period problems involve , while Condition 4 speaks about ; relating them requires a backward induction over stages in which almost-sure equality on stage is transported to stage through the balance equation. This step needs the occupancy measures of all policies in the class, including policies other than , to be equivalent to , which is where Assumption 3 enters. The naive variant with a stationary policy class fails (Example 1).
The state and action spaces are arbitrary measurable spaces (the paper takes Borel subsets of Euclidean spaces; no argument uses that structure). Cost and kernel are given on all state-action pairs; the cost is bounded. Policies are deterministic, stationary and measurable; parameters live in EuclideanSpace ℝ (Fin d), so gradients and norms are Euclidean. is never defined as an infimum: an optimal policy is a hypothesis, with . Stages and sub-vectors are numbered from by a measurable stage index and a block index on coordinates; the product structure of is encoded as closure under exchanging one block.
Hypotheses beyond the printed sentence of Theorem 3, all disclosed in the item statements: Assumption 3 (announced on p. 17 as required, used in the proof); Condition 0 (needed for Lemma 6, which the proof invokes), in a joint form that the proof of Lemma 6 uses and that implies the printed partial-map form; the standing Assumptions 1 and 2 of §2; and, inside Condition 4, differentiability of on , the premise of Definition 1. The Bellman operators carry the factor omitted in the printed (3)–(4). The stage-wise balance equation is stated for ; the printed range fails at the absorbing state.
A formalization in which the goal assumes the stage-wise characterization (31), the balance equation, or on any stage is not Theorem 3; neither is one where "contains an optimal policy" means optimal only within . Stationarity includes differentiability, so a junk zero gradient never makes a point stationary.
Needed infrastructure: occupancy measures as series of iterated kernels and their balance equation, the cost-to-go as a bounded measurable function, the performance difference identity, the policy gradient theorem, and the decomposition of integrals over the stage partition. The occupancy-measure and policy gradient results are reusable for every mission of this series; contributions of these general lemmas are welcome.
Policy gradient methods optimize a parameterized control policy by gradient descent on its long-run cost. They underlie much of modern reinforcement learning, from REINFORCE and actor-critic methods to trust-region and proximal policy optimization, and they are used in operations problems such as inventory control and optimal stopping. Their objective is almost never convex in the policy parameters, even in textbook problems, so the classical guarantees of first-order optimization do not explain why they reach good policies.
Bhandari and Russo (arXiv:1906.01786v3, Operations Research, 2024, doi:10.1287/opre.2021.0014) identify structural conditions under which this non-convex landscape is benign. Their Theorem 1 shows that, for a policy class closed under policy improvement, every stationary point is globally optimal. This mission formalizes their Theorem 2, the quantitative version: approximate stationarity implies approximate optimality, a gradient dominance (Polyak–Łojasiewicz-type) inequality that yields convergence rates.
Timeline. Polyak (1963) introduced the inequality for unconstrained problems. Kakade and Langford (2002) proved the performance difference lemma for finite Markov decision processes. Fazel, Ge, Kakade and Mesbahi (2018) established gradient dominance of policy gradient for linear-quadratic control, and Agarwal, Kakade, Lee and Mahajan (2021) for tabular policies with direct and softmax parameterizations. Bhandari and Russo (preprint 2019, journal 2024) give a single condition-based argument covering general state spaces and several of these examples.
A Markov decision process has a measurable state space , feasible action sets , a bounded expected cost , a transition kernel , a discount factor and an initial distribution . A stationary policy maps states to feasible actions; is the set of measurable such policies. Its cost-to-go is , its discounted state-occupancy measure is , and its loss is . An optimal policy has for every .
The Bellman operator is and is its optimality version. The weighted policy iteration objective is
A policy class is with convex, and the policy gradient objective is . For , the map is the single-period problem that one step of policy iteration within the class would solve.
A function is -gradient dominated over (, ) if for all
The hypotheses are Condition 0 (differentiability of in the policy and occupancy arguments), Condition 1 (closure: for every some minimizes over all of ) and Condition 2.B (each single-period objective is -gradient dominated over ). The effective concentrability coefficient is the smallest with for all , .
If Conditions 0, 1 and 2.B hold and , then
It is stated for every satisfying the concentrability inequality, which is the page's statement at .
The remark of §3 that differentiable -strongly convex functions are -gradient dominated and convex ones -gradient dominated, and Corollary 1: under Conditions 0 and 1, convexity (strong convexity) of every single-period objective makes gradient dominated of degree one (two).
Gradient dominance of degree two gives linear convergence of projected gradient methods, and degree one gives sublinear rates, so Theorem 2 converts structural knowledge about one-step policy improvement into iteration complexity for the multi-period problem. The constant makes explicit the dependence on the initial distribution: an exploratory with small is what the guarantee needs. The paper instantiates the conditions for tabular MDPs, linear-quadratic control, optimal stopping with threshold policies, and finite-horizon inventory control.
The result is proved in the paper. As far as is known, none of it is machine-checked: Mathlib has convexity, strong convexity, gradients and Markov kernels but no discounted dynamic programming on general spaces, no occupancy measures and no policy gradient theorem. The formal development would supply the general-space performance difference identity and the policy gradient theorem, reusable for every other result of the paper and for related work on policy optimization.
The policy gradient objective is not convex, so the usual derivation of a Polyak–Łojasiewicz inequality from convexity is unavailable. Gradient dominance of the single-period objective does not transfer to by comparing the two functions: they differ by how a change of policy moves the state distribution, these terms do not vanish, and the minimum of over is not the minimum of . The mismatch between , and is unavoidable, which is why a concentrability factor appears in the constants. On a general state space each identity also needs the right measurability and integrability (the measurable-selection assumption is what makes measurable), and Condition 0 must be strong enough to justify a total-derivative expansion.
All declarations live in PGLandscape.GradDom. and are arbitrary measurable spaces; the cost is bounded and measurable and, like the kernel, given on all of . Policies are measurable maps; the cost-to-go is a series of integrals against -step kernels; is a measure of total mass one. The parameter space is EuclideanSpace ℝ (Fin d), so is the Euclidean gradient and the norm. is for an optimal given as a hypothesis; no real infimum over policies is used.
Committed conventions and disclosed additions:
A formalization that assumes gradient dominance of , the closure bound, or a finite state space would not be this theorem; the goal assumes only Conditions 0, 1, 2.B and concentrability.
Contributions welcome: Markov-chain lemmas for iterKernel (summability, measurability, the fixed-point equation ), the general-space performance difference identity, and proofs of any milestone.