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?
Reliability theory classifies life distributions by how they age. A device whose remaining life, once it has survived to age , is stochastically shorter than the life of a new device is called new better than used (NBU). The NBU class, together with the classes IHR (increasing hazard rate) and IHRA (increasing hazard rate average), organizes much of the theory of maintenance and replacement: Marshall and Proschan showed that the NBU property is what makes certain replacement policies beneficial, and Barlow and Proschan's monographs build the statistical theory of reliability on these classes.
A question that runs through this literature is where such ageing properties come from physically. Esary, Marshall and Proschan (Ann. Probability 1973) answer it for shock models: a device is hit by shocks arriving in time as a Poisson process, each shock adds a random amount of damage, and the device fails when the accumulated damage exceeds its threshold. Section 4 of their paper treats a fixed threshold and shows that the life is IHRA for every damage law. Section 5, the subject of this mission, lets the threshold itself be random, which models the variation between individual items of a production lot. It then asks which ageing properties of the threshold law are inherited by the life distribution, and which are forced if the inheritance is to hold whatever the damage law.
All distributions are laws of non-negative random variables. For a distribution on with for (a damage law), denotes the -fold convolution of , with the point mass at ; thus for independent .
A threshold law is a distribution with for ; write for its survival function. If the threshold is independent of the damages, the probability of surviving shocks is
If shocks arrive as a Poisson process of rate , the device's life distribution has survival function
A survival function is NBU if for all ; it is IHR if is non-increasing in for each , and IHRA if is non-increasing in . The discrete analogue of NBU for the sequence is submultiplicativity, .
For a threshold law with for :
the quantifier ranging over every damage law ; and if is NBU, then for every damage law and every the life distribution of (5.2) is NBU.
Theorem 5.1 (the life is exponential for every iff is exponential) and Theorem 5.2 (b), (c) (an IHR threshold makes non-increasing for every ; non-increasing for every forces to be IHRA) are posed as companion statements from the same section.
Theorem 5.3 is a characterization: the NBU class is exactly the class of threshold laws for which the cumulative-damage mechanism preserves the discrete NBU property under every damage law. Combined with Theorem 3.1 (3.5), it gives a physical derivation of NBU life distributions: an item with an NBU random strength, subject to Poisson shocks with arbitrary i.i.d. non-negative damage, has an NBU life. Theorems 5.1 and 5.2 place the exponential and the IHR/IHRA classes in the same framework, and the authors record that whether an IHRA threshold suffices in Theorem 5.2 (b) is left unresolved.
The results are proved in the paper. No machine-checked version is known to exist; this mission produces one. A complete development also supplies reusable infrastructure: convolution powers of laws on as Mathlib measures, Poisson mixtures of a sequence, and the ageing classes of p. 631 as predicates on survival functions.
The equivalence couples a property of one function, , to a family of inequalities indexed by every damage law, and the left side is about convolutions while the right side is pointwise. Two points make the statement harder than it looks. First, (5.1) as printed is , whereas the paper's proof works with ; the two agree only when and have no common discontinuities, and they can disagree as soon as has an atom where has one, a case the left side of the equivalence includes. A formal proof cannot invoke that convention. Second, the second sentence of the theorem passes through a Poisson series (5.2) whose terms involve the whole sequence , so the NBU property of is a statement about a power series in , not about any single .
Measure.conv power with , and is the mass of .Contributions welcome: proofs of the milestones, a library for Poisson mixtures and convolution powers of laws on , and the extra items of §5.
Many models in probability, statistical physics and the theory of stochastic networks are interacting particle systems: infinitely many sites, each in state 0 or 1, each updating at random according to the states of a few other sites. A basic question about such a system is ergodicity: does it have a unique stationary distribution, and does its law converge to it from every initial configuration? For infinite systems the question is hard, because the state space is uncountable and standard Markov chain arguments do not apply.
Holley and Liggett (Ann. Probab. 3 (1975), 643–663) introduced a class of such systems, the proximity processes, which arise from a coupling of more general weakly interacting systems (the settings of Vasershtein (1969), Dobrushin (1971) and Chover (1974)), and showed that each proximity process is dual to a process of finite sets, the branching process with interference. Duality turns a question about an infinite-dimensional process into a question about a process whose states are finite sets. The paper uses it to give short proofs of ergodicity criteria and, in its §5, to study the invariant measures of the voter model. Duality of this kind became one of the main tools of the field; see Liggett, Interacting Particle Systems (Springer, 1985).
This mission formalizes the discrete-time half of the paper: the duality theorem (1.6) and its first applications, Corollary (3.1) and Corollary (4.1).
Let be a countable set of sites and the set of configurations , with the product -algebra. For , is the set of occupied sites.
The data of the model are, for each site , a sequence of finite subsets of and a probability distribution on .
The proximity process is the Markov chain on whose transition function is the product measure
where puts mass on . In words: each site independently picks an index with probability and becomes exactly when the set contains an occupied site. denotes the law at time started from .
The branching process with interference (b.p.i.) is the Markov chain on the collection of finite subsets of with transition function
the sum over all sequences with : each particle at splits into particles on with probability , and particles landing on the same site merge. denotes probabilities for the chain started at .
For , .
For all , and ,
The proof is an induction on whose steps are four displayed identities on p. 647:
and the point mass on the all-zero configuration is the only stationary distribution; along the way, (3.5): .
The duality identity expresses every finite-dimensional "all vacant" probability of the proximity process, which determine its law, through a chain on finite sets. Consequences in the paper: a sufficient condition for convergence to the all-zero configuration (Corollary (3.1)), which in the nearest-neighbour example on gives ; the sharper range , i.e. , for that example (Corollary (4.1)), which the interference term makes possible; and, in continuous time, the analysis of the invariant measures of the voter model.
The results are classical and proved; a search of Prove2Me and Mathlib found no machine-checked proof of any of them. A formalization contributes a Lean model of an infinite-product Markov kernel on with its -step laws, a model of a set-valued branching chain, and the duality between them, which are reusable for other duality arguments (contact process, voter model, coalescing random walks).
The two sides of (1.7) are defined independently and live on different spaces. The left side is the time- law of a chain on the uncountable space , obtained by iterating an infinite product kernel; the right side comes from a transition matrix on the countable set of finite subsets of , whose entries are themselves infinite sums over sequences indexed by a finite set. Neither side can be computed in closed form beyond , so no direct evaluation proves the identity for general .
Two technical points stand in the way of a naive argument. Evaluating a product kernel on a cylinder event and integrating it against a previous law requires the kernel to be measurable in , a statement about cylinder sets of an infinite product that a hand proof passes over. And the natural recursion for -step probabilities of the b.p.i. adds the new step at the end, while the comparison with the proximity process needs information about the first step; the two orders agree only by a Chapman–Kolmogorov argument over a countable state space with -valued sums. Corollary (4.1) further needs quantitative estimates of survival probabilities for specific initial sets on .
All objects are in the namespace HolleyLiggett.Duality, in one definitions file.
Bool (true = 1), is Config I := I → Bool with the product -algebra, is Finset I.[Countable I], N : I → ℕ → Finset I (finite sets) with N i 0 = ∅, and f : I → PMF ℕ (probability distributions). A finite collection is the case for .Measure.infinitePi of the two-point measures; the -step law is proxLaw, iterating Measure.bind from the point mass at . Measurability of the kernel is a true fact that solvers must prove; it is not assumed.bpiProb follow the last-step recursion . All probabilities are in ℝ≥0∞, and each over sequences is an unconditional sum over ↥F → ℕ.The continuous-time duality (Theorem (2.12)), Corollaries (3.9) and (4.15) and the voter model of §5 are out of scope. Contributions welcome: the measurability and probability facts for proxStep, Chapman–Kolmogorov for bpiProb, and proofs of the milestones.
Newton's method for a nonlinear system , with , solves the linear system at every step. For large systems that solve is itself iterative (a Krylov method such as GMRES), and it is stopped early. The resulting inexact Newton methods, introduced by Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19 (1982)), accept any step with , where the forcing term controls how accurately the linear system is solved. Their theory is local: it applies once the iterates are near a solution with invertible derivative.
Practical solvers (Newton–Krylov codes in large-scale simulation, nonlinear solver libraries such as PETSc's SNES and SUNDIALS' KINSOL) combine such inexact steps with a globalization, most often backtracking along the step. Eisenstat and Walker (SIAM J. Optim. 4 (1994)) gave the global convergence theory for this combination: what can be said about the iterates from an arbitrary starting point, with no assumption that a solution exists or that is invertible anywhere.
Timeline. Dembo, Eisenstat and Steihaug (1982) proved local convergence of inexact Newton methods. Dembo and Steihaug (Math. Program. 26 (1983)) studied truncated Newton methods for unconstrained minimization. Brown and Saad (1990) studied globalized Newton–Krylov methods with line searches and model trust regions, under the inner-product norm. Eisenstat and Walker (1994) gave the general framework treated here, for an arbitrary norm. Their 1996 paper (SIAM J. Sci. Comput. 17) proposed the forcing-term choices that are now standard.
Let be with an arbitrary norm , and let be continuously differentiable with derivative . A point is a limit point of if every ball contains for infinitely many .
Algorithm GIN (global inexact Newton method). Fix . At each , find a level and a step with
and set . Condition (2.1) says that reduces the norm of the local linear model by the factor . Condition (2.2) asks that itself decrease by a fixed fraction of that predicted reduction.
Algorithm MR (minimum reduction method). Fix and . At step , choose and a curve with for (5.1). Start at . While (2.2) fails for , replace by for some . Then set .
Algorithm INB (inexact Newton backtracking). Choose and an inexact Newton step at level . While (2.2) fails, shorten the step, , and raise the level, . INB is MR with the backtracking curve (6.1).
An algorithm does not break down if it produces an infinite sequence of iterates, in particular if every while-loop exits.
If Algorithm INB does not break down and is a limit point of at which is invertible, then
The statement assumes no solution, bounded level set, Lipschitz derivative or particular norm. The last clause says that backtracking eventually stops, so the local rate is governed by the forcing terms .
In attack order:
Further items, which are not milestones: Corollary 6.2 (exact Newton with backtracking takes full Newton steps eventually), Theorem 5.2 for Algorithm TL, Lemma 3.1 (existence of acceptable GIN steps), and Proposition 2.1 (the Goldstein–Armijo alpha condition implies (2.2) in the Euclidean norm).
The result. Theorem 6.1 is the global convergence guarantee for the inexact Newton backtracking method that Newton–Krylov solvers implement. It separates three outcomes: the iterates diverge, they accumulate only at points where is singular, or they converge to a solution with invertible derivative and eventually take the unmodified inexact Newton steps. In the third case the local theory of Dembo, Eisenstat and Steihaug applies from some iteration on, so the forcing terms alone set the convergence rate. Theorem 5.2 is the template: §§6–8 of the paper derive the convergence of backtracking, equality-curve and dogleg-type methods from it by verifying (5.6).
Formalizing it. The results are proved on paper and none of them has a machine-checked proof that we know of. The mission produces a library of algorithm-run predicates with explicit while-loops for inexact Newton methods. It also checks the paper's reduction chain (INB is a run of MR, MR is a run of GIN) and the global convergence theorems in an arbitrary finite-dimensional norm.
The obvious argument fails at both ends. Sufficient decrease (2.2) alone gives monotonicity of , but not convergence of the iterates. On the page, admits sequences satisfying (2.2) with both as limit points. Convergence of to needs , and nothing in the algorithm states this. In Theorem 5.2 it has to be derived from the exit level of the while-loop, which depends on a neighbourhood of where the linearization error is uniformly controlled. A solver must combine a limit-point argument (only infinitely many iterates are near , not all of them) with the loop's worst-case backtracking factor . The invertibility of enters only through the bound (5.6) for the backtracking curve, which must be established uniformly in .
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]). This is exactly " with an arbitrary norm". Fin n → ℝ (sup norm) and EuclideanSpace would each fix one norm. Only Proposition 2.1 assumes an inner product space, as the page does.fderiv ℝ F, with ContDiff ℝ 1 F (the paper's standing assumption). Invertibility is ContinuousLinearMap.IsInvertible, and is ContinuousLinearMap.inverse.IsGINRun, IsMRRun, IsINBRun, plus IsTLRun, IsENBRun). The steps and levels the algorithm says to "find" or "choose" are data constrained only by the stated conditions. A while-loop is recorded by its number of passes and factors . Every trial before the last fails the loop's test and the last one passes it. Termination is part of the run.MapClusterPt xstar atTop x. "For all sufficiently large " is ∀ᶠ k in atTop. The paper's "whenever is sufficiently near [and is sufficiently large]" is ∃ Γ, ∃ δ > 0, [∃ K,] ∀ k [≥ K], x k ∈ ball xstar δ → …. precedes ("independent of "), and the " large" clause appears only in (3.2), where the page has it.F = id on ) confirms that the INB, GIN and ENB run predicates and the goal's hypotheses are satisfiable, so the goal is not vacuous.Reliability theory classifies life distributions by how they age. The IHRA class (increasing hazard rate average) is the smallest class of life distributions that contains the exponential distributions and is closed under forming coherent systems and taking limits in distribution (Birnbaum, Esary and Marshall 1966). It is therefore the natural class for the lifetime of a system built from components that wear out. A distribution belongs to it when its survival function satisfies: is decreasing in .
Esary, Marshall and Proschan (Ann. Probability 1 (1973) 627–649) asked where such ageing comes from physically. Their answer is a shock model: a device receives shocks at the epochs of a Poisson process, each shock does random damage, and the device fails when the accumulated damage exceeds its capacity. The central result of their §4, formalized in this mission, is that this model always produces an IHRA life, whatever the damage distribution. In the authors' words, "the IHRA property has been obtained … as an implication of a natural physical model. The only hypothesis imposed upon is that it be the distribution of a nonnegative random variable." The paper is a standard reference of reliability theory and the source of the cumulative damage model used across maintenance and insurance applications.
Shocks arrive according to a Poisson process with rate . Write for the probability that the device survives the first shocks; then (display (2.2)). Conditioning on the number of shocks in gives the shock survival function (2.1):
with for . The weights are the Poisson probabilities.
In the cumulative damage model the th shock causes a damage , the damages are independent with common distribution function (so for ), and the device survives shocks when , for a fixed threshold . Hence (4.1)
where is the -fold convolution of and is degenerate at . A distribution with survival function is IHRA if is decreasing in ; throughout, "decreasing" means non-increasing.
For every distribution on , every and every threshold ,
This is the first of the three statements of Corollary 4.2; the second ((4.7a), independent damages that worsen with ) is an extra item of this mission, and the third ((4.7b), dependent damages satisfying (4.3)–(4.5)) belongs to mission III of this series.
Lemma 4.1a and Corollary 4.2 (4.7a); Theorem 4.4 ( is constant in iff has no mass in ); Corollary 4.5 ((4.7) is exponential iff has no mass in ); Corollary 4.11 ( is decreasing for the count of an ordinary renewal process).
The goal turns a modelling assumption into a theorem: anyone who models failure as accumulated nonnegative damage under Poisson shocks obtains, without further checks, every consequence of IHRA proved in reliability theory, including the closure of the class under the formation of coherent systems. Theorem 3.1 (3.4) is reusable on its own: it reduces the IHRA property of any Poisson mixture to a discrete condition on the , and the same scheme drives the first passage result for wear processes (Theorem 4.10, mission III). Lemma 4.1, applied to renewal processes, gives Corollary 4.11, a statement about renewal counts with no shock model in sight.
All results are proved in the paper; none has a machine-checked proof that we know of. The Mathlib library has the Poisson distribution and the convolution of measures, but no reliability classes, no total positivity and no variation diminishing property. The mission's output is a formal proof of the paper's chain of results and, along the way, reusable statements about Poisson mixtures and convolution powers.
Two steps resist a direct argument. The first is the transfer from sequences to functions: knowing that changes sign at most once says nothing pointwise about the series . The paper invokes the variation diminishing property of the totally positive Poisson kernel (Karlin, Total Positivity, 1968), which is not in Mathlib. The second is Lemma 4.1, an inequality between convolution powers of an arbitrary law: no density, moments or continuity may be assumed, atoms at and at are allowed, so any argument through densities or Laplace transforms loses generality. A further subtlety is the passage from "one sign change of for every " to the monotonicity of , which needs care where vanishes.
Measure.conv) starting from the point mass at , and is the real number .A complete development needs: the variation diminishing property of the Poisson kernel (reusable for every Poisson mixture), monotonicity of via convolution integrals, and elementary facts about real powers and sign changes. Proofs of any milestone or extra item, and general total positivity lemmas, are welcome.
In a conversation reported by Chvátal, Victor Klee asked for the smallest number such that every region bounded by a simple closed -gon is dominated by points: every point of the region sees one of them along a segment inside the region. In the picturesque language that gave the problem its name, is the number of guards needed to watch any art gallery with walls. A comb-shaped polygon (Figure 1 of the paper) shows .
V. Chvátal's three-page note (J. Combin. Theory Ser. B 18 (1975) 39–41) proves the matching upper bound by reducing it to a purely combinatorial statement about triangulated polygons: every such triangulation splits into at most fans, and a fan is watched by a single guard. The combinatorial theorem is the result this mission formalizes.
Timeline.
An -triangulation (p. 39) is a planar graph with vertices such that one face is bounded by an -gon and every other face by a triangle. Its vertices are labelled in their cyclic order around the -gon, and indices are taken mod ; the sides of the -gon are the pairs . Every other edge of is inner; it is a diagonal of the -gon. Two diagonals cross when their endpoints are distinct and alternate around the polygon.
Combinatorially, an -triangulation requires and is the same thing as a set of diagonals that pairwise do not cross and is maximal with this property. Its triangles are the 3-element vertex sets all of whose pairs are edges of ; there are of them, and they are the bounded faces.
Two triangles are adjacent when they share an edge. A set of triangles is dual-connected when any two of its members are joined by a chain of adjacent members; such an is a sub-polygon of , a -triangulation with , whose inner edges are the edges shared by two of its triangles. Following the paper, a -triangulation is a fan if one of its vertices, the centre, meets all of its inner edges. A partition of into fans is a family of fans, pairwise disjoint as sets of triangles, covering all triangles of . Fans may share vertices and edges.
For every and every -triangulation there is a partition of into fans with
The goal's only constant is the paper's , which milestone 5 shows is best possible.
The result. The fan partition is a strengthening of the guard bound: the centres of the fans form a set of at most vertices meeting every triangle, but the partition also says that the triangles split into star-shaped pieces, each visible from one vertex. With the existence of triangulations of simple polygons it yields , the art gallery theorem; with Figure 1 it gives .
Formalizing it. The theorem has been proved since 1975, and the platform already has Fisk's consequence: ProofsInTheBook.Chapter36.chapter36 and chapter36_artgallery_combinatorial (Proofs from THE BOOK, Chapter 36) prove that an inductively built family of triangles has a hitting set of at most vertices, and ProofsInTheBook.PolygonGeometryDischarge.artGallery_strict_of_residue proves a geometric guard bound conditional on two assumed inputs. Neither states the fan partition, which is strictly stronger than a hitting set, and neither uses the cyclic labelling of a triangulated polygon. This mission asks for a machine-checked proof of Chvátal's own theorem and of the claims of his proof, on a reusable encoding of triangulated polygons (cyclic labels, non-crossing diagonals, triangles, cutting along a diagonal) that other results on polygon triangulations can build on.
The induction itself is short on paper; the work is in what the paper calls easy. Cutting along a diagonal and relabelling each piece cyclically must be shown to produce triangulations again, with the triangles split exactly between the two pieces; this is a statement about non-crossing chords that has no counterpart in Mathlib. The case analysis "it is easy to verify that we have one of the following four cases" is an enumeration of all triangulations of a 5-, 6- or 7-gon whose diagonals have span at most 3, and its exhaustiveness (including the mirror images of (2) and (4)) is precisely what the four inductive constructions rely on. The constructions then enlarge one fan of a smaller triangulation, so the induction must be carried out for partitions of arbitrary triangulations, with fans that share edges.
Fin n (vertex is the paper's ) plus a finset D : Finset (Sym2 (Fin n)) of diagonals that pairwise do not cross and is maximal. Maximality is binding: without it the empty set would "triangulate" every polygon and the goal would hold vacuously.n / 3 in ℕ. The goal assumes only .Fin.rev); the four cases are an explicit disjunction on the diagonal set of . The minimality of enters as the hypothesis that inner edges of have span at most 3.All definitions are in one file, ChvatalArtGallery.FanPartition.Triangulation; the triangle and cut machinery is reusable for any result on triangulated polygons. Proofs of the milestones, general lemmas on non-crossing diagonal sets (the count , existence of ears, the dual tree), and alternative proofs of the goal are all welcome.
Chance-constrained programming replaces a linear program subject to by a problem in which some data are random and each constraint only has to hold with a prescribed probability. Charnes and Cooper introduced the idea in 1959 for scheduling heating-oil production against weather-dependent demand, and the formulation is now a standard modelling tool in operations research, finance, energy systems and engineering design (Charnes and Cooper 1959; Prékopa 1995).
A chance-constrained problem is not directly solvable: its constraints are probabilities of events that depend on the decision. The 1963 paper of Charnes and Cooper (doi:10.1287/opre.11.1.18) asks when such a problem has a deterministic equivalent, an ordinary mathematical program with the same feasible decisions and corresponding objective values, and when that equivalent is a convex program. Its first answer, for the expected-value ('E') model under linear decision rules and normality, is the subject of this mission. The resulting constraint form, a mean slack dominating standard deviations, is an early instance of the second-order-cone reformulation of individual normal chance constraints used throughout modern stochastic and robust optimization.
Timeline. 1959: Charnes and Cooper, chance-constrained programming with the heating-oil model. 1963: this paper, deterministic equivalents for the E, V and P models under linear decision rules . 1965: Miller and Wagner treat joint chance constraints with independent rows (doi:10.1287/opre.13.6.930). 1971: Prékopa's logarithmically concave measures give convexity of joint chance constraints under log-concave laws.
Let be a probability space. The data are a constant matrix with rows , a random right-hand side and random objective coefficients . A linear decision rule is an real matrix ; it chooses after is observed. Write , and .
The E-model (18) is
with one probability level per row: the constraints are row-wise, as in (3) of the paper, not a single joint constraint.
For let be the standard normal -quantile. With the moment functions (30),
the paper's deterministic program (29) in the variables , , is
Assume every is square integrable, every and integrable, and uncorrelated (), every variate normal (for every and , zero variance allowed), and . Then
The result. The theorem turns a problem whose constraints are probabilities into a finite-dimensional convex program whose data are the first two moments of and the means of . The optimal rules of (18) minimize (29), whose optimal value is the negative of the maximum in (18). The slack variables separate each constraint into a "quality" part (the mean slack ) and a "risk" part ( standard deviations), which is the interpretation the paper develops in (31) and its Appendix. The same constraint set serves the V-model (33), so only the objective changes between the two models.
Formalizing it. The result is classical and its proof is elementary, but the paper's argument is informal in ways that matter for a machine-checked version: it divides by a standard deviation it then allows to vanish, writes for what must be an upper-tail function, and labels a variance as while defining as a raw second moment. This mission produces a statement in which each of these points is settled, with every hypothesis explicit. No machine-checked version of the result is known to exist.
The chance-constraint step itself is a one-dimensional fact about the normal law, but three points need care. The variance of may be zero for some and ; then the law is a point mass, the quotient in (27) is undefined, and the equivalence must be argued separately, as footnote † of p. 28 indicates. The quadratic constraint of (29) alone, , describes both nappes of a hyperboloid and is not convex; convexity needs and the positive semidefiniteness of , which comes from square integrability of and not from normality. Finally, the identity relating , and the variance requires the integrals to be genuine, so the integrability hypotheses cannot be dropped.
Everything is in the namespace ChanceDetEquiv.EModel. The probability space is (Ω, P) with [IsProbabilityMeasure P]; A : Matrix (Fin m) (Fin n) ℝ, b : Ω → Fin m → ℝ, c : Ω → Fin n → ℝ, D : Matrix (Fin n) (Fin m) ℝ; is (A *ᵥ (D *ᵥ b ω)) i. Expectations are Bochner integrals and probabilities are P.real. Explicit readings of the paper's phrases:
Convex ℝ of the feasible set of (29) in , included; for the V model it also asserts ConvexOn ℝ of ;gaussianReal μ s for some and ; joint normality of is not assumed, since it would be a stronger hypothesis;Cohen2019_Robust_Phi; in (26)–(27) is read as the upper-tail function of , and is added so that is finite;Positive variance is a hypothesis of milestones 2 and 3, where (27) has a denominator. The goal and later milestones admit zero variance. The statements admit no trivializing reading: the normality hypothesis is satisfied by constant and by Gaussian , the integrability hypotheses rule out the junk value of non-integrable expectations, and rules out the junk value of .
A complete development needs: the normal CDF and quantile, the law of an affine image of a random variable, variance as in , and convexity of the epigraph of a seminorm composed with an affine map. The convexity milestones need no probability beyond and are reusable for any second-order-cone representation of individual chance constraints. Proofs of any milestone, and of the goal from the milestones, are welcome.
The related open platform item KallMayer.Chance.chapter2_theorem2_5 (convexity of a single normal chance-feasible set in ) is credited here and not restated: no item of this mission states the convexity of the set of feasible for (18). Related published items that are about other models: DRCVRP.RCI.prob_le_iff_valueAtRisk_le (chance constraints and value-at-risk for a general law) and the log-concavity results of NumStochOpt.LogConcave.
Many assignment questions reduce to one combinatorial question: given finitely many sets, can one choose a different element from each? Workers are matched to jobs they are qualified for, rows of a matrix to columns with nonzero entries. The criterion for when this is possible is Hall's marriage theorem, first stated and proved by P. Hall in a five-page note in 1935 (DOI 10.1112/jlms/s1-10.37.26). It underlies bipartite matching, the integrality of the assignment polytope, the Birkhoff–von Neumann theorem on doubly stochastic matrices, and transversal theory in matroids.
Hall's note was written with a second question in view. In 1916 D. König proved, in the language of bipartite graphs, that if a set of things is divided into classes of things in two ways, then one can choose things that represent every class of both divisions at once ("Über Graphen und ihre Anwendungen", Math. Annalen 77 (1916), 453). Van der Waerden (1927) and Sperner (1927) gave the set-theoretic form and a short proof. Hall's contribution was a criterion for a common system of representatives of two divisions in which the classes need not have equal sizes, obtained from the marriage theorem in two short steps.
Let be any set, finite or infinite, and let
be a finite system of subsets of . The sets may be infinite and need not be distinct; when one speaks of of the sets, indices are meant, so a repeated set is counted with multiplicity. A complete set of distinct representatives, or C.D.R., of (1) is a choice of pairwise distinct elements of with
The system satisfies Hall's condition when any of the sets contain between them at least elements of , for . The meet of all C.D.R.s, written , is the set of elements of that occur as a representative in every C.D.R. of (1).
A division of into classes is a family of pairwise disjoint sets whose union is . The paper writes and for intersection and union; this mission writes and .
In Lean the system is T : ι → Set α over a finite index type, a C.D.R. is an injective a : ι → α with a i ∈ T i (IsCDR), Hall's condition is HallCondition, and the meet of all C.D.R.s is cdrMeet, all in the namespace HallReps.CDR.
Let be divided into classes in two ways, , each a division into pairwise disjoint classes. If, for each , any of the classes contain between them elements from at least of the classes , then for some permutation of there are elements
The set and the classes may be infinite, and no class is assumed non-empty.
A companion item states König's theorem (§1, p. 26), which the paper deduces from Theorem 3 on p. 30.
Theorem 3 gives a necessary and sufficient criterion for two partitions of a set into classes to admit a common system of representatives. Necessity is immediate, and the paper proves sufficiency. It contains König's theorem, and through it the statement that a regular bipartite multigraph has a perfect matching, as the case of equal class sizes. Hall remarks that R. Rado's generalization of König's theorem (1933) also follows. Theorem 2, the passage from "distinct elements" to "elements of distinct classes", is the form used for transversals of partitions and is the first instance of what later became the theory of common transversals and matroid intersection.
On the formal side, Hall's theorem for finite sets is in Mathlib as Finset.all_card_le_biUnion_card_iff_existsInjective' (in Mathlib/Combinatorics/Hall/Finite.lean), and the platform already has a proved equivalence for arbitrary sets with a finite index type (YogeshwaranDM.sdr_iff, included in this mission as a reference item) as well as finite bipartite-graph forms. For that reason Theorem 1 is a milestone and not the goal. What this mission adds is Hall's own proof structure, namely the meet of all C.D.R.s and the Lemma about it, which has not been formalized; Theorems 2 and 3 for divisions of a possibly infinite set; and König's theorem in its set-partition form. To our knowledge none of these statements has a machine-checked proof on the platform.
Theorem 3 does not follow from Theorem 1 applied to the classes directly. Theorem 1 produces distinct elements, but the conclusion needs elements in distinct classes , and two distinct elements of may lie in the same . The paper's route goes through Theorem 2, which allows any number of classes. That route needs Theorem 1 for systems whose sets can be infinite, because a single may meet infinitely many classes, so the finite-set version of Hall's theorem in Mathlib is not enough on its own. In Hall's own proof of Theorem 1, the work lies in the Lemma. It is an exchange statement about all C.D.R.s at once, whose object is defined by a universal quantifier over C.D.R.s, and it must be established over an arbitrary finite index type with possibly infinite sets.
α, with no finiteness or decidability assumed. The system (1) is T : ι → Set α with [Finite ι] (or Fin (m + 1) in the two induction steps, where the paper's is the Lean m + 1, its last set is T (Fin.last m), and (4) is fun i : Fin m => T i.castSucc).Set.encard in ℕ∞, so an infinite union counts as infinite. Set.ncard is used only for subsets of Fin m, for the finite set (with its finiteness stated), and in König's theorem.Finset ι of indices, so repeated sets count with multiplicity.cls : α → κ in Theorem 2, with κ arbitrary, and p q : α → Fin m in Theorem 3 and König's theorem. A class map makes the classes cover and be pairwise disjoint by construction. Empty classes are allowed.p (a i) = i ∧ q (a i) = σ i.cdrMeet is all of α). The first induction step omits the page's C.D.R. of (4), because its hypothesis already implies one. König's theorem adds , which the page presumes and without which the statement is false.Finset α would reduce Theorem 1 to Mathlib and lose the page's "It is not necessary that the sets shall be finite". Measuring unions by ncard would make Hall's condition fail exactly when a union is infinite. An infinite index type would make Theorem 1 and the Lemma false. None of these is used.Mathlib/Combinatorics/Hall/Finite.lean and Mathlib/Combinatorics/Hall/Basic.lean. https://github.com/leanprover-community/mathlib4Open shops model production and service systems in which every job must visit every machine, but the order of the visits is free: a car that needs an inspection, a wash and a tyre change, a patient who needs several tests, a student who sits several exams. The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) fixed the three-field notation that the scheduling literature still uses, and classified the complexity of the problems it can express. Among the polynomially solvable cases, the preemptive open shop with makespan objective, , is one of the few multi-machine problems whose optimal value has a closed form for any number of machines and jobs.
Timeline.
There are machines and jobs . Job consists of operations ; operation must be processed on machine for time units. The processing-time matrix is : its rows are machines and its columns are jobs. Every job is available at time .
Preemption is allowed: an operation may be interrupted and resumed later. A schedule is a finite list of pieces , each meaning that processes during . A schedule is feasible if
The makespan is the time at which the last piece ends, and is its minimum over feasible schedules. The load of machine is the row sum , the length of job is the column sum , and
A row or column is tight if its sum equals and slack otherwise. A decrementing set is a set of strictly positive entries of with exactly one element in each tight row and each tight column and at most one in each slack row and each slack column.
For every ,
This says that the optimal makespan is exactly the largest machine load or job length, and that it is attained.
The result. The theorem turns an optimization over continuous-time schedules into the computation of sums. It certifies optimality by a counting argument, it is the base case for preemptive open shops with release dates and due dates, and it is used elsewhere in the survey (§4.4.6) to reduce problems on unrelated machines with preemption to open-shop instances. Because a nonnegative matrix whose row and column sums are all equal is a multiple of a doubly stochastic matrix, the theorem is a scheduling form of the Birkhoff–von Neumann decomposition. It also underlies timetabling and edge-colouring results for bipartite multigraphs.
Formalizing it. The theorem has been proved since 1976 and is textbook material. No machine-checked proof is known to exist: Mathlib has the Birkhoff–von Neumann theorem for doubly stochastic matrices but no model of open-shop schedules. A formalization adds a reusable model of preemptive multi-machine schedules with both disjointness requirements, a checked proof of the decrementing-set construction, and a termination argument the survey asserts without proof.
The lower bound is a one-line counting argument. The difficulty is the construction of a schedule of length exactly . Scheduling each machine's operations back to back gives length , but may run one job on two machines at once. Scheduling job by job has the symmetric defect. A greedy list schedule that only respects both constraints can leave machines idle and overshoot . The construction must keep every tight line busy at every moment while never letting a slack line fall behind. The existence of the decrementing set at each stage is the combinatorial core: it is a Hall-type matching condition, not a local choice. Termination is also not automatic, because a careless choice of step length can produce infinitely many shrinking steps.
All objects live in the namespace SchedSurvey.OPmtn. Machines and jobs are Fin m and Fin n, both 0-based, and processing times and piece endpoints are real numbers; integer data are a special case. A schedule is a List of pieces. Feasibility requires nonnegative start times, disjointness for pieces sharing a machine or a job (touching intervals allowed), and exactly units of processing for every pair . Every theorem assumes .
" is the maximum" is the predicate IsMaxLoad P C: all line sums are at most and one equals . The goal is stated in threshold form and mentions no maximum at all. The display defining on p. 313 prints for the second term; the following sentence shows it means the row sums , and the formalization uses those. The hypothesis matters only for , where the empty schedule finishes by every .
A trivializing formalization is ruled out: the goal mentions neither decrementing sets nor . Its "if" direction asserts that a schedule exists. Feasibility counts work per pair (machine, job), not per job, and forbids a job from running on two machines at once. Without either requirement the statement would be a different and easier theorem.
A complete development needs: list sums of interval lengths over disjoint intervals, the existence of decrementing sets (via Birkhoff–von Neumann, König's theorem or Hall's theorem on the bipartite graph of positive entries), the step and termination lemmas, and concatenation of schedules. The schedule model and the decrementing-set lemma are reusable for other preemptive shop problems. Contributions of alternative proofs of any milestone, for example a direct Hall-theorem proof of the existence of decrementing sets, are welcome.
Shop scheduling asks how to sequence jobs that each need processing on several machines. In an open shop, a job's operations may be executed in any order, as in testing stations, repair bays, or classroom and examination timetables, where the order in which a candidate visits the stations is irrelevant. The objective studied here is the makespan , the time at which the last operation finishes.
The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) introduced the three-field notation that the scheduling literature still uses, and classified the complexity of the problems it names. For the open shop, its §5.2.1 presents a simplified exposition of the result of Gonzalez and Sahni (J. ACM 23, 1976): with two machines and no preemption, the obvious lower bound on the makespan is always achieved. The same page records that the three-machine case is binary NP-hard, so two machines is exactly where the problem is easy.
Timeline. Gonzalez and Sahni (1976) gave the linear-time algorithm for , proved NP-hardness for , and gave a polynomial algorithm for the preemptive problem . Graham et al. (1979, §5.2.1) gave the shorter construction formalized here, and observed (§5.2.2) that it implies preemption brings no advantage for . Lenstra (cited as forthcoming in the survey) showed , and unary NP-hard.
There are jobs and two machines , . Job has an operation on of length and an operation on of length . There is no preemption, and every job is available at time . A schedule assigns start times and to the two operations of , which then occupy on and on .
A schedule is feasible if
Write and for the two machine loads. The survey's construction uses the sets
two distinct jobs , with and , and , .
and the optimum is attained. Formally, for every : a feasible schedule completing every operation by exists if and only if , and for all . The goal mentions neither , , , nor the case analysis; those are the milestones.
The result. The theorem gives a closed form for the optimal makespan of a two-machine open shop, together with a linear-time construction of an optimal schedule. The survey uses it immediately: since the bound is also a lower bound for preemptive schedules, is solved by the same schedules, so preemption gives no advantage on two machines (§5.2.2). It is the standard example of a shop problem whose trivial lower bound is tight, and the contrast with the binary NP-hard marks the complexity boundary for nonpreemptive open shops.
Formalizing it. The result is classical and proved on paper; no machine-checked proof is known to exist on this platform. The mission produces a reusable model of nonpreemptive two-machine open-shop schedules with real processing times, a verified lower bound, and a verified constructive argument. Unlike many existence-of-schedule results, the survey's construction is explicit (orders and start times), so it can be formalized directly rather than through an abstract existence argument.
The lower bound is the easy half. The difficulty is the construction: a schedule must meet the bound simultaneously on both machines and for every job. The natural first idea, running every job on then in some order (a flow-shop schedule), fails: Johnson's rule then gives a makespan that can exceed , because the open shop needs some job to visit first. The survey's construction moves exactly one job, , to the front of , and its correctness depends on the choice of and and on the case split on versus . Figures 5.3 and 5.4 are drawn for ; in the other subcases the start times shown in the figures need adjustment, and the formal statements of the cases assert lengths rather than the figures' exact start times.
All declarations live in the namespace SchedSurvey.O2. Jobs are Fin n, 0-based ( is index ). Processing times and start times are real numbers with ; the survey's integer data are a special case, and every claim of §5.2.1 holds over the reals. A schedule is a pair of start-time functions s₁ s₂ : Fin n → ℝ. Interval non-overlap is s + p ≤ s' ∨ s' + p' ≤ s, so touching intervals are allowed and a zero-length operation occupies nothing. Feasibility (IsFeasible) contains both disjointness constraints of §2.1, the machine constraint and the job constraint, with the two operations of a job in either order. The job constraint is essential: without it the optimum would be and the goal false.
"Length at most " is CompletesBy a b S L: every operation ends by . Optimality is stated in threshold form, which avoids taking a supremum or infimum over a possibly empty set and is equivalent to " equals the maximum and is attained". A maximum over or appears as a bound on every member, which is also correct for empty or . The orders of and are duplicate-free lists whose members are exactly those sets; back-to-back start times are given by contigStart.
The milestone on the choice of , assumes , which the page presupposes; the goal does not, and covers as well. The lower bound assumes , which matters only for .
A trivializing formalization is ruled out: feasibility includes both disjointness constraints and nonnegative start times, the threshold is quantified over all , and no constant is fixed.
Contributions welcome: proofs of the lower bound (a sum of disjoint intervals inside ), of the list-based block lemmas, of the case lemmas, and of the goal from them. The interval and back-to-back-schedule lemmas are reusable for other shop problems.
Queueing results often relate an average accumulated over customers to an average accumulated over time. In the familiar relation , the long-run average number in a system equals the arrival rate times the average time spent there. Glynn and Whitt study a broader relation, , that can represent queue lengths and waiting times but also costs, work, and other cumulative inputs. Their framework is deterministic: a stochastic model may supply a sample path, yet the central comparison is a statement about functions on that path. This lets the same theorem apply to different queueing models without choosing a probability law for each one. Glynn and Whitt (1989)
The paper asks for more than the usual forward implication from a customer average to a time average. Its main theorem identifies conditions under which either average has a finite limit exactly when the other does. It also compares lim inf and lim sup when ordinary limits fail to exist. Both questions matter when sample paths fluctuate: convergence of one average cannot simply be inferred from a visual similarity between the two ways of indexing the input. Glynn and Whitt (1989), §§1–2
A cumulative input is a real-valued function on , nondecreasing separately in the customer coordinate and the time coordinate . Its marginal limits and are finite for every fixed argument. The first counts all eventual input associated with customers through index ; the second counts all input accumulated through time . The marginal averages are
The paper permits cumulative inputs that are not distribution functions of measures on rectangles. In particular, it does not require a rectangle-increment inequality or nonnegative values of . The finite marginal limits and monotonicity are the actual assumptions of its general framework. Glynn and Whitt (1989), p. 635, (1)
A time change , for , is finite, nonnegative, nondecreasing, and right-continuous, and tends to infinity with . Its right-continuous inverse is . The two time changes may differ. Both have the same asymptotic rate for a positive finite . The paper's two approximation conditions are
as , where is the left limit. Condition (14) concerns input already present by a left-limit time; condition (15) concerns input not yet present by a right-limit time. Glynn and Whitt (1989), p. 638, (3), (14)–(15)
With only (14) and the rate for , the corrected upper bounds are
With only (15) and the rate for , the corrected lower bounds reverse both inequalities. The two bounds remain useful separately when only one approximation condition holds. Their lim inf and lim sup may be infinite. Glynn and Whitt (1989), p. 639, Theorem 1(a)–(b) and Remark 2
Under both conditions, Theorem 1(c) asserts equality of the respective lim inf and lim sup. The mission goal is Theorem 1(f): for finite real limits,
Here the equivalence means existence of finite limits, with the second clause identifying their values. The lim inf and lim sup statement is retained as a milestone because it also covers nonconvergent paths. Glynn and Whitt (1989), p. 639, Theorem 1(c), (f)
The goal gives a two-way transfer between customer-indexed and time-indexed long-run averages. If an application establishes one finite average, the theorem supplies the other and fixes its value. The one-sided milestones give meaningful bounds when only one approximation condition is available; the lim inf and lim sup milestone retains information when neither average converges. These outcomes are stated for a general cumulative input, so applications can supply their own , , and without changing the theorem. Glynn and Whitt (1989), §§2–4
The paper proves these results on paper. The formalization target is a machine-checked interface for the paper's deterministic framework, its inversion lemmas, its asymptotic inequalities, and the two-way limit theorem. At this drafting stage the Lean theorem statements compile with proof placeholders; no machine-checked proofs of these new statements are claimed. The definitions and inverse-rate lemma can be reused in other sample-path results.
The two marginal averages examine different slices of , and a time change may jump or have flat intervals. A direct substitution of does not give an equality between and under the paper's assumptions. The left limit in (14) and the value in (15) also behave differently at jumps. The inverse connects the coordinates, but its boundary behavior and rate must be handled before comparing the averages. These issues are present even without stochastic randomness. Glynn and Whitt (1989), pp. 638–639
Lean represents by nonnegative real numbers and by a real-valued function with separate monotonicity and bounded marginal ranges. Real suprema represent and ; the boundedness fields ensure those suprema are the paper's finite limits. The inverse is an infimum of a nonempty set because . The left limit is the supremum over earlier nonnegative arguments, with . Ratios at zero use Lean's total division convention, but every ratio assertion is asymptotic at infinity.
Lim inf and lim sup are taken in the extended reals so an unbounded average retains an infinite limit. Multiplication by happens in the reals before conversion. Ordinary limits in Theorem 1(f) are finite real limits. The two time changes are independent and share only the positive rate . The goal assumes only (14), (15), and the stated time-change rates; it does not assume its own inverse-rate or asymptotic conclusions. No nonnegativity or rectangle inequality is imposed on .
Theorem 1(a) and (b) have their hypothesis pairing reversed in print. The formalized one-sided bounds use the corrected pairing, and the milestone text preserves the printed source for audit. The intermediate expressions involving are excluded from the corrected statements because the framework does not assume customer-coordinate right continuity. Theorem 1(c) and (f) use both conditions and are true as printed. The scope includes the definitions, Lemmas 1–2, corrected parts (a)–(b), and parts (c) and (f). Contributions toward their proofs and reusable time-change lemmas are welcome. Glynn and Whitt (1989), p. 639, Theorem 1
An integer program is a linear program whose variables must take integer values. Its linear relaxation can be solved efficiently, while the integer program itself is NP-hard in general, so a recurring question in integer programming is how much the optimal solution of the relaxation says about the integer optimum. Simple rounding of the fractional optimum does not answer it: examples show that the integer optimum need not lie within distance one of the LP optimum, even when the right-hand side is large.
R. E. Gomory's 1965 note in the Proceedings of the National Academy of Sciences (doi:10.1073/pnas.53.2.260) showed that, for right-hand sides lying deep inside the cone of an optimal LP basis, the integer program is solved exactly by the LP solution plus a correction computed in a finite abelian group. The resulting group relaxation (the "corner polyhedron" of Gomory's later work, Gomory 1969) underlies a large body of work on cutting planes, the master group problem, Gomory–Johnson functions and asymptotic integer programming.
Timeline. Gomory's fractional cutting-plane algorithm (Gomory 1958) introduced the "fractional rows" of the simplex tableau; the 1965 note identifies the group they generate with and proves the asymptotic theorem formalized here. Gomory 1969 develops the corner polyhedron; Gomory and Johnson (1972) study the continuous valid functions of the corner polyhedron.
Let be an integer matrix of the form , let and . Problem P1 is
and P2 is P1 with integer. A basis is a nonsingular submatrix of ; after rearranging, with and , and . The relative cost of a nonbasic column is , and is an optimal basis when all . The cone of the basis is ; removing from it all points within Euclidean distance of its boundary gives the reduced cone .
Let and the lattice of integer combinations of . The factor module is a finite abelian group with elements; write , for the classes of , . The group problem (4) is
with optimal value . Finally .
If , then P1, P2 and (4) attain their optima, the value of P2 is
an optimal solution of P2 is
for an optimal solution of (4) with , and , are -periodic: .
In the order of the paper's proof: (p. 262); periodicity of (4) (p. 263); the cost identity (5)–(6); " is ", the simplex optimality criterion (a published, proved theorem); the projection of a solution of P2 to a solution of (4); the bound (7), ; the extension of a solution of (4) to an integer solution; the LEMMA (an optimal solution of (4) with ); and the bound that places in .
THEOREM 2: the optimal satisfies . THEOREM 4 (with the bound corrected, see below): if an optimal of (4) has , the optimum of (4) is not unique.
THEOREM 1 reduces integer programming, for right-hand sides far from the boundary of an optimal cone, to a shortest-path-type problem over a group of order : the integer optimum is determined by the LP optimum and a periodic correction, and it can be computed in time polynomial in and (THEOREM 3, not formalized here). It explains why rounding fails while a structured correction succeeds, and it is the starting point of the corner-polyhedron and cutting-plane theory built on the group relaxation. THEOREM 2 bounds how far the integer optimum lies from a lattice point of , an early proximity result.
The results are classical and proved in the paper; none of them has a machine-checked proof that this mission is aware of. The mission produces a Lean statement and proof of the asymptotic theorem, together with reusable statements about the group and the zero-sum shortening argument of the LEMMA.
The decomposition is a direct computation. The difficulty is the converse: an optimal solution of the group problem extends to an integer point , but nothing in (4) forces . Optimality of alone does not bound : an optimal solution may carry zero-cost cycles of arbitrary length, and then can leave the cone . The theorem therefore depends on choosing the right optimal solution of (4), one whose total size is bounded by the group order, and on relating that combinatorial bound to the Euclidean geometry of the cone.
Needed infrastructure: the cardinality of (available in Mathlib through determinants of basis changes), a zero-sum/pigeonhole argument in a finite abelian group, the simplex optimality criterion (published), and elementary Euclidean estimates. The group-theoretic lemmas are reusable for other group-relaxation and proximity missions. Proofs of the milestones, alternative arguments and the extension to the open-ball reading of are welcome.
The maximal multi-commodity flow problem asks how much total flow several commodities, each travelling from its own sources to its own sinks, can send through a network whose arcs have shared capacities. It arises in communication and transportation planning: Kalaba and Juncosa's 1956 study of communication networks (Management Science 3(1)) leads to linear programs of this form. For a single commodity the problem has a clean combinatorial theory: the max-flow min-cut theorem of Ford and Fulkerson (1956, doi:10.4153/CJM-1956-045-5) and the labeling algorithm. With several commodities both fail: the min-cut equality is false, and simplex bases are no longer triangular.
In a short note received in October 1957 and published in Management Science in 1958, L. R. Ford Jr. and D. R. Fulkerson proposed a way to solve the multi-commodity problem with the simplex method anyway (doi:10.1287/mnsc.1040.0269, reprinted 2004). They use the arc-chain formulation, which has one variable per chain from a source to a sink of a commodity. That formulation has far too many variables to write down. The note's point is that the simplex method never needs them explicitly. The "pricing" step (finding a variable to enter the basis, or recognizing that none exists) can be carried out by one shortest-chain computation per commodity, with the simplex multipliers as arc lengths.
Timeline. Ford (1956, RAND P-923) gave the label-correcting shortest-chain procedure the note uses. Ford and Fulkerson (1958) applied it to price the columns of the arc-chain program. Dantzig and Wolfe (1960) generalized the idea into the decomposition principle. Gilmore and Gomory (1961) applied the same pattern to the cutting-stock problem, and it is now called column generation.
A network has finitely many nodes and arcs . Each arc joins two nodes, has a capacity , and is either directed (traversable one way only) or undirected (traversable both ways). There are finitely many commodities; commodity has a set of sources and a set of sinks .
A chain from to is the arc set of a path with distinct nodes, each arc traversable from to . A commodity chain of is a chain from a node of to a node of . List the commodity chains, for all commodities, as , and let be the incidence matrix: if contains and otherwise. With the flow along and the slack of arc , the problem is the linear program
A basis is a set of columns of forming an invertible matrix . Its simplex multipliers satisfy, for every basic column ,
Read as arc lengths, the give each chain the length . The labeling process for a source set starts with labels on and elsewhere. It repeatedly finds an arc traversable from to with and replaces by . In Lean the labels are lab : V → WithTop ℝ, the multipliers are α : E → ℝ, and all objects live in the namespace FordFulkerson58.ArcChain.
Let be a basis with basic feasible solution and multipliers . Then:
Further items state the remarks of §3–§4: a negative multiplier lets a slack enter; the slack basis is a feasible start; dominated chains can be ignored; limited supplies reduce to the same problem by adding new directed source arcs; Figure 2 is the incidence matrix of Figure 1; with negative lengths the labeling process may not terminate.
The result. The test turns a linear program with exponentially many columns into one whose pricing step costs one shortest-path computation per commodity. Only the basis is ever stored. This is the first instance of column generation, which now underlies solvers for multi-commodity flow, cutting stock, vehicle routing, crew scheduling and many other set-partitioning models, typically inside branch-and-price. Part (a) together with milestones 2–3 also gives the correctness of Ford's label-correcting algorithm with non-negative lengths, started from a source set and with any order of arc scans.
Formalizing it. The results are classical and proved in the paper's informal style. None of them is formalized: the platform has no arc-chain LP, no column pricing, and no formal statement of Ford's label-correcting process. The general LP facts are on the platform (the simplex optimality criterion and weak duality, both proved) and are included as references. This mission adds the network-specific layer: chains as arc sets of simple paths, the labeling process as a relation on labelings, and the link from final labels to reduced costs. One sentence of the paper is corrected. The trace-back "eventually" reaches only along some backward path, because zero-length cycles can trap a naive backward search, and milestone 3 states the true version.
The obvious argument for termination says each step lowers a label and there are finitely many chains. It fails: labels are lengths of walks, not chains, and with zero-length arcs (multipliers are often ) there are infinitely many walks. Termination needs the finiteness of the set of walk lengths below a bound, not positivity. The correctness of the final labels needs both properties of the labeling: it is produced by the process (so every label is the length of a walk from ), and it is terminal. A terminal labeling alone, such as all labels , is not a distance labeling. Finally, the optimality claim is an LP statement about the full, never-enumerated column set. It must be derived from (4), and the shortest-chain lengths, with the chain columns indexed abstractly.
Nodes, arcs and commodities are finite types V, E, ι. Each arc has tail, head, a per-arc directed flag and a capacity b : E → ℝ; commodities have src snk : ι → Finset V. Parallel arcs and mixed directed/undirected networks are allowed. No sign of the capacities and no disjointness of sources and sinks is assumed, except 0 ≤ b in the zero-flow item, where it is disclosed. Chains are arc sets of simple paths. The null chain at a source is a chain, so sources have distance . Columns are pairs (commodity, chain), so one arc set used by two commodities gives two columns. The columns of are indexed by Col N ⊕ E. A basis is β : E → Col N ⊕ E with IsUnit (basisMatrix N β).det; its basic feasible solution and multipliers (4) are hypotheses about this β. Labels are in WithTop ℝ with ⊤ for . Shortest-chain lengths are finite infima (Finset.inf), equal to ⊤ when there is no chain. The process scans arcs, not node pairs, which handles parallel arcs and the undirected case .
The standing assumption of §3 ("a stage has been reached in the computation where all are non-negative", p. 1779) is a hypothesis of the goal and of milestones 1–4. Milestones 1–3 are stated for any non-negative length function. The paper has no numbered theorems; every milestone is an unnumbered sentence of §3, cited by page and position.
A trivializing formalization is ruled out: the goal does not assume shortest-chain lengths, the trace-back, or any reduced-cost fact beyond (4). Statements about final labels require labelings that are both reachable from the initial labels and terminal, and part (a) shows such labelings exist.
Reusable beyond this mission: the chain and labeling layer (a label-correcting shortest-path algorithm from a source set over mixed networks) and the arc-chain LP. Contributions to the LP layer, which can import the referenced Matoušek–Gärtner results after reindexing, are particularly welcome.
Dynamic traffic assignment models how commuters choose routes and departure times when travel times change over the day. In the model of Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41 (1993)), the time to traverse a path is built recursively from arc exit-time functions: a vehicle that enters an arc at time leaves it at time . The equilibrium conditions of that model refer to the inverses of these functions, so the model is only well defined when every arc exit-time function is invertible.
Invertibility has a direct traffic meaning. A strictly increasing exit time is the first-in-first-out (FIFO) property: a vehicle that enters later cannot leave earlier, so no overtaking occurs on the arc. Whether a given delay model respects FIFO was an active question in the early 1990s, because several delay functions used in practice violate it for some inflow patterns.
Timeline:
Consider one arc. Vehicles enter it at the entry rate , a continuous function of time ; the first vehicle enters at time . For an exit-time function , the arc volume at time is the inflow mass of the vehicles that entered during and have not left by time :
The linear delay function (18) of the paper is
a fixed free-flow travel time plus a queueing time determined by the service rate . The exit time is entry time plus delay, so is pinned by the exit-time equation
The equation is implicit: appears on the right through the volume. The proof partitions time at , ; in particular is the exit time of the first vehicle. In Lean these objects are linearDelay, arcVolume, IsLinearExitTime and tSeq in FrieszDUE.FIFO.
For and a nonnegative continuous entry rate , every satisfying the exit-time equation is strictly increasing on :
and hence injective there, so exists.
A supporting, non-milestone item states that the exit-time equation has a solution for every admissible .
The result makes the path exit-time functions of the dynamic network model invertible whenever the arc delays are linear in volume. That invertibility is what allows the path costs, and through them the variational inequality of Theorem 2 of the same paper, to be written down. In traffic terms it certifies that linear volume-based delays never let a later entrant overtake an earlier one, whatever the continuous inflow profile.
The theorem is proved in the paper. As far as is known it has no machine-checked proof. The mission produces one, together with a formal model of a single arc whose exit time is defined implicitly through the volume, which is reusable for other delay functions and for FIFO questions in dynamic traffic assignment.
The obvious argument differentiates and bounds the outflow rate. But the volume can only be written as once is known to be invertible, which is the conclusion. The paper breaks the circularity by working forward in time: on the volume depends only on restricted to the earlier interval, whose invertibility is already established. A formal proof must make this forward dependence rigorous for an exit time given only by the implicit equation, handle one-sided derivatives at the junctions , where is generally not differentiable, and show that the junctions do not accumulate.
Time is real; the entry rate is a function with and continuous on . Both are added hypotheses: Theorem 1 names none, nonnegativity is implicit in "entry rate", and the remark after the proof covers "all continuous entry rate patterns". Integrals are Lebesgue integrals. Monotonicity is claimed on only, the entry times that the equation constrains. Derivative claims in the milestones are taken within the closed interval . The paper's separate pieces are one global function here, so the junction identities (27), (30), (33) are automatic. Lemma 1 adds the hypothesis , without which it is false.
The exit time τ is pinned by the implicit equation τ(t) = t + αx(t) + β, where x(t) is the inflow mass of vehicles that entered by time t and have not exited by time t; no monotonicity or invertibility of τ is assumed. A formalization that defined the volume through or assumed monotone would assume the conclusion and is ruled out.
The development needs one-sided derivatives of parametric integrals, the inverse-function derivative on an interval, and a forward induction over the partition. Contributions of proofs for any milestone, of the existence item, and of a uniqueness result for the exit-time equation are welcome.
Temporal-difference (TD) methods learn to predict an eventual outcome from the differences between successive predictions rather than from the difference between each prediction and the final outcome. Sutton's 1988 paper Learning to predict by the methods of temporal differences introduced the TD() family and gave the first convergence proof for a TD method; before it, as the paper notes (p. 23), "no TD method has ever been proved stable or convergent to the correct predictions". TD learning is now the core of policy evaluation in reinforcement learning, and later analyses (Dayan 1992, Tsitsiklis and Van Roy 1997) start from the setting fixed here.
Timeline:
An absorbing Markov chain has a finite set of nonterminal states, a finite set of terminal states and transition probabilities (, ) with . Let be the matrix . "Absorbing" means that every sequence terminates with probability one; for a finite chain this is .
A sequence starts in a nonterminal state drawn from a distribution , follows the chain through nonterminal states until it enters a terminal state , and then produces a scalar outcome drawn from a distribution with finite mean . Let . The ideal prediction of state is the expected outcome from ,
The learner does not see states, only an observation vector for each , and predicts linearly, . Linear TD(0) with weight updates after each sequence keeps fixed during a sequence and then sets, with ,
Sequences are experienced independently; is the weight vector after sequences. Let be the expected number of visits to in one sequence, , and the matrix with columns .
For every absorbing chain, start distribution , outcome laws with finite means and linearly independent , with every , there is such that for and every ,
The threshold is existential, as in the paper; no explicit value is fixed.
Theorem A.1 (Neumann series under ); (5) the ideal predictions; (7) ; the mean recursion ; Theorem A.2 ( nonsingular); Theorem A.3 (); the Lemma of p. 27; positive definite; the eigenvalues of have positive real parts; and for small .
Theorem 3: under repeated presentations of a finite training set, batch linear TD(0) converges (deterministically) to the maximum-likelihood predictions , with its two supporting steps ( and ). Theorem 1: linear TD(1) and Widrow–Hoff produce the same per-sequence weight changes.
Theorem 2 shows that a bootstrapping method, which learns from its own earlier predictions, is not biased by them in the limit: in expectation it reaches the same predictions as supervised (Widrow–Hoff) learning. Theorem 3 says more: on a fixed data set, TD(0) converges to the predictions that would be exact if the maximum-likelihood model of the process were correct, which differs from the least-squares answer Widrow–Hoff converges to. Together they are the formal basis for preferring TD to Monte-Carlo targets in multi-step prediction.
The results are proved on paper, and not formalized in Lean. A formalization adds a precise model of the experience (i.i.d. sequences of an absorbing chain with terminal-dependent outcome laws), the integrability facts the paper leaves implicit, and a correct proof of the positive definiteness of , whose printed argument has a gap (see below). The matrix lemmas (Neumann series under ; real-part positivity of eigenvalues of for symmetric and positive definite in the non-symmetric sense; the step-size threshold) are reusable for other linear stochastic-approximation analyses.
The obvious argument writes as a linear function of and observes that the iteration matrix is a contraction for small . Two steps of this fail as printed. First, the paper proves that is positive definite through the Lemma of p. 27 with a weakened notion of diagonal dominance (weak in every row, strict in one), under which the Lemma is false; with the standard notion, is in general not strictly diagonally dominant (a row with that cannot leave in one step has row sum ). A correct proof combines weak dominance with reachability of every state from the support of , which is where enters. Second, is not symmetric, so a small does not make a contraction in the Euclidean norm; the argument goes through its eigenvalues, and turning eigenvalues of modulus below one into is a spectral-radius argument. The probabilistic step is also not free: is a polynomial in random sequences of unbounded length, and its integrability and the factorization need independence across sequences.
States are finite types N (nonempty) and T; the chain is the structure AbsorbingChain with blocks pN, pT and the field . Observation vectors are x : N → Fin K → ℝ with LinearIndependent ℝ x; is Matrix (Fin K) N ℝ. A sequence is an Episode (list of nonterminal states, terminal state, outcome); IsEpisodeStream states measurability, mutual independence (iIndepFun) and the law . Expectations are Bochner integrals, and the goal asserts integrability of , so a non-integrable junk value cannot satisfy it. is defined as an expectation (a sum over sequences), not as , so (7) is not circular. "Positive definite" is the paper's footnote 6 ( for real , no symmetry), not Mathlib's Matrix.PosDef.
Trivializations ruled out: the hypothesis is the paper's own discarding of never-visited states (without it the goal is false: an unvisited state's weight never moves); N is nonempty and sums to one, so the hypotheses are satisfiable and the goal is not vacuous; the sequences cannot be arbitrary random variables or a fixed sequence, since their law is pinned to , and ; is chosen before , and the probability space; and the update is per sequence, not the intra-sequence variant of §5.
Corrected slips: "For each nonterminal state " (p. 24) means terminal; the diagonal-dominance definition of p. 27 is replaced by the standard one; (p. 28) means . Not formalized: the variance and TD() conjectures of p. 29, §4.3, and the extension claims of §5.
Related open goals on this platform (different models, credited, not re-posed): SuttonBartoRL.BatchTD.batch_td_converges_to_certainty_equivalence (tabular, discounted analogue of Theorem 3), and SuttonBartoRL.LinearTD.keyMatrix_posDef, posDef_of_row_col_sums, expected_td_update (continuing discounted chain with stationary , where every row sum of is positive). Contributions of any milestone, of general matrix lemmas, and of reusable infrastructure for i.i.d. episode streams are welcome.
A postman, a snowplough or a street sweeper must traverse every street of a district and return to the depot. When some streets are one-way, the street network is a mixed graph: some edges are directed and must be traversed in a prescribed direction, the others are undirected and may be traversed either way. The first question about such a route is whether a closed route exists that traverses every street exactly once, an Euler tour of the mixed graph. When one exists, it is an optimal postman route; when none exists, the postman problem asks which streets to repeat.
J. Edmonds and E.L. Johnson treat this question in §6 of Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), the paper that solved the undirected Chinese postman problem by matching. Section 6 gives an algorithm that finds an Euler tour in any mixed graph that is connected, of even degree and symmetric, and §7 uses it for the mixed postman problem.
Timeline.
A mixed graph has a finite set of nodes and a finite set of edges. Each edge meets two distinct nodes; several edges may meet the same pair of nodes. Some edges are directed: an edge directed away from node toward node must be traversed from to . In Lean an edge has a tail, a head (distinct) and a Boolean directed; for an undirected edge the order of the two ends carries no meaning.
If is connected, even and symmetric, then for every node
The goal contains two classical theorems as special cases. With every edge undirected it is Euler's theorem for connected even multigraphs. With every edge directed it is the theorem that a connected balanced digraph is Eulerian. The milestones connect the two cases: an orientation reduces the mixed case to one the Rule can handle. The Rule itself is the van Aardenne-Ehrenfest–de Bruijn construction, which underlies the BEST theorem counting Euler tours. Milestone 5 decides whether the mixed postman problem has any feasible solution. The mixed postman problem is the standard model for routing on one-way street networks.
All results here are proved in the paper, so none is open. No Lean proof of any of them in this form is known. Mathlib's Eulerian walks are for simple graphs; it has no multigraph or mixed-graph Euler theorem, no directed Euler theorem and no arborescence-based traversal. The mission produces these, together with a reusable vocabulary of mixed multigraphs, walks that respect directions, and arborescences given by parent edges.
The obvious approach to the goal is to forget the directions and apply Euler's theorem. This fails because the tour it produces may traverse a directed edge backwards. Orienting all undirected edges at once also fails: an arbitrary orientation of the undirected edges need not keep every node balanced.
The difficult part of the Rule is showing that the greedy traversal does not get stuck before using every edge. It cannot stop at a node other than because of the degree conditions. The hard step is showing that no edge is left unused when it stops at . The answer depends on the ordering condition: without the arborescence edge last at every node, the Rule can return to with edges still unused. The assignment step needs an invariant: the orientation must keep every node symmetric while it extends a spanning structure of directed edges.
Fintype V, Fintype E). Parallel edges are allowed, including a directed and an undirected edge on the same pair. Loops are excluded (tail e ≠ head e), following the paper's standing setting of §2 (p. 91: edges meet two different nodes). Edges are a type, not a relation on nodes, so parallel edges stay distinct in every walk.Contributions are welcome at every level: proofs of the milestones, a direct proof of the goal, and general lemmas about mixed multigraph walks.
A matching in a graph is a set of edges no two of which share a vertex. Finding a matching of maximum cardinality is one of the basic problems of combinatorial optimization: it models pairing tasks (workers to shifts, kidney donors to recipients, players to rounds), it is a subroutine of algorithms for the travelling salesman and Chinese postman problems, and it was the first problem shown to need more than linear programming over the obvious constraints to be solved exactly.
For bipartite graphs, König's theorem (1931) gives a min–max formula: the maximum size of a matching equals the minimum size of a set of vertices meeting every edge. In general graphs this fails already for a triangle, where a single edge is a maximum matching but two vertices are needed to meet all three edges. Jack Edmonds' paper Paths, trees, and flowers (1965) gave both a polynomial-time algorithm for maximum matching in general graphs, the blossom algorithm, and, as a by-product of its analysis, the correct min–max theorem for general graphs.
Timeline.
A graph is a finite set of vertices and a finite set of edges, each edge meeting exactly two distinct vertices, its end-points. Several edges may join the same two vertices; this is needed because shrinking creates parallel edges. A matching is a set of edges no two of which meet the same vertex; a vertex is exposed if it meets no edge of . "Maximum" refers to cardinality.
An odd set is a set of vertices with an odd number of elements. Its capacity is
A one-vertex set covers the edges meeting its vertex; a set of vertices covers the edges with both end-points in it. An odd-set cover is a family of odd sets such that every edge is covered by some member, and its capacity-sum is .
The proof uses the following objects of §3–§4 of the paper. An alternating path is a simple path whose edges alternate between and the non-matching edges . An alternating tree is a tree whose vertices are split into inner and outer vertices, every edge joining an inner to an outer vertex and every inner vertex meeting exactly two tree edges; it is planted if restricted to the tree is a maximum matching of the tree whose one exposed vertex (the root) is exposed in , and Hungarian if its outer vertices are adjacent only to its inner vertices. A blossom is an odd circuit on which is a maximum matching, leaving one vertex exposed; with a stem (an alternating path from an exposed vertex ending in a matching edge at ) it forms a flower. Shrinking a vertex set replaces it by a single vertex , deletes the edges inside and keeps all other edges; and denote the result for a blossom .
It is stated as: there are a maximum matching and a minimum odd-set cover with .
The matching-duality theorem gives a certificate of optimality: a matching and an odd-set cover of equal size prove each other optimal, and the blossom algorithm produces both. It is equivalent to the Tutte–Berge formula , it contains König's theorem as the case where all members of the cover are singletons, and it is the cardinality case of Edmonds' description of the matching polytope by odd-set constraints, which underlies weighted matching, -matching and the polyhedral approach to combinatorial optimization.
The theorem has been proved since 1965, with several independent proofs (via Tutte's theorem, via the Gallai–Edmonds decomposition, via linear programming). Mathlib contains Tutte's perfect-matching theorem for simple graphs, but neither the Tutte–Berge formula nor odd-set covers, alternating trees, blossom shrinking or Berge's augmenting-path theorem in a multigraph setting. This mission produces a machine-checked version of Edmonds' statement together with the lemmas of his algorithmic proof (4.12, 4.14, 4.15, 4.17), which are the correctness core of the blossom algorithm.
Weak duality and Berge's theorem are elementary. The difficulty is the strong direction. The obvious argument, a search for augmenting paths from an exposed vertex, fails because an alternating search tree in a non-bipartite graph can close an odd circuit, after which a vertex is reachable both by an even and by an odd alternating path; a naive search either misses augmenting paths or must back-track exponentially. The proof therefore has to work in shrunken graphs, whose vertices are nested sets of original vertices, and transfer maximality and covers back through every shrinking (4.12–4.15). Keeping track of nested blossoms, of the identity of edges under shrinking and of the parity bookkeeping of 5.8 is the main formal burden.
EdmondsMatching65.Polyhedron.Graph V E (a map from edges to unordered pairs of distinct vertices) with finite V, E; parallel edges are allowed and loops are not. Matchings are Finset E. Maximum and minimum are by cardinality, stated with explicit comparisons rather than sSup/sInf.Finset (Finset V); repeating a member only adds capacity, so this does not change the minimum. The capacity of a singleton is , not .Reusable beyond this mission: the multigraph shrinking construction, blossom sets, alternating and Hungarian trees, and Berge's theorem in the multigraph setting; these are shared with the companion mission on the invariance of the dual (Gallai–Edmonds). Proofs of any milestone, and alternative proofs of the goal (e.g. through Mathlib's Tutte theorem), are welcome.
Stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto in 1991, is the standard method for multistage stochastic linear programs with many stages, such as hydro-thermal scheduling and long-term energy planning. It approximates each stage's expected future cost from below by the maximum of finitely many linear functions (cuts), built from LP dual solutions at sampled states, and alternates a forward simulation pass with a backward cut-generation pass. Practitioners stop the method when a simulated upper bound is close to the lower bound . Whether this procedure converges at all is the question of this mission.
Timeline:
There are stages. Stage has a decision in , costs , a matrix and, for , a matrix coupling to the next stage. At stage the constraint is . For the right-hand side is random: , where takes values with probabilities , independently across stages. The expected cost-to-go is defined backwards from :
and is the problem [LP1]. Assumption (A4) says every stage problem met along the way has a nonempty, bounded feasible region.
The approximate problem [AP] replaces by over the cuts generated before iteration ; its value is . A scenario fixes one outcome per stage . Each DOASA iteration (i) samples one forward scenario and solves [AP] along it, giving states ; (ii) for runs the Cut Calculation Algorithm (CCA): it solves [AP] at for the outcomes in a backward sample , stores optimal extreme-point dual solutions in a collection , picks for every outcome the best stored dual, and averages them into a new cut on . DOASA-N instead traverses a fixed list of scenarios in every iteration.
If, with probability 1, every scenario prefix is followed by the forward pass jointly with each outcome being in the backward sample infinitely often (property J), then with probability 1 every DOASA run has an iteration after which the cuts no longer change, the policy they induce is optimal for [LP1], and
The theorem justifies SDDP, AND, ReSa and CUPPS as exact methods: on a finite scenario tree, sampling-based cutting-plane schemes reach an optimal policy and a tight lower bound after finitely many iterations, almost surely. The finiteness argument (Lemma 1) is the template for later finite-convergence proofs of SDDP variants.
The paper's proofs are informal. No part of this development is machine-checked, and the printed statement of Theorem 4 is false (see below), so a formal proof also settles exactly which sampling hypothesis is enough. The finite-cut lemma and the cut-validity milestone are reusable for any Benders-type multistage method.
The obvious argument goes: cut sets stabilize (Lemma 1), and every scenario and every outcome is sampled infinitely often, so the limiting cuts must be exact. The last step fails. A cut at a state is exact only if, for every outcome, a dual that is optimal at that state has been collected. Sampling the forward scenario and the backward outcomes infinitely often, but separately, does not ensure this. Lemma 1 itself is also delicate: the dual vectors grow in dimension with , so the collection of extreme-point duals can be infinite even though the cut coefficients take finitely many values. The algorithm's choices (extreme-point duals, ties among best duals) must be handled for every run, not for a convenient one.
Stages are numbered with variable dimensions per stage. B t is the paper's , the matrix multiplying in stage . Value functions are real infima, used only on reachable states. Iterations are numbered from in Lean. Explicit choices, each recorded in the item statements:
A trivializing encoding, in which cuts are arbitrary valid hyperplanes, duals are taken for all outcomes, or the sampling hypotheses directly assume exactness of the cuts, is ruled out: the run relation transcribes CCA steps 1–3 as printed.
A complete development needs LP weak and strong duality (published on the platform as LinearOptimization.lp_weak_duality and LinearOptimization.lp_strong_duality, in their own encoding), finiteness of the set of extreme points of a polyhedron, and the almost-sure intersection of finitely many events (Mathlib). Contributions to any milestone, to the proof that J holds for independent sampling, and to the counterexample showing FPSP and BPSP are insufficient are welcome.
The number of successes in many rare trials is approximately Poisson. For independent trials the quality of that approximation was quantified by Le Cam in 1960: if are independent Bernoulli variables with , and , the total variation distance between the law of and the Poisson law with mean is bounded by a constant multiple of , and by a constant multiple of when . Many applications have dependent trials: occurrences of a pattern in a sequence, exceedances of a high level by a stationary process, failures in a system with local interactions. L. H. Y. Chen's 1975 paper extended Charles Stein's method of normal approximation to the Poisson case and obtained explicit bounds for dependent trials. The approach became known as the Stein–Chen method, and is now the standard tool for Poisson approximation of dependent counts.
Timeline.
This mission formalizes the order- bound of that paper, Theorem 4.2.
Let be a probability space and let be Bernoulli trials: random variables with values in and . Following the paper, set for and . Put
For a bounded real function on the nonnegative integers, the Poisson expectation is
the mean of under the Poisson law with parameter . The quantity of interest is for all with . Its supremum over such is twice the total variation distance between the law of and the Poisson law.
Dependence is measured by Ibragimov's mixing condition (4.1). Let . There must be a non-increasing sequence such that for all and every event ,
A sequence is -dependent when and are independent for all . It then satisfies (4.1) with for .
The proof works with the partial sums , , and . It also uses the Stein solution , the solution for of .
For every and every with ,
The bound involves only the law of through , the success probabilities, the window and the mixing rate. The window is free, so the statement covers every trade-off between local dependence and mixing.
The milestones follow the paper's proof:
Theorem 4.2 gives an error of order times the excess variance , plus a mixing remainder. When the trials are nearly uncorrelated, and the bound is small even though is large. This is the regime where the companion Theorem 4.1, which carries a factor , is weaker. The independent case recovers Le Cam's order with constant 10. The -dependent case gives explicit Poisson limit theorems for scan statistics and pattern counts.
All results of the paper are proved there, and the proofs are elementary apart from the measure theory of Lemma 4.1. To our knowledge none of them has a machine-checked proof. Mathlib has the Poisson distribution and conditional expectation, but no Stein–Chen bound and no mixing inequality of Ibragimov's type. A formal proof would give the first checked quantitative Poisson approximation for dependent trials. It would also give reusable covariance inequalities for -mixing sequences (Lemmas 4.2 and 4.3).
Most of the work is bookkeeping, and it is heavy. Identity (2.2) needs a telescoping over windows whose ends can fall outside . (4.15)–(4.18) need to be compared with with explicit constants.
The genuinely probabilistic step is the decoupling of Lemma 4.2. Condition (4.1) controls conditional probabilities of events. Lemma 4.2 needs a bound on conditional expectations of functions of a whole random vector. Passing from one to the other requires a regular conditional distribution that is uniformly close to the unconditional law on a set of full measure (Lemma 4.1). The naive route, applying (4.1) to each level set of a simple function, loses a factor that grows with the number of levels and does not give the constant .
The bound (4.16) applies Lemma 4.4 to a subsequence of the trials. This uses the fact that dropping variables preserves (4.1) with the same , because is non-increasing.
A trivializing formalization is ruled out. Measurability of the trials is part of the definition, because otherwise conditional expectations in (4.1) collapse to . The goal mentions only , , , , , and . It does not mention or any milestone quantity.
A complete development needs the Stein solution and its bounds, a Bernoulli-sum calculus over integer
windows, regular conditional distributions on standard Borel spaces, and the mixing covariance
inequalities. The last two are reusable beyond this mission. Contributions to any milestone are
welcome, as are alternative proofs of Lemma 4.2 through Mathlib's condDistrib.
Sampling uniformly from a bounded region can be difficult when direct transformation of a familiar random variable is unavailable and rejection sampling spends most of its trials outside the region. Robert L. Smith studied procedures that move within the region: from the current point, choose a direction, form the line set through that point inside the region, and choose the next point uniformly on that line set. The resulting sequence is a homogeneous Markov chain. The Random Directions Algorithm, later commonly called hit-and-run, is a central instance of this construction. Smith's 1984 paper establishes conditions under which the chain approaches the uniform distribution even when its initial point is fixed rather than sampled uniformly (Smith 1984, pp. 1298–1301).
For simulation, the initial point is usually chosen because it is known to be feasible. The question is therefore whether the distribution after many moves forgets that particular choice. A stationary distribution alone does not answer this: stationarity describes what happens if the chain already starts with that distribution. Smith's Theorem 2 gives the stronger, pointwise starting-state statement for the class of symmetric mixing algorithms satisfying his two regularity assumptions (Smith 1984, p. 1301).
Let be the state region and its finite, nonzero content measure. In Smith's geometric setting, is a bounded -dimensional measurable region in , and is -dimensional content; at , content is counting measure. A Markov transition kernel assigns to every current point a probability of entering a measurable set on the next move. For the associated chain , the -step transition probability is .
The uniform law is . Smith's Assumption (a) gives a measurable transition density relative to :
For a symmetric mixing algorithm, the paper states that this density satisfies for all . Assumption (b) says for all such pairs. These are pointwise conditions, including states of zero -measure. A nonempty measurable set is closed if for every . The chain is indecomposable in the paper's sense when it has no two disjoint closed sets (Smith 1984, pp. 1299–1300).
Lemma 1 asserts that is stationary: for every measurable . Lemma 2 excludes two disjoint closed sets. Both are direct prerequisites of the goal. Smith's Theorem 1 also establishes uniqueness of the stationary distribution and almost-sure convergence of empirical visit frequencies under a stationary start; it is described in the source, but its trajectory-level formalization is outside this proposal (Smith 1984, p. 1300).
The mission goal is Smith's Theorem 2. For every and every measurable ,
This is the paper's explicit meaning of strongly mixing. The milestone list also records the proof's stated nonperiodicity condition: for every , the -step transition law has no two disjoint closed sets. It is a target in its own right because it concerns all higher-step kernels, not only the one-step chain (Smith 1984, p. 1301).
Theorem 2 makes the uniform law the limiting distribution of the sample at time , for any fixed feasible initial point. The paper's Theorem 1 supplies a different guarantee about long-run empirical frequencies under a stationary start, although it is not a target of this proposal. Smith later specializes the framework to the Random Directions Algorithm and gives a quantitative rate under additional geometric conditions; that rate is the subject of the companion mission (Smith 1984, pp. 1303–1304).
These results are proved in the paper but the declarations in this proposal are theorem statements with sorry, not machine-checked proofs. A completed formalization would turn the paper's measure-theoretic claims into reusable statements about general measurable state spaces and kernels. The normalized content law, the density interface, and closed-set predicate can be reused when studying other Monte Carlo kernels with the same hypotheses.
The main obstacle is the jump from stationary behavior to convergence from every starting point. Symmetry identifies the candidate stationary law, and strict positivity limits how the chain can split into closed parts, but neither sentence by itself establishes the claimed limit of . The distinction matters especially at starting points in -null sets: an almost-everywhere starting-state result would leave out precisely the universal claim in Theorem 2. The paper appeals to a general-state Markov-chain convergence result for this step (Smith 1984, p. 1301).
Lean uses a measurable type as the whole region , a finite measure with , a Markov kernel , and an extended-nonnegative density . The density is jointly measurable and is linked to by the integral identity above; symmetry is pointwise, and positivity is added only for Lemma 2 and Theorems 1–2. This abstract representation retains the hypotheses those results use without fixing a particular Euclidean dimension. It covers the counting-content case as well as continuous content, although it does not construct the geometric direction-and-chord algorithm. The Random Directions kernel belongs to the companion mission.
The uniform law is normalized by . Finiteness and nonzero total content prevent a meaningless inverse or an empty probability space. The -step law is the published MarkovChainCLT.iterKernel. Theorem 2 quantifies over every , rather than -almost every , and uses setwise convergence on each measurable . No invariance, uniqueness, minorization, or convergence premise is added to the goal. Detaching from would empty out the substantive assertion. Formal contributions can target the density-to-invariance argument, the closed-set conditions, and the general-state convergence theorem needed for the goal. The paper's separate pathwise Theorem 1 remains an appropriate later extension.
Convex minimization often has a simple objective but no useful closed form for its minimizer. A proximal method replaces one difficult minimization by a sequence of regularized minimizations. The familiar quadratic regularizer treats all directions through a Euclidean norm. In applications with nonnegative variables, entropy-like geometry can be more natural: a step can be penalized by a Bregman distance generated by a strictly convex function. Chen and Teboulle studied a proximal minimization algorithm with this geometry and established a rate in objective values together with convergence of the iterates under the paper's assumptions. Their analysis also removed a bounded-below assumption used in an earlier treatment and allowed step sizes whose sum diverges even if individual steps approach zero (Chen and Teboulle, 1993, pp. 539–540).
This mission records the complete theorem of that paper, rather than only its rate when a minimizer is known to exist. The distinction matters because a proper convex objective can have an infimum of or a finite infimum that it never attains. The rate against each comparison point remains meaningful in those cases, and the theorem's value convergence does not presuppose a minimizer.
Let be a finite-dimensional real normed space, the nonempty effective domain of a proper lower semicontinuous convex objective, and its finite restriction. Its value outside is . Thus is an extended-real number that may equal , and is the set of minimizers, possibly empty.
A Bregman function with zone is a function on the closure of an open set . It is continuously differentiable on , strictly convex and continuous on , and satisfies the bounded partial-level-set and two sequential conditions of Definition 2.1 (Chen and Teboulle, 1993, p. 539). Its distance-like expression is
It is nonnegative and zero exactly when , but need not be symmetric or satisfy a triangle inequality. The zone contains the relative interior of . Starting from and positive steps , a PMD run selects minimizing over , for . Write . The paper calls this proximal minimization with D-functions (Chen and Teboulle, 1993, pp. 539–540).
For every and every finite comparison point , the goal includes
If , then in the extended reals, including when . This is Theorem 3.4's inequality (20) and its ensuing value-convergence claim (Chen and Teboulle, 1993, p. 542).
For every , the same rate gives
When and , the entire sequence converges to a point of . The displayed bound is (21), and convergence of the iterates is the final clause of Theorem 3.4. The milestone list follows the authors' statements: the three-point identity, nonnegativity of the distance, Lemma 3.2, and the three parts of Lemma 3.3. Display (17) is an additional supporting theorem item (Chen and Teboulle, 1993, pp. 539–542).
The rate compares a PMD iterate with any admissible point, so it gives a finite-horizon certificate even before an optimal point is identified. If a minimizer exists, substituting it gives an explicit objective-gap bound. With divergent cumulative steps, the theorem identifies the limiting objective value without assuming that value is finite. Its final clause goes further: when the optimum is attained, the points themselves converge, not merely their objective values (Chen and Teboulle, 1993, p. 542).
The mathematical result was proved in 1993. The formalization task is to state and prove it in Lean with the extended objective, full Bregman-function conditions, and sequence limits visible to later developments. The three-point identity is already posed as a separate public platform theorem from a later mirror-descent treatment; this mission reuses that statement. The remaining statements here are proof obligations, not claims of completed machine-checked proofs. Their definition layer can also support analyses of other nonquadratic proximal algorithms.
The direct one-step minimization comparison alone does not yield the global estimate with and the exact weighted distance terms of Lemma 3.3(iii). It also does not settle convergence of the points: decreasing objective values can coexist with several cluster points. The Bregman function's bounded partial level sets and sequential conditions are needed to rule out that behavior. A further issue appears when : replacing the infimum by a real number, or assuming a minimizer to define it, removes a case that Theorem 3.4 explicitly covers. The original paper separates these issues across Lemmas 3.2–3.3 and Theorem 3.4 (Chen and Teboulle, 1993, pp. 540–542).
Lean uses a finite-dimensional real normed space in place of ; none of the statements depends on a chosen Euclidean inner product. A derivative is a continuous linear functional, and its value on a vector represents the paper's gradient pairing. The Bregman distance is the already-published definition with the derivative at its second argument. The paper's is represented by a total function whose values outside are unused. Strict convexity on includes convexity of . The last sequential condition explicitly requires its first arguments to lie in , the domain where the paper defines .
The extended objective is a nonempty convex domain , a real-valued restriction , and an extended-real function equal to off . Lower semicontinuity applies to that extended function. The infimum is taken in the extended reals; it cannot silently become zero when the values are unbounded below. A PMD run is a predicate on an existing sequence, recording a minimizer in at each step. This makes explicit the existence consequence for which the paper assumes the gradient of has full range; it does not define iterates by a choice operator. Every Bregman distance differentiates at a point of , where is . The rate starts at , so and no finite value is demanded of . No lower bound on is imposed. Contributions proving the milestone inequalities, the extended-real value limit, the Bregman-function examples, and the compactness step for iterate convergence are within scope.
The number of successes in many rare, roughly independent trials is approximately Poisson. This law of small numbers is used for counts of rare events in reliability, insurance, epidemiology, queueing and random combinatorics. A quantitative version says how large the error is. For independent Bernoulli trials with success probabilities and , Le Cam (1960) showed that the error in total variation is of order . When all are small this tends to zero, but it does not say what the leading part of the error is.
L. H. Y. Chen's 1975 paper (Ann. Probab. 3, 534–545) adapted Charles Stein's method for normal approximation to the Poisson case. The result is now called the Stein–Chen method. The paper's §2–§4 give first-order error bounds for dependent (mixing) trials. Its §5, "A refinement", goes one order further for independent trials. It identifies the first-order correction explicitly and shows that what remains is of order . Kerstan (1964) had obtained a similar expansion by a different method. Chen's version comes from iterating the basic identity of the Stein–Chen method. This mission formalizes §5.
Timeline:
Let be independent random variables on a probability space, each taking only the values and , with success probabilities . Put
For a bounded real function on the nonnegative integers, the Poisson expectation is
the mean of under the Poisson law with parameter . The Stein equation is . For its solution is
Write and . Chen's second-order operator is
For another parameter , and apply the Stein solution and the operator with parameter to the function .
In Lean: poissonExp, stein, delta, shiftL, stU, prob, lam, lamExcept, W, Wi, all in the namespace PoissonDepTrials.SecondOrder.
If are independent, and , then for every with ,
The paper writes the constant as "an absolute constant not greater than ". The formal goal fixes at that value, which is the same statement.
In order: the Stein solution (2.3)/(2.5); the difference identity (3.6); Lemmas 3.1, 3.2, 3.3 and 3.5 (bounds on and ); the first-order identity (5.8) ; Lemmas 5.1 and 5.2 (dependence of Poisson expectations on the parameter); Lemmas 5.3–5.5 (bounds on , and ); the bound (5.9),
and the closing inequality .
The theorem gives an explicit first correction to the Poisson approximation of a Poisson-binomial law, with a remainder of the next order. When all equal , the first-order error is replaced by the remainder , which is smaller by the factor . The correction term is a functional of the Poisson law alone, . It can be evaluated without knowing the distribution of . The method of proof applies the basic identity twice. The paper notes that further iteration gives expansions to any order.
On the formal side, Mathlib has the Poisson distribution but no Stein–Chen machinery and no quantitative Poisson approximation. The theorem has, as far as is known, no machine-checked proof. This mission produces the Stein solution and its standard bounds (Lemmas 3.1–3.5), which are reusable by any Stein–Chen argument. It also produces the parameter-perturbation estimates of Lemmas 5.1–5.2 and a complete second-order expansion. Missions 1 and 2 of this series formalize the first-order bounds of §4 under a mixing condition. They share the Stein-solution layer.
The first-order bound needs only that is uniformly small (Lemma 3.4). A second-order bound needs more. After the first application of the identity, the error has to be expanded again. That requires control of the iterated operator with a different parameter , because is approximately Poisson with mean , not . The bound on (Lemma 5.5) grows linearly in . Applying the uniform bounds of §3 throughout loses a factor and produces an error of order instead of . The linear growth has to be paired with the variance of . The averaging over pairs in the final step uses the condition , which keeps every comparable to .
Conventions committed to in Lean:
X : ℕ → Ω → ℕ. Each is measurable with values in almost surely. for and , which is the paper's own padding convention (p. 535). Independence is iIndepFun (fun i => X i) P over all of ℕ. Because the padding variables are constants, this is equivalent to independence of .Hypotheses added relative to the page, each disclosed in the item's Formalization Note:
The random indices that the paper introduces to shorten notation in (5.8)–(5.9) are not formalized. The same quantities are written as finite sums over indices.
Ruled out: the second-order term must be the operator built from the Stein solution exactly as on p. 543. A free function, or evaluated at the junk value , would empty the theorem.
Welcome contributions include:
Finite-horizon Markov decision processes ask which decisions minimize accumulated cost over a specified number of stages. In a stationary process, the same costs and transitions apply at every stage. This compact input can describe a horizon much larger than the state set, so a method that processes all stages one by one may take time exponential in the length of the written horizon. Papadimitriou and Tsitsiklis identified this issue while comparing sequential and parallel algorithms for decision processes. For the deterministic stationary case, their Theorem 5 states an NC classification, supported by a finite structural description of a cheapest long walk. Papadimitriou and Tsitsiklis (1987)
The structural description is the subject of this mission. It connects a policy optimization problem to bounded-length graph objects and an exact cost identity. This is useful independently of a particular model of parallel computation: it says which shorter walk and cycle costs determine the answer even when the horizon is very large. Papadimitriou and Tsitsiklis (1987), p. 447
Let be a finite nonempty set of states, with , and fix an initial state . At each state , a finite nonempty set contains the available decisions. A decision has a certain successor state and a real cost . The model is stationary: these data do not depend on time. The corresponding directed graph has one arc for each decision. It may have loops and parallel arcs, because distinct decisions can share endpoints. This is the deterministic graph translation made in §3 of the paper. Papadimitriou and Tsitsiklis (1987), pp. 444–445
A policy is a function of both state and time. Starting at , it produces . In the convention of the paragraph before Theorem 5, horizon means decisions and therefore a walk with arcs. Its cost is
A walk records the states and the decision arc used at each step; states may repeat. A simple path has no repeated state. A simple cycle has positive length, returns to its starting state, and has no other repeated state. A closed walk may repeat states internally and need not be a simple cycle. The distinction matters because the structural claim uses a simple cycle, whereas the computation in the target identity uses a cheapest closed walk of a chosen length.
The first milestone identifies with the minimum cost of a -arc walk from . The next milestones record a decomposition into a simple path and simple cycles, the restriction on cycles repeated more than times, and the existence of a cheapest walk with a short prefix and one repeated simple cycle. These are claims in the paragraph preceding Theorem 5, with corrections to the printed exchange and its connectivity justification documented in the formal statements. Papadimitriou and Tsitsiklis (1987), p. 447
For and , let be the cheapest -arc walk from that visits . Let be the cheapest closed -arc walk at . Only choices for which these walks exist are included. The mission's goal is
The bound is the paper's finite compression claim. The divisibility condition makes an integer number of cycle copies. The goal states an exact value, with the inner minima taken over genuine walks and the outer optimum still taken over all policies. Papadimitriou and Tsitsiklis (1987), p. 447
The identity replaces an optimization over arbitrarily many time-dependent policy decisions with costs of walks having fewer than arcs and closed walks of at most arcs. It gives the mathematical statement that must hold before the paper's proposed parallel calculation can be trusted. It also applies when several different decisions have the same endpoints, because each decision remains a separate weighted arc. Papadimitriou and Tsitsiklis (1987), pp. 445, 447
The paper proves the result informally and states the NC classification. The mission seeks machine-checked proofs of the graph and cost statements, including the printed argument's delicate boundary cases. The local proposal contains open Lean theorem statements, not proofs. Reusable outcomes include a decision-walk representation, a cycle decomposition that preserves the multiset of arcs, and finite-horizon policy-to-walk equivalence. A related published result, TropicalLA.exists_repeat, detects repetition for dense max-plus matrices; it does not state this weighted multigraph decomposition or the min-cost identity.
The obstacle is preserving both walk feasibility and the exact number of arcs when repeated cycles are rearranged. A cycle may be the only connection to other parts of a walk, so deleting its last copy can invalidate the remaining sequence. The printed exchange paragraph also reverses the cost-improving direction and appeals to a no-ties perturbation without carrying it through the bounded-prefix conclusion. Those issues affect the claimed bound; merely knowing that a long walk repeats a vertex does not establish the target identity. Papadimitriou and Tsitsiklis (1987), p. 447
Lean represents and each as finite types and uses real costs. The decision sets are nonempty, making policies and arbitrarily long walks available. Policies depend on state and time, as in §2. A walk stores its decisions as well as its states, so loops and parallel arcs are represented. Cycle decompositions preserve endpoints, length, cost, and the multiset of decision arcs. A loop is a simple cycle of length one. Time starts at zero, and an -arc walk has states at indices .
The paper's general finite-horizon definition sums costs from through , while the Theorem 5 paragraph explicitly asks for a -arc walk. This mission follows the latter convention: decisions occur at . The goal also imposes , which the printed loop leaves implicit, and uses a closed walk for because that is what the length- graph calculation computes. It does not assume distinct walk costs. The condition is retained from the paper even though related identities may hold in other ranges. Papadimitriou and Tsitsiklis (1987), pp. 444, 447
Theorem 5's NC membership, processor and parallel-time bounds, the membership-in-P discussion, log-space reductions, PSPACE membership, and Corollaries 1–2 are outside this mission. Mathlib does not supply the PRAM and complexity-class framework those claims require. The target is the exact cost identity behind the algorithm. Defining the optimum directly as the right-hand minimum, restricting policies to stationary policies, or allowing an empty policy class would trivialize or change it. Contributions proving the milestones, the goal, or reusable walk and cycle facts are welcome.
A sum of many rare events is approximately Poisson. For independent Bernoulli trials this is the classical law of small numbers, and its quantitative form goes back to Prohorov (1953) and Le Cam (1960): if are independent with , then the law of is close to the Poisson law with mean , with an error controlled by . Many applications need the same conclusion for dependent trials: runs and clusters in sequences, exceedances of a stationary time series, matches in DNA sequences, extremes of mixing processes.
Louis H. Y. Chen's 1975 paper adapted Charles Stein's method for normal approximation (1970, published 1972) to the Poisson case and obtained explicit error bounds for sums of dependent Bernoulli trials under mixing and -dependence. The technique, now called the Stein–Chen method, became the standard tool for Poisson approximation, through Arratia, Goldstein and Gordon (1989) and Barbour, Holst and Janson, Poisson Approximation (1992).
Timeline:
Let be a probability space and Bernoulli random variables, possibly dependent, with success probabilities . Put
For a real function on the nonnegative integers, the Poisson expectation of is
the mean of under the Poisson distribution with parameter . The quantity to be bounded is for all with ; its supremum over such is twice the total variation distance between the law of and the Poisson law.
Dependence is measured by Ibragimov's mixing condition. Write for the -algebra generated by and for that generated by . The sequence satisfies (4.1) with a nonincreasing sequence if, for all and every event ,
Thus bounds how much knowledge of the first trials can change the probability of an event determined by trials at distance at least . A sequence is -dependent if and are independent whenever ; then (4.1) holds with for , and independent trials are the case .
For every and every with ,
The parameter is free: it trades the local term against the mixing term .
The milestones follow the paper's proof:
The theorem bounds the distance to the Poisson law by quantities a user can compute or estimate: the variance of , the , and the mixing rate. When the trials are weakly dependent and individually rare, , is small, and the bound is small. It recovers Le Cam's independent-case bound up to the constant and extends it to -dependent and -mixing sequences. The expansion (2.6) and the bounds on the Stein solution in §3 are reused throughout the later literature on the Stein–Chen method.
The results of this paper are proved on paper; none of them is formalized in a proof assistant. Mathlib has the Poisson distribution, conditional expectation, independence and regular conditional distributions, but no Stein–Chen identity, no bounds on the Stein solution, and no covariance inequality for -mixing sequences. This mission produces all three, and the companion missions of this series (Theorem 4.2, an order- bound, and Theorem 5.1, a second-order refinement for independent trials) rely on the same objects.
The identities (2.2), (2.6) and (4.7) are finite manipulations, and the bounds of §3 on are elementary real analysis. The main difficulty is the transfer of the mixing condition from events to functions. Condition (4.1) bounds conditional probabilities of single events almost surely, with a null set that depends on the event. Lemma 4.2 needs a bound on for an arbitrary bounded function of a past vector and a future vector ; this requires a regular conditional distribution of given and one null set that works for all events at once (Lemma 4.1). That step uses that is a standard Borel space, and it fails for an argument that handles one event at a time. Lemma 4.3 then needs care with the independent copy and with the three-block decomposition.
All objects are defined in PoissonDepTrials.MixSqrt.Setting. The conventions are:
StandardBorelSpace.Added hypotheses: in the identity (2.6) and in Lemmas 3.3, 3.4 and (2.5), because divides by ; and in Lemmas 4.2 and 4.3, because (4.1) concerns lags of a sequence starting at . The goal has no hypothesis : at every trial vanishes almost surely and both sides are zero.
The goal does not mention , or ; it is stated only in terms of , , the , , , and . The mixing condition is required to hold with a nonincreasing tending to , so it cannot be satisfied vacuously.
Reusable infrastructure includes the Stein–Chen identity (2.2), the bounds on the Stein solution (Lemmas 3.3, 3.4), and the covariance inequalities for -mixing sequences (Lemmas 4.2, 4.3), which apply beyond Poisson approximation. Proofs of any milestone are welcome, as are proofs of the companion results from the goal.
Two parties who can cooperate for mutual benefit must still agree on how to share the benefit. In The Bargaining Problem (Econometrica, 1950) John Nash asked which agreement two rational bargainers of equal skill should reach. His answer is not a model of haggling: it is a list of conditions any reasonable rule should satisfy, together with a proof that exactly one point of the set of feasible agreements is compatible with them. That point maximizes the product of the two parties' utility gains. Known as the Nash bargaining solution, it is the reference point of cooperative bargaining theory. Economics, operations research and networking all use it: in supply contracts, in wage bargaining, and in fair bandwidth allocation, where maximizing a product of gains becomes maximizing a sum of logarithms (proportional fairness).
Timeline:
A bargaining problem is a pair . Here is the set of utility pairs the two players can reach by agreement, including lotteries over agreements. is the disagreement point, the utilities of no cooperation. As in the platform goal, is compact and convex, and some has and (both individuals could gain). Write for the set of such pairs.
A bargaining solution is a map from to . Nash requires:
The paper has no separate INV axiom. It normalizes the disagreement utility to and notes that each utility is then determined only up to a positive multiple (p. 158), so the solution must not depend on that choice.
The goal is the platform theorem NashBargaining.nash_bargaining_solution_unique, posed by
Nickrobbins95 and currently Open. This mission references it and does not restate it. It
asserts that there is a solution such that a solution satisfies selection, INV, SYM, IIA and
PAR if and only if , and that for every
Nash's paper proves the necessity half: a solution satisfying the conditions must select the maximizer of the Nash product. The sufficiency half, that the maximizer map satisfies the five conditions, is not argued in the paper. It must be supplied by whoever closes the goal.
Two further items formalize the paper's examples: the Bill–Jack barter, whose solution is the vertex reached by exactly one exchange, and trade with money, where the solution gives equal money profits.
The Nash product characterization is used, mostly without proof, wherever a "fair" split of a cooperative surplus is needed. Examples are generalized Nash bargaining in supply-chain contracting and labour economics, the proportional-fairness criterion in network rate control, and the Nash-in-Nash models of bilateral negotiations. Many papers that build on it apply it to a specific feasible set. They therefore rely on the necessity direction, which is the step that makes the maximizer the unique answer rather than one answer among several.
The result has been proved since 1950, while the referenced Prove2Me goal remains Open. This mission supplies the milestones of Nash's own argument in the encoding of that goal, so that the necessity direction can be assembled from them. Sufficiency remains as separate work. The two examples are small, concrete checks of the solution concept.
Each step is elementary. The difficulty is in keeping the bookkeeping honest across the normalizations. The axioms are stated on the class , and a solution is a function on a subtype. Every application of INV, SYM or IIA therefore needs a membership proof for a transformed set: the image of under an affine map, or the enclosing square. It also needs the disagreement point to be carried along. The tempting short cut is to argue "without loss of generality and ". That is exactly what INV licenses, but only after compactness, convexity, the point where both gain, and the location of inside the square have been re-established for each transformed problem. Uniqueness of the maximizer also needs care at the boundary of the quadrant, where the product vanishes.
Utility pairs are ℝ × ℝ, with u.1 player 1's utility and u.2 player 2's. Milestones 1–5 work
at , the paper's normalization. Milestone 6 has a general and the goal's encoding.
Milestones 1–5 make the following readings explicit:
Milestone 6's five hypotheses are copied verbatim from the goal, and its conclusion is the goal's last conjunct for the given . It does not restate the goal: it has no existence claim and no "if and only if".
Trivializing formalizations are ruled out. The point where both gain is a hypothesis wherever uniqueness is claimed; without it a segment on an axis has many maximizers of . The square is a concrete set, not "some symmetric compact convex set", and the solution's properties are quantified over the goal's class , which is nonempty.
The examples need finite sums, convex hulls of finite sets, and extreme points, all in Mathlib. Contributions are welcome on each milestone and on the sufficiency half of the goal.
Related platform work treats other bargaining models. These are Rubinstein's alternating-offers
game (RubinsteinBargaining.PEP) and the Chatterjee–Samuelson sealed-offer double auction
(ChatterjeeSamuelson). Neither is used here. The von Neumann–Morgenstern utility theorem behind
the normalization is formalized as TheoryOfGames.Utility.utility_existence_uniqueness.
An online matching algorithm must commit to each assignment when a request arrives, before it sees later requests. This limitation arises whenever waiting for the full instance is impossible: an available resource can be assigned to a current request or saved for an unknown future request. The quality of the assignment is measured by how many requests can be matched. The central question is how much the lack of future information costs, even when an algorithm uses randomness. Karp, U. Vazirani, and V. Vazirani studied this question for bipartite graphs and proved an asymptotic ceiling of for the expected fraction matched by any randomized online rule on graphs with a perfect matching (Karp, Vazirani, and Vazirani, 1990).
The paper also analyzes RANKING and gives a matching asymptotic guarantee from below. This mission concerns the separate upper-bound result: the existence of hard instances for every algorithm. The upper bound matters independently of any particular proposed rule. It says that improving an algorithm's decisions cannot remove the worst-case loss due to decisions made before all columns are revealed. Its quantifiers make the adversarial model precise: the graph is selected with knowledge of the algorithm, before that algorithm's random choices are made.
There are boys, represented by rows, and girls, represented by columns. A bipartite graph records which boy and girl pairs may be matched. The graph is assumed to contain a perfect matching: some bijection between the two sides uses only edges of . This assumption supplies an offline benchmark of matches. Without it, a graph with no edges would make every upper bound on matching size empty of content.
Girls arrive one at a time. On arrival, the algorithm learns the edges incident to that girl, chooses an as-yet-unmatched adjacent boy, or declines to match her. A choice cannot later be changed. The paper labels columns so that they arrive in the order . A deterministic algorithm can base its action on the neighborhoods revealed so far. A randomized algorithm can additionally use internal random choices. Its performance is the minimum, over a graph with a perfect matching and a preselected arrival order, of its expected number of matches; the expectation is over its own randomness (Karp, Vazirani, and Vazirani, 1990, p. 352).
The paper's hard family begins with the complete upper-triangular graph , where row is adjacent to column exactly when . Its columns arrive from largest to smallest. Relabeling the rows by a permutation gives an instance that still contains a perfect matching. The algorithm RANDOM takes an eligible boy uniformly whenever at least one is available. Write for RANDOM's expected number of matches on , beginning with no matched rows (Karp, Vazirani, and Vazirani, 1990, p. 357).
For every , there is one threshold such that, for every and every randomized online algorithm on rows and columns, a graph with a perfect matching satisfies
The threshold is uniform over algorithms. The graph may depend on . This is the quantified upper-bound reading of Theorem 2's (Karp, Vazirani, and Vazirani, 1990, Theorem 2).
Lemma 13 identifies the average size produced by any deterministic greedy algorithm on a uniformly permuted with RANDOM's expected size on . Lemma 14 bounds the worst-case performance of every randomized algorithm, including non-greedy algorithms, by that value. Lemma 16 identifies the value itself by the two-sided limit
Together these statements give the finite-instance comparison and the asymptotic value named in the goal (Karp, Vazirani, and Vazirani, 1990, Lemmas 13, 14, 16).
Theorem 2 limits what any randomized online matching rule can guarantee under the paper's oblivious-adversary performance measure. Since the hard graph always admits a perfect matching, the gap from is caused by the order of information and the required irrevocable decisions. The statement applies to the entire algorithm class, rather than comparing two selected procedures. It therefore provides the ceiling against which the paper's lower guarantee for RANKING is measured.
Formalizing the result requires a reusable description of finite online algorithms, their visible histories, and expected matching size. It also requires a definition of uniform random choice from currently eligible rows with an explicit empty-choice case. The 1990 result is proved in the paper; the statements in this mission are targets for machine-checked proofs, not claims of an existing formal proof. The model can support later statements about other matching rules and hard-input distributions without changing the meaning of an online decision.
For a fixed graph, an algorithm can be designed around the graph's particular perfect matching, so one hard graph cannot simply be announced in advance for all deterministic algorithms. The theorem instead has to bound each randomized algorithm against a graph selected for that algorithm. Even then, checking the triangular graph against one rule does not establish a universal bound: different rules can respond differently to the same revealed neighborhoods. The crucial mathematical obstacle is a comparison across all such rules while preserving the restriction that future columns remain unseen. A further asymptotic step is needed to determine RANDOM's value on the triangular family, including both sides of the claim in Lemma 16.
Both sides are Fin n. An edge set is a subset of row-column pairs. The published perfect-matching predicate is reused: it asks for a bijection whose every selected pair is an edge. The paper's one-based column order is represented by zero-based order ; arrival number zero is the largest column. A deterministic rule receives only the neighborhoods of columns that have arrived, including the current column. A randomized rule is a probability mass function on the finite set of deterministic rules, allowing arbitrary correlations among its choices. The expected size is a finite sum over that mass function.
RANDOM is represented by the conditional-expectation recursion for uniform choice among eligible rows. If none is eligible, the column remains unmatched and there is no division by zero. For , the matching and RANDOM value are zero; the main theorem is eventual in and Lemma 16's value at zero does not affect the limit. Lemma 16 uses a two-sided limit. The paper's in Theorem 2 is stated as with before the algorithm, so the error is uniform across algorithms. A hard graph must contain a perfect matching; dropping this condition would let the empty graph satisfy the inequality trivially.
Useful contributions include finite probabilistic averaging, the greedy comparison, analysis of the recursive RANDOM value, and a proof joining Lemmas 14 and 16 into the uniform goal. The history and matching-run definitions are reusable for other finite online bipartite matching statements. The two numbered claims inside the paper's proof of Lemma 13 and its later remarks are outside the mission's curated milestone list.