Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many 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.
A seller with limited stock can charge a high price while demand is strong and lower the price before the selling season ends. The timing depends on how many units remain: a markdown that is sensible with ample stock may be premature when only one unit is left. Feng and Gallego studied this decision when each price generates a Poisson demand stream and only one price change is allowed. Their 1995 paper proves that the optimal decision has a threshold in remaining time for every inventory level. This mission formalizes their markdown theorem, including its value-function representation, rather than just the existence of a switching rule.
The model is a finite-inventory revenue problem, relevant when an unsold unit loses its value at the end of a season. It is also a continuous-time stopping problem: the seller observes actual sales and may react to them. A fixed calendar date for the markdown cannot describe all of those decisions. The paper treats the markdown case separately from the markup case, because the order of prices, arrival rates and revenue rates reverses the behavior of the switching boundary. The present mission concerns the markdown case alone.
Let be the initial stock and the time to go. The seller first charges price and may change once to a lower price . Demands at the two prices are independent Poisson counts with positive rates and . A lower price produces more arrivals, so and . Feng and Gallego also assume that lowering the price increases the revenue rate: . There is no salvage payment for inventory left when time expires. These conventions come from §2 and the case split on pp. 1375–1376.
Write for the observed sales count at the initial price by time . If the price changes at deterministic time , let be the expected total revenue. The count after the change is independent of , and their sum has Poisson mean . The optimal value allows the switch time to depend on the counts observed so far. An admissible lies between zero and , is a stopping time for the history of , and occurs before stock is exhausted almost surely. At , is the revenue from charging immediately. The paper defines these quantities in §3, pp. 1377–1379.
The goal is Theorem 1, p. 1380. It asserts a strictly increasing sequence of inventory-dependent thresholds. When , switching immediately earns the optimal value; when , a correction is added:
The theorem specifies the correction, rather than leaving it as an arbitrary difference of values. It starts with . For , set , where is the Poisson-tail expression from §4.1. The threshold is the first nonnegative zero of . A function satisfies for positive time and ; is zero below and equals at and above it. If is the first zero of , the theorem also gives and for .
Three supporting targets match the source's attack path. Equation (17) differentiates immediate-switch revenue. Lemma 2 gives the zeros and one sign change of in the markdown case. Lemma 1 identifies a value function through differential inequalities and its stopping payoff. Each is recorded with its page-level statement in the milestone list.
The threshold sequence turns an adaptive stopping problem into a state rule: inspect remaining inventory and time to go, then compare time with the corresponding threshold. The value representation supplies the expected-revenue quantity on both sides of that comparison. Strict increase means a larger stock requires a larger remaining-time threshold before charging the higher initial price is worthwhile. These are the conclusions of Theorem 1, already proved in the paper.
The work here is a Lean statement and eventual machine-checked proof of that known result. The current theorem items are open proof targets. Formalizing the model gives reusable Poisson-tail revenue expressions and a continuous-time stopping-value interface; Lemma 1 can also serve other Poisson-driven stopping problems once proved. A checked proof would establish that the threshold representation and the optimal stopping value agree under the stated assumptions, including boundary cases that informal notation leaves implicit.
The obvious comparison of two fixed switching times misses the information contained in the sales path. The switch decision can change after each observed arrival, while the threshold for inventory depends on the correction at stock . Showing that every such comparison is organized by one increasing threshold requires more than differentiating the fixed-switch revenue. The paper's appendix handles the interaction between the sign of , the recursive correction, and the stopping-value verification; these are distinct formal targets pp. 1387–1388.
The printed verification lemma and one word of Lemma 2 require care. Lemma 1 omits boundary and regularity conditions needed by its proof. Lemma 2 calls the zero sequence “bounded,” although its thresholds tend to infinity; the usable claim is that they stay above a positive lower bound. The formal statements expose these corrections and retain the rest of the source's conclusions.
Lean represents the first demand stream by a counting process built from independent exponential interarrival times. The terminal revenue after a switch is expressed using the Poisson law of the sum of the two independent counts. The stopping class records the count-generated history, bounds the stopping time by the horizon, and requires stock to remain at stopping almost surely. Its expected payoff uses the number sold before stopping and the immediate-switch value for the unsold stock. Prices and rates are positive, the markdown ordering and revenue-rate inequality are explicit, and the probability measure is named explicitly even though the exponential-interarrival law already entails it.
The paper uses nonnegative real time, inventories indexed by positive integers, and zero salvage. Lean uses a real supremum for the value and a real infimum for each threshold; the admissible payoff is bounded and measurable, and every threshold-defining zero set is asserted nonempty. The ODE is expressed with an actual derivative at positive time. The auxiliary Poisson-tail definition maps a negative mean to zero, but all model applications have nonnegative means. The threshold construction, its ODE, and the equality with the stopping value are all conclusions of the goal, so none is an assumed solution.
For Lemma 1, the formal target adds the initial-time and zero-stock boundary values, domination of terminal revenue, and local Lipschitz regularity in time. The first three conditions are used in the source's own proof or reformulation; local Lipschitz regularity makes its integral calculation valid. Contributions may establish the Poisson-tail calculus, the sign and threshold results, the verification theorem, or the complete markdown theorem. The referenced arrival-process definition is shared infrastructure; the two-price revenue and stopping model are specific to this paper.
Temporal-difference (TD) methods learn to predict an eventual outcome from the differences between successive predictions rather than from the difference between each prediction and the final outcome. Sutton's 1988 paper Learning to predict by the methods of temporal differences introduced the TD() family and gave the first convergence proof for a TD method; before it, as the paper notes (p. 23), "no TD method has ever been proved stable or convergent to the correct predictions". TD learning is now the core of policy evaluation in reinforcement learning, and later analyses (Dayan 1992, Tsitsiklis and Van Roy 1997) start from the setting fixed here.
Timeline:
An absorbing Markov chain has a finite set of nonterminal states, a finite set of terminal states and transition probabilities (, ) with . Let be the matrix . "Absorbing" means that every sequence terminates with probability one; for a finite chain this is .
A sequence starts in a nonterminal state drawn from a distribution , follows the chain through nonterminal states until it enters a terminal state , and then produces a scalar outcome drawn from a distribution with finite mean . Let . The ideal prediction of state is the expected outcome from ,
The learner does not see states, only an observation vector for each , and predicts linearly, . Linear TD(0) with weight updates after each sequence keeps fixed during a sequence and then sets, with ,
Sequences are experienced independently; is the weight vector after sequences. Let be the expected number of visits to in one sequence, , and the matrix with columns .
For every absorbing chain, start distribution , outcome laws with finite means and linearly independent , with every , there is such that for and every ,
The threshold is existential, as in the paper; no explicit value is fixed.
Theorem A.1 (Neumann series under ); (5) the ideal predictions; (7) ; the mean recursion ; Theorem A.2 ( nonsingular); Theorem A.3 (); the Lemma of p. 27; positive definite; the eigenvalues of have positive real parts; and for small .
Theorem 3: under repeated presentations of a finite training set, batch linear TD(0) converges (deterministically) to the maximum-likelihood predictions , with its two supporting steps ( and ). Theorem 1: linear TD(1) and Widrow–Hoff produce the same per-sequence weight changes.
Theorem 2 shows that a bootstrapping method, which learns from its own earlier predictions, is not biased by them in the limit: in expectation it reaches the same predictions as supervised (Widrow–Hoff) learning. Theorem 3 says more: on a fixed data set, TD(0) converges to the predictions that would be exact if the maximum-likelihood model of the process were correct, which differs from the least-squares answer Widrow–Hoff converges to. Together they are the formal basis for preferring TD to Monte-Carlo targets in multi-step prediction.
The results are proved on paper, and not formalized in Lean. A formalization adds a precise model of the experience (i.i.d. sequences of an absorbing chain with terminal-dependent outcome laws), the integrability facts the paper leaves implicit, and a correct proof of the positive definiteness of , whose printed argument has a gap (see below). The matrix lemmas (Neumann series under ; real-part positivity of eigenvalues of for symmetric and positive definite in the non-symmetric sense; the step-size threshold) are reusable for other linear stochastic-approximation analyses.
The obvious argument writes as a linear function of and observes that the iteration matrix is a contraction for small . Two steps of this fail as printed. First, the paper proves that is positive definite through the Lemma of p. 27 with a weakened notion of diagonal dominance (weak in every row, strict in one), under which the Lemma is false; with the standard notion, is in general not strictly diagonally dominant (a row with that cannot leave in one step has row sum ). A correct proof combines weak dominance with reachability of every state from the support of , which is where enters. Second, is not symmetric, so a small does not make a contraction in the Euclidean norm; the argument goes through its eigenvalues, and turning eigenvalues of modulus below one into is a spectral-radius argument. The probabilistic step is also not free: is a polynomial in random sequences of unbounded length, and its integrability and the factorization need independence across sequences.
States are finite types N (nonempty) and T; the chain is the structure AbsorbingChain with blocks pN, pT and the field . Observation vectors are x : N → Fin K → ℝ with LinearIndependent ℝ x; is Matrix (Fin K) N ℝ. A sequence is an Episode (list of nonterminal states, terminal state, outcome); IsEpisodeStream states measurability, mutual independence (iIndepFun) and the law . Expectations are Bochner integrals, and the goal asserts integrability of , so a non-integrable junk value cannot satisfy it. is defined as an expectation (a sum over sequences), not as , so (7) is not circular. "Positive definite" is the paper's footnote 6 ( for real , no symmetry), not Mathlib's Matrix.PosDef.
Trivializations ruled out: the hypothesis is the paper's own discarding of never-visited states (without it the goal is false: an unvisited state's weight never moves); N is nonempty and sums to one, so the hypotheses are satisfiable and the goal is not vacuous; the sequences cannot be arbitrary random variables or a fixed sequence, since their law is pinned to , and ; is chosen before , and the probability space; and the update is per sequence, not the intra-sequence variant of §5.
Corrected slips: "For each nonterminal state " (p. 24) means terminal; the diagonal-dominance definition of p. 27 is replaced by the standard one; (p. 28) means . Not formalized: the variance and TD() conjectures of p. 29, §4.3, and the extension claims of §5.
Related open goals on this platform (different models, credited, not re-posed): SuttonBartoRL.BatchTD.batch_td_converges_to_certainty_equivalence (tabular, discounted analogue of Theorem 3), and SuttonBartoRL.LinearTD.keyMatrix_posDef, posDef_of_row_col_sums, expected_td_update (continuing discounted chain with stationary , where every row sum of is positive). Contributions of any milestone, of general matrix lemmas, and of reusable infrastructure for i.i.d. episode streams are welcome.
A postman, a snowplough or a street sweeper must traverse every street of a district and return to the depot. When some streets are one-way, the street network is a mixed graph: some edges are directed and must be traversed in a prescribed direction, the others are undirected and may be traversed either way. The first question about such a route is whether a closed route exists that traverses every street exactly once, an Euler tour of the mixed graph. When one exists, it is an optimal postman route; when none exists, the postman problem asks which streets to repeat.
J. Edmonds and E.L. Johnson treat this question in §6 of Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), the paper that solved the undirected Chinese postman problem by matching. Section 6 gives an algorithm that finds an Euler tour in any mixed graph that is connected, of even degree and symmetric, and §7 uses it for the mixed postman problem.
Timeline.
A mixed graph has a finite set of nodes and a finite set of edges. Each edge meets two distinct nodes; several edges may meet the same pair of nodes. Some edges are directed: an edge directed away from node toward node must be traversed from to . In Lean an edge has a tail, a head (distinct) and a Boolean directed; for an undirected edge the order of the two ends carries no meaning.
If is connected, even and symmetric, then for every node
The goal contains two classical theorems as special cases. With every edge undirected it is Euler's theorem for connected even multigraphs. With every edge directed it is the theorem that a connected balanced digraph is Eulerian. The milestones connect the two cases: an orientation reduces the mixed case to one the Rule can handle. The Rule itself is the van Aardenne-Ehrenfest–de Bruijn construction, which underlies the BEST theorem counting Euler tours. Milestone 5 decides whether the mixed postman problem has any feasible solution. The mixed postman problem is the standard model for routing on one-way street networks.
All results here are proved in the paper, so none is open. No Lean proof of any of them in this form is known. Mathlib's Eulerian walks are for simple graphs; it has no multigraph or mixed-graph Euler theorem, no directed Euler theorem and no arborescence-based traversal. The mission produces these, together with a reusable vocabulary of mixed multigraphs, walks that respect directions, and arborescences given by parent edges.
The obvious approach to the goal is to forget the directions and apply Euler's theorem. This fails because the tour it produces may traverse a directed edge backwards. Orienting all undirected edges at once also fails: an arbitrary orientation of the undirected edges need not keep every node balanced.
The difficult part of the Rule is showing that the greedy traversal does not get stuck before using every edge. It cannot stop at a node other than because of the degree conditions. The hard step is showing that no edge is left unused when it stops at . The answer depends on the ordering condition: without the arborescence edge last at every node, the Rule can return to with edges still unused. The assignment step needs an invariant: the orientation must keep every node symmetric while it extends a spanning structure of directed edges.
Fintype V, Fintype E). Parallel edges are allowed, including a directed and an undirected edge on the same pair. Loops are excluded (tail e ≠ head e), following the paper's standing setting of §2 (p. 91: edges meet two different nodes). Edges are a type, not a relation on nodes, so parallel edges stay distinct in every walk.Contributions are welcome at every level: proofs of the milestones, a direct proof of the goal, and general lemmas about mixed multigraph walks.
A matching in a graph is a set of edges no two of which share a vertex. Finding a matching of maximum cardinality is one of the basic problems of combinatorial optimization: it models pairing tasks (workers to shifts, kidney donors to recipients, players to rounds), it is a subroutine of algorithms for the travelling salesman and Chinese postman problems, and it was the first problem shown to need more than linear programming over the obvious constraints to be solved exactly.
For bipartite graphs, König's theorem (1931) gives a min–max formula: the maximum size of a matching equals the minimum size of a set of vertices meeting every edge. In general graphs this fails already for a triangle, where a single edge is a maximum matching but two vertices are needed to meet all three edges. Jack Edmonds' paper Paths, trees, and flowers (1965) gave both a polynomial-time algorithm for maximum matching in general graphs, the blossom algorithm, and, as a by-product of its analysis, the correct min–max theorem for general graphs.
Timeline.
A graph is a finite set of vertices and a finite set of edges, each edge meeting exactly two distinct vertices, its end-points. Several edges may join the same two vertices; this is needed because shrinking creates parallel edges. A matching is a set of edges no two of which meet the same vertex; a vertex is exposed if it meets no edge of . "Maximum" refers to cardinality.
An odd set is a set of vertices with an odd number of elements. Its capacity is
A one-vertex set covers the edges meeting its vertex; a set of vertices covers the edges with both end-points in it. An odd-set cover is a family of odd sets such that every edge is covered by some member, and its capacity-sum is .
The proof uses the following objects of §3–§4 of the paper. An alternating path is a simple path whose edges alternate between and the non-matching edges . An alternating tree is a tree whose vertices are split into inner and outer vertices, every edge joining an inner to an outer vertex and every inner vertex meeting exactly two tree edges; it is planted if restricted to the tree is a maximum matching of the tree whose one exposed vertex (the root) is exposed in , and Hungarian if its outer vertices are adjacent only to its inner vertices. A blossom is an odd circuit on which is a maximum matching, leaving one vertex exposed; with a stem (an alternating path from an exposed vertex ending in a matching edge at ) it forms a flower. Shrinking a vertex set replaces it by a single vertex , deletes the edges inside and keeps all other edges; and denote the result for a blossom .
It is stated as: there are a maximum matching and a minimum odd-set cover with .
The matching-duality theorem gives a certificate of optimality: a matching and an odd-set cover of equal size prove each other optimal, and the blossom algorithm produces both. It is equivalent to the Tutte–Berge formula , it contains König's theorem as the case where all members of the cover are singletons, and it is the cardinality case of Edmonds' description of the matching polytope by odd-set constraints, which underlies weighted matching, -matching and the polyhedral approach to combinatorial optimization.
The theorem has been proved since 1965, with several independent proofs (via Tutte's theorem, via the Gallai–Edmonds decomposition, via linear programming). Mathlib contains Tutte's perfect-matching theorem for simple graphs, but neither the Tutte–Berge formula nor odd-set covers, alternating trees, blossom shrinking or Berge's augmenting-path theorem in a multigraph setting. This mission produces a machine-checked version of Edmonds' statement together with the lemmas of his algorithmic proof (4.12, 4.14, 4.15, 4.17), which are the correctness core of the blossom algorithm.
Weak duality and Berge's theorem are elementary. The difficulty is the strong direction. The obvious argument, a search for augmenting paths from an exposed vertex, fails because an alternating search tree in a non-bipartite graph can close an odd circuit, after which a vertex is reachable both by an even and by an odd alternating path; a naive search either misses augmenting paths or must back-track exponentially. The proof therefore has to work in shrunken graphs, whose vertices are nested sets of original vertices, and transfer maximality and covers back through every shrinking (4.12–4.15). Keeping track of nested blossoms, of the identity of edges under shrinking and of the parity bookkeeping of 5.8 is the main formal burden.
EdmondsMatching65.Polyhedron.Graph V E (a map from edges to unordered pairs of distinct vertices) with finite V, E; parallel edges are allowed and loops are not. Matchings are Finset E. Maximum and minimum are by cardinality, stated with explicit comparisons rather than sSup/sInf.Finset (Finset V); repeating a member only adds capacity, so this does not change the minimum. The capacity of a singleton is , not .Reusable beyond this mission: the multigraph shrinking construction, blossom sets, alternating and Hungarian trees, and Berge's theorem in the multigraph setting; these are shared with the companion mission on the invariance of the dual (Gallai–Edmonds). Proofs of any milestone, and alternative proofs of the goal (e.g. through Mathlib's Tutte theorem), are welcome.
Stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto in 1991, is the standard method for multistage stochastic linear programs with many stages, such as hydro-thermal scheduling and long-term energy planning. It approximates each stage's expected future cost from below by the maximum of finitely many linear functions (cuts), built from LP dual solutions at sampled states, and alternates a forward simulation pass with a backward cut-generation pass. Practitioners stop the method when a simulated upper bound is close to the lower bound . Whether this procedure converges at all is the question of this mission.
Timeline:
There are stages. Stage has a decision in , costs , a matrix and, for , a matrix coupling to the next stage. At stage the constraint is . For the right-hand side is random: , where takes values with probabilities , independently across stages. The expected cost-to-go is defined backwards from :
and is the problem [LP1]. Assumption (A4) says every stage problem met along the way has a nonempty, bounded feasible region.
The approximate problem [AP] replaces by over the cuts generated before iteration ; its value is . A scenario fixes one outcome per stage . Each DOASA iteration (i) samples one forward scenario and solves [AP] along it, giving states ; (ii) for runs the Cut Calculation Algorithm (CCA): it solves [AP] at for the outcomes in a backward sample , stores optimal extreme-point dual solutions in a collection , picks for every outcome the best stored dual, and averages them into a new cut on . DOASA-N instead traverses a fixed list of scenarios in every iteration.
If, with probability 1, every scenario prefix is followed by the forward pass jointly with each outcome being in the backward sample infinitely often (property J), then with probability 1 every DOASA run has an iteration after which the cuts no longer change, the policy they induce is optimal for [LP1], and
The theorem justifies SDDP, AND, ReSa and CUPPS as exact methods: on a finite scenario tree, sampling-based cutting-plane schemes reach an optimal policy and a tight lower bound after finitely many iterations, almost surely. The finiteness argument (Lemma 1) is the template for later finite-convergence proofs of SDDP variants.
The paper's proofs are informal. No part of this development is machine-checked, and the printed statement of Theorem 4 is false (see below), so a formal proof also settles exactly which sampling hypothesis is enough. The finite-cut lemma and the cut-validity milestone are reusable for any Benders-type multistage method.
The obvious argument goes: cut sets stabilize (Lemma 1), and every scenario and every outcome is sampled infinitely often, so the limiting cuts must be exact. The last step fails. A cut at a state is exact only if, for every outcome, a dual that is optimal at that state has been collected. Sampling the forward scenario and the backward outcomes infinitely often, but separately, does not ensure this. Lemma 1 itself is also delicate: the dual vectors grow in dimension with , so the collection of extreme-point duals can be infinite even though the cut coefficients take finitely many values. The algorithm's choices (extreme-point duals, ties among best duals) must be handled for every run, not for a convenient one.
Stages are numbered with variable dimensions per stage. B t is the paper's , the matrix multiplying in stage . Value functions are real infima, used only on reachable states. Iterations are numbered from in Lean. Explicit choices, each recorded in the item statements:
A trivializing encoding, in which cuts are arbitrary valid hyperplanes, duals are taken for all outcomes, or the sampling hypotheses directly assume exactness of the cuts, is ruled out: the run relation transcribes CCA steps 1–3 as printed.
A complete development needs LP weak and strong duality (published on the platform as LinearOptimization.lp_weak_duality and LinearOptimization.lp_strong_duality, in their own encoding), finiteness of the set of extreme points of a polyhedron, and the almost-sure intersection of finitely many events (Mathlib). Contributions to any milestone, to the proof that J holds for independent sampling, and to the counterexample showing FPSP and BPSP are insufficient are welcome.
The number of successes in many rare trials is approximately Poisson. For independent trials the quality of that approximation was quantified by Le Cam in 1960: if are independent Bernoulli variables with , and , the total variation distance between the law of and the Poisson law with mean is bounded by a constant multiple of , and by a constant multiple of when . Many applications have dependent trials: occurrences of a pattern in a sequence, exceedances of a high level by a stationary process, failures in a system with local interactions. L. H. Y. Chen's 1975 paper extended Charles Stein's method of normal approximation to the Poisson case and obtained explicit bounds for dependent trials. The approach became known as the Stein–Chen method, and is now the standard tool for Poisson approximation of dependent counts.
Timeline.
This mission formalizes the order- bound of that paper, Theorem 4.2.
Let be a probability space and let be Bernoulli trials: random variables with values in and . Following the paper, set for and . Put
For a bounded real function on the nonnegative integers, the Poisson expectation is
the mean of under the Poisson law with parameter . The quantity of interest is for all with . Its supremum over such is twice the total variation distance between the law of and the Poisson law.
Dependence is measured by Ibragimov's mixing condition (4.1). Let . There must be a non-increasing sequence such that for all and every event ,
A sequence is -dependent when and are independent for all . It then satisfies (4.1) with for .
The proof works with the partial sums , , and . It also uses the Stein solution , the solution for of .
For every and every with ,
The bound involves only the law of through , the success probabilities, the window and the mixing rate. The window is free, so the statement covers every trade-off between local dependence and mixing.
The milestones follow the paper's proof:
Theorem 4.2 gives an error of order times the excess variance , plus a mixing remainder. When the trials are nearly uncorrelated, and the bound is small even though is large. This is the regime where the companion Theorem 4.1, which carries a factor , is weaker. The independent case recovers Le Cam's order with constant 10. The -dependent case gives explicit Poisson limit theorems for scan statistics and pattern counts.
All results of the paper are proved there, and the proofs are elementary apart from the measure theory of Lemma 4.1. To our knowledge none of them has a machine-checked proof. Mathlib has the Poisson distribution and conditional expectation, but no Stein–Chen bound and no mixing inequality of Ibragimov's type. A formal proof would give the first checked quantitative Poisson approximation for dependent trials. It would also give reusable covariance inequalities for -mixing sequences (Lemmas 4.2 and 4.3).
Most of the work is bookkeeping, and it is heavy. Identity (2.2) needs a telescoping over windows whose ends can fall outside . (4.15)–(4.18) need to be compared with with explicit constants.
The genuinely probabilistic step is the decoupling of Lemma 4.2. Condition (4.1) controls conditional probabilities of events. Lemma 4.2 needs a bound on conditional expectations of functions of a whole random vector. Passing from one to the other requires a regular conditional distribution that is uniformly close to the unconditional law on a set of full measure (Lemma 4.1). The naive route, applying (4.1) to each level set of a simple function, loses a factor that grows with the number of levels and does not give the constant .
The bound (4.16) applies Lemma 4.4 to a subsequence of the trials. This uses the fact that dropping variables preserves (4.1) with the same , because is non-increasing.
A trivializing formalization is ruled out. Measurability of the trials is part of the definition, because otherwise conditional expectations in (4.1) collapse to . The goal mentions only , , , , , and . It does not mention or any milestone quantity.
A complete development needs the Stein solution and its bounds, a Bernoulli-sum calculus over integer
windows, regular conditional distributions on standard Borel spaces, and the mixing covariance
inequalities. The last two are reusable beyond this mission. Contributions to any milestone are
welcome, as are alternative proofs of Lemma 4.2 through Mathlib's condDistrib.
Sampling uniformly from a bounded region can be difficult when direct transformation of a familiar random variable is unavailable and rejection sampling spends most of its trials outside the region. Robert L. Smith studied procedures that move within the region: from the current point, choose a direction, form the line set through that point inside the region, and choose the next point uniformly on that line set. The resulting sequence is a homogeneous Markov chain. The Random Directions Algorithm, later commonly called hit-and-run, is a central instance of this construction. Smith's 1984 paper establishes conditions under which the chain approaches the uniform distribution even when its initial point is fixed rather than sampled uniformly (Smith 1984, pp. 1298–1301).
For simulation, the initial point is usually chosen because it is known to be feasible. The question is therefore whether the distribution after many moves forgets that particular choice. A stationary distribution alone does not answer this: stationarity describes what happens if the chain already starts with that distribution. Smith's Theorem 2 gives the stronger, pointwise starting-state statement for the class of symmetric mixing algorithms satisfying his two regularity assumptions (Smith 1984, p. 1301).
Let be the state region and its finite, nonzero content measure. In Smith's geometric setting, is a bounded -dimensional measurable region in , and is -dimensional content; at , content is counting measure. A Markov transition kernel assigns to every current point a probability of entering a measurable set on the next move. For the associated chain , the -step transition probability is .
The uniform law is . Smith's Assumption (a) gives a measurable transition density relative to :
For a symmetric mixing algorithm, the paper states that this density satisfies for all . Assumption (b) says for all such pairs. These are pointwise conditions, including states of zero -measure. A nonempty measurable set is closed if for every . The chain is indecomposable in the paper's sense when it has no two disjoint closed sets (Smith 1984, pp. 1299–1300).
Lemma 1 asserts that is stationary: for every measurable . Lemma 2 excludes two disjoint closed sets. Both are direct prerequisites of the goal. Smith's Theorem 1 also establishes uniqueness of the stationary distribution and almost-sure convergence of empirical visit frequencies under a stationary start; it is described in the source, but its trajectory-level formalization is outside this proposal (Smith 1984, p. 1300).
The mission goal is Smith's Theorem 2. For every and every measurable ,
This is the paper's explicit meaning of strongly mixing. The milestone list also records the proof's stated nonperiodicity condition: for every , the -step transition law has no two disjoint closed sets. It is a target in its own right because it concerns all higher-step kernels, not only the one-step chain (Smith 1984, p. 1301).
Theorem 2 makes the uniform law the limiting distribution of the sample at time , for any fixed feasible initial point. The paper's Theorem 1 supplies a different guarantee about long-run empirical frequencies under a stationary start, although it is not a target of this proposal. Smith later specializes the framework to the Random Directions Algorithm and gives a quantitative rate under additional geometric conditions; that rate is the subject of the companion mission (Smith 1984, pp. 1303–1304).
These results are proved in the paper but the declarations in this proposal are theorem statements with sorry, not machine-checked proofs. A completed formalization would turn the paper's measure-theoretic claims into reusable statements about general measurable state spaces and kernels. The normalized content law, the density interface, and closed-set predicate can be reused when studying other Monte Carlo kernels with the same hypotheses.
The main obstacle is the jump from stationary behavior to convergence from every starting point. Symmetry identifies the candidate stationary law, and strict positivity limits how the chain can split into closed parts, but neither sentence by itself establishes the claimed limit of . The distinction matters especially at starting points in -null sets: an almost-everywhere starting-state result would leave out precisely the universal claim in Theorem 2. The paper appeals to a general-state Markov-chain convergence result for this step (Smith 1984, p. 1301).
Lean uses a measurable type as the whole region , a finite measure with , a Markov kernel , and an extended-nonnegative density . The density is jointly measurable and is linked to by the integral identity above; symmetry is pointwise, and positivity is added only for Lemma 2 and Theorems 1–2. This abstract representation retains the hypotheses those results use without fixing a particular Euclidean dimension. It covers the counting-content case as well as continuous content, although it does not construct the geometric direction-and-chord algorithm. The Random Directions kernel belongs to the companion mission.
The uniform law is normalized by . Finiteness and nonzero total content prevent a meaningless inverse or an empty probability space. The -step law is the published MarkovChainCLT.iterKernel. Theorem 2 quantifies over every , rather than -almost every , and uses setwise convergence on each measurable . No invariance, uniqueness, minorization, or convergence premise is added to the goal. Detaching from would empty out the substantive assertion. Formal contributions can target the density-to-invariance argument, the closed-set conditions, and the general-state convergence theorem needed for the goal. The paper's separate pathwise Theorem 1 remains an appropriate later extension.
Convex minimization often has a simple objective but no useful closed form for its minimizer. A proximal method replaces one difficult minimization by a sequence of regularized minimizations. The familiar quadratic regularizer treats all directions through a Euclidean norm. In applications with nonnegative variables, entropy-like geometry can be more natural: a step can be penalized by a Bregman distance generated by a strictly convex function. Chen and Teboulle studied a proximal minimization algorithm with this geometry and established a rate in objective values together with convergence of the iterates under the paper's assumptions. Their analysis also removed a bounded-below assumption used in an earlier treatment and allowed step sizes whose sum diverges even if individual steps approach zero (Chen and Teboulle, 1993, pp. 539–540).
This mission records the complete theorem of that paper, rather than only its rate when a minimizer is known to exist. The distinction matters because a proper convex objective can have an infimum of or a finite infimum that it never attains. The rate against each comparison point remains meaningful in those cases, and the theorem's value convergence does not presuppose a minimizer.
Let be a finite-dimensional real normed space, the nonempty effective domain of a proper lower semicontinuous convex objective, and its finite restriction. Its value outside is . Thus is an extended-real number that may equal , and is the set of minimizers, possibly empty.
A Bregman function with zone is a function on the closure of an open set . It is continuously differentiable on , strictly convex and continuous on , and satisfies the bounded partial-level-set and two sequential conditions of Definition 2.1 (Chen and Teboulle, 1993, p. 539). Its distance-like expression is
It is nonnegative and zero exactly when , but need not be symmetric or satisfy a triangle inequality. The zone contains the relative interior of . Starting from and positive steps , a PMD run selects minimizing over , for . Write . The paper calls this proximal minimization with D-functions (Chen and Teboulle, 1993, pp. 539–540).
For every and every finite comparison point , the goal includes
If , then in the extended reals, including when . This is Theorem 3.4's inequality (20) and its ensuing value-convergence claim (Chen and Teboulle, 1993, p. 542).
For every , the same rate gives
When and , the entire sequence converges to a point of . The displayed bound is (21), and convergence of the iterates is the final clause of Theorem 3.4. The milestone list follows the authors' statements: the three-point identity, nonnegativity of the distance, Lemma 3.2, and the three parts of Lemma 3.3. Display (17) is an additional supporting theorem item (Chen and Teboulle, 1993, pp. 539–542).
The rate compares a PMD iterate with any admissible point, so it gives a finite-horizon certificate even before an optimal point is identified. If a minimizer exists, substituting it gives an explicit objective-gap bound. With divergent cumulative steps, the theorem identifies the limiting objective value without assuming that value is finite. Its final clause goes further: when the optimum is attained, the points themselves converge, not merely their objective values (Chen and Teboulle, 1993, p. 542).
The mathematical result was proved in 1993. The formalization task is to state and prove it in Lean with the extended objective, full Bregman-function conditions, and sequence limits visible to later developments. The three-point identity is already posed as a separate public platform theorem from a later mirror-descent treatment; this mission reuses that statement. The remaining statements here are proof obligations, not claims of completed machine-checked proofs. Their definition layer can also support analyses of other nonquadratic proximal algorithms.
The direct one-step minimization comparison alone does not yield the global estimate with and the exact weighted distance terms of Lemma 3.3(iii). It also does not settle convergence of the points: decreasing objective values can coexist with several cluster points. The Bregman function's bounded partial level sets and sequential conditions are needed to rule out that behavior. A further issue appears when : replacing the infimum by a real number, or assuming a minimizer to define it, removes a case that Theorem 3.4 explicitly covers. The original paper separates these issues across Lemmas 3.2–3.3 and Theorem 3.4 (Chen and Teboulle, 1993, pp. 540–542).
Lean uses a finite-dimensional real normed space in place of ; none of the statements depends on a chosen Euclidean inner product. A derivative is a continuous linear functional, and its value on a vector represents the paper's gradient pairing. The Bregman distance is the already-published definition with the derivative at its second argument. The paper's is represented by a total function whose values outside are unused. Strict convexity on includes convexity of . The last sequential condition explicitly requires its first arguments to lie in , the domain where the paper defines .
The extended objective is a nonempty convex domain , a real-valued restriction , and an extended-real function equal to off . Lower semicontinuity applies to that extended function. The infimum is taken in the extended reals; it cannot silently become zero when the values are unbounded below. A PMD run is a predicate on an existing sequence, recording a minimizer in at each step. This makes explicit the existence consequence for which the paper assumes the gradient of has full range; it does not define iterates by a choice operator. Every Bregman distance differentiates at a point of , where is . The rate starts at , so and no finite value is demanded of . No lower bound on is imposed. Contributions proving the milestone inequalities, the extended-real value limit, the Bregman-function examples, and the compactness step for iterate convergence are within scope.
The number of successes in many rare, roughly independent trials is approximately Poisson. This law of small numbers is used for counts of rare events in reliability, insurance, epidemiology, queueing and random combinatorics. A quantitative version says how large the error is. For independent Bernoulli trials with success probabilities and , Le Cam (1960) showed that the error in total variation is of order . When all are small this tends to zero, but it does not say what the leading part of the error is.
L. H. Y. Chen's 1975 paper (Ann. Probab. 3, 534–545) adapted Charles Stein's method for normal approximation to the Poisson case. The result is now called the Stein–Chen method. The paper's §2–§4 give first-order error bounds for dependent (mixing) trials. Its §5, "A refinement", goes one order further for independent trials. It identifies the first-order correction explicitly and shows that what remains is of order . Kerstan (1964) had obtained a similar expansion by a different method. Chen's version comes from iterating the basic identity of the Stein–Chen method. This mission formalizes §5.
Timeline:
Let be independent random variables on a probability space, each taking only the values and , with success probabilities . Put
For a bounded real function on the nonnegative integers, the Poisson expectation is
the mean of under the Poisson law with parameter . The Stein equation is . For its solution is
Write and . Chen's second-order operator is
For another parameter , and apply the Stein solution and the operator with parameter to the function .
In Lean: poissonExp, stein, delta, shiftL, stU, prob, lam, lamExcept, W, Wi, all in the namespace PoissonDepTrials.SecondOrder.
If are independent, and , then for every with ,
The paper writes the constant as "an absolute constant not greater than ". The formal goal fixes at that value, which is the same statement.
In order: the Stein solution (2.3)/(2.5); the difference identity (3.6); Lemmas 3.1, 3.2, 3.3 and 3.5 (bounds on and ); the first-order identity (5.8) ; Lemmas 5.1 and 5.2 (dependence of Poisson expectations on the parameter); Lemmas 5.3–5.5 (bounds on , and ); the bound (5.9),
and the closing inequality .
The theorem gives an explicit first correction to the Poisson approximation of a Poisson-binomial law, with a remainder of the next order. When all equal , the first-order error is replaced by the remainder , which is smaller by the factor . The correction term is a functional of the Poisson law alone, . It can be evaluated without knowing the distribution of . The method of proof applies the basic identity twice. The paper notes that further iteration gives expansions to any order.
On the formal side, Mathlib has the Poisson distribution but no Stein–Chen machinery and no quantitative Poisson approximation. The theorem has, as far as is known, no machine-checked proof. This mission produces the Stein solution and its standard bounds (Lemmas 3.1–3.5), which are reusable by any Stein–Chen argument. It also produces the parameter-perturbation estimates of Lemmas 5.1–5.2 and a complete second-order expansion. Missions 1 and 2 of this series formalize the first-order bounds of §4 under a mixing condition. They share the Stein-solution layer.
The first-order bound needs only that is uniformly small (Lemma 3.4). A second-order bound needs more. After the first application of the identity, the error has to be expanded again. That requires control of the iterated operator with a different parameter , because is approximately Poisson with mean , not . The bound on (Lemma 5.5) grows linearly in . Applying the uniform bounds of §3 throughout loses a factor and produces an error of order instead of . The linear growth has to be paired with the variance of . The averaging over pairs in the final step uses the condition , which keeps every comparable to .
Conventions committed to in Lean:
X : ℕ → Ω → ℕ. Each is measurable with values in almost surely. for and , which is the paper's own padding convention (p. 535). Independence is iIndepFun (fun i => X i) P over all of ℕ. Because the padding variables are constants, this is equivalent to independence of .Hypotheses added relative to the page, each disclosed in the item's Formalization Note:
The random indices that the paper introduces to shorten notation in (5.8)–(5.9) are not formalized. The same quantities are written as finite sums over indices.
Ruled out: the second-order term must be the operator built from the Stein solution exactly as on p. 543. A free function, or evaluated at the junk value , would empty the theorem.
Welcome contributions include: