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.
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?
The newsvendor problem is the basic model of stocking under uncertain demand: an order quantity is fixed before a random demand is observed, and every unit short or left over is penalized. Its solution is a quantile of the demand distribution. In practice that distribution is unknown and only a sample of past demands is available. The standard remedy, sample average approximation (SAA), replaces the expectation by the empirical average over the sample and orders the corresponding sample quantile. The practical question is how many observations make the SAA order nearly as good as the true optimum, without assuming anything about the demand distribution.
Levi, Roundy and Shmoys (Math. Oper. Res. 32(4), 2007) gave the first distribution-free answer, using Hoeffding's inequality. Levi, Perakis and Uichanco (Oper. Res. 63(6), 2015) improved it with Bernstein's inequality. The improvement matters most when the service level is high, which is the typical case in inventory practice. This mission formalizes that improved bound, Theorem 2 of the 2015 paper.
A retailer orders units before a real demand with law and cdf is realized. Unmet demand costs per unit (underage cost) and unsold stock costs per unit (overage cost). The expected cost is
which is finite when . The critical quantile is , and it minimizes .
An order is -optimal when its relative regret is at most , i.e. . The set of such orders is . The function is convex with one-sided derivatives
The LRS interval is
Given an i.i.d. sample from , the empirical cdf is , and the SAA solution is the sample quantile
It is a random variable through the sample.
For every demand law with , every and every ,
The earlier LRS bound has the exponent . Theorem 2 replaces the square by the first power. When the critical ratio approaches (high service levels), is small, and the required sample size drops accordingly. Raising the service level from 95% to 99% multiplies the sample size the LRS bound requires by 25, but the sample size Theorem 2 requires only by 5 (p. 9). The bound holds for every demand distribution, with no density, continuity or support assumption.
The milestones are reusable on their own. One is the one-sided derivative formula for the expected newsvendor cost. Another is Bernstein's inequality for i.i.d. bounded variables, which Mathlib does not have; it has Hoeffding's inequality. The third is a distribution-free concentration statement for sample quantiles. The result is proved in the paper. To our knowledge none of these statements is formalized; this mission produces machine-checked versions.
A Hoeffding-type argument yields only the squared dependence on . The improvement needs the variance of the indicator , which is small near extreme quantiles. Bernstein's inequality applies at a fixed point . The sample quantile, however, is random, and can jump. The event that falls left of the target quantile therefore has to be reduced to deviations of at deterministic points, with care at atoms of , where and differ. The final step from the derivatives to the relative regret requires convexity of and a lower bound on that holds for every distribution.
μ on ℝ, with no sign restriction (the page's plays no role here). is Mathlib's cdf μ, and is μ (Set.Iio q). The realized cost is the published InventoryControl.newsboyLoss h b q d, and is a Bochner integral. Every statement that evaluates assumes Integrable id μ (). This is the standing assumption under which is an expectation. It also rules out the trivializing formalization in which a non-integrable cost integrates to and every order is -optimal.sInf) of sets that are nonempty and bounded below under the hypotheses, never argmins or choice functions. The sample is x : Fin N → ℝ under the product measure Measure.pi (fun _ => μ), with ; the indices are 0-based.A complete development needs the following:
The Bernstein inequality and the sample-quantile concentration are useful beyond this mission. Contributions to any milestone are welcome.
The linear complementarity problem asks, for a real square matrix of order and a vector , for a vector with
It is the common form of the Kuhn–Tucker conditions of linear and convex quadratic programs and of the equilibrium conditions of two-person non-zero-sum (bimatrix) games. In 1964 Lemke and Howson gave a constructive existence proof for equilibrium points of bimatrix games by following a path of adjacent extreme points of a polyhedron (Lemke–Howson 1964). In 1965 Lemke adapted that path-following technique to the general problem above, under a condition on that covers the positive semidefinite case treated by Dantzig and Cottle and the case (Lemke 1965). The resulting procedure, now called Lemke's algorithm or complementary pivoting, became a standard method for linear complementarity problems and a template for later path-following existence proofs (Cottle, Pang, Stone 1992).
Timeline:
Fix a finite index set of size , a real matrix and . Inequalities between vectors are componentwise and is the all-ones vector.
Suppose is non-degenerate and that for every
Then
The Corollary (p. 5: , gives an odd number of equilibrium points), Theorem 3 (p. 5: if for all , at most one equilibrium point) and Theorem 5 (p. 8: if moreover , has at least rays).
Theorem 4 is an existence theorem for a class of linear complementarity problems that contains convex quadratic programming (the case for all ) and strictly positive matrices, and its proof is an algorithm: the path followed is the sequence of pivots of Lemke's method. The parity statements (Theorem 2, the Corollary) are an early instance of the path-following parity arguments later abstracted in the complexity class PPAD (Papadimitriou 1994).
The theorem is classical and proved. To our knowledge neither Lemke's theorem nor the polyhedral path machinery of Theorems 1–2 has a machine-checked proof in Lean or Mathlib. This mission produces the vocabulary of non-degenerate complementarity polyhedra (the matrix , open edges, rays, adjacency paths), the parity theorem, and the existence theorem itself; the Farkas-type Lemma 2 (p. 4) is already available on the platform.
The algebraic part (Lemma 3 and (22)–(25)) is short. The difficulty is combinatorial-geometric: Theorem 1 requires that, under non-degeneracy, every extreme point of has exactly incident edges, that each point of is an extreme point or lies on an open edge, and that the edges contained in form paths whose end-points are exactly the equilibrium points; the parity of Theorem 2 then needs finiteness of the set of extreme points. None of this polyhedral structure (edges as zero-pattern classes, their closures and end-points) is in Mathlib. Moreover, the printed proof of Theorem 4 applies Theorem 2 to , whose non-degeneracy the paper obtains from an informal perturbation remark, and it sketches the step from the end of the augmented path to a ray of ; a complete proof of the goal must supply these steps or take another route.
Contributions welcome: the polyhedral lemmas for non-degenerate (extreme points have edges, finitely many extreme points), the parity argument, and any complete route to Theorem 4.
A birth-and-death process describes a population in which each individual independently gives birth and dies at given rates. Kendall's 1948 paper (doi:10.1214/aoms/1177730285) solved the process with arbitrary time-dependent rates and, in its §4, introduced a second random variable alongside the population size: the cumulative population , the number of individuals that have ever been alive up to time . Kendall gives two readings. If is the number of current cases of a disease, is the total number of cases recorded so far, and for an epidemic that is almost certain to die out, measures its overall severity. If is the viable count of a bacterial population, is the total count, in which living and dead organisms are not distinguished.
The question of this mission is the exact distribution of for the simplest transient process, with constant rates. Kendall answers it in §5 by solving a first-order partial differential equation for the joint generating function of . The resulting law involves central binomial coefficients, the same numbers that count the total progeny of a critical binary branching process.
Let and be constants. In the simple birth-and-death process with these rates, a population of size moves to at rate and to at rate . It starts from one ancestor, . The cumulative population starts at and shares all the positive jumps of , so it never decreases. The process is transient (dies out with probability one) when .
Write for the joint law of and
for its generating function (30). Kendall shows that satisfies
and solves it with the roots of the quadratic (49), :
Setting forgets , so generates the law of . Finally
The Lean names are disc, alpha, beta, psi, x, Q and SolvesPDE, in the namespace KendallBD.Cumul.
For :
The result. The law (52) gives the full distribution of the total size of a transient linear birth-and-death population, not only its moments: the probability that the ancestor dies childless, the tail behaviour, and the dichotomy between the subcritical case (finite mean , geometric-type tail with ratio ) and the critical case (heavy tail, infinite mean). In the epidemic reading this is the distribution of the final size of a minor outbreak; it is also the total-progeny law of the embedded binary Galton–Watson tree (Harris 1963).
Formalizing it. The result is classical and proved, but it is not formalized anywhere known to this mission. A formal proof would combine three separate pieces: the explicit solution of a first-order PDE by characteristics, checked as a classical solution on the region where a probability generating function lives; a limit that selects one root of a quadratic; and the binomial series of together with its boundary value at . The companions make the moments (48), which §4 derives by a separate route, a consequence of the law.
Checking that (50) satisfies (31) is calculus once the derivatives exist. The obstacles are elsewhere. First, the roots must be ordered as , which fails at when (the roots are then and ): every statement about , , has to be made for , and the law is identified from the power series on that interval. Second, the normalization is a statement at the boundary of the series for ; at this is , the edge of the disc of convergence, where convergence of the series is not automatic and where the value uses . For the same series sums to , so the hypothesis is essential. Third, the asymptotic in the balanced case needs the asymptotics of central binomial coefficients.
All objects are real functions; the process and the joint law are not constructed, exactly as in the paper. "The law of " is read, as on p. 11, as the coefficients of the generating function , and is tied to the process through the equation (31) and the boundary condition (32). The committed conventions are:
Real.sqrt the nonnegative root;SolvesPDE: both partial derivatives exist as HasDerivAt facts and satisfy the equation, never an equation between deriv values;A goal that only asserted the power series identity would be a different and easier theorem with no birth-and-death content; the goal therefore ties to of (50) and to the equation (31)–(32).
A complete development needs the binomial series for with real coefficients (Mathlib has Nat.centralBinom and general binomial series, and the platform has the generating function of the central binomial coefficients as a proof tool), the boundary behaviour of a power series with nonnegative coefficients, and Stirling-type asymptotics of . These are reusable well beyond this mission. Contributions proving any milestone or companion, or the series lemma on its own, are welcome.
Every pure integer program can be relaxed, by dropping the nonnegativity of the basic variables of an optimal linear-programming basis, to a problem over a finite Abelian group: find nonnegative integers , one for each nonzero group element, with . R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969) 451–558) studies the convex hulls of the solutions of these group equations, the corner polyhedra, and the master polyhedron that contains all of them as faces. These polyhedra are the source of the group-theoretic approach to cutting planes: their faces are valid inequalities for every integer program with the same group, and their vertices are the candidate optimal solutions of the group relaxation.
The paper's first section shows that every vertex of such a polyhedron is an irreducible solution, and remarks (p. 460) that the converse fails in general: a typical group has many irreducible solutions that are not vertices. Section 3F identifies a family of groups where the two notions coincide, which is what makes the vertices of these polyhedra countable in closed form.
Let be a finite Abelian group written additively, with zero , and . For the group equation is
The master polyhedron is the convex hull in of its nonnegative integer solutions (for the solution is excluded). A vertex is an extreme point of .
A nonnegative integer vector is irreducible if any two integer vectors with and are equal. A finite set of group elements is independent if with integers forces for each .
The groups of §3F are those in which every nonzero element has order 2, the groups , or every nonzero element has order 3, the groups .
If every nonzero element of has order , with or , and , then for every nonnegative integer solution of the group equation
and the support of such a vertex is an independent set.
THEOREM 23 turns a polyhedral question into a combinatorial one for the elementary Abelian 2- and 3-groups: the vertices of are read off from independent subsets of the group and residues below . Gomory uses this on pp. 506–507 to count all vertices of all exactly and to derive their asymptotic number. It also marks the boundary of the general picture: groups with elements of other orders have irreducible solutions that are not vertices.
The result has been proved since 1969; no machine-checked proof exists. The mission produces a Lean statement and, once solved, a verified proof of the theorem together with the general fact that vertices of the master polyhedron are irreducible, a reusable layer for the other group-polyhedron results of the same paper. Two sentences of the printed proof (p. 506) are false as written (see Formalization scope); formalization records their corrected forms.
The direction "vertex irreducible" holds in every group and is a midpoint argument. The difficulty is the converse: showing that an irreducible solution cannot be written as a proper convex combination of other solutions, which are infinitely many and unbounded. The natural route, exhibiting a linear objective that uniquely minimizes, does not work with the objective printed on the page: solutions with the same support as but larger entries are tied with it. The argument must control those solutions through the arithmetic of residues modulo , and this is where the exponent 2 or 3 is used; the analogous residue statement fails for .
{g : G // g ≠ 0}; integer solutions are -valued and cast to ; vertices are Set.extremePoints ℝ of the convex hull of the cast solutions.convexHull, extremePoints_convexHull_subset), and finite sums in Abelian groups. Contributions welcome: any of the milestones, and a general lemma that a unique minimizer of a nonnegative linear function over the integer solutions is a vertex.A Markov decision problem with the average reward criterion asks for a policy that maximises the long-run reward per period of a controlled finite Markov chain. It is the standard model for repeated operational decisions with no natural horizon: inventory replenishment, machine maintenance, queue admission and routing. For finitely many states and actions, Howard (1960) and Blackwell (1962) showed that a pure stationary average optimal policy exists, and policy iteration finds one.
Linear programming formulations are older for the discounted problem (d'Epenoux, 1960) and for chains with a single recurrent class (Manne, 1960). Without a structural assumption, a stationary policy can split the state space into several recurrent classes, the multichain case, and the gain becomes a vector rather than a number. Denardo and Fox (1968) gave a linear programming approach for this case. Hordijk and Kallenberg (1979) showed that a single pair of dual linear programs suffices: an optimal policy can be read off an extreme optimal solution of the dual program. Kallenberg's tract (1983, Chapter 4) is the systematic account of this theory, and this mission formalizes its §4.2–4.4.
Let be a finite set of states. Each state has a nonempty finite set of actions, a reward for each action, and transition probabilities with . A policy chooses, at each epoch , a probability distribution on that may depend on the whole history. A stationary policy uses fixed weights at every epoch. A pure stationary policy always plays . Write , , and , in the pure case.
The average reward of from state is
and is the same expression with . The AMD-value-vector is , where ranges over all policies, and is average optimal if . A policy is Blackwell optimal if it maximises the discounted reward for all discount factors in some interval .
For a stochastic matrix , the stationary matrix is the Cesàro limit of , and the deviation matrix is . For a pure policy, and .
A vector is AMD-superharmonic if some satisfies and for all , . For weights with , the primal program (4.2.10) minimises over such pairs. Its dual is
Write .
If is an optimal solution of (4.2.11) and an extreme point of its feasible set, then a decision rule with
exists, and every such is average optimal.
The goal is stated for every finite model, with no assumption on the chain structure, and for every rule-conforming .
Theorem 4.2.4 reduces the multichain average reward problem to one linear program. Combined with Theorems 4.3.3 and 4.3.4, every pure stationary average optimal policy arises from some extreme optimal solution, so enumerating extreme optimal solutions enumerates all of them (Remark 4.2.5). The same program is the starting point for the constrained average reward problems of §4.7, where a policy must also satisfy linear constraints on its state–action frequencies. Theorem 4.4.1 is the evaluation step of multichain policy iteration.
The results are proved in the tract and, earlier, in Hordijk and Kallenberg (1979). None of them is formalized in a proof assistant. The platform has machine-checked average reward results only for unichain models, where the gain is a scalar. This mission adds the multichain theory, with general history-dependent randomized policies as competitors, and also yields reusable statements about stationary and deviation matrices of finite chains.
Under a unichain assumption, the dual variables form a stationary distribution and the -variables are unnecessary, so the obvious argument reads a policy off alone. In the multichain case the -part of an optimal solution can vanish on whole sets of states, and on those states the policy must be read off . The argument then has to show that these states are transient under the selected policy, which is where extremality is essential. For a non-extreme optimal solution the book passes instead to the randomized policy (4.3.1), which needs the separate argument of Theorem 4.3.3. A second obstacle is that optimality is against all history-dependent randomized policies, so the comparison of with must pass through the superharmonic characterisation (Theorem 4.2.2), whose proof uses the existence of a Blackwell optimal policy.
The model is the published MarkovDecisionProcesses.StationaryMDP: finite state and action types, a nonempty Finset of admissible actions per state, and stochastic rows. General policies are the published AvgHRPolicy (decision rules depending on the epoch and the full history). The criteria are the published gainInf, gainSup and optGainInf; all values are real. Average optimality is the book's lim inf notion, for every . It is not Puterman's stronger IsAverageOptimal. The stationary and deviation matrices are the published Cesàro limitMatrix and deviationMatrix. Their existence and invertibility (Theorem 2.4.1) are never assumed as hypotheses. LP variables are indexed by admissible state–action pairs, so Set.extremePoints is the book's notion of extreme feasible solution. Recurrence is the classical finite-chain notion: every state accessible from leads back to . The ergodic set of a recurrent state is the set of states accessible from it.
A formalization that assumes a unichain or ergodic model trivializes the mission (it reduces Theorem 4.2.4 to known unichain results). No statement here makes such an assumption, and the weights are strictly positive and sum to one, as in (4.2.10).
The proofs need finite Markov chain theory: the Cesàro limit, , , transience versus , and positivity of the stationary distribution on ergodic sets. They also need LP duality with complementary slackness and the existence of a Blackwell optimal pure policy. The last result is posed separately on the platform (Blackwell 1962, Theorem 5). LP duality is available as proved platform theorems (LinearOptimization.*), whose sign conventions must be matched. Contributions on the Markov chain layer are reusable across the whole series.
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.
A Markov decision chain with finitely many states and actions is the basic model of sequential decision making under uncertainty in operations research. Inventory control, maintenance, queueing control and many other problems reduce to it. Under the average reward criterion the decision maker optimizes the long-run reward per period. For the discounted criterion one linear program yields an optimal pure stationary policy (d'Epenoux 1960). For the average criterion, De Ghellinck (1960) and Manne (1960, DOI 10.1287/mnsc.6.3.259) gave linear programs for the unichain case, where every stationary policy has a single recurrent class. In a multichain model the optimal average reward may differ from state to state, and the unichain construction no longer applies.
Hordijk and Kallenberg (Management Science 25(4):352–362, 1979, DOI 10.1287/mnsc.25.4.352) proved that in the general multichain case an average optimal policy can be found by solving only one linear program. This mission formalizes that result, Theorem 7 of the paper, together with the chain of results its proof rests on.
Timeline, following the paper's introduction:
The state space is a finite nonempty set . In state a finite nonempty set of actions is available; choosing earns the reward and moves the system to state with probability (, ). A policy chooses actions at times , possibly at random and using the whole history. For a policy and an initial state ,
is the average expected reward, and is the optimal one. A policy is average optimal if for every . A decision rule picks in every state; is the pure stationary policy that always applies . Its transition matrix is and its reward vector . The α-discounted value enters through Theorems 1, 3, 4 and 5.
Fix weights with . The dual program has a variable pair for every state and every :
for all . Its linear programming dual, the primal program, minimizes over superharmonic pairs : and for all , . For a dual solution put .
Let be an optimal solution of the dual program that is an extreme point of its feasible set, which is what the simplex method returns. Let be any decision rule with
Then is average optimal: for every , the comparison running over all policies.
In the order the proof uses them:
Theorem 7 turns the multichain average-reward problem into one linear program and one pass over its solution. No unichain or communicating assumption is required, and neither the second linear program nor the search step of the earlier Denardo–Fox–Derman procedure is needed. The rule is local: any action with a positive -variable, otherwise any action with a positive -variable, gives an optimal policy. The paper's later results (Theorem 8, the correspondence between optimal dual solutions and optimal randomized stationary policies, and Theorem 10, on extreme points) build on the same program. Companion missions of this series formalize them.
The results are proved in the paper; no machine-checked proof of any of them is known. The formalization adds a machine-checked link between linear programming duality (complementary slackness, extreme points of polyhedra) and the limit theory of finite Markov chains (Cesàro limit matrices, transient states), over the history-dependent policy class of the published average-reward model.
The obvious argument reads off any optimal dual solution and uses complementary slackness to obtain and . The second equation holds only on , and outside nothing controls the reward of . The argument closes only when is transient under , so that the stationary distribution of ignores those states. Transience is not a consequence of optimality. It uses extremality: an ergodic set inside would make the corresponding -columns of the constraint matrix linearly dependent. For a general optimal solution the paper proves optimality only of a randomized stationary policy built from (its Theorem 8(b), a companion mission), not of a pure selection. The extremality hypothesis is therefore part of the statement.
Upstream of the linear program, Theorem 6 depends on Derman's theorem and Blackwell's expansion of the discounted value near . Both compare against all history-dependent policies and need the full limit theory of and .
The model is the published MarkovDecisionProcesses.StationaryMDP (finite nonempty S, finite A, nonempty admissible sets, stochastic transitions) with history-dependent randomized policies AvgHRPolicy. is gainInf (the lim inf of the average of the first expected rewards) and is optGainInf, a real supremum that is finite because rewards are bounded. and are the published limitMatrix and deviationMatrix; the identities of Theorem 2 are the published Blackwell Lemma 1(a), (d). Conventions:
IsAverageOptimal in the published file.totalReward. "α near enough to 1" means some such that the property holds on .Pair M), so the feasible set lies in (Pair M → ℝ) × (Pair M → ℝ) and its extreme points are those of the paper's polyhedron.Set.extremePoints). A goal without extremality is a different and unproved statement, and any version that quantifies over some instead of every obeying the rule is weaker than the paper's. Both are ruled out.IsRecurrent. Maxima over and are stated as an upper bound plus attainment, so that is part of Theorem 5.A complete development needs Cesàro limits of stochastic matrices, the deviation matrix, Abelian limits of discounted values, linear programming duality with complementary slackness, and the characterization of extreme points of by linear independence of the active columns. The last two are reusable well beyond this mission, as is the identification of gainInf of a stationary policy with . Contributions to any of them, including proofs of individual milestones, are welcome.
A Markov decision chain is a controlled Markov chain: in each state the controller picks an action, collects a reward and moves to a random next state with probabilities that depend on the state and the action. Under the average reward criterion, the long-run reward per step, an optimal policy can be computed by linear programming. For chains in which every stationary policy has a single recurrent class (the unichain case) this goes back to Manne (1960), de Ghellinck (1960) and d'Epenoux (1960): the variables of the dual linear program are long-run state–action frequencies, and the vertices of its feasible set are exactly the pure stationary policies.
In the general multichain case a policy may split the state space into several recurrent classes with transient states between them, and the frequency picture breaks down. Denardo and Fox (1968) and Denardo (1970) gave linear programs that require solving several programs in sequence. Hordijk and Kallenberg (Management Science 25(4), 1979) showed that one pair of dual linear programs suffices: from an optimal dual solution one reads off an average optimal policy (their Theorems 7 and 8). To make the correspondence between policies and dual solutions explicit, they attach to every stationary policy a representative, a particular feasible solution of the dual program, and prove (Theorem 10) that the representative of a pure stationary policy is a vertex of the feasible set. This mission formalizes Theorem 10.
Timeline:
The state space is finite. Each state has a finite nonempty set of actions; action in state earns and moves to with probability , . Fix weights with .
The dual linear program has one pair of variables for each state and each admissible action . Its feasible set consists of the with
A pure stationary policy uses the action whenever the chain is in state . Its transition matrix is . For a stochastic matrix , the limit matrix exists, and the deviation matrix is . A state is recurrent if every state reachable from it can reach it back, and transient otherwise; the set collects the transient states, and the states reachable from a recurrent state form an ergodic set. Write for the ergodic sets of .
The representative of is
with for and, for , . The paper defines the same formulas for randomized stationary policies , with in place of .
for every finite Markov decision chain, every positive probability vector and every pure stationary policy . The statement contains feasibility of the representative.
Theorem 10 is the vertex half of the policy–solution correspondence of Hordijk and Kallenberg: every pure stationary policy appears as a basic feasible solution of one linear program, in the multichain case and without any communication assumption. It connects the simplex method on that program with the set of pure policies, and it is a building block for the later literature on linear programming for multichain Markov decision problems. The paper also records that the converse fails: an extreme point may induce a randomized policy.
The result is proved in the paper. As far as is known it has not been machine-checked. A formal proof also checks the exact form of : the paper prints the denominator of as , a sum over all states, and with that reading the representative is not feasible as soon as transient states feed an ergodic set (two states, : ). The denominator is the one the paper's own feasibility computation on p. 360 uses, and it is the one stated here.
Feasibility is a calculation with the identities and . Extremality is the substance. Restricted to the pairs , the constraints become the square system (7) in the state variables, and system (7) determines and the transient part of , but on each ergodic set it determines only up to adding a multiple of the stationary distribution of that class: the matrix is singular, with one degree of freedom per ergodic set. The naive argument, that the equality constraints alone pin the point down, therefore fails as soon as there is an ergodic set; the extra information has to come from the nonnegativity constraints, and that is why the exact value of matters. In the general multichain setting this requires the class structure of a finite Markov chain (closed classes, transient states, the support of , uniqueness of invariant vectors on a closed communicating class), little of which is in Mathlib in usable form.
MarkovDecisionProcesses.StationaryMDP: finite states, finite actions, admissible sets (nonempty), transition probabilities nonnegative with unit row sums. and are the published limitMatrix and deviationMatrix of Blackwell's Lemma 1, whose identities are the open platform theorems BlackwellDiscreteDP.NearOne.lemma_1a and lemma_1d.Set.extremePoints ℝ. Membership in it includes feasibility.vecMul. Recurrence and accessibility are the published IsRecurrent and Accessible; the ergodic set of a recurrent is the set of states accessible from . The maximum in is a Finset.sup' over that finite nonempty set.The ellipsoid method decides questions about a convex set by maintaining an ellipsoid that contains the relevant part of and shrinking it step by step. Introduced for convex minimization by Yudin and Nemirovskii and by Shor in the 1970s, it became famous in 1979 when Khachiyan used it to show that linear programming is solvable in polynomial time. Grötschel, Lovász and Schrijver (Combinatorica 1 (1981)) observed that the method never needs an explicit description of : it only needs, for a query point , either a confirmation that is (nearly) in or a hyperplane (nearly) separating from . From this they derived that optimization and separation are polynomially equivalent for convex bodies, which in turn gives polynomial algorithms for problems with exponentially many constraints: matroid intersection, submodular function minimization, and the stable set problem in perfect graphs.
The engine of all of these applications is a single quantitative statement, Theorem (2.4) of the paper: with a weak separation oracle and with all numbers rounded to a fixed number of binary digits, a prescribed number of ellipsoid steps produces an -optimal point.
Timeline. 1976–1977: Yudin–Nemirovskii and Shor, the method for convex programming. 1979: Khachiyan, polynomial-time linear programming. 1981: Gács–Lovász publish a complete proof of Khachiyan's result with the explicit rounded update; Grötschel–Lovász–Schrijver state and prove the weak-oracle version, Theorem (2.4), and its combinatorial consequences; Bland–Goldfarb–Todd survey the method (Oper. Res. 29 (1981)). 1988: the monograph of Grötschel, Lovász and Schrijver (Springer) gives the full theory of weak oracles.
All norms are Euclidean: , and for a symmetric matrix is the largest absolute eigenvalue. is the closed Euclidean ball of radius about , and the set of points within distance of .
A convex body consists of a compact convex , , and with
A weak separation oracle with precision answers a query either with "", or with a vector , , such that for all .
Given an objective and an accuracy (with and ), set
Start from , . At step query the oracle at . If it answers "feasible", is a feasible index and ; otherwise . Put and
and obtain , by rounding , to binary digits, keeping symmetric. The ellipsoids are , and is the set of points of whose objective value is at least that of every feasible centre found before step .
In Lean, IsRoundedRun K c a₀ R δ p N x A feas a d records exactly these conditions, Kk is , and is the published LinearOptimization.ellipsoid (x k) (A k).
If is a feasible index whose centre is best among the feasible centres, , then
The statement is for every run, i.e. for every sequence of valid oracle answers and every admissible rounding.
Theorem (2.4) turns any weak separation procedure for a convex body into a weak optimization procedure, with a number of oracle calls and a numerical precision polynomial in , , , and . This is the "only if" half of the paper's Theorem (3.1), and through it the source of the polynomial algorithms of Chapters 4–6 of the paper and of the 1988 monograph. Its rounding analysis is what makes the method an algorithm on finite-precision numbers rather than an argument about exact real arithmetic.
The result is proved, and has been for over forty years. What this mission adds is a machine-checked proof of the rounded, weak-oracle version, including the error analysis that the paper compresses into "rounding errors can be estimated similarly". Related items already on the platform formalize exact-arithmetic ellipsoid methods: Bertsimas–Tsitsiklis's central-cut method for polyhedra (LinearOptimization.ellipsoid_method_correct, proved) and Bubeck's version for convex minimization with a first-order oracle (arXiv:1405.4980). Neither has a weak oracle, the inflated factor , or rounding.
For the exact update with factor and an exact separating hyperplane through the centre, containment and volume decrease are a classical computation. Here three perturbations interact. The cut is shifted by , so the retained half-ellipsoid is slightly larger than a half. The rounded matrix differs from by up to in norm, which could destroy positive definiteness if the smallest eigenvalue were not controlled from below, and Lemma (2.1)'s bound is what controls it. The containment must absorb both errors, and it is the inflation factor , chosen larger than the optimal one, that leaves room. The paper bounds the remainder term in (29) only by "similar methods"; making that bound explicit is the bulk of the work. The final step also needs the volume rate in (32), which is sharper than iterating Lemma (2.2) and requires the exact per-step volume ratio of the inflated update.
is Fin n → ℝ with Lebesgue measure. Since Lean's norm on Fin n → ℝ is the sup norm, the Euclidean norm is written out (euclNorm), and the bounds , are stated as quadratic-form (eigenvalue) bounds. uses the natural logarithm and the integer ceiling.
The runs generalize the page in three ways, each of which makes the theorems stronger: the oracle's answers are any answers valid for its specification; rounding is any symmetric value within entrywise; and data are real rather than rational.
The page's standing assumptions , , (p. 173) are hypotheses. Two hypotheses are added, because the page's , and are absolute numbers and the claims fail at extreme scales:
Neither is needed in (13) or (34).
A run predicate without the oracle clause would make Lemma (2.3) false, and one with exact equality instead of rounding would state a weaker theorem; the goal quantifies over every run, never over some run. Positive definiteness of the is a consequence (Lemma (2.1)), not a hypothesis: since Lean's inverse of a singular matrix is , assuming it would hide the lemma's content.
Out of scope: the paper's polynomial-time claims (Theorem (3.1) and its consequences), the bit length of the numbers, and the rationality of inputs, since no oracle-machine model with bit complexity exists in Mathlib or on the platform.
Reusable infrastructure: volumes of ellipsoids and of cone pieces, Sherman–Morrison-type inverses, and perturbation bounds for positive definite matrices. Contributions of these as separate lemmas are welcome.
Every manufacturer who makes a part in batches faces the trade-off Ford W. Harris described in 1913: large lots spread the fixed set-up cost of an order over many pieces, but they also tie up money in stock that must be carried. Harris's article "How many parts to make at once" (Factory, The Magazine of Management 10(2), 1913, reprinted in Operations Research 38(6), 1990) resolved the trade-off with a closed formula, the square-root or economic order quantity (EOQ) formula. It is the starting point of deterministic inventory theory and is still taught as the first model of every operations-management course.
Timeline. Harris published the formula in 1913, without proof ("the solution of this problem involves higher mathematics"). The same formula was popularised by R. H. Wilson in 1934 and was for decades attributed to him. D. Erlenkotter traced it back to Harris (Operations Research 38(6), 1990, 937–946), and the article was reprinted in the same issue. Later work built stochastic (Q, r) models on top of it; Zheng (1992) compared the EOQ heuristic with the optimal (Q, r) policy.
A part is used at a regular rate of units per month (the movement). Each unit costs dollars (the unit cost), and each order costs dollars to set up. Parts are made in lots of units, the lot size. Under regular movement a lot of is delivered when the stock reaches nothing and is then used up at rate , so the stock at time (months, from a delivery) is the sawtooth
with the fractional part. Interest and depreciation on stock are charged at ten per cent a year, a rate the paper fixes.
Harris prices a unit in three parts:
The cost per unit is therefore
and the economic lot size is . In Lean these are stockLevel, interestPerPiece, costPerUnit and econLotSize in the namespace HarrisEOQ.Lot.
For ,
This is Harris's claim that the value of giving the minimum value to "reduces to the square root of (240MS divided by C)": is admissible, attains the minimum, and is the only lot size that does.
These justify the objective , not its minimization; the paper gives no argument for the minimization.
The result. The square-root formula gives the cost-minimising batch size in closed form from three observable numbers. Its consequences are the ones Harris draws: lot sizes grow only with the square root of demand (so consumption must quadruple to double a lot), the cost curve is flat near the optimum and asymmetric (erring small is worse than erring large), and at the optimum the set-up cost balances the variable carrying cost. Every later deterministic and stochastic lot-sizing model reduces to this one in its simplest case.
Formalizing it. The result is classical and proved in textbooks, but Harris's paper itself contains no proof. A formalization supplies the missing argument for the paper's exact objective, which differs from the textbook EOQ by charging interest on the set-up cost ( in the stock value) and by the fixed ten per cent rate. It also makes the paper's modelling step precise: the claim that the average stock is becomes a statement about a time average of a sawtooth function. To our knowledge none of these statements has a machine-checked proof on the platform; the EOQ items of Zheng (1992) concern a different model, with backorders.
The minimization is elementary calculus; the substance of the mission is fidelity. The objective must be the display as printed, with meaning , and the claim includes uniqueness, not only that is a minimizer. The average-stock milestone needs a genuine long-run average of a discontinuous periodic function over with not a whole number of cycles, which is where the integration and limit bookkeeping lies.
All quantities are real numbers; lot sizes are not restricted to integers (the paper's own optimum is 48.5). The hypotheses are not written on the page; they are implicit in the meaning of a usage rate, a price and a cost, and are added. Every quantifier over lot sizes is over . Time is measured in months, and the interest rate is fixed at ten per cent, so the constant appears as printed; the formula is not generalized to an arbitrary rate.
A trivializing formalization is ruled out: is defined as the printed display, not rewritten around ; the average stock is an integral of the stock level, never defined as ; and the goal does not quantify over all real , where Lean's convention would make a spurious minimizer.
The manufacturing interval and the safe stock minimum play no role in the formula and are not modelled. The examples' cost figures (0.188 cents, $0.00028, and so on) are not formalized. The development needs only Mathlib's real numbers, square roots, fractional parts, interval integrals and limits; contributions of proofs of any item are welcome.
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.
Minimizing a smooth function over a closed convex set is the basic problem of constrained continuous optimization. When the constraint set is simple enough that the nearest point of the set to any given point can be computed (a ball, a box, an orthant, an affine subspace), the most direct method is the gradient projection method: take a gradient step and project back onto the set. The method is the ancestor of the projected gradient and proximal gradient algorithms used today in signal processing, machine learning, and optimal control, where the variable is often a function, so that the natural setting is an infinite-dimensional Hilbert space rather than .
A. A. Goldstein's 1964 note in the Bulletin of the AMS (Goldstein 1964) is one of the two founding papers of the method, alongside the independent work of Levitin and Polyak (1966). It states, in a Hilbert space and with an explicit step-size window, that the iterates stay in the initial level set, that the objective values converge, and that under convexity they converge to the optimal value, with weak and strong convergence of the iterates under further hypotheses. Goldstein motivates the method by applications to control theory (Balakrishnan 1963; Goldstein, Minimizing functionals on Hilbert space, 1964).
Timeline.
Let be a real Hilbert space with inner product and norm . Let be closed and convex, and let be the projection onto : is the point of closest to . In Lean, IsProjection C P says that and for all .
Let , , and let
be the level set (levelSet f C x0). Let be an open set containing the convex hull of . Write for the Fréchet derivative of at applied to , for the gradient (so ), and
for the directional second derivative in the sense of Gâteaux (d2 f x h). The curvature hypothesis is that for some , at every and for every , these derivatives exist and
Choose and step sizes . The method is
A point is stationary if for every .
Assume is bounded below and continuous on . There is such that
The goal is the whole theorem, because its five parts share one limit and one standing setting.
The projection inequality for ; the Lipschitz property of ; the characterization of stationarity for convex at a differentiability point; the one-step Taylor estimate; the step lemma (for the new point stays in and the decrease is at least ); parts (i) and (ii); the strong-convexity bound on ; the supporting-hyperplane inequality of the proof of (iii); parts (iii), (iv) and (v). A companion item states the last clause of (ii) under convexity of on .
The result. The theorem gives a step-size rule that needs only a curvature bound near the level set, not a global Lipschitz constant of the gradient, and it covers the infinite-dimensional case directly: (iii) gives convergence of the objective values to the optimal value without assuming that a minimizer exists, (iv) yields minimizers as weak cluster points when the level set is bounded, and (v) gives strong convergence of the iterates under strong convexity on the level set. These are the prototypes of the convergence statements now proved for projected and proximal gradient methods.
Formalizing it. The result is classical and proved on paper; it has no machine-checked proof. The note is two pages long and its proof is terse ("The proof of (ii) being straightforward"), and checking it in Lean exposes two places where the printed statement needs repair (see Formalization scope). A complete development also produces reusable infrastructure: the variational inequality and Lipschitz property of the metric projection in a Hilbert space, a one-dimensional Taylor estimate from a Gâteaux second derivative along a segment, and weak lower semicontinuity of convex continuous functions on closed convex sets used through cluster points in WeakSpace.
The obvious argument for (i) applies a quadratic upper bound for along the segment from to . That bound is only available where the curvature hypothesis holds, on , and nothing guarantees in advance that , or the segment, lies in . Ruling this out requires control of up to the boundary of the level set, which the printed hypotheses do not give; this is where the added continuity hypothesis enters. In (iii) the iterates may be unbounded and no minimizer need exist, so compactness arguments are unavailable. In (iv) the cluster points are weak, so norm-closedness arguments do not apply directly.
[NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. The inner product is ⟪x, y⟫_ℝ, and is Mathlib's gradient f.IsProjection C P; there is no chosen projection and no junk value.SecondDerivBound) states both differentiabilities before the bound, so the bound is never on a junk zero.IsGLB (f '' C) L. Weak cluster points are cluster points in WeakSpace ℝ H.Contributions welcome: proofs of any milestone, in particular the projection inequality and Lipschitz property (independent of the rest), the Taylor estimate from the Gâteaux second derivative, and the weak-closedness argument of (iv).
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.
3SUM asks whether three distinct positions in a list of integers contain values summing to zero. It is a central problem in fine-grained complexity.
This mission formalizes a deterministic algorithm for 3SUM on polynomially bounded integers, on a word RAM with -bit words. Alman and Vassilevska Williams's 2026 breakthrough gives a truly subquadratic bound, refuting the integer 3SUM hypothesis in this model.
The mission uses the accompanying Lean specification and shares the Exact Triangle milestone with Truly Subcubic APSP on a Word RAM.
Theorem_22_3SUM.Many decisions in operations research and machine learning minimize an expected cost whose distribution is unknown and is seen only through independent samples. The sample-average approximation replaces by the empirical distribution and is known to produce decisions with poor out-of-sample performance when is small. Distributionally robust optimization instead minimizes the worst-case expected cost over a set of distributions that are plausible given the data. Mohajerin Esfahani and Kuhn (arXiv:1505.05116v3, published in Mathematical Programming 171, 2018) take this set to be a ball in the Wasserstein metric around the empirical distribution, and show that such balls deliver both finite-sample certificates and asymptotic consistency. This mission formalizes the statistical half of that paper: Section 3 and Appendix A.
A data-driven method should, at a minimum, be consistent: as the sample grows, its optimal value and decisions should approach those of the true problem. For Wasserstein balls this requires a measure concentration inequality for empirical distributions in the Wasserstein metric, which was supplied by Fournier and Guillin (PTRF 2015). The paper combines that inequality with the Kantorovich–Rubinstein duality and the Borel–Cantelli lemma.
Let be with an arbitrary norm and its Borel -algebra. A decision ranges over a feasible set ; the random vector has distribution , supported on the uncertainty set ; the loss is . The true problem (1) has optimal value
The Wasserstein distance between distributions with finite first moment is
Given samples drawn independently from (joint law , and for the infinite sequence), the empirical distribution is , and the Wasserstein ball is the set of distributions on with . The distributionally robust program (5) has optimal value
and an optimizer of it is written .
The light-tail condition (Assumption 3.3) asks for an exponent with . Under it, and for , Theorem 3.4 (Fournier–Guillin) gives constants with
for all , . Solving the right-hand side for gives the radius
Let with and , and use the radius in (5).
(i) If is upper semicontinuous on and on , then -almost surely
(ii) If moreover is closed and is lower semicontinuous on , then -almost surely every accumulation point of is an optimal solution of (1).
Theorem 3.2 (Kantorovich–Rubinstein duality, ), which the proof of (i) uses, enters as a reference item: the open platform theorem WassersteinDRO.Duality.kantorovich_rubinstein, stated on the whole space for all Borel probability measures. It is not a milestone, because that statement is more general than the paper's version on (the two agree for distributions in by extending Lipschitz functions from to the whole space).
A companion item, Example 1 (1), records that upper semicontinuity cannot be dropped in (i): for , and one has but for every radius .
Theorem 3.5 makes the robust optimal value an upper confidence bound on the out-of-sample cost of the robust decision. Theorem 3.6 shows that this protection does not cost consistency: with radii shrinking at a rate governed by summable confidence levels, such as , both the certificate and the decisions converge to their true counterparts. Together they are the statistical justification for the Wasserstein ambiguity sets that the rest of the paper reformulates as finite convex programs, and they are cited as the reference consistency results for Wasserstein distributionally robust optimization.
All results here are proved in the paper. None of them, nor the Fournier–Guillin inequality, is formalized on Prove2Me or in Mathlib to our knowledge. The mission adds machine-checked versions of the finite-sample and consistency statements, a monotone Lipschitz approximation lemma for semicontinuous functions with linear growth (useful wherever Lipschitz duality has to be extended to semicontinuous integrands), and a convergence lemma for measures in shrinking Wasserstein balls.
The obvious argument for (i) bounds the worst-case expectation by the true expectation plus a Lipschitz constant times the radius. That fails, because is only upper semicontinuous in , not Lipschitz, and has no Lipschitz constant to multiply. The expectations of a merely semicontinuous loss must be controlled uniformly over every distribution in the ball, including data-dependent worst-case distributions, and the almost-sure convergence of the empirical distribution alone does not give this. Example 1 of the paper shows that each regularity hypothesis is needed. On the formal side, the Wasserstein distance is an infimum over couplings on a Polish space; even its triangle inequality (gluing of couplings) and the Kantorovich–Rubinstein duality are substantial.
is a finite-dimensional real normed space with its Borel -algebra (BorelSpace), and is its dimension; decisions live in EuclideanSpace ℝ (Fin n). The definitions (type ), , , and the worst-case expectation are the published WassersteinDRO.Duality definitions. The optimal values and are extended reals. Standing conventions and pinned hypotheses:
A statement in which (7) could not hold for any constants would make the goal vacuous. The concentration inequality is satisfiable (for instance by a Dirac distribution with any constants), and is defined by the paper's formula, not chosen freely.
Welcome contributions: the triangle inequality and Kantorovich–Rubinstein duality for , the Borel–Cantelli step for product measures, Lemma A.1, and the Fatou argument of (ii).
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.
Generating points uniformly distributed over a bounded region is a basic subroutine in Monte Carlo integration, in estimating the volume of a region, in randomized search for optimization, and in identifying redundant constraints of mathematical programs. When is given only implicitly, for instance by a system of inequalities, the classical methods break down in high dimension: transformation methods need a tractable description of , and rejection from an enclosing box or ball accepts a fraction of proposals that decays exponentially with .
Smith (Oper. Res. 32(6), 1984) studied a family of Markov chain methods, mixing algorithms, that avoid rejection altogether. The best known member is the Random Directions Algorithm, now called hit-and-run: from the current point, pick a direction uniformly at random and move to a uniformly random point of on the line through the current point in that direction. Boneh and Golan (1979) proposed it for constraint identification and conjectured, without proof, that it generates uniform points; Smith (1980, 1984) proved asymptotic uniformity, and Section 3 of the 1984 paper gives an explicit geometric convergence rate. This mission targets that rate, Theorem 3.
Later work, in particular Lovász (Math. Program. 86, 1999) and Lovász and Vempala (SIAM J. Comput. 35, 2006), proved polynomial mixing bounds for hit-and-run on convex bodies. Smith's bound is exponential in , but it holds for every open bounded region, convex or not, and from every starting point.
Write for -dimensional Lebesgue measure (content) on and for the Euclidean norm. Let be open, bounded and nonempty.
with the normalized surface measure of the sphere, and is its -step iterate.
the fraction of its smallest enclosing ball that fills.
For , every , every measurable and every ,
The constant is the paper's. The bound is uniform in the starting point and in , and it depends on only through and .
The result. Theorems 1 and 2 of the paper (the companion mission) establish only that the chain converges to . Theorem 3 makes this quantitative: the deviation from uniformity decays geometrically, at a rate computable from the dimension and the shape ratio alone. It shows which features of a region govern convergence, it gives a stopping rule with a guarantee, and it holds for non-convex regions, which the later polynomial-time analyses of hit-and-run do not cover. The paper notes the bound is of practical use only in low dimension; its value lies in being explicit and fully general.
Formalizing it. The theorem is proved in the paper, but parts of the proof are heuristic: the density is derived by a limit over small cubes, and the step from to uses a claim about circumscribed spheres that is false as stated (see below). A machine-checked proof would produce, as reusable components, a general-state-space Doeblin bound (no such theorem currently exists on the platform; the existing Doeblin results are finite-state), a measure-theoretic definition of hit-and-run as a Markov kernel, and the polar-coordinates computation of its density. None of these has, to our knowledge, been formalized.
The obvious argument is: the density is bounded below on , so Doeblin's condition holds, so the chain converges geometrically. Each step hides work. The density is not given by the algorithm but must be derived: the algorithm draws a direction and a scalar, and the change of variables from (direction, signed distance) to the endpoint is two-to-one and carries the Jacobian , which is where and the factor 2 come from. The Doeblin step needs a stationary law and the fact that the chain started in never leaves . For non-convex , the paper's "diameter along the ray" must be replaced by the measure of the line set, and the maximal chord does not bound the distance ; the diameter of is needed instead. Finally, the paper's assertion that the ball of radius circumscribes fails already for an equilateral triangle, so the final comparison must go through the smallest enclosing ball's radius .
EuclideanSpace ℝ (Fin n) with Lebesgue measure. The region is a set S with IsOpen S and Bornology.IsBounded S; boundedness is the paper's standing assumption ("bounded regions").ProbabilityTheory.Kernel built operationally from the algorithm: the uniform law on the line set, integrated against the normalized surface measure of the unit sphere (Mathlib's Measure.toSphere, divided by its total mass ). Off the kernel is the identity, which the chain started in never uses. The -step law is the published MarkovChainCLT.iterKernel.A matroid abstracts the dependence structure of the columns of a matrix: which sets of columns are linearly independent, forgetting the numbers themselves. Graphs are the special case of incidence matrices over the integers mod 2, where a set of edges is independent exactly when it contains no cycle. A natural combinatorial question in this setting is the minimum partition (or covering) problem: how few independent sets are needed to cover all the elements? For a graph this is the least number of forests that cover its edges, its arboricity.
J. Edmonds answered this question for every finite matroid in Minimum partition of a matroid into independent subsets (J. Res. NBS 69B, 1965, doi:10.6028/jres.069b.004). The answer is a good characterization in Edmonds's sense: there is a short certificate both that a partition into independent sets exists (the partition itself) and that it does not (a single subset that is too large for its rank). The paper is also the source of the matroid partition algorithm, which together with matroid intersection became a basic tool of combinatorial optimization.
Timeline:
Let be a finite set of elements and call some subsets of independent. Edmonds's two axioms are:
A matroid is a system satisfying both. The rank of is the largest cardinality of an independent subset of ; in a matroid every maximal independent subset of has exactly elements.
A circuit is a minimal dependent set. A span (closed set) is a set such that no circuit has exactly one element outside , and the span of is the minimal span containing . A partition into independent sets is a family of mutually disjoint independent sets whose union is ; any number of the may be empty.
For every finite matroid and every integer , the elements of can be partitioned into independent sets if and only if there is no with
The condition ranges over all subsets of , as printed.
The milestones follow the paper's own lemmas and the claims of its main proof, in order.
A further item states the paper's COROLLARY (Nash-Williams): the edges of a loopless finite graph can be colored with colors so that no circuit is one color if and only if no nonempty node set has , where is the set of edges with both ends in .
THEOREM 1 is the base case of matroid union: the sets coverable by independent sets form a matroid whose rank is , and the paper's proof is the origin of the polynomial-time matroid partition algorithm and of Edmonds's later matroid intersection theory. Its graphic case gives the arboricity formula of Nash-Williams, used for sparse-graph decompositions and orientation problems. The criterion is a certificate: a single set with proves that no partition exists.
The theorem has been proved since 1965 and appears in every matroid textbook. As far as the platform and Mathlib record, it has no machine-checked proof: Mathlib has matroids, circuits, closure and strong circuit elimination for its own Matroid structure, but no matroid union or partition theorem. This mission produces a formal proof from Edmonds's own axioms (Axiom 2 as an equal-cardinality condition, not an exchange axiom), together with the equivalences between his axiom systems, which are themselves standard results.
The "only if" direction is a three-line count. The difficulty lies in the converse: a greedy procedure that fills the sets one after another fails even for matroids, so an element that fits in no current set must be accommodated by moving other elements between sets. Such a chain of exchanges must keep all sets independent and disjoint at every step and must terminate; stating it with sets whose contents change while their labels persist is the part that needs careful bookkeeping in a formal proof. A second, smaller difficulty is the translation between the paper's equal-cardinality Axiom 2 and the circuit and span language its proof uses (PROPOSITIONS 1–5).
Finset.univ, subsets are Finset α, and the independent sets are a predicate Indep : Finset α → Prop.IndepI1 and rankOfIndep (WhitneyMatroid.RankIndep.Postulates). The rank is integer-valued, and every inequality versus is compared in with .Matroid.Fin k → Finset α of pairwise disjoint independent sets covering , with empty parts allowed and included.ends : E → Sym2 V (parallel edges allowed, loops excluded), with independence as linear independence of incidence columns over . It quantifies over nonempty : as printed, makes the statement false.Contributions welcome: proofs of the axiom equivalences (reusable for any work with Edmonds-style or circuit-axiom matroids), the span lemmas, the augmentation step, and bridges to Mathlib's Matroid that would let its circuit and closure library be reused.
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.
Delivering goods from one depot to many customers with a fleet of trucks is the vehicle routing problem. Dantzig and Ramser formulated it in 1959 as the "truck dispatching problem" (Management Sci. 6 (1959), doi:10.1287/mnsc.6.1.80). Five years later Clarke and Wright proposed the savings procedure (Oper. Res. 12 (1964), 568–581, doi:10.1287/opre.12.4.568): start with one truck per customer and repeatedly join two routes where joining saves the most distance, as long as the trucks can still carry the loads. On the twelve-customer example of Dantzig and Ramser it reached 290 units against their 294.
The savings procedure became the standard construction heuristic for vehicle routing. It appears in every textbook treatment of the problem, is the initial solution of many metaheuristics, and is the benchmark against which later construction methods are compared. The paper states the procedure and its bookkeeping (the half matrix, the vector , Table II) but proves nothing about it. That every run of the procedure ends, and ends in a feasible allocation, is left to the reader.
A depot serves customers . The distance between every two points is given, and customer requires a load . Trucks come in capacity classes: trucks of capacity are available, with , and the trucks of the smallest capacity are unlimited, (p. 569).
A run is the ordered list of customers served by one truck, which drives . Its load is . A state of the procedure is a list of runs; its mileage is the total length of its runs. A list of runs is an allocation if every customer lies on exactly one run, and it is feasible if each run can be given a truck of capacity at least its load without using more trucks of any class than are available.
The saving of the cell is . The half matrix records if and are adjacent on a run, and counts how many ends of runs lie at . Table II counts, for each capacity level , the runs with load above and the trucks with capacity above .
The procedure starts with the runs , so for every customer. A cell is admissible if (I) and ; (II) and are on different runs; (III) after replacing those two runs by one run of load , no column of Table II has more runs than trucks. A step links an admissible cell of maximum saving, ties broken arbitrarily, by joining the two runs end to end at and . The procedure stops when no cell is admissible.
Assume symmetric distances, , , and that the initial one-truck-per-customer allocation passes the Table II test. Then every run of the procedure is finite whatever the tie-breaks; at every reachable state from which a link is possible a step exists; and every final state is a feasible allocation satisfying relation (A), for every customer, with
relation (A) at every reachable state, the permanence of links between customers, and
which together give feasibility of every reachable state. Two further milestones: when and the distances are a metric, the optimum equals the traveling salesman optimum (p. 569); and on the data of Table I every run of the procedure ends with total distance 290.
The goal is the specification the paper's procedure meets: it always terminates, never gets stuck, and outputs routes the fleet can actually drive, with the mileage the half-matrix bookkeeping predicts. The equivalence of the Table II test with truck feasibility is the reason the procedure can check capacities by counting columns instead of solving an assignment problem; it is a nested-class instance of Hall's marriage condition and is reusable for any routing or bin-assignment problem with ordered vehicle classes.
None of these statements is formalized anywhere, and the paper does not prove them. The paper makes no claim of optimality ("near-optimal", p. 568, is not quantified), and the mission does not either. A formal model of the procedure as a nondeterministic transition system is a base on which later results about savings heuristics (worst-case ratios, parallel and sequential variants) can be stated.
The obvious argument for termination, "each link removes a run", needs the invariant that every reachable state is a partition of the customers into runs; the procedure manipulates ordered lists and reverses runs, so the invariant must be carried through every step. Feasibility is not preserved by an arbitrary link but only by one that passes condition (III), and turning the column test into an actual assignment of runs to trucks is a matching argument that fails without both and the ordering of the capacities. Because ties are broken arbitrarily, every statement must hold for all runs of a nondeterministic procedure, not for one canonical execution. The worked example requires following every tie-break.
Points are Fin (M+1) with depot 0, and a run's length is SupplyChainTheory.routeCost from the referenced module SupplyChainTheory_vrp. Capacity class i : Fin (n+1) is the paper's ; availabilities are in ℕ∞; loads and capacities are real. A state is a list of runs, each an ordered list of customers; the matrix and the vector are computed from the state. The procedure is a step relation, and every invariant is stated for reachable states. Termination is Acc of the step relation at the initial state.
Choices committed to:
A correctness claim only about final states, without termination and progress, would hold for a procedure with no moves; a step relation with a fixed tie-break would prove less than the paper; invariants for arbitrary states are false; and a mileage identity for an arbitrary partition says nothing about the procedure's output. None of these is the target.
Not formalized: the informal , the shadow-cost reading of p. 571, the decomposition savings (2)–(5) of the general scheme, the load-splitting reduction of pp. 572–573, the Dantzig–Ramser methods, and the empirical comparisons and appendices.
Contributions welcome: proofs of the milestones, in particular the Table II equivalence, which needs a Hall-type argument for nested classes, and a decision procedure for the worked example.
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:
All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph. It is a fundamental problem in graph algorithms and a fundamental problem in fine-grained complexity.
This mission formalizes a deterministic algorithm for APSP on directed -vertex graphs with polynomially bounded integer edge weights and no negative cycles, on a word RAM with -bit words. This is a truly subcubic bound and refutes the integer-weight APSP hypothesis in this model.
Theorem_22_APSP.