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?
Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is
with symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid is contained in the explicitly constructed ellipsoid ,
and the volume contracts:
. Two integer-data estimates make the contraction decisive: every extreme point of with entries bounded by has coordinates in (Lemma 8.2), and a full-dimensional bounded such polyhedron has (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball of volume at most containing , with a lower bound on when is nonempty, the ellipsoid method correctly decides whether is empty within iterations — the explicit iteration count behind the polynomial-time headline.
Why do network linear programs return integer answers for free? This mission formalizes the structural theory of the minimum cost network flow problem of Chapter 7 of Bertsimas & Tsitsiklis: a directed graph with external supplies , arc costs , and the node-arc incidence matrix — an matrix in which every column has exactly one (start node) and one (end node) — so that flow conservation reads , forcing the standing assumption . Because the rows of sum to zero, the book works with the truncated matrix of the first rows. The combinatorial heart is the correspondence between algebra and graph structure: a set of arcs forming a tree determines a unique tree solution of , off (Theorem 7.3); connectedness makes full-rank (Corollary 7.1); and a flow vector is a basic solution if and only if it is a tree solution (Theorem 7.4). The goal theorem is the integrality theorem (Theorem 7.5): for the uncapacitated problem on a connected graph, every basis matrix has an integer inverse (its determinant is by the tree/lower-triangular argument), integer supplies make every basic solution integer, and integer costs make every dual basic solution integer — whence integer optimal primal and dual solutions exist whenever the optimal cost is finite (Corollary 7.2). This is the fountainhead of combinatorial integrality in linear optimization, feeding the max-flow min-cut mission that follows.
How does the optimal cost of a linear program respond when the problem data change? Chapter 5 of Bertsimas-Tsitsiklis studies the standard form problem (rows of linearly independent) as the requirement vector and the cost vector vary. On the convex set of feasible right-hand sides, and under the standing assumption that the dual feasible set is nonempty, the optimal cost is finite and convex (Theorem 5.1) — indeed over the extreme points of the dual feasible set, a piecewise linear convex function whose breakpoints are exactly where the dual optimum is non-unique. The capstone (Theorem 5.2) identifies the generalized gradients of : if the primal at is feasible with finite optimal cost, then is an optimal solution of the dual if and only if is a subgradient of at (Definition 5.1: for all ) — the precise sense in which dual variables are marginal costs. Dually (Theorem 5.3), the set of cost vectors with finite optimal cost is convex, the optimal cost is concave on , and near any with a unique primal optimum , is linear with gradient . Local ranging (Section 5.1) and parametric programming (Section 5.5) are the procedural companions, folded into the design notes.
Every linear programming problem has a shadow. To the primal we associate the dual , whose variables price the primal constraints: one dual variable per primal constraint and one dual constraint per primal variable, with signs governed by the correspondence of Table 4.1. This mission formalizes §4.1–4.5 of Bertsimas–Tsitsiklis: the dual of a general-form linear program, the involution "the dual of the dual is the primal" (Theorem 4.1), and weak duality for any primal-feasible and dual-feasible (Theorem 4.3) with its two corollaries — an unbounded primal forces an infeasible dual (Corollary 4.1), and feasible with are automatically both optimal (Corollary 4.2). The goal theorem is strong duality (Theorem 4.4): if a linear programming problem has an optimal solution, so does its dual, and the respective optimal costs are equal — proved in the book by running the simplex method with the lexicographic pivoting rule of Mission IV on a standard-form transform. The statement is deliberately the book's attainment form: by Table 4.2 the primal and the dual can be simultaneously infeasible (Example 4.5), so an unguarded equality of optimal values is false. The mission closes with complementary slackness (Theorem 4.5): feasible and are simultaneously optimal if and only if for all and for all — the certificate structure behind the dual simplex method and every LP optimality check.
How does one actually solve a linear program? Chapter 2 showed that if a standard-form problem subject to , has an optimal solution, it has an optimal basic feasible solution; the simplex method searches among basic feasible solutions, moving along edges of the feasible set in cost-reducing directions. This mission formalizes the mathematics of Chapter 3 of Bertsimas–Tsitsiklis: feasible directions, the reduced costs
measuring the cost rate along the basic directions, the optimality conditions of Theorem 3.1 ( implies optimality, and conversely at nondegenerate optima), the basis change of Theorem 3.2, and the pivot iteration itself — encoded as a predicate relating a basis/BFS pair to its successor, so that every theorem covers every pivoting rule. The goal theorem is Theorem 3.3: if the feasible set is nonempty and every basic feasible solution is nondegenerate, the simplex method terminates after a finite number of iterations, ending either with an optimal basis and an associated optimal basic feasible solution, or with a direction satisfying , , certifying optimal cost . The secondary capstone, Theorem 3.4, removes the nondegeneracy assumption: under the lexicographic pivoting rule every tableau row other than the zeroth stays lexicographically positive, the zeroth row strictly increases lexicographically, and the simplex method terminates on every problem — the anticycling guarantee that also supplies the optimal-basis existence used by the strong duality theorem of Mission V.
Every linear programming problem asks to minimize a linear cost over a polyhedron — a set of the form , or in standard form . Chapter 2 of Bertsimas–Tsitsiklis develops the geometry of these feasible sets, and its central achievement is making the intuitive notion of a "corner point" rigorous. There are three natural candidates: the extreme point — a point of that cannot be written as a convex combination of two other points of (purely geometric, representation-independent); the vertex — the unique minimizer of some linear cost over (geometric, via supporting hyperplanes); and the basic feasible solution — a feasible point at which linearly independent constraints are active (algebraic, the object the simplex method actually computes with). This mission formalizes polyhedra, active constraints, vertices and basic (feasible) solutions, and proves the fundamental Theorem 2.3: for a nonempty polyhedron all three notions coincide. Around the capstone sit the supporting pillars: polyhedra are convex (Theorem 2.1), the characterization of points pinned down by linearly independent active constraints (Theorem 2.2), finiteness of the set of basic solutions (Corollary 2.1), and the basis-column characterization of basic solutions in standard form (Theorem 2.4) — the combinatorial engine behind the simplex method of Chapter 3 and the root of the entire series.
A continuous piecewise linear (CPWL) function is one assembled from finitely many flat pieces glued along flat seams. Every ReLU network computes such a function, and every such function is computed by some ReLU network. Questions about how deep a network must be are therefore questions about the internal structure of CPWL functions.
In 1993 Breiman built such functions from hinges: maxima of two affine maps. Sums of hinges approximate anything, but from two dimensions up they fail to represent most CPWL functions exactly. Wang and Sun (2005) widened the maxima, proving that every CPWL function on ℝⁿ is a signed sum of maxima of at most n+1 affine maps. Twenty years on it remains the workhorse structural fact, reducing any question about a network to a question about a single max gate and underpinning every known upper bound on the depth of exact representation.
That includes the newest one: at STOC 2026, Bakaev et al disproved the short standing conjecture that ⌈log₂(n+1)⌉ hidden layers are necessary, showing ⌈log₃(n−1)⌉+1 suffice. In this mission we deliver a machine-checked proof of the Wang and Sun theorem so future formalizations of network expressivity can invoke it rather than reprove it. Note that we take as given the lattice representation of Tarela and Martínez, independently proved by Ovchinnikov, which writes any CPWL function as a max of mins of its affine pieces. That is the one external ingredient the argument consumes, and our definition of CPWL builds it in.
How quickly does the empirical mean of independent random variables concentrate around the true mean? This question is the analytic engine of the entire theory of stochastic bandits: every optimistic algorithm (Explore-Then-Commit, UCB and its relatives) is calibrated by a tail bound on the sample mean. This mission formalizes the subgaussian framework of Chapter 5 of Lattimore–Szepesvári's Bandit Algorithms: a random variable is -subgaussian when for all , and the Cramér–Chernoff method converts this moment-generating-function control into the exponential tail . The goal theorem is the Hoeffding-type bound: the sample mean of independent -subgaussian deviations exceeds the true mean by with probability at most , together with its confidence form — the exact bound every UCB index is built from. These few lines of analysis are cited by every regret bound in the series.
Multi-agent reinforcement learning approximates a global value function by summing per-agent local value functions learned independently — a trick that works surprisingly well in practice (ride-hailing dispatch, restless bandits) but had no general theoretical justification. Chen and Peng (arXiv:2506.02385) explain why: they define a Markov entanglement measure for the joint transition dynamics of a multi-agent MDP, directly analogous to quantum entanglement of a two-party state, and show it controls exactly how much error this value-decomposition trick incurs. This mission formalizes their sharpest quantitative bound (Theorem 4): the error of decomposing the global Q-function into per-agent local Q-functions is controlled, entrywise, by the agent-wise total-variation measure of Markov entanglement.
A platform sourcing items from monopolistic sellers with private quality cannot tractably maximize its true profit: the bundle revenue is neither monotone, submodular, supermodular, subadditive, nor superadditive. Theorem 4.6 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers shows that the simple surrogate threshold mechanism — maximize the linearized objective — is profit-optimal up to a factor in large markets. Prove it: Bernoulli concentration for the bundle quality plus sub-exponential control of the dispersion gap (Lemma 4.5).
A Hadamard matrix is a square array of +1s and −1s whose rows are mutually orthogonal — equivalently, one whose determinant attains the absolute maximum that Jacques Hadamard proved in 1893 any ±1 matrix can reach. The story opens earlier, with James Joseph Sylvester's 1867 doubling construction producing such matrices in every power-of-two order; Hadamard himself added orders 12 and 20. The conjecture bearing his name asserts that a Hadamard matrix exists for every order divisible by four. Raymond Paley's 1933 construction from finite fields settled vast new families, and computer searches filled stubborn gaps — beginning with order 92 at JPL in 1962 and reaching order 428 only in 2005, after which 668 became the smallest order whose existence is still unknown. Far from a curiosity, these matrices are workhorses of applied mathematics, underpinning error-correcting codes (the Reed–Muller code that sharpened Mariner spacecraft imagery), spread-spectrum and CDMA signal design, optimal statistical designs of experiments, and coded-aperture spectroscopy. Settling the conjecture would close a 130-year-old gap where combinatorics, number theory, and design theory meet.
Show that every nonconstant complex polynomial has a complex root.
A complete formal proof of Fermats Last Theorem for exponent 5: for all positive natural numbers a,b,c, a^5 + b^5 != c^5. The proof follows the classical Legendre-Dirichlet approach (1825-1830): Case 1 (5 does not divide a,b,c) is dispatched by congruences, and Case 2 (5 divides one of them) uses infinite descent through the ring Z[zeta_5]. The open hard leaf is the Z[zeta_5] PID step (flt5_zeta5_ring_witnesses).
Nearly every measure of Boolean function complexity was known to be equivalent — except sensitivity. Proving the conjecture unified the whole picture.
Prove a deterministic algorithm for integer 3SUM in the campaign's shared word-RAM model, improving the verified bound.
A promising parameter choice is , , , and . Lean-checked arithmetic certificates give , , and . The predicted Exact Triangle saving is , giving a 3SUM cutoff of and a strict margin below the target.
The algorithmic claim remains open. The milestones are to establish the faster inner solver, then verify the integer computations for and and prove the total Exact Triangle cost, including preprocessing and scans. The existing verified reductions and foundation definitions can then be reused. The numerical certificates alone do not prove the mission.
Improve deterministic integer 3SUM to time in the foundation mission’s word-RAM model.
The existing Corollary 26 routine admits the tighter bound . Keep and change the grouping parameter to , implemented using the integer root of of order . Balancing the instance costs and scans gives an Exact Triangle saving of , and the verified 3SUM reduction gives time.
The supporting theorem establishes every rational exponent , including . This changes the algorithm’s grouping parameter and improves the earlier cutoff . All other model definitions and the shared reduction lemmas are reused.
Prove deterministic time for 3SUM on polynomially bounded integers, using the same word-RAM model and definitions as the foundation mission.
The existing uniform Exact Triangle bound has saving . The verified 3SUM reduction yields time, so every fixed rational exponent above is attainable, including . This mission sharpens the bound extracted from the existing algorithm.
The supporting theorem covers all rational ; it does not assert an exact bound. The proof reuses the shared, proved APSP and 3SUM lemmas from Anthropic’s formalization.
This mission formalizes A. Erschler and T. Zheng, Growth of periodic Grigorchuk groups, Invent. Math. 219 (2020) 1069–1155 (doi:10.1007/s00222-019-00922-0). Page and result numbers are those of arXiv:1802.09077v2.
The growth function of a group generated by a finite set counts the elements of word length at most . A group has polynomial growth, exponential growth, or intermediate growth, strictly between the two. Grigorchuk's groups were the first groups of intermediate growth, and for forty years the precise asymptotics of their growth was open, even for the most studied of them, the first Grigorchuk group . Erschler and Zheng determine its growth exponent:
where and is the positive root of . The upper bound was known; the new lower bound comes from random walks.
Timeline.
is the rooted binary tree, its vertices the finite words over and its boundary the infinite rays; automorphisms act on the right, . For a string , the Grigorchuk group is generated by certain automorphisms of , . The automorphism changes the first letter of a word, swapping the two subtrees of the root, while are defined as follows. They fix , and on a word each of them either changes the first letter of or does nothing, depending on the letter of the string: if , then and change it and does nothing; if , then and change it and does nothing; if , then and change it and does nothing. The string gives the first Grigorchuk group.
Assumption asks that every block contain or ; it implies that is periodic. is the sum of the entries of for three explicit matrices: the lengths of the words the substitutions of §2 produce.
A measure on a group is a function of total mass 1. A function is -harmonic if , the entropy is , and the Poisson boundary of is non-trivial when some bounded -harmonic function is not constant.
For every there is such that for every satisfying there is a non-degenerate symmetric probability on of finite entropy and non-trivial Poisson boundary with, writing for the word length,
and hence, for some depending on ,
The printed theorem has in place of ; that version is weaker and does not give the exponent.
The abstract's headline, that the volume exponent of the first Grigorchuk group is , is the last milestone, ErschlerZheng.hasVolumeExponent_firstString_alpha0: Theorem A combined with Bartholdi's upper bound.
The result. It answers the growth question for : the exponent is . It gives near-optimal lower bounds for every with satisfying , and its measures are the first examples on these groups of random walks with non-trivial Poisson boundary and power-law tails. The method, building a measure with non-trivial boundary and controlled tail and reading off a volume bound from entropy, applies beyond Grigorchuk groups.
Formalizing it. No machine-checked proof of these results exists; Mathlib has neither Grigorchuk groups nor Poisson boundaries. On this platform the mission builds on the published bundle of the first Grigorchuk group, Garrido_Grigorchuk, from the Garrido Amenable Groups III mission, and on Chou's word balls, Chou_Growth. The general Markov-chain inputs (Cheeger, Faber–Krahn and Nash inequalities, and off-diagonal heat-kernel bounds) are separate standalone theorems.
Lower bounds by anti-contraction of word lengths (Grigorchuk, Leonov, Bartholdi, Brieussel) stall well below . The entropy route needs a measure with non-trivial Poisson boundary, but on a group of subexponential growth every finitely supported symmetric measure has trivial boundary. The measure must therefore have heavy tails, and the lower bound it gives is only as good as its tail decay. The difficulty is to make the tails as light as allows while keeping the boundary non-trivial. That needs a non-homogeneous random walk on the Schreier graph of to be transient enough to fix the germ at , and heat-kernel bounds for jump processes that are not translation invariant.
Tree automorphisms are permutations of finite words (Garrido.BinaryTreeAut), acting on rays on the right by , so that . A measure is a function summed with tsum; it is symmetric when , and non-degenerate when its support generates as a semigroup. The Poisson boundary is non-trivial (HasNontrivialPoissonBoundary) when some bounded harmonic function is not constant on the submonoid generated by the support of ; for the non-degenerate measures of the goal this is the criterion of p. 2 (ErschlerZheng.hasNontrivialPoissonBoundary_iff_exists_bounded_isHarmonic_ne_of_isNondegenerate). Growth is evaluated at real radii. The definitions are in the bundles ErschlerZheng_Walks, ErschlerZheng_Germs, ErschlerZheng_Grigorchuk and ErschlerZheng_Construction.
Where a statement departs from the print, its milestone description says so: under Correction when the printed claim is false or undefined ((2.3), the substitutions on p. 15, Fact 3.5, the Gray code on p. 34, Fact 7.3, on p. 59, Lemmas 7.9, 7.17 and 7.21, Propositions 7.12 and 7.18, and the uniform digits on p. 55), and under Formalization note when it reads the print or strengthens it (Lemma 2.1, Proposition 7.19, Corollary 8.2, and the constants and ). The goal is Theorem 8.3 with the its proof gives, as above.
The goal is not trivial: its measure must be a non-degenerate symmetric probability on , and the growth bound is about the generating set itself.
Reusable beyond this mission: Grigorchuk groups for every with their substitutions, germ groupoids of group actions, entropy and the Poisson boundary of random walks.
What is left out. Theorems B and C, Corollary 8.4 and the other applications in §8 to general , which need the upper bounds of Bartholdi and Erschler (doi:10.5802/aif.2902); the side results of §§4–6 on the first Grigorchuk group (Theorem 5.7 and the critical constant of recurrence); the illustrative Examples 2.4 and 7.10; and the remarks and questions of §9. They are planned for a sequel mission.
All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an -vertex weighted directed graph. Floyd–Warshall solves it in time, and for decades no algorithm beat for any constant on graphs with polynomially bounded integer weights. The APSP conjecture of fine-grained complexity asserted that none exists. In 2026, Alman and Vassilevska Williams (arXiv:2610.06783) refuted it with a deterministic algorithm. That bound is the campaign's first entry, and it is formally proved on the platform.
This entry records the deterministic exponent , obtained by tightening the accounting in the same algorithm.
The model is the campaign's fixed deterministic word RAM (foundation mission: Truly Subcubic APSP on a Word RAM). A finite program uses add, subtract and multiply modulo , indirect load and store, a sign branch, and accept or reject, on words of width . Inputs have integer weights of absolute value at most for a fixed , and there are no negative cycles. The machine has no source of randomness, so randomized (Las Vegas) algorithms do not count.
The goal is the campaign template with the value :
which says there is a deterministic word-RAM program that solves APSP in steps.
The core of the published algorithm is a data structure for thin min-plus-type products with inner dimension . It has preprocessing and queries , with parameters (recursion ratio) and (switch threshold). Four changes improve the saving from to about :
The explicit parameters , and satisfy the thinness condition () and give . Since , the slack absorbs all polylogarithmic factors.
The randomized version of the same argument reaches about by repeating random-prime hashing. That bound is out of reach in this deterministic model. Closing the gap between deterministic and randomized collision handling is a natural next target for the campaign.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-85 mission already covers every , the new work is the range from 80 to 85.
The cutoff came down from 90 to 85 in two days, through moona3k's proofs at 89, 88, 87 and 85. The step to 89 sharpened the estimates of the cutoff-90 argument. The step to 85 added a new idea, a weighted pair-curvature and confinement estimate. How far that idea reaches is not known; 80 asks for five more units. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 80 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryThis entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from85 to84. For every real p≥84, the foundation's unchanged cyclic constant is the least constant comparing the triple deficit with the pair-deficit sum for every complex coordinate triple in every finite dimension.
The statement includes unequal and zero input vectors and dimension zero. It concerns complex diagonal matrices through their coordinate norms; it does not settle the conjectured cutoff2 or the full noncommutative matrix problem.
Both exact proof submissions have been ACCEPTED by Prove2Me, and both theorem records are Proved. Their accepted sources match the submitted files and exact target statements in the pinned environment. This proposal references those existing verified results; the remaining steps are human submission and campaign moderation.
The construction is by Ezzeri Esa (GitHub savarin), with the accepted cutoff90 formalization by BrunoDCDO. Claude Opus5.5 produced moona3k's accepted89,88,87 work. Codex's accepted85 continuation and new84 extension reuse their verified generic calculus and transfer arguments.
On[84,85], an exact rational matrix sum-of-squares certificate proves a coupled radial energy estimate throughout a larger localization box. Residual estimates give nonnegative actual deficit Hessians and box convexity. Tight logarithm/Taylor bounds and exact positive Bernstein certificates localize every normalized failure. Orbit averaging and circle transfer prove the real and complex bounds, and the cyclic obstruction establishes leastness. The accepted85 development supplies the remaining tail.
The campaign began with cutoff256, followed by90,89,87,85. This entry instantiates its exact template with84 over the same foundation definitions.
A single machine must process jobs, each with a processing time and a deadline, and some jobs must be finished before others may start. The first question of any planner is whether the deadlines can be met at all. Without precedence constraints the answer is classical: Jackson's rule (J. R. Jackson, 1955, reported by W. E. Smith, 1956) says that all jobs can be completed on time if and only if they are completed on time when sequenced by earliest deadline first. Precedence constraints break this rule, because the earliest-deadline order may put a job before one of its required predecessors.
E. L. Lawler and J. M. Moore (Management Science 16 (1969) 77–84) repair the rule by replacing each deadline by a modified deadline that accounts for the deadlines of the job's successors. Their §2 Theorem says that a single sequence, the one in increasing order of modified deadlines, decides feasibility. They use it as the first step of their dynamic programming method for sequencing with deadlines and precedence constraints: because the sequence does not depend on processing times, the jobs to be scheduled on time can always be taken in this one fixed order.
There are jobs . Job has a processing time and a deadline . A sequence lists every job exactly once; the machine starts at time and processes the jobs in the order of , one after another, without idle time. The completion time of job is the sum of the processing times of and of all jobs before it in . Job is on time in if .
Precedence constraints are a partial order on the jobs (reflexive, antisymmetric, transitive). If and , job must precede job ; such a is a successor of , and every job counts as one of its own successors. A sequence is consistent with if no job appears before a job that must precede it. The jobs are numbered so that implies .
For a number the modified deadline of job is
the earliest deadline among and its successors, plus a tie-breaking term. The paper takes to be "a small number"; here that means and whenever .
Let be the sequence in which increases. Then
The Theorem reduces a question over all sequences consistent with to the evaluation of one sequence, and the sequence depends only on the deadlines and on , not on the processing times. This independence is what the paper's later sections rely on: it lets a subset-selection dynamic program (Eq. (1) of the paper) process jobs in a fixed order. Without precedence constraints ( the identity) the Theorem is Jackson's rule. The operational form, "always take next, from among the available jobs, a job which has a successor with the earliest possible deadline", is a list-scheduling rule of the same kind as the backward rule of Lawler (1973) for .
The result has been proved on paper since 1969. As far as is known it has no machine-checked proof. This mission produces a formal proof of the Theorem and of the exchange step behind it, stated on the same sequence and completion-time model as the platform's existing single-machine scheduling missions.
The obvious argument is the exchange argument for Jackson's rule: swap an adjacent pair that is out of order and check that nothing becomes late. Two things fail without care. First, the swap must not violate precedence; this is why the deadline of a job is replaced by the minimum over its successors. Second, after the swap, job completes when job used to complete, but need not be at least : one must find a successor of that is later in the sequence, on time, and due no later than . That step uses the smallness of : with a large the tie-breaking term outweighs a difference of deadlines, and the Theorem fails (three jobs without precedence, , , ). Finally, the exchange step must be turned into a terminating transformation of an arbitrary feasible sequence into , a bubble-sort argument over lists.
Fin n, 0-based: the Lean job j is the paper's job , and the tie-break is . Processing times and deadlines are real.MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (a duplicate-free list of all jobs; start at time , no idle time). Idle time never helps meet a deadline, so this loses nothing. Consistency with is the published LawlerPrec.MinMax.IsFeasible.insert j {k | ρ j k}, which is nonempty; for the reflexive of the paper this is ("considering a job to be one of its own successors").Related platform items: Jackson's rule for unrestricted jobs is already posed as MooreLateJobs.NumLate.jackson (Moore 1968) and is not re-posed here; Lawler's theorem is posed as LawlerPrec.MinMax.sequencing_theorem. Contributions welcome: general list-exchange lemmas (adjacent swaps, bubble-sort termination toward a sorted list) are reusable well beyond this mission.
A many-server queue in which customers arrive at the epochs of a renewal process and are served for exponential times is the basic model of a telephone exchange, a call centre, or a bank of identical machines. Its continuous-time queue-length process is not Markovian unless the arrivals are Poisson, so Erlang's birth–death formulas for M/M/s do not apply. In 1953 D. G. Kendall showed how to analyse such systems by the method of the imbedded Markov chain: observe the system only at the arrival epochs, where the number of customers present does form a Markov chain, and read the equilibrium behaviour off that chain (Kendall 1953).
Timeline:
Customers arrive with independent inter-arrival times of law on and mean , . There are servers and a single queue served first come, first served. Service times are independent of one another and of the input, negative-exponential with mean , . The relative traffic intensity is .
The state of the imbedded chain at an arrival epoch is the number of persons found ahead (waiting or in service) by the arriving customer. Its transition matrix of eq. (8) is given in three blocks, written with the death-process probabilities of (9)–(10), the probabilities of (11)–(12), and the Poisson probabilities of (13)–(14):
The key function is
The queue size met by an arrival is . The waiting time is, given , the sum of independent exponential variables of mean .
When the chain has a limiting distribution , and with the root of in and ,
with both conditioning events of positive probability. The goal fixes no constant beyond those the theorem names: and are determined by , and .
Theorem IV says that, whatever the input law and the number of servers, the part of the equilibrium waiting-time law away from zero is exponential and the part of the queue-size law away from zero is geometric, both governed by the single number . All equilibrium quantities of GI/M/s (Theorems II–III and the delay distribution) then reduce to computing from a one-dimensional equation and the finitely many 's from a triangular linear system. This is the standard textbook treatment of G/M/c queues and the template for many later matrix-geometric results.
The results are proved in the paper, partly by appeal to Feller's theory of denumerable chains and to "tedious but elementary" verifications. None of them is machine-checked. The mission formalizes the paper's chain of argument: the explicit transition matrix, its stochasticity, the reduction of the invariance equations, the passage from a summable invariant vector to the limiting distribution, and the computation of the laws of and from it. The single-server special cases are posed separately on the platform (QueueingFundamentals.GM1.arrival_point_geometric, GM1.waiting_time_cdf, GM1.arrival_point_means, GM1.mean_waiting_times, FosterQueues.GIM1.gim1_classification); they do not cover .
The obvious route is to guess the geometric tail and check it against the balance equations. For this works, but the rows of the block involve the convolution integral (11), and the equations for couple the geometric tail to the boundary terms . Showing these are solvable, and that the row sums of the three-block matrix equal one, requires handling (11) explicitly. The second obstacle is the limit theorem itself: an invariant vector does not, by itself, give . That step needs Feller's dichotomy for irreducible aperiodic denumerable chains, which Mathlib does not provide. Finally, the conditional waiting-time law requires summing an Erlang mixture with geometric weights in closed form.
The queue process itself is not formalized. The chain is defined by its transition matrix (8)–(14), and by the Erlang mixture of p. 349, as the paper derives both by a modelling argument. A chain is any TransitionMatrix P of the published Markov-chain vocabulary with P.p = gimsMatrix s A b; states are -based. "Ergodic" is Feller's: Aperiodic ∧ PositiveRecurrent. The limiting distribution is asserted as Tendsto (P.stepProb n i j) atTop (𝓝 (π j)) for all , not as a stationary vector. The input law satisfies the published IsInterarrivalLaw A a⁻¹ (a probability measure carried by , integrable, mean ), and is the published serviceProb A (s/b) n. Conditional laws are stated multiplied out, together with positivity of the conditioning probabilities. Every series identity is stated with HasSum.
Trivializing formalizations are ruled out: is tied to on rather than free; is the limiting distribution of , asserted to exist, not a probability vector handed to the statement; the conditioning events are asserted to have positive probability; the matrix is the GI/M/s matrix, not the GI/M/1 one; and the 's of Theorems II–III are characterized by the invariance equations, never defined from .
A complete development needs: Feller's limit theorem for irreducible aperiodic positive recurrent chains (reusable well beyond this mission), Foster's sufficiency criterion (referenced, open), Fubini for the stochastic-matrix identities, parametric interval integrals for the block , and Erlang distribution functions. Contributions to the general Markov-chain milestones are as welcome as those specific to GI/M/s.
The single-server queue with general independent interarrival and service times (the GI/G/1 queue) is the basic model of congestion in operations research: customers arrive at a service facility, wait if the server is busy, are served in order of arrival, and leave. The first question about any such system is whether it settles down. If customers keep arriving faster than they can be served, waiting times grow without bound; otherwise one expects an equilibrium distribution of waiting time that capacity planning, staffing and performance analysis can be based on.
D. V. Lindley's 1952 paper Lindley 1952 answered this question for the GI/G/1 queue in complete generality. It introduced the recursion for successive waiting times that now carries his name, connected the queue with a random walk, and proved that an equilibrium exists exactly when the mean service time is smaller than the mean interarrival time, with the degenerate deterministic case as the only exception. The paper is the starting point of the random-walk approach to queueing theory and of the later work of Kiefer and Wolfowitz, Spitzer, Loynes and Kingman.
Customers arrive in order at a single server; customer is served after all its predecessors. On a probability space let
Assumption 1: the are independent and identically distributed with finite mean . Assumption 2: the are independent and identically distributed with finite mean , and the families and are independent of each other.
Put ; the are i.i.d. and integrable, and denotes their common mean. The waiting time of customer (time from arrival to start of service) satisfies Lindley's recursion
Write for the waiting-time distribution function, for the law of , and for the associated random walk. Lindley shows that converges for every to
The theorem is the stability criterion for the GI/G/1 queue, and its proof identifies the equilibrium waiting time with the supremum of a random walk with negative drift. Every later result on the equilibrium waiting time (Pollaczek–Khinchine for M/G/1, Kingman's bounds, the Wiener–Hopf factorization, heavy-traffic limits) presupposes this existence statement. The critical case is the part that goes beyond the law of large numbers: there is no equilibrium even though the queue has no drift.
The result has been proved since 1952 and appears in every queueing textbook. No machine-checked proof of it is known to exist. The platform already has related open statements in other frameworks: a law-level one-step identity and the stationary-delay equation from Gross et al. (QueueingFundamentals.GG1), and Loynes' theorem in a stationary ergodic Palm framework (PalmQueueing.Loynes.loynes_stability). None of them states convergence of the customer-indexed waiting-time distributions, and none treats the critical case. This mission produces the customer-indexed model, the random-walk duality, and the complete iff, including the Chung–Fuchs recurrence theorem for one-dimensional random walks, which is of independent use.
Cases (i) and (ii) follow from the strong law of large numbers, which Mathlib provides. The obstacle is the critical case : the strong law only gives , which says nothing about whether is finite. One needs the recurrence of mean-zero random walks (Chung–Fuchs), which is not in Mathlib. A second, smaller difficulty is eq. (3): it is an identity of probabilities, not of events, since the waiting time is built from sums taken in the reverse order of the walk's partial sums. Finally, the iff needs a careful passage from pointwise limits of distribution functions to convergence to a probability measure.
All objects live in one definitions file, LindleyQueue.Stability.Model. The input is a structure Input Ω P holding measurable sequences s t : ℕ → Ω → ℝ with iIndepFun for each family, identical distribution, integrability, independence of the two families as random elements of , and nonnegativity. Theorems assume IsProbabilityMeasure P. Committed conventions:
w 0 is the paper's , F r is , U n u i is the paper's .u 0; is the push-forward law of u 0, and Stieltjes integrals are integrals over Set.Iic x.Trivializing formalizations are ruled out: the goal is about the queue's , not the random walk's absorption probabilities; the limit must be a probability distribution, since "converges to some function" is already the limit milestone; and "" is almost-sure, not pointwise. A verification file builds an Input with , so the hypotheses are satisfiable.
Needed infrastructure: exchangeability of finite i.i.d. vectors, continuity of measure along decreasing events, the strong law (in Mathlib), recurrence of one-dimensional random walks, and convergence of distribution functions. The Chung–Fuchs theorem and the random-walk duality are reusable well beyond queueing; contributions of either are welcome.
The newsvendor problem is the basic single-period inventory model: a decision maker orders units before a random demand is observed, pays per unit of unmet demand and per unit left over, and minimizes the expected cost . When the distribution of is known, the optimal order is the quantile of . In practice the distribution is unknown and only a sample of past demands is available; the standard data-driven order is the sample average approximation (SAA), the quantile of the empirical distribution.
R. Levi, G. Perakis and J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights (Operations Research 63(6), 2015), ask how many samples guarantee that the SAA order is -optimal with high probability. Levi, Roundy and Shmoys (2007) gave a distribution-free bound. Levi, Perakis and Uichanco show that, asymptotically in , the right measure of difficulty is a single scalar of the demand law, the weighted mean spread at the critical quantile, and that for the class of log-concave demand distributions (normal, uniform, exponential, logistic, Laplace and many others used in inventory theory) this scalar is bounded below by . That uniform bound turns a distribution-dependent sample-size guarantee into one that holds for every log-concave demand, and is markedly tighter than the distribution-free one.
This mission formalizes the bound (Proposition 2) and the chain of lemmas the paper uses to prove it. The source is the authors' accepted manuscript of the paper (MIT DSpace), cited by its own page numbers.
Fix costs , and the critical ratio . A demand law is given by a probability density : measurable, nonnegative, with . Its cdf is , and its quantile is
The absolute mean spread (AMS, Definition 1) at is the gap between the conditional means above and below ,
and the weighted mean spread (WMS, Definition 2) is .
A density is log-concave (Definition 3) if is concave on its support. Equivalently, for all and ; this form allows to vanish outside an interval.
For a log-concave and a point with , the number is a supergradient of at , written , if for all with . The paper splits the class of log-concave densities into the subclasses of densities with quantile , and , and minimizes the AMS over each subclass (problem (11)). The minimizer is the truncated exponential density
and zero elsewhere (display (12)), with AMS in closed form.
The Lean development uses the names IsPdf, cdfOf, quantileOf, ams, IsLogSupergradient, tildeF and zStar for these objects, in the namespace DataDrivenNV.WMS.
For every log-concave density ,
The statement has no further hypothesis: no moment condition, no continuity, no restriction on .
The proposition is what makes the paper's log-concave sample-size bound (Theorem 4) parameter-free: the probability that the biased SAA order is -optimal is, asymptotically, at least (Theorem 3), and Proposition 2 replaces the unknown by . A manager who only knows that demand is log-concave can then size a sample without estimating any parameter of the law.
The result is proved in the paper; nothing about it is open. As far as is known it has no machine-checked proof. Formalizing it produces a checked lower bound for an inventory-theory quantity together with reusable facts about log-concave densities on the line: exponential envelopes from a supergradient, the quantile-and-slope constraints of Lemma 1, and the comparison of conditional means behind the Domination Lemma.
The definitions are elementary, but the proof passes through an infinite-dimensional optimization problem over a class of densities. The obvious first step, "the AMS is minimized by the most concentrated density", has no direct meaning without fixing the density value and the slope of at the quantile; after fixing them, one needs the envelope of Lemma 2, a stochastic comparison (Lemma 3) and an explicit integral of a truncated exponential. The Domination Lemma as printed is false (a density whose support has a gap to the right of is a counterexample), so it is formalized under the hypothesis that the dominating density is positive exactly on an interval around , which is how Proposition 1 uses it. The case (uniform minimizer) and the two boundary values of (one-sided exponential minimizers) are not covered by the closed form (12) and must be handled separately in a proof of the goal. Finally, Lemma 1 rests on the monotonicity of the failure rate and the reversed hazard rate of log-concave laws, which must be proved from log-concavity.
Densities are functions ℝ → ℝ with IsPdf f (measurable, nonnegative everywhere, integrable, total integral 1); the law of is never introduced separately. Log-concavity is the published definition ConvexOptimization.LogConcaveOn Set.univ f (power form, zeros allowed). Concavity of Real.log ∘ f is not used, because Real.log 0 = 0 would treat as off the support. The quantile is an sInf; for its defining set is nonempty and bounded below. The AMS is the difference of two ratios of integrals. At the quantile both denominators are positive, and the goal and Proposition 1 assume no integrability of , since log-concave densities have exponential tails. The value is taken pointwise; lies in the interior of the support, where a log-concave density is continuous.
Conventions and disclosed departures from the page:
Assumption 1 of the paper (monotonicity of beyond ) and the continuity assumption of §3 are hypotheses of Theorems 3–4 only and are not used here. A formalization in which or takes a junk value (a non-integrable , a zero denominator) would make the goal trivially true or false; the hypotheses above exclude this, and no statement assumes the conclusion of another.
Contributions welcome: proofs of the milestones in any order; general lemmas on log-concave densities on (exponential tails, integrability of moments, monotone hazard rates, continuity in the interior of the support); and the boundary cases of problem (11).