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?
A lattice in is the set of integer combinations of linearly independent vectors. Many problems in algorithmic number theory, cryptography and integer programming reduce to finding a short nonzero vector of a lattice, or a few short independent ones. Finding the shortest vector exactly is hard, but in 1982 A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász introduced a notion of reduced basis that can be computed in polynomial time and whose vectors are provably short up to a factor depending only on the dimension (Lenstra, Lenstra, Lovász 1982). Their paper used it to factor polynomials in in polynomial time; the same reduction (now called LLL) became a standard tool for simultaneous Diophantine approximation (the paper's own (1.39)), for H. W. Lenstra's integer programming algorithm in fixed dimension (Lenstra 1983), and for cryptanalysis of knapsack and RSA variants.
What makes a reduced basis useful is a set of explicit inequalities proved in Section 1 of the paper, before any algorithm appears. They compare the lengths of the basis vectors with the lattice determinant and with arbitrary lattice vectors, with constants such as and . This mission formalizes those inequalities.
Let and let and be the ordinary inner product and Euclidean length on . Vectors form a basis for a lattice when they are linearly independent over and . The determinant of is
the written as columns (1.1). The Gram–Schmidt vectors and coefficients () are defined inductively by
the are pairwise orthogonal and not normalised. The basis is reduced if
and
The first condition is a size condition on the coefficients; the second (the Lovász condition) says that swapping and would not shrink the -th Gram–Schmidt length by more than the factor (pp. 516–517).
Let be a reduced basis for and let be linearly independent. Then
The statement quantifies over every reduced basis and every independent family of lattice vectors. Its case is Proposition (1.11).
In the order of the paper's proofs (pp. 517–518):
The rest of Proposition (1.6) and the remark after it: (proof of (1.6)); (1.8) ; (1.9) ; and Hadamard's inequality (1.10) for an arbitrary basis.
Proposition (1.11) says the first vector of a reduced basis approximates a shortest nonzero lattice vector within the factor ; (1.12) extends this to all of the first basis vectors, so that is within of the -th successive minimum of (the remark after (1.12)). These are the guarantees on which the paper's factoring algorithm rests: in Section 2 a reduced basis of a lattice built from a -adic factor yields, through (1.11) and (1.12), an irreducible factor of the polynomial. Inequality (1.9) gives simultaneous Diophantine approximation in polynomial time, and (1.8) bounds how far a reduced basis is from orthogonal.
All of these results are proved in the paper and in textbooks. Verified LLL developments exist in Isabelle/HOL (Bottesch et al., A verified LLL algorithm, AFP 2018), but Mathlib, the library this platform builds on, has neither the reduced-basis predicate of (1.4)–(1.5) nor these bounds. A Lean development produces a reusable definition layer for lattices with the paper's conventions, Gram–Schmidt length estimates, and Hadamard's inequality in determinant form, which the other missions of this series (the reduction algorithm and the factoring application) build on.
The estimates on Gram–Schmidt lengths are single-variable inductions once (1.5) has been rewritten using orthogonality. The step that does not follow from a direct estimate is (1.12): the vectors are arbitrary independent lattice vectors with no relation to the basis order, so a bound on each by a single Gram–Schmidt length does not by itself say which it controls. A naive argument that pairs with fails. The determinant statements need the link between Mathlib's matrix determinant of the columns and the Gram–Schmidt lengths, which Mathlib does not state in this form.
is EuclideanSpace ℝ (Fin n) (abbreviated Vec n), a basis is a family b : Fin n → Vec n, the lattice is Submodule.span ℤ (Set.range b), and "basis for " is linear independence over together with equality of that span with . The vectors are Mathlib's unnormalised InnerProductSpace.gramSchmidt, and is (1.3) verbatim. is the absolute determinant of the column matrix; it is not defined as , which would make the first companion statement true by definition. Section 1 begins "Let be a positive integer", so every statement carries .
Lean indices run from to : the paper's is Lean's b ⟨i-1, _⟩, an exponent at paper index is at Lean index , and the pair of (1.5) is . Exponents , and are real powers. The maximum in (1.12) is a Finset.sup' over the nonempty index set of the , and the statement is empty at , as on the page.
Every statement about a reduced basis also assumes linear independence: the reducedness inequalities alone hold for degenerate dependent families, whose Gram–Schmidt vectors vanish, and would make the targets trivial. The goal does not assume (1.7), (1.13) or any ordering of the ; those appear only as milestones. Proofs of the milestones and companions, and general lemmas on Gram–Schmidt and determinants that would belong in Mathlib, are welcome.
A correlated equilibrium (Aumann 1974) describes play in a game where a mediator draws a profile of recommended actions from a joint distribution and tells each player only that player's own recommendation; the distribution is an equilibrium when no player gains, on average, by departing from the recommendation. Correlated equilibria are the natural outcome of regret-minimizing learning dynamics and the solution concept underlying much of algorithmic game theory, so it matters in which games they are guaranteed to exist.
For finite games existence follows from Nash's theorem, since every Nash equilibrium is a correlated one. Hart and Schmeidler (1989) gave a direct proof based on linear duality, with no fixed-point theorem, and then extended it beyond finite games. This mission formalizes the last and most general of their three existence theorems: games with arbitrarily many players whose strategy spaces are compact Hausdorff spaces.
Timeline.
A game consists of a nonempty set of players, possibly uncountable; for each player a nonempty set of pure strategies; and for each player a payoff function on the set of strategy profiles . For a profile and a strategy , denotes the profile obtained from by replacing player 's coordinate with ; thus .
In this mission each is a compact Hausdorff space with its Borel σ-algebra , the profile space carries the product topology, and is the Borel σ-algebra of . The product σ-algebra generated by the is contained in , and the inclusion may be strict when is not metrizable (the paper's footnote 13).
Let be a probability measure on . Think of as the mediator's distribution; player learns the coordinate of the drawn profile. A deviation of player is a -measurable map that replaces each recommendation by an action. The measure is a correlated equilibrium with respect to and when, for every player and every deviation ,
The left side is the expected gain from obeying the recommendation instead of following .
If every is compact Hausdorff and every is continuous on with the product topology, then
"Countably additive" in the paper's statement is automatic: is a measure.
An optional milestone records the remark on p. 23 that, for a finite strategy set , condition (4) for player is equivalent to the earlier condition (3), one inequality per recommendation and alternative .
The result. Theorem 3 guarantees correlated equilibria, with a genuine (countably additive) probability measure, in every continuous game on compact strategy spaces, however many players there are. It also justifies taking to be the full Borel σ-algebra rather than the smaller product σ-algebra, so that every Borel-measurable deviation rule is allowed. Nash existence under the same hypotheses (Fan 1952, Glicksberg 1952) implies existence of correlated equilibria too, but through a fixed-point theorem; the proof here uses only finite-dimensional duality and compactness.
Formalizing it. The theorem is classical and its proof is published; nothing here is open. To our knowledge no machine-checked proof of Theorem 3, or of any existence result for correlated equilibria in infinite games, exists. Finite-game existence results are on the platform (AGT.nash_existence; the correlated-equilibrium encodings of Aumann 1987 and Foster and Vohra 1997, and AGT.swap_regret_correlated_equilibrium). The formalization would add reusable measure-theoretic tools on compact products: the regular cluster point of a net of probability measures, the regularity of marginals, and uniform partitions for continuous functions on a product.
The obvious argument is the one that proves Theorem 2: approximate the game by finite games , take correlated equilibria , extract a weak-* cluster point , and pass the inequalities of to the limit. Passing to the limit works only for integrands that are continuous in , because is a cluster point against continuous functions only. The integrand of (4) is , and is merely Borel measurable, so this integrand need not be continuous and the limit step fails. Restricting to continuous deviations would avoid the difficulty but would prove a weaker theorem. Two further points need care: on a non-metrizable product the Borel σ-algebra is larger than the product σ-algebra, and the f-sets ordered by inclusion are not a directed set.
The profile space is a type synonym Profile S of ∀ i, S i carrying the product topology and the instance borel (Profile S), so measures on live on the Borel σ-algebra and not on Mathlib's product σ-algebra MeasurableSpace.pi (). The pair is Function.update s i t. Players form a type ι with Nonempty ι; each S i is nonempty, compact and Hausdorff with BorelSpace (S i); payoffs are h : ι → Profile S → ℝ with each h i continuous. Deviations are all maps ζ : S i → S i with Measurable ζ.
The predicate IsCorrelatedEq h μ requires IsProbabilityMeasure μ and, for each player and measurable deviation, both integrability of the integrand and nonnegativity of its integral. The integrability clause prevents a trivializing reading in which a non-integrable integrand, whose Lean integral is , satisfies (4) vacuously; restricting deviations to continuous maps, or using the product σ-algebra, would also change the theorem and is ruled out.
The f-set net is indexed by the f-sets containing a fixed profile , which are directed; the paper's "ordered by inclusion of the sets " over all f-sets is not directed, and anchoring repairs this without affecting any statement of the paper. A correlated equilibrium of is encoded by its finite support and weights (IsFSetCE). The special case is stated for a regular cluster point of the given by these constructed objects, not for an arbitrary measure.
A complete development needs Banach–Alaoglu or the compactness of probability measures on a compact space, the Riesz–Markov–Kakutani representation (RealRMK), regularity of measures (Measure.Regular), Urysohn's lemma, and uniform continuity on compact spaces, all available in Mathlib in some form. Proofs of any milestone, including the general-purpose milestones 2, 3 and 5, are welcome.
The contact process is the basic model of an infection spreading on a lattice: each infected site recovers at a constant rate, and each healthy site becomes infected at a rate that depends on how many of its neighbours are infected. It was introduced by T. E. Harris in Contact Interactions on a Lattice (Ann. Probab. 2, 1974), and it became one of the central examples of interacting particle systems, alongside the voter model and the stochastic Ising model (Liggett, Interacting Particle Systems, 1985, Ch. VI). Its main question is whether a finite infection dies out with probability one or survives forever with positive probability, and how that answer depends on the rates.
Harris's paper gives the first answers. It shows that, under natural conditions on the rates, the probability of survival is monotone, subadditive and submodular as a function of the initial set, and it uses these properties to prove a condition for certain extinction: Theorem 7.1. For the linear contact process (recovery rate , infection rate per infected neighbour) the condition is . Holley obtained Theorem 7.1 by different methods at about the same time (footnote 4, p. 981); Holley and Liggett (Ann. Probab. 3, 1975) later developed the duality theory of such processes.
Let be the -dimensional integer lattice, . Sites are neighbours, , if ; is the set of the neighbours of . A configuration is a finite set of infected sites; is the set of all of them, , and means and has a neighbour in .
The parameters are a recovery rate and infection rates . The contact process started from a finite set is the continuous-time Markov chain on that leaves at rate
and jumps to () at rate and to () at rate (4.5). The empty set is absorbing. Write for its transition function, for the transition matrix of its imbedded jump chain, and
The process is increasing, subadditive or submodular if, for all and , respectively , , or ((5.2)–(5.4)).
If
then
Theorem 7.1 gives a computable sufficient condition for extinction that holds in every dimension and for every non-linear infection law satisfying it. For the linear process it gives the lower bound on the critical infection rate; the paper's §9 shows conversely that the process survives for large , so the critical rate is non-trivial. The monotonicity, subadditivity and submodularity theorems of §§5–6 are the comparison tools on which much of the later theory of attractive spin systems was built, and Lemma 5.8 is the prototype of comparison between processes with ordered rates.
The results are proved in the paper, and the proof of Theorem 7.1 is half a page once §§5–6 are available. No machine-checked version of the contact process, of its comparison theorems, or of Theorem 7.1 is known to exist. A formalization produces a continuous-time Markov chain with unbounded rates and an absorbing state on a countable state space, its minimal transition function, a non-explosion criterion, first-step analysis for absorption probabilities, and coupling arguments for monotone comparison. The companion mission Contact Interactions on a Lattice II treats Theorem 7.6, the integrability of the expected size, on the same model.
The obvious argument is first-step analysis on singletons and pairs, (7.2) and (7.3). It fails as it stands because (7.3) involves of every three-point set , and no finite system of first-step equations closes; some inequality between survival probabilities of nested sets is needed, and the milestones record the one the paper uses. Submodularity, subadditivity and monotonicity are not consequences of the rates by direct computation: the paper proves each by building several contact processes on one probability space (Tables 1–4), which in a formal development means constructing couplings of chains with unbounded rates and checking that each marginal has the right law. The reduction from general to the linear case also needs the comparison Lemma 5.8, another coupling. Finally the rates grow linearly in , so uniformization does not apply and non-explosion (Theorem 4.3) must be proved before transition probabilities are known to sum to one.
The process is the countable-state chain of §4, not the Feller process on all subsets of of §2: sites are Fin d → ℤ, configurations are Finsets, and is the minimal transition function of the rates (4.4)–(4.5), defined as the increasing limit of Feller's backward recursion. There is no measure-theoretic process object; and enter only through . Consequently Theorem 4.1 ( is stochastically closed) is built in, and every statement is made for finite initial sets, including those the page makes for arbitrary ((5.2)–(5.4), Lemma 5.8); for infinite the page itself notes .
The committed conventions:
Trivializing formalizations are ruled out: the survival probability is not taken from an arbitrary semigroup or a uniformization (the rates are unbounded); is not a real infimum or limUnder, whose junk value would make the goal free; is indexed by the number of infected, not vacant, neighbours, and forbids spontaneous infection; and (7.2) is stated for every site and every neighbour, not for one fixed pair.
A complete development needs: non-explosion for chains with linearly growing rates; the Chapman–Kolmogorov and strong Markov properties of the minimal chain at jump times; lattice symmetries (translations and coordinate reflections) acting on the chain; and couplings of several contact processes realised as one chain on a product type space. The chain infrastructure and the coupling lemmas are reusable beyond this mission, in particular by its companion. Contributions to any milestone are welcome, including proofs of the milestones under the paper's hypotheses by methods other than Harris's.
Telephone exchanges, call centers, hospital wards and cloud server pools are queues with a large number of parallel servers. For such systems two classical approximations pull in opposite directions. Holding fixed and letting the traffic intensity gives the conventional heavy-traffic limit, in which almost every customer waits. Letting grow with fixed below one gives a limit in which almost nobody waits. Real systems sit in between: a positive fraction of customers wait, and waits are short. Halfin and Whitt (Operations Research 29 (1981) 567–588) identified the scaling that produces this middle regime and the limit laws it yields. The scaling is now called the Halfin–Whitt or quality-and-efficiency-driven (QED) regime, and it underlies square-root staffing: run servers for an offered load of Erlangs. Borst, Mandelbaum and Reiman (Operations Research 52 (2004) 17–34) built staffing rules for large call centers on it.
Timeline. Erlang (1917) gave the delay probability of the M/M/s queue. Iglehart (1965) proved diffusion limits for M/M/s queues with the number of servers growing and the traffic intensity fixed. Halfin and Whitt (1981) proved that the delay probability has a limit strictly between 0 and 1 exactly when converges to a positive constant (their Proposition 1), derived the limit of the stationary queue length (Theorem 1), and extended the process-level limit to GI/M/s queues. Later work extended the regime to many-server queues with general service times and abandonment.
An M/M/s queue has Poisson arrivals at rate , servers, and exponential service times with rate . Its traffic intensity is . The number of customers in the system (waiting or in service) is a birth–death process on with birth rate and death rate in state . When , converges in distribution to , whose law is the unique probability distribution solving the balance equations of this chain. The probability of delay is the Erlang-C formula.
The mission studies a sequence of such queues: queue has servers, the fixed service rate , and arrival rate with and . Its stationary queue length is , and the scaled queue length is
Throughout, and denote the standard normal distribution function and density, and for
The standing assumption of the paper's Section 2 is the heavy-traffic condition
Under (2.2), with ,
The limit is exponential with rate above zero and a normal law truncated at zero below it, with masses and .
and for with ,
Theorem 1 is the stationary half of the Halfin–Whitt regime. It turns the Erlang-C formula, a ratio of sums with terms that is opaque for large , into a two-parameter description of congestion: is the fraction of customers who wait, is the scaled safety margin of servers, and the conditional laws above give the distribution of the number waiting and of the number of idle servers. Proposition 1 and Theorem 1 are what square-root staffing rules evaluate; Corollary 1 supplies the mean and variance used in the paper's numerical approximations.
All results of this mission are proved in the paper, by direct calculation from (1.1)–(1.3), Stirling's formula and the central limit theorem for Poisson variables. None has a machine-checked proof. Proposition 1 and the two Section 1 facts are posed on the platform as open theorems from the Gross et al. queueing textbook series; this mission adds the conditional and local limits, the weak-convergence theorem and the moment results on the same definitions, so that a closed development would give a fully checked derivation of the Halfin–Whitt limit from the balance equations.
The stationary law is explicit, so nothing here needs a stochastic process. The difficulty is analytic and uniform: each statement is a limit of ratios of sums of or infinitely many terms, below and a geometric tail above , in which and at linked rates. The lower half needs a central limit theorem for Poisson laws whose parameter moves with and is evaluated at a moving point; the local limits (2.10) and (2.12) need Stirling's formula with explicit control of to second order. Weak convergence then needs tightness, or a direct argument from the conditional limits, and the moment limits need uniform integrability, which the fixed- moment recursions do not give by themselves. Holding fixed, or taking limits in and one after the other, gives degenerate answers ( or ); the two limits must be taken together.
The Lean development lives in the namespace HalfinWhitt81.Stationary. The law of is a sequence p n : ℕ → ℝ satisfying IsSteadyState (fun _ => lam n) (mmcDeath μ n) (p n) of the referenced definition QueueingFundamentals.BirthDeath.Balance (nonnegative, summing to one, solving the balance equations of the M/M/n chain); the Erlang-C formula and are erlangC and halfinWhittAlpha of QueueingFundamentals.BirthDeath.Erlang, and , are Mathlib's cdf (gaussianReal 0 1) and gaussianPDFReal 0 1. These, and the three open theorems for (1.1)–(1.3), (1.2) and Proposition 1, come from the Gross et al. (2008) series and are referenced, not restated. The related Borst–Mandelbaum–Reiman items (DimCallCenters.*.lemma_4_1, for the continuous extension of Erlang-C) state a different result and are not used.
Conventions committed to:
p n (probLE, probGE, probEqInt); a conditional probability with is the ratio ; is Int.floor, with for ;The goal cannot be met trivially: the law of is the M/M/n steady state, not a free sequence; the limit measure is asserted to exist together with its three properties and the convergence, so no vacuous "for every " reading is possible; and the statement alone is Proposition 1, already posed.
A complete development needs: the closed form of the M/M/n steady state, Poisson central limit and local limit theorems with a moving parameter, Stirling's formula with error terms, a criterion for weak convergence from convergence of distribution functions, and uniform integrability for the moments. The Poisson limit theorems and the weak-convergence criterion are reusable beyond this mission. Proofs of the referenced open theorems, of individual milestones, and alternative routes to Theorem 1 (moment convergence, or the process-level limit) are all welcome.
The linear complementarity problem asks, for a real square matrix of order and a vector , for a vector with
It is the common form of the Kuhn–Tucker conditions of linear and convex quadratic programs and of the equilibrium conditions of two-person non-zero-sum (bimatrix) games. In 1964 Lemke and Howson gave a constructive existence proof for equilibrium points of bimatrix games by following a path of adjacent extreme points of a polyhedron (Lemke–Howson 1964). In 1965 Lemke adapted that path-following technique to the general problem above, under a condition on that covers the positive semidefinite case treated by Dantzig and Cottle and the case (Lemke 1965). The resulting procedure, now called Lemke's algorithm or complementary pivoting, became a standard method for linear complementarity problems and a template for later path-following existence proofs (Cottle, Pang, Stone 1992).
Timeline:
Fix a finite index set of size , a real matrix and . Inequalities between vectors are componentwise and is the all-ones vector.
Suppose is non-degenerate and that for every
Then
The Corollary (p. 5: , gives an odd number of equilibrium points), Theorem 3 (p. 5: if for all , at most one equilibrium point) and Theorem 5 (p. 8: if moreover , has at least rays).
Theorem 4 is an existence theorem for a class of linear complementarity problems that contains convex quadratic programming (the case for all ) and strictly positive matrices, and its proof is an algorithm: the path followed is the sequence of pivots of Lemke's method. The parity statements (Theorem 2, the Corollary) are an early instance of the path-following parity arguments later abstracted in the complexity class PPAD (Papadimitriou 1994).
The theorem is classical and proved. To our knowledge neither Lemke's theorem nor the polyhedral path machinery of Theorems 1–2 has a machine-checked proof in Lean or Mathlib. This mission produces the vocabulary of non-degenerate complementarity polyhedra (the matrix , open edges, rays, adjacency paths), the parity theorem, and the existence theorem itself; the Farkas-type Lemma 2 (p. 4) is already available on the platform.
The algebraic part (Lemma 3 and (22)–(25)) is short. The difficulty is combinatorial-geometric: Theorem 1 requires that, under non-degeneracy, every extreme point of has exactly incident edges, that each point of is an extreme point or lies on an open edge, and that the edges contained in form paths whose end-points are exactly the equilibrium points; the parity of Theorem 2 then needs finiteness of the set of extreme points. None of this polyhedral structure (edges as zero-pattern classes, their closures and end-points) is in Mathlib. Moreover, the printed proof of Theorem 4 applies Theorem 2 to , whose non-degeneracy the paper obtains from an informal perturbation remark, and it sketches the step from the end of the augmented path to a ray of ; a complete proof of the goal must supply these steps or take another route.
Contributions welcome: the polyhedral lemmas for non-degenerate (extreme points have edges, finitely many extreme points), the parity argument, and any complete route to Theorem 4.
Many stochastic systems have an accumulated cost or passage time that grows with the length of an observation window. Splitting a window at an intermediate time gives an upper bound on the total, even when it does not give an equality. First-passage percolation and products of random matrices are examples discussed by Kingman (1973). A central question is whether the cost per unit time settles to a long-run rate on almost every sample path.
Hammersley and Welsh introduced subadditive stochastic processes in 1965. Kingman's 1968 theorem established the almost-sure limit for the stationary process considered here. His 1973 paper restated the result, identified the limit's expectation, and set out the process model and related formulations used in later applications. The 1973 article explicitly attributes the proof of Theorem 1, its maximal inequality, and its decomposition to the 1968 work; this mission formalizes the statements as presented in the 1973 paper.
Fix a probability space . For integers , let be a measurable random variable. Think of as the accumulated quantity over the interval from to . Condition S₁ is subadditivity: whenever . The stronger equality defines an additive process.
Condition S₂ says that shifting every interval one time unit forward leaves the joint distribution of the whole family unchanged. It concerns the law of as a single countable path. The one-dimensional statement that each has a distribution depending only on is called S₂′ in the paper; it does not replace S₂. Condition S₃ says that every positive-time variable is integrable and that, for some real , its mean satisfies for all . A subadditive process satisfies S₁, S₂, and S₃.
The associated mean growth rate is . The time index starts at one in this infimum because division by zero would introduce an unrelated value. S₃ gives a finite lower bound; the subadditive mean relation makes this infimum the limit of . Kingman also considers the invariant σ-field : events determined by the entire path and unchanged by the shift . It records the part of the process that can remain random in the limiting rate. Source: §§1.1–1.2, pp. 883–885.
For every subadditive process there is an integrable real random variable such that
These are three distinct claims: almost-sure convergence, convergence in mean, and an identity for the limit's expectation. The limit need not be a constant. The milestone list also covers the convergence of the means, the maximal inequality (1.2.5), the decomposition (1.2.6), the measure-preserving formulation (1.3.4)–(1.3.5), and the representation through in (1.2.4). Each statement comes from the 1973 paper, §§1.1–1.3.
For a measure-preserving map , condition Sᴱ concerns integrable functions with for and a linear lower bound on their expectations. It yields an integrable with almost surely and in mean. Neither invertibility nor ergodicity of is assumed. Source: §1.3, p. 886.
The theorem assigns a finite sample-path growth rate to an entire class of stationary subadditive systems. It also ties the average of that rate to the infimum of the normalized expected values. The equality is useful when a system's finite-window means are easier to estimate than its individual long-run paths. The invariant σ-field statement explains why a stationary system can have different rates on different paths without contradicting the mean identity. Kingman's examples show how the same framework reaches percolation and matrix products.
The result is mathematically proved, as the 1973 article states. The remaining work here is a machine-checked development of its process model and the displayed results. A published Prove2Me item, PalmQueueing.Ergodic.kingman_subadditive, is open and concerns an ergodic bijective flow with a constant possibly infinite limit; it does not supply this nonergodic finite-limit theorem or convergence in mean. The draft statements in this mission compile with proof placeholders. No machine-checked proof of these new statements is claimed.
Subadditivity gives bounds when intervals are joined, but it does not express as a sum of identically distributed increments. The ordinary additive ergodic theorem therefore does not immediately give convergence for . Nor does convergence of the expectations alone force convergence on individual paths or in mean. The process may also have a nonconstant limit: stationarity is a joint-law condition, not an ergodicity assumption that erases invariant information. These are the gaps the formalization must close without strengthening the hypotheses. Source: §§1.1–1.3.
Lean represents as a function of two natural-number indices and a sample point, but every condition and conclusion uses only . S₁ and the Sᴱ cocycle inequality follow the paper's pointwise displays; random-variable equality in the decomposition is stated almost surely at each valid index pair. Measurability of each valid coordinate is explicit. S₂ compares two probability measures on the full countable path space, so equality of individual marginals cannot satisfy it. The probability measure is normalized, and S₃ requires Bochner integrability to keep every mean finite. The constant is a real infimum over positive times, used only under S₃. The goal's limit is real and integrable; Kingman's separate Theorem 2 treats a possible value of and belongs to another mission.
The invariant σ-field is the pullback of the path-space shift-invariant σ-field. Its measurability claim is made through an almost-everywhere equal version, since almost-sure limits are insensitive to changes on null sets. Conditional expectation uses this explicit sub-σ-field. All limits in this mission take positive integer time to infinity. The Sᴱ definition requires measure preservation but no inverse and no ergodicity. Thus neither a marginal-law substitution for S₂ nor an ergodic constant-limit specialization can trivialize the target.
A complete proof can reuse Mathlib's measure theory, conditional expectation, product measurable spaces, measure-preserving maps, and subadditive-sequence results. The two process definitions, the invariant σ-field interface, and auxiliary statements are useful to later formalizations of stationary growth models. Contributions that prove the stated results or develop general-purpose lemmas for these objects fit the mission.
Population models often allow each individual to produce a new individual or die at rates that change over time. Seasonal conditions, exposure to an epidemic, and changing conditions in a laboratory population all make a constant rate a restrictive assumption. In Kendall's 1948 paper, the question is how the entire distribution of the population size evolves when the per-individual birth and death rates are prescribed functions of time. The distribution matters even when its mean is known: a population can have a stable expected size while still having a substantial chance of extinction. Kendall presents the varying-rate model as a generalization of the constant-rate process discussed by Feller in 1939 (Kendall 1948, §1).
This mission concerns Kendall's solution for a population descended from one ancestor. It includes the explicit distribution, the forward equations that connect it to the birth and death model, and the formulas for its mean, variance, and chance of eventual extinction. The paper has no numbered theorems; its results are identified here by its equation numbers and printed pages.
At time , let be the number of individuals. Each individual gives birth at instantaneous rate and dies at rate , so a population of size moves to at rate and to at rate . Both rates are nonnegative. The initial state is . Write for the probability that . The forward equations in §2, (2)–(4), p. 2 are
The formula for reflects that a population already at zero cannot reproduce. The term vanishes at , as it must. The model is expressed through these real-valued probability functions; it does not require a sample-space construction of a stochastic process.
Define the integrated rate difference and the function by §2, (10a)–(11), p. 4:
Set and . Kendall's modified-zero geometric law is and for . The zero state has its own mass; the positive states form a geometric tail. For the nonnegative rates in this mission, and on , so the displayed formulas have their ordinary probabilistic meaning.
The goal is the full claim of §2, (8), (10a)–(12), pp. 3–4: the explicit starts from one ancestor, is nonnegative and sums to one for every , and satisfies the forward equations above. In symbols, the distribution part is
The milestones record the paper's intermediate statements in reading order: the rational generating function in (9); the pair of equations for and obtained from the generating-function equation (6); the equations for and ; the differential equation and integral representation of ; the alternate formulas (10b)–(10c); and the explicit expressions (12). Each is a statement made in the source, with the page and equation displayed beside its milestone.
The companion target from §3, (18)–(19), p. 6 writes and states
When has finite limit , the limiting extinction chance is . Companion statements also retain the mean , all three expressions for the variance in (14c), the criterion that extinction has zero chance exactly when vanishes identically, and the necessary divergence of for almost-sure extinction (Kendall 1948, pp. 4, 6–7).
The geometric law supplies every finite-time population probability from the rate functions. Its zero mass yields an extinction probability without taking limits of an unspecified process, while its first two moments quantify expected growth and fluctuations. The extinction criterion distinguishes a population that dies out with probability one from one that retains a positive chance of survival even when its eventual mean behavior is simple. The variance formulas give later sections of Kendall's paper a way to compare rate schedules with the same expected population (§§3, 6).
The result was proved in the 1948 paper. The work here is to state its model and conclusions precisely in Lean, preserving the initial condition, normalization, boundary state, and time-dependent rate conventions. The current files are theorem statements with proof placeholders; a successful build checks their syntax and types, not the mathematical proofs. Once proved, the definitions and the moment and extinction statements can also support formal work on time-dependent branching and population models.
Knowing the expected population is insufficient to determine the distribution. The forward equation for each couples it to both neighboring states, producing an infinite system. A direct finite truncation would change the birth rate at its upper boundary and would therefore no longer be Kendall's model. The zero state also behaves differently from positive states: a purely geometric law on all does not capture its mass. The generating function has a rational form, but its time dependence must still agree with the forward system for every state and with a normalized probability law. The extinction statement adds an improper integral, whose finite and divergent regimes require distinct limits.
Lean represents as continuous functions that are nonnegative for . The paper calls the rates specified functions and assumes their nonnegativity; global continuity is an explicit convenience for the two-sided derivatives and interval integrals. Only nonnegative time appears in the probabilistic statements. The oriented intervalIntegral from zero to represents every finite integral. HasDerivAt expresses each derivative, and HasSum expresses both normalization and the moment and generating-function series. The law lives on natural-number states, with handled separately. The coefficient at state is the real number , not an implicit extension to a negative state.
The positivity of on nonnegative time must follow from the rates. The definitions are total Lean real functions, so a result that relies on a division states the hypotheses that keep its denominator nonzero. The limit expresses divergence of the paper's improper integral. No uniqueness of solutions to the forward equations is included, because the cited passage does not establish that claim. The goal requires the explicit law to solve the forward equations and to be a probability law; merely expanding its generating function would leave the population model unformalized. Contributions that prove the formulas, establish the required positivity and convergence facts, or develop reusable lemmas for time-dependent linear birth and death equations all fit the scope.
The traveling salesman problem is NP-hard in general, so special cost structures under which it can be solved exactly in polynomial time are of lasting interest in combinatorial optimization and scheduling. One of the earliest and most cited such cases comes from sequencing on a machine whose condition is described by a single real number: a furnace temperature, a knife setting, a fill level. Each job must start at a prescribed state and leaves the machine in another, and changing the state between consecutive jobs costs money or time. Finding the cheapest cyclic order of the jobs is a traveling salesman problem with asymmetric costs.
P. C. Gilmore and R. E. Gomory solved this problem exactly in 1964 (Oper. Res. 12(5), 655–679) with an algorithm of simple steps. Their construction became the standard example of a solvable TSP case: it is the starting point of the survey literature on polynomially solvable TSPs (Gilmore, Lawler and Shmoys 1985; Burkard, Deineko, van Dal, van der Veen and Woeginger 1998), and it appears in the no-wait flow shop literature, where two-machine no-wait scheduling reduces to exactly this cost structure.
There are jobs . Job must be started when the state of the machine is and leaves the machine in state ; the jobs are numbered so that implies . Two cost densities satisfy : raising the state through costs per unit, lowering it costs per unit. The changeover cost of having job follow job is
A permutation of the jobs assigns to each job its successor and has cost . It is a tour if for every nonempty proper subset of the jobs, i.e. if it is a single cycle through all jobs.
A permutation ranks the if implies . The interchange swaps and ; applying it to gives (first , then ), which exchanges the successors of and , at cost . The graph links and for every ; a spanning tree of is a minimal set of additional arcs that makes it connected, with cost . Node is of type 1 if and of type 2 otherwise.
Given a minimal cost spanning tree of made of arcs , the tour is obtained from by executing the interchanges , , first those of type 1 in decreasing order of , then those of type 2 in increasing order of .
This is the paper's main theorem. It fixes no constant and no special form of ; it asserts that the specific tour produced by the algorithm is optimal among all tours.
In the order the proof uses them:
Off the goal's path: Theorem 7, a minimal tour for is minimal for .
The theorem shows that a traveling salesman problem whose costs come from a one-dimensional state is solved by three polynomial steps: sorting (an optimal assignment), a minimum spanning tree over candidate arcs, and a prescribed sequence of interchanges. It is the base case for a family of later results on solvable TSPs and for the two-machine no-wait flow shop, where it gives an exact polynomial algorithm.
The result has been proved since 1964. No machine-checked proof of it is known to exist. The proof in the paper argues largely from figures ("evident geometrically"), and its statement of Theorem 3 lists the interchanges in an order that contradicts its own proof: executed in the printed order, the paper's numerical example yields a tour of cost 39 instead of the optimum 34. A formal proof settles which order is correct and fills in the geometric steps. Partial contributions are useful: the permutation facts (Lemmas 1, 8 and Theorem 2) are independent of the cost model and reusable.
The obvious argument fails at two points. First, interchanges do not commute in cost: once one interchange is executed, the cost of the next one depends on the new successors, so the cost of is not simply plus the tree cost for an arbitrary execution order. Showing that the specific order of Lemma 5 avoids all interference requires tracking how type-1 and type-2 nodes behave as interchanges are applied. Second, optimality is not a local statement: an arbitrary tour is not reachable from by tree interchanges, so the lower bound needs the separate underestimate and a counting argument relating every tour to a spanning tree of . Neither step follows from general minimum spanning tree theory.
Jobs are Fin (n + 1) (), so the paper's job is index ; the adjacent arc is indexed by q : Fin n and joins q.castSucc and q.succ. Permutations are Equiv.Perm (Fin (n + 1)), and is ψ * Equiv.swap i j (Mathlib's composition, "first , then "). Costs are real; (1) uses oriented interval integrals and (17) set integrals.
Explicit readings of the paper's loose phrases:
The order of is that of the proof of Lemma 5 and of steps T2–T4 (p. 673), not the order printed in Theorem 3.
Trivializing formalizations are ruled out: the goal quantifies over all tours, not over permutations (that is Theorem 1) nor over tours reachable from ; is constructed from and , not taken as an arbitrary tour of the right cost; is both inclusion-minimal and cost-minimal; and the costs keep both branches of (1) with general densities, not . The TSP items already on the platform concern symmetric or metric distances with tours as visiting orders, a different model, and are not reused.
Needed infrastructure: cycle structure of permutations under transpositions (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, interval integrals of locally integrable functions. Contributions to any milestone are welcome; the purely combinatorial ones (Lemmas 1, 8, Theorem 2, Lemma 7) are independent of the integrals.
Freedman's inequality bounds the probability that a martingale with increments bounded above by reaches a level before its accumulated conditional variance exceeds : the bound is (D. A. Freedman, On Tail Probabilities for Martingales, Ann. Probab. 3 (1975) 100–118, Theorem (4.1), doi:10.1214/aop/1176996452). It is the standard tool for concentration of martingales whose variance is random, and it is used throughout online learning, bandit theory and the analysis of randomized algorithms.
The same paper shows that the exponent cannot be improved in general. For a martingale with increments bounded by in absolute value, Freedman's estimate (1.10) bounds from below the probability that level is crossed while the conditional variance used is still below . The analytic core of that lower bound is isolated in the paper as Proposition (4.10), p. 109: a statement about a single nonnegative random variable whose Laplace transform is controlled from both sides. The paper calls its proof "disappointingly hard". This mission formalizes Proposition (4.10) and the steps of its proof.
Let be a probability space. For real put (Definition (1.2), p. 101)
Both are nonnegative and equal near . Fix and a nonnegative random variable . The two Laplace-transform bounds are, for every ,
In the paper is the conditional variance accumulated up to the first time the martingale reaches ; for that variable (4.11a) and (4.11b) are Theorems (1.12) and (1.8). Here is abstract. The hypotheses are consistent: the first-passage time of standard Brownian motion to level has , and since for , it satisfies both bounds.
The parameter conditions (4.12) on positive reals are
The proof uses the notation (4.14): , , , , the five intervals , , , , , and the terms
In Lean these objects are FreedmanTail.LowerTail.e, f, LaplaceUpper, LaplaceLower, ParamConditions, phi, lamStar, kStar, NStar, I1–I5 and eta.
Under (4.11a)–(4.11b) for all and (4.12a)–(4.12c),
In the order of the proof:
The result. Proposition (4.10) converts two-sided control of a Laplace transform into a lower bound for a left tail, with an explicit constant and an explicit range of validity. Applied to the crossing variance it gives Freedman's lower bound (1.10) for , which matches the exponent of the upper bound of Theorem (4.1) up to the term . That is the statement that Freedman's inequality is sharp in the regime , .
Formalizing it. The proposition is proved in the 1975 paper; no machine-checked proof is known. Mathlib contains Chernoff-type upper bounds and the layer-cake formula, but no lower tail bound derived from two-sided Laplace-transform control. The mission produces a self-contained, constant-explicit Tauberian-type lemma for nonnegative random variables, usable without any martingale structure. The companion missions of this series formalize Theorem (4.1) and the Laplace bound (1.8); together they would give the sharpness statement for martingales.
The obvious route is to invert the Laplace-transform bounds directly. A lower bound on does not by itself bound from below: the mass that makes the Laplace transform large could sit at small values of or be spread over a wide range. Without (4.11a) the conclusion fails, and with it every contribution from values of away from must be shown negligible at a precision of order , where is large. The main term is smaller than the total by the factor , so every error term must be estimated with constants explicit enough to stay below it. The thresholds (4.12b)–(4.12c) are what make all of these comparisons hold at once.
The probability space is a measurable space Ω with a measure P and [IsProbabilityMeasure P]. is a measurable function Ω → ℝ with W ω ≥ 0 for every ω. The expectations in (4.11) are Bochner integrals of and ; for these integrands lie in , so they are integrable and the integrals are genuine expectations. Probabilities are P.real {ω | W ω < x}, with the strict event as on the page. The integrals in are Lebesgue integrals over and over the intervals ; the integrand is a nondecreasing function of times , hence measurable and, as , integrable.
Conventions and corrections, each also disclosed in the items:
A trivializing formalization is ruled out: the hypotheses are satisfied by the Brownian first-passage time above, the parameter conditions hold for instance at , , , and no integral in a hypothesis or conclusion can take a default value .
Needed infrastructure: Markov's inequality and the layer-cake formula (both in Mathlib), the identity for , and elementary estimates of and of the convex function of (4.21). The layer-cake identity and the left-tail bound (4.18) are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the unnumbered steps (4.20)–(4.30).
The source is the published article in The Annals of Probability (a scanned copy); page numbers are the journal's.
Many problems in mechanics and optimal control are posed as the minimization of a convex functional of the form , where is a differential operator and is non-smooth: an obstacle, a friction term, a plasticity threshold. Splitting the variable, , separates the linear operator from the non-smooth function, and a Lagrange multiplier for the constraint turns the problem into a sequence of two simpler ones: a linear system in and a pointwise nonlinear problem in . The scheme that alternates between the two and then updates the multiplier is now called the alternating direction method of multipliers (ADMM). It is one of the standard algorithms of large-scale convex optimization, statistics and imaging (Boyd, Parikh, Chu, Peleato and Eckstein, 2011).
Gabay and Mercier (IRIA report RR-126, 1975; Comput. Math. Appl., 1976) gave a convergence proof of this method in Hilbert space, for a stepsize anywhere in , where is the penalty parameter of the augmented Lagrangian.
Timeline.
and are real Hilbert spaces; and are the inner product and norm of , the norm of . is a continuous linear operator and is a continuous linear functional on , with value at . The dual of is identified with . The function is a sum where
The problem is
and a solution is a point where this value is finite and minimal. The Lagrangian and augmented Lagrangian are, for and ,
The modified dual algorithm (3.4) starts from any and, for ,
denotes the orthogonal projection of onto the range , which is closed by (2.5).
For and every stepsize with
every run of the algorithm satisfies
where is the unique solution of . The multipliers need not converge.
and its sum over . 7. for . 8. (3.22)–(3.23): a contraction-plus-summable-forcing recursion for , and the scalar lemma that such recursions tend to . 9. and for .
The theorem says that ADMM converges without any step-size tuning beyond , and that the primal iterates converge in norm in infinite dimension, which is what makes the method usable for finite element discretizations of variational problems (the companion mission on internal approximations treats the discretization). It covers obstacle problems, Bingham fluids and elasto-plastic torsion, where is an indicator or a non-differentiable norm.
The result is proved in the 1975 report. To our knowledge it has no machine-checked proof. Formalizing it adds a library-level convergence theorem for ADMM in Hilbert space with -valued convex functions, a saddle-point existence theorem for linearly constrained convex problems, and the energy estimate (3.19) as a reusable lemma. The formalization also fixes two defects of the printed text (see Formalization scope): a sign in Step 1 and a qualification hypothesis that is too weak.
The energy estimate (3.19) only controls the multiplier through its component in , and only the -error through . The natural first idea, a Lyapunov function in alone that decreases at each step, does not work for : the component obeys a separate recursion whose contraction factor is below one only for , and whose forcing term must be shown summable from the -estimate. The existence of a multiplier, i.e. of a saddle point, is a separate difficulty: it needs the subdifferential chain rule in infinite dimension, under a constraint qualification.
Lean conventions:
InnerProductSpace ℝ with CompleteSpace; multipliers are elements of ; is a StrongDual ℝ V.f₁' at every point (HasGradientAt) that is continuous; "weakly continuous on finite-dimensional subspaces" is then automatic.EReal, with IsProperFn, IsConvexFn, IsSubgradient from the published InertialFB.IFB.ConvexAnalysis and Mathlib's LowerSemicontinuous. No subtraction in EReal occurs: the variational inequalities (3.6), (3.9) are stated as subgradient inclusions, and the Lagrangians as a real part plus .Bornology.IsBounded (Set.range λ).Corrections to the printed text, each explained in the item's statement:
Ruled out: the solution is a hypothesis of the goal, so the hypotheses must not be contradictory. They are met by , , , , , and a proper excludes the degenerate reading in which every point "solves" with value .
A complete development needs: existence of minimizers of coercive convex l.s.c. functions on a Hilbert space; the subdifferential sum and chain rules under a continuity qualification; orthogonal projections onto closed ranges; and elementary facts about summable sequences. The saddle-point theory (Theorems 2.1–2.2) and the scalar lemma (3.23) are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal by a different route.
For sums of independent bounded random variables, the inequalities of Bernstein and Bennett bound the probability of a large deviation by an exponential in the deviation and the variance (Bennett 1962; Hoeffding 1963). Many processes met in probability, statistics and learning theory are not sums of independent terms but martingales or supermartingales: sequential estimators, stochastic approximation iterates, the regret of an online algorithm. For them the relevant scale is not a fixed variance but the conditional variance accumulated along the path, which is itself random.
David A. Freedman's paper On Tail Probabilities for Martingales (Ann. Probab. 3 (1975) 100–118) extended the Bernstein–Bennett inequality to this dependent case, with the conditional variance in place of the variance and with a bound that holds simultaneously for all times. The result, now called Freedman's inequality, is the standard tool for martingale concentration with variance-sensitive rates and is used throughout bandit and reinforcement-learning analyses, random-graph arguments and stochastic optimization. This mission formalizes that theorem, (4.1) of the paper, together with the chain of lemmas the paper uses to prove it.
Let be a probability space and an increasing sequence of sub--fields of (a filtration). Let be real random variables with measurable with respect to . Define
Freedman treats as an intrinsic clock: read at time rather than , the process resembles Brownian motion. The paper's condition (3.4) is
so is a supermartingale whose increments are bounded above by ; no lower bound is assumed. The auxiliary functions are and , with time first and position second. A stopping time takes values in with , and is allowed.
In Lean these are FreedmanTail.Bernstein.S, V, T (on Filtration ℕ m, with V given by Mathlib's condVar) and FreedmanTail.Bernstein.e, Q.
Under (3.4), for all and ,
The first bound is of Bennett type, the second of Bernstein type. The event is a union over all times; the bound does not depend on any horizon.
In the order the paper's proof uses them:
The inequality bounds the probability that a supermartingale ever reaches level before its accumulated conditional variance exceeds . Since it holds for all times at once, fixed-horizon versions follow immediately, as do versions with stopping times, and with a peeling argument over it gives the variance-adaptive confidence sequences used in sequential testing and in the analysis of algorithms. Freedman's paper uses it to derive the law of the iterated logarithm for martingales; later work uses it wherever a martingale's conditional variance is much smaller than the square of its increment bound.
The theorem has been proved for fifty years. What this mission adds is a machine-checked statement and proof of the full infinite-horizon form under the one-sided hypothesis (3.4), together with the exponential supermartingale and the optional-stopping bound (3.3) as reusable lemmas. Prove2Me already has fixed-horizon Bernstein-form consequences for martingale differences; the infinite-horizon Bennett form under (3.4) does not appear in Mathlib or on the platform.
The naive route of applying Markov's inequality to at a fixed gives a bound for one time only and requires a deterministic bound on . Taking a union over all loses everything. The content of the theorem is that the random clock and the supremum over time can both be absorbed, which requires an exponential process compensated by the random and an optional-stopping bound for stopping times that may be infinite with positive probability. The process need not be uniformly integrable, and the increments have no lower bound. A second, smaller, difficulty is the variance form of (3.5): the bound uses rather than , which is strictly sharper when and is needed to compensate with conditional variances.
Lean conventions this mission commits to:
X : ℕ → Ω → ℝ used from index (X 0 is never read), so , and carry the paper's indices. The filtration is Mathlib's Filtration ℕ m, and " is -measurable" is StronglyMeasurable[ℱ n] (X n) for .condVar (ℱ (n - 1)) (X n) P. Mathlib sets a conditional expectation of a non-integrable function to , so every increment is assumed square integrable (MemLp (X n) 2 P). This is the one hypothesis added to the page. Under (3.4) the page also allows increments of infinite variance, for which its is ; the formalization narrows the class of processes and leaves every conclusion as printed. Milestone (3.5) likewise assumes , which is the case the page reduces to.Supermartingale.Ω → WithTop ℕ with IsStoppingTime; is . In (3.3) the integral over is a lower Lebesgue integral in , so the bound does not presuppose integrability, and , are read only on .A fixed-horizon statement (, or ), a martingale hypothesis , or a two-sided bound would each be a strictly weaker theorem than (4.1) and is not an acceptable formalization of the goal.
The development needs exponential supermartingales compensated by conditional variance, optional stopping for stopping times that may be infinite, and elementary real analysis of . The real-analysis milestones (3.1), (3.2) and the two calculus steps are independent and reusable; (3.5) is a self-contained moment-generating-function bound; the supermartingale and (3.3) are reusable for every exponential-supermartingale argument. Contributions to any milestone, and alternative proofs of the goal, are welcome.
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.
Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical scheduling, in which finishing early is never penalized.
Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988) 330–348) study the symmetric version on one processor: each task has a preferred starting time, and the penalty is the absolute deviation from it. Their §2.1 settles the complexity of the most natural objective, the sum of these deviations, by proving it NP-complete. The result explains why the rest of their paper, and much of the later literature, turns to special cases that can be solved efficiently: a fixed task order, equal task lengths, or the maximum deviation instead of the sum.
A short history of the model:
There are tasks . Task has a length and a preferred midtime . A schedule assigns every task a starting time such that no two tasks overlap on the single processor: for , either or . Idle time is allowed. The actual midtime of is , and the total discrepancy of is
The paper works with midtimes because the special case below is then symmetric. Preferred midtimes and preferred starting times are interchangeable through .
Total discrepancy (the decision problem). Given and , is there a schedule with ?
Even-odd partition. Given positive integers , can they be split into two sets of equal sum so that each set contains exactly one of for every ?
The special case. For tasks with and one common preferred midtime , write and . A schedule is ordered if, on each side of , shorter tasks lie nearer to . The bracket is the schedule that puts at midtime and packs the listed tasks against it in the listed order.
The hypothesis is the one result the paper imports (Garey and Johnson, 1979). The conclusion includes membership in NP and polynomial-time many-one reductions from every NP language, with Turing machines as the model of computation.
THEOREM 1 is the hardness boundary for one-processor scheduling with symmetric earliness–tardiness penalties and arbitrary preferred times. It is the reason exact algorithms for this objective are enumerative, and the reason polynomial results are sought under extra structure, such as the fixed-order algorithm of the same paper. The special-case lemmas characterize every optimal schedule for a common, unrestrictive midtime, not just one of them: shortest task centered at , the -th pair of lengths in the -th positions on either side, either member on either side. This characterization holds independently of the reduction.
The result has been proved since 1988, and no machine-checked version of it is known to us. A formalization adds three things. First, the parts the paper calls "straightforward" or "a simple exercise", membership of both problems in NP. Second, the two places where the published argument is imprecise. The instance D has half-integer midtimes and threshold although the decision problem asks for integers, so a correct reduction must rescale. And the special-case lemmas are proved for a large midtime but applied with , so they must be restated for every . Third, a reusable formal treatment of absolute-deviation scheduling objectives and of reductions between number problems written in binary.
The obvious argument fails at the step from the special case to the instance D. The lemmas on pp. 333–336 assume the common midtime is large, so that the constraint never binds. In D the midtime is , exactly half the total length, and the reduction works because the constraint binds. The tasks before must fit in , and the extra task must sit at . Together these force the two sides to have equal total length. A proof that only cites the large- lemmas proves nothing about D. Conversely, dropping makes the reduction false: put the shorter element of every pair after .
The other obstacle is the complexity bookkeeping. NP-completeness here means Turing machines, binary codes, and polynomial bounds, and a full proof must compute D from the code of , double the times to clear the half-integers, and certify membership in NP for a problem whose schedules have real starting times. The certificate cannot be the real starting times themselves.
Fin N from . In the special case is index , and the paper's () are the indices for .CookPvsNP_defs (Cook's one-tape Turing machines, NP, NPComplete) and the published ProjSchedTW.Complexity.Encoding (four-letter alphabet and binary codes). This mission defines positivePartitionLang by restricting the imported equal-sum predicate to nonempty lists of positive integers, as on p. 333. Only codes of well-formed instances belong to the even-odd and total discrepancy languages.NPComplete evenOddLang as the hypothesis instead would drop LEMMA 1 and is not what is asked.Contributions welcome: proofs of any milestone, and reusable lemmas on Turing-machine computability of arithmetic on binary codes, which the two membership results and both reductions need.
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.