Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The proximal point algorithm is a basic iterative scheme of convex optimization and monotone operator theory. To solve a problem governed by a monotone operator, it replaces the problem by a sequence of better-conditioned problems, each regularized by a quadratic term centred at the previous iterate. Augmented Lagrangian methods, the Douglas–Rachford and ADMM splitting schemes, and many bundle methods can all be read as instances of it.
The scheme first appeared in a five-page note by Bernard Martinet in the Revue française d'informatique et de recherche opérationnelle (1970), under the name régularisation par approximations successives. Martinet stated it for a monotone variational inequality on a bounded closed convex subset of a Hilbert space and proved that the weak cluster points of the iterates are solutions. This mission formalizes that first convergence theorem as it was originally stated.
Timeline.
Let be a real Hilbert space with inner product and norm . Let be its dual, and write for the value of a functional at . Let be convex, closed and bounded, and let be
The variational inequality (1) asks for such that
Its solution set is denoted (solSet T C in Lean).
Martinet's regularization algorithm starts from . Given , it determines such that
In words, solves the variational inequality for the operator , which is strongly monotone. A point is a weak cluster point of if every neighbourhood of in the weak topology contains for infinitely many .
Every weak cluster point of the regularized iterates solves (1). The paper's Lemme 2 states the same thing. The goal assumes neither that (1) has a solution nor that is bounded on .
The result. Théorème 1 is the first convergence theorem for the proximal point method. The method only needs to solve strongly monotone subproblems, and those are well posed even when the original problem is not. Together with the existence result, the theorem says the iterates accumulate weakly only at solutions. When the solution is unique, the whole sequence converges weakly (the Corollaire). The later theory of Rockafellar, Brézis–Lions and the splitting literature refines this statement.
Formalizing it. The result has been proved since 1970. What this mission adds is a machine-checked version that follows the original hypotheses: an operator into the dual, hemicontinuity rather than continuity, and no maximality assumption. The cited ingredients, the Lions–Stampacchia existence theorem in an infinite-dimensional Hilbert space and Minty's lemma, are not in Mathlib as far as this mission is aware. Formalizing them is part of the work and is reusable well beyond this paper. The milestone items on the platform are statements awaiting proof. None of them has a machine-checked proof yet.
Lemme 1 and inequality (7) follow from the defining inequality (2) and the algebra of the inner product. The difficulty is at two other points.
First, the iterates satisfy the variational inequality only approximately, and only with evaluated at the iterate. A weak cluster point gives no control over , because is merely hemicontinuous and is not assumed weakly continuous or bounded. The obvious idea, to pass to the limit in , fails for this reason. Passing to the limit requires the reformulation in which is evaluated at a fixed point of . That reformulation is Minty's characterization (5), and proving it uses hemicontinuity along segments.
Second, the proof of Lemme 1 needs a solution of (1) to exist. In infinite dimensions that is the Lions–Stampacchia theorem. Its standard proof goes through Brouwer's fixed point theorem on finite-dimensional sections together with weak compactness of , and this is the heaviest item of the mission.
NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H. The paper says only "espace de Hilbert". Its ordered inequalities force real scalars.StrongDual ℝ H, and is φ y. is not replaced by a map through the Riesz isomorphism.IsRegSeq): any sequence with that satisfies (2) at every step. Existence and uniqueness of the step are milestone 2, not built into a definition.MapClusterPt in WeakSpace ℝ H, a cluster point in the weak topology. It is not a cluster point in the norm topology, which would make the goal weaker.Filter.liminf on returns a junk value on sequences that are unbounded below.A trivializing formalization is ruled out. The goal does not assume , boundedness of , or strong cluster points. Its hypotheses are satisfiable: , , , is an instance, checked locally.
Not formalized: Remarques 1 and 2 of §II (a variable-weight variant of (2), whose printed form is apparently misprinted, and the removal of boundedness of under a coercivity condition), because the paper gives neither a proof. Théorème 2 (§III) and the convex-minimization §IV are not formalized either. §IV is the subject of the companion mission.
Contributions are welcome on each milestone, and especially on the general infrastructure: Minty's lemma, Hartman–Stampacchia/Lions–Stampacchia existence for monotone hemicontinuous operators, and the fact that bounded sequences in a Hilbert space have weak cluster points. A proved Brouwer fixed point theorem (AGT.brouwer_fixed_point) and a Banach–Alaoglu theorem (FamousTheorems.banach_alaoglu) are available on the platform as tools.
Many problems in optimization and equilibrium modelling, among them linear and nonlinear complementarity problems, variational inequalities over polyhedra, and the Karush–Kuhn–Tucker conditions of nonlinear programs, can be written as a single generalized equation
where is the normal-cone operator of a closed convex set . S. M. Robinson introduced strong regularity of such an inclusion at a solution in Strongly regular generalized equations (1980) and proved an implicit-function theorem for it: when the linearised inclusion has a locally unique, Lipschitz inverse, solutions of the perturbed problem exist, are locally unique and depend Lipschitz-continuously on the perturbation. Strong regularity has since become the standard stability notion behind sensitivity analysis and the local convergence of Newton-type methods for variational problems; see Dontchev and Rockafellar, Implicit Functions and Solution Mappings (Springer, 2nd ed. 2014, doi:10.1007/978-1-4939-1037-3).
Strong regularity depends only on the linearisation, so deciding it means deciding it for a linear generalized equation. For a general polyhedral set the paper's appendix does this by a reduction: locally around the problem is equivalent to a homogeneous problem on a cone, the reduced form, and strong regularity is equivalent to unique solvability of that reduced form. This mission formalizes that appendix and the criterion it yields.
Work in with the standard inner product, which identifies with its dual. For the normal cone at is
A set is polyhedral convex if it is the intersection of finitely many closed half-spaces. Fix a nonempty polyhedral convex , an real matrix and , and consider
It is strongly regular at a solution with constant if there are neighbourhoods of and of such that for each the perturbed inclusion
has exactly one solution in , and on .
The reduction uses the following objects, all built from the data:
The reduced form of (A.1) at is the inclusion for ; in an orthonormal basis adapted to , and it is with an matrix . It is vacuous when .
If solves (A.1), then (A.1) is strongly regular at if and only if
No Lipschitz constant is fixed: the left side is "strongly regular for some ".
Theorem A.4 turns a local stability property, defined through neighbourhoods and an inverse map, into a finite-dimensional algebraic question about one homogeneous problem on a polyhedral cone. Combined with the Schur-complement criterion of Theorem 3.1, it gives checkable conditions (Corollary 3.2): nonsingularity of a block and positive definiteness, or the P-matrix property, of its Schur complement. Through the KKT reformulation of §4 this is the route by which strong second-order sufficiency and linear independence of binding constraint gradients imply strong regularity in nonlinear programming. The example of p. 53 shows the criterion deciding cases where itself is neither positive definite nor a P-matrix.
The results are classical and proved in the paper; to our knowledge none of them has a machine-checked proof. The formalization adds a coordinate-free statement of the reduced form, which the paper writes only in an adapted basis; a Lean account of exposed faces and tangent cones of polyhedra, with their local conic structure (Propositions A.1–A.2), which the paper lists "without proof" and cites to Rockafellar; and checked versions of the corollary and the example.
The definition of strong regularity is local, while condition (ii) is global on . The obvious argument, "linearise and read off the inverse", does not apply, because is a set-valued map whose graph changes shape from point to point. The step that carries the weight is Proposition A.3: a perturbation of may move the solution off the face , and only polyhedrality, through the finitely many values of on and the local conic structure of A.1–A.2, rules this out uniformly in a neighbourhood. The direction from strong regularity to (ii) needs positive homogeneity of the reduced form to pass from uniqueness near to uniqueness on all of . The direction from (ii) to strong regularity needs the Lipschitz property of a single-valued inverse of a polyhedral multifunction (Robinson 1979, cited as [12, Proposition 2]), which is not elementary.
EuclideanSpace ℝ (Fin n), with inclusions written as memberships: (A.2) is . A matrix acts through Matrix.toEuclideanLin. The normal cone carries the clause , so off ; without it every inclusion would be satisfiable at points outside and the statements would change meaning.Submodule.starProjection.A constrained system can be written as a generalized equation: a smooth or linear expression must balance the normal cone of a feasible set. This form includes variational inequalities and the first-order conditions of many optimization problems. It is useful to know whether a small change in the right-hand side determines one nearby solution and how far that solution moves. In the linear finite-dimensional case, Robinson's Theorem 3.1 gives matrix conditions that guarantee something stronger: a unique solution for every right-hand side, with one Lipschitz bound valid over the entire space. The theorem also identifies an exact matrix criterion when the feasible set is a product with a nonnegative orthant.
The question is relevant whenever some coordinates of a system are free and others are constrained by inequalities. Eliminating the free coordinates produces a smaller matrix, the Schur complement. The resulting condition can be checked on the reduced block, and in the orthant case it becomes the familiar P-matrix criterion from linear complementarity. Robinson states both claims in a single theorem and relates them to the behavior of a generalized equation rather than to an isolated matrix property Robinson, pp. 51–52.
Let be positive integers and give its Euclidean norm. Write , with and . Let be nonempty, closed, and convex, and put . For , the normal cone is
For , is empty. Thus the inclusion itself enforces feasibility. This is Robinson's indicator-subdifferential convention Robinson, pp. 43 and 51.
Partition the real square matrix into blocks , , , and , where is . When is nonsingular, its Schur complement in is
A real matrix is positive definite in the theorem's sense when for every nonzero . Symmetry is not assumed. A P-matrix has strictly positive determinants for every nonempty principal submatrix. Write for the vectors with all components nonnegative. These conventions are stated or used in Theorem 3.1 and its proof.
For , the first target is the sufficient condition
Here “is Lipschitz” includes that exactly one inverse value exists at every . The assertion holds for every nonempty closed convex ; it is not restricted to polyhedral sets.
When , the second target is an equivalence:
The goal theorem is the conjunction of these two statements, matching Theorem 3.1. Its milestones record the paper's local upper Lipschitz assertion for polyhedral multifunctions, the block reduction, the reduced inverse result, the complementarity characterization, and the necessity of nonsingularity.
The first part gives a global sensitivity guarantee for a generalized equation with an arbitrary nonempty closed convex lower-block constraint. For any two right-hand sides, their unique solutions differ by at most a fixed multiple of the distance between those right-hand sides. The second part tells when this guarantee holds for the orthant model: the P-matrix condition is necessary as well as sufficient. These are the precise conclusions of Robinson's theorem; the mission concerns their machine-checked formalization, not an unresolved mathematical conjecture.
A complete development would provide reusable definitions of the normal-cone generalized equation, an explicitly nonsymmetric notion of positive definiteness, P-matrices, and the global inverse property. It would also formalize the linear complementarity characterization quoted in the paper. The current draft has Lean-checked statements with proof placeholders. No proof of Theorem 3.1 or of its milestones is claimed here.
Nonsingularity of the full matrix alone does not decide whether the constrained inverse exists uniquely: the normal cone can change as reaches different faces of . A pointwise uniqueness argument also does not by itself supply one Lipschitz constant on all of . For the orthant case, checking only the full determinant or leading principal minors would miss the criterion Robinson invokes; every nonempty principal minor matters. The difficulty is to connect a global statement about all right-hand sides with the reduced matrix condition while preserving the normal cone's behavior at boundary points Robinson, pp. 51–52.
Lean represents as a Euclidean space indexed by the disjoint union of and . This gives the paper's Euclidean norm rather than the sup norm of a product type. The normal cone is empty off its set, and the inverse property explicitly requires existence for every right-hand side, uniqueness, and one global real Lipschitz bound. The Schur complement appears only with a nonsingular in the substantive claims; matrix inversion on a singular input would otherwise be totalized by Lean. Positive definiteness does not add a symmetry hypothesis. The goal retains as printed; the paper's later remark about zero-dimensional blocks is outside this theorem.
The polyhedral milestones use finite intersections of closed half-spaces. The reduced-operator milestone uses a nonempty closed convex , matching the theorem's setting. The LCP milestone allows any finite dimension; at dimension zero, both its universal uniqueness statement and its empty-minor P-matrix condition hold. A weaker encoding in which the inverse is merely single-valued where it happens to exist would erase the global conclusion and is excluded here.
Solvers can contribute the block-normal-cone equivalence, the global inverse statement for the reduced operator, the polyhedral Lipschitz result, the P-matrix characterization, and the final theorem. The normal-cone and matrix definitions can also serve later generalized-equation missions that use the same conventions.
The job-shop scheduling problem asks how to time a set of tasks on shared machines so that every product is finished as early as possible. Around 1959 several authors proposed to solve it with Gomory's then new integer programming (Gomory 1958). The obstacle is the noninterference condition: two tasks on the same machine must not overlap, so one of them must finish before the other starts. That is an "either-or" condition. It describes a nonconvex set, and classical linear programming cannot express it.
A. S. Manne's note On the Job-Shop Scheduling Problem (Operations Research 8 (1960) 219–223) writes the either-or condition as two linear inequalities in integers. It adds one 0–1 variable per pair of tasks that compete for a machine, and it uses a large constant derived from a bound on the start days. This is the origin of the big-M disjunctive formulation, which remains the standard textbook integer program for job shops and, more broadly, the standard way to linearize a disjunction of two linear inequalities.
Timeline. Johnson (1954) introduced the make-span criterion for two- and three-stage production schedules. Bowman (1959) and Wagner (1959) proposed integer programs for machine scheduling. Manne (1960), stimulated by Bowman's paper, gave the formulation stated here. He counted its unknowns as 275 for 5 machines with 10 tasks each, against 600 for Wagner's formulation on the same example (p. 222).
There are tasks and machines. Task requires the single machine for consecutive days, where is an integer. An integer horizon bounds the start days: the integer unknown is the day on which task begins. A pair with and is a conflicting pair. For each such pair the tasks must not overlap:
The instance may also impose precedence for given pairs (5a), exact delays for given pairs (5c), and delivery dates for given tasks (6). A schedule is an satisfying (1), (5a), (5c) and (6). Its make-span is
the calendar time needed for all jobs when the shop starts on day .
Manne's integer program has integer unknowns with , one integer for each conflicting pair, and the minimand , subject to (5a), (5c), (6),
and for every (7). The value means that precedes ; means that precedes .
For every instance and every integer ,
Both minima are required to exist. In particular the program has an optimum exactly when a schedule exists. The paper claims this when it says that "the problem now consists of the minimization of " subject to (2)–(7) (p. 221).
The result. The goal certifies that a single integer program, with one binary variable per conflicting pair, computes the optimal make-span of a job shop with precedence, exact delays and delivery dates. The same pattern is used whenever a disjunction or of bounded linear forms has to be put into a mixed-integer program: a binary variable selects the active branch, and a constant at least as large as the range of the inactive form switches the other branch off. Milestone 1 is that pattern in its simplest form, and milestone 4 shows why the binary variable cannot be relaxed.
Formalizing it. The paper's argument is informal. It rests on a summary table of admissible values of that holds only when the gap is large enough. A machine-checked version fixes the exact hypotheses: integrality of , the bound , and nonemptiness of the task set. To the best of the curators' knowledge, no machine-checked proof of the correctness of the big-M job-shop formulation exists; the definitions here can serve later scheduling missions that need a disjunctive integer program.
The mathematics is elementary, and the difficulty lies in stating it exactly. The obvious reading, "(3)–(4) are equivalent to (1)", is false without the bound . For instance, with condition (4) reads , which cuts off valid orders if start days may lie beyond the horizon. It is also false for real . Equally, "minimize subject to (7)" equals the maximum of only after the optimum over and over are interchanged and the empty task set is excluded. A naive formalization that states the schedule side as "the least with (7)" proves nothing about the make-span.
Tasks are Fin n (the paper's task is index ), machines Fin M. Start days, durations, horizon, delays, delivery dates, and are integers (ℤ), so that and are not truncated. Durations are not assumed positive except in milestones 2 and 4, where positivity is necessary. One definitions file, ManneJobShop.Formulation.Model, holds the instance, the conflicting pairs, schedules, the make-span (Finset.sup', so is required via [NeZero n]) and the integer program.
Explicit readings of loose phrases:
IsLeast of the feasible values of , matched against IsLeast of the set of make-spans of schedules.Trivializing formalizations are ruled out: the make-span is a maximum, not a restatement of (7); is an integer; the horizon appears on both sides; the goal is stated for every instance with , including infeasible ones. The (5b) example is (5a) for two pairs. Wagner's comparison, the remarks on Gomory's algorithm, Dantzig's secondary constraints and Monte Carlo methods, and the economic discussion of the make-span are not formalized. Proofs of every milestone and of the goal are welcome.
Many problems of optimization and equilibrium can be written as one inclusion. Some examples are the Karush–Kuhn–Tucker conditions of a nonlinear program, nonlinear complementarity problems, variational inequalities and the equilibrium conditions of economic and traffic models. In each of them a point has to satisfy . In applications the data depend on parameters: estimated coefficients, prices, or the iterate of an algorithm. One then wants to know whether a solution persists under a perturbation of the parameter, whether it stays locally unique, and how fast it moves. For a smooth equation the classical implicit-function theorem answers all three questions. Inequality constraints make the solution set nonsmooth, and the classical theorem no longer applies.
S. M. Robinson's paper Strongly regular generalized equations (Math. Oper. Res. 5 (1980) 43–62) introduced the condition of strong regularity and proved an implicit-function theorem for generalized equations under it. The condition and the theorem became the starting point of the stability theory of variational inequalities and nonlinear programs. Later work characterises strong regularity for nonlinear programs (Robinson's own §4, through the strong second-order sufficient condition), and develops it in the theory of metric regularity and of single-valued Lipschitz localisations (Dontchev–Rockafellar, Implicit Functions and Solution Mappings, Springer 2009/2014). Its sensitivity results underlie the convergence analysis of Newton and sequential quadratic programming methods for these problems.
This mission formalizes §1–§2 of the paper: the definition, the implicit-function theorem (Theorem 2.1) with its proof, and the three results derived from it.
Let be a real normed linear space and its topological dual, the continuous linear functionals on . Let be closed and convex. The normal-cone operator of is
A generalized equation is the inclusion , for a function from an open set to . For it is the equation . For the nonnegative orthant of it is the nonlinear complementarity problem. For a general closed convex it is the variational inequality over .
Let solve the generalized equation, and let be Fréchet differentiable at . Linearising gives the multifunction
The generalized equation is strongly regular at with associated Lipschitz constant if there are neighbourhoods of in and of with the following property: for every the inclusion has exactly one solution in , and on . The condition depends only on , and .
In the parametric problem the function is , with in a topological space and base point . Its partial derivative in is .
Assume that exists on , that and are continuous at , and that solves , strongly regularly with constant . Then for every there are neighbourhoods of and of , and a function , with two properties. First, is the unique solution in of . Second,
Write for the linearisation at , for the residual, and . The milestones are four claims of the proof:
Theorem 2.1 reduces the stability of a nonsmooth problem to a property of one linearised problem at the base point. Once strong regularity is checked at , the solution exists, is locally unique and moves in a Lipschitz manner for every nearby parameter. Corollary 2.2 and Theorem 2.3 make this quantitative. Theorem 2.3 shows that a linear complementarity problem or a quadratic program approximates the nonlinear solution to first order. Theorem 2.4 is the analogue of Banach's perturbation lemma, which keeps an operator invertible under small perturbations. The later sections of the paper give checkable criteria for strong regularity: a Schur-complement test, a reduced-form test over polyhedral sets, and second-order conditions for nonlinear programs. Those criteria are the subject of the companion missions II–IV.
The theorems have been proved since 1980 and have been restated in textbooks. No machine-checked version of strong regularity or of this implicit-function theorem is known. Mathlib has the classical implicit- and inverse-function theorems for maps between Banach spaces, and the contraction mapping principle. It has nothing on normal-cone operators, generalized equations or Lipschitz localisations. The formalization adds this layer. It also shows that Theorem 2.1 needs no completeness of .
The obvious approach is to apply the classical implicit-function theorem. It fails because is set-valued and is not differentiable in any useful sense. The inverse is localised only to a neighbourhood and is single-valued only there. So every step must keep the iterates inside sets on which strong regularity says something. The neighbourhoods have to be chosen in the right order: from , then and , then the ball radius , then the parameter neighbourhood. The estimate (2.4) has to come out with the constant and no larger. The page applies the contraction principle in a space it calls only normed. A faithful proof must also obtain the fixed point without completeness of , for example through the completeness of .
StrongDual ℝ X, the normal cone is a Set (StrongDual ℝ X) that is empty off , and an inclusion is written .HasFDerivAt at every point of , for every . Continuity of at is joint and in operator norm.A complete development needs the following:
The definitions of normal cone and strong regularity are reusable for variational inequalities in general. Contributions are welcome at any level: proofs of the milestones, the goal from the milestones, or the companion results from the goal.
Prediction with expert advice asks a learner to predict a binary label in each of a sequence of trials, having seen the predictions of a pool of prediction algorithms (the experts), and to make not many more mistakes than the best of them, with no probabilistic assumption on how the instances and labels are generated. Littlestone and Warmuth's Weighted Majority Algorithm (Littlestone, Warmuth 1994) maintains a weight for each pool member, predicts by a weighted vote, and shrinks the weights of members that err. Its mistake bounds are the origin of the multiplicative-weights method used throughout online learning, game theory and optimization (Arora, Hazan, Kale 2012).
A deterministic master with binary predictions can be forced to err in every trial in which the weight is split evenly, which costs it a factor of about two against the best expert. Section 6 of the paper introduces a randomized master, WMR, which predicts with probability equal to the weighted average prediction of the pool. Theorem 6.1 bounds its expected number of mistakes under a precisely stated condition on how its randomization interacts with the choice of instances and labels.
Timeline:
A pool of algorithms is run for trials on a probability space . In trial the pool member predicts , the label is , and the master predicts . All of these are random variables; deterministic sequences are a special case. Write .
Each member carries a weight. The initial weights are positive, and the update step (5.1) multiplies the weight of member in trial by a factor that depends on , and :
where and . WMR updates in every trial. Let , so and , and let
be the weighted average prediction. WMR predicts with probability . Its number of mistakes is .
The weak independence condition (p. 238) requires, for ,
The conditioning includes the current predictions of the pool and the current label. It allows instances and labels to depend on the master's past predictions, and it holds, for instance, when WMR draws one uniform number and predicts whenever , provided the instances and labels are generated independently of .
Under the weak independence condition, and with almost surely,
The statement fixes neither the pool, nor the update factors within (5.1), nor the distribution of instances and labels.
The step of the proof on p. 240: under the weak independence condition, almost surely, and hence
Theorem 6.1 gives the randomized master the same bound that Theorem 5.2 gives the deterministic master WMC, whose predictions are allowed to lie in . With equal initial weights, for every pool member with total loss , and the bound yields Corollary 6.1 (p. 241): . For close to this is better by nearly a factor of two than the bound for the deterministic binary master WMG. The weak independence condition is also what makes the bound valid against labels that adapt to the master's past predictions, which is the setting of later regret analyses.
The result is proved in the paper; this mission produces a machine-checked version. The platform has proofs of the randomized weighted majority bound in the form of Hazan's Lemma 1.4 and of Mohri et al.'s Theorem 8.4, but both state an expectation over the algorithm's internal distribution with deterministic data, unit weights and one fixed update rule. Neither covers random instances and labels, the conditional-expectation condition, or the whole class of updates (5.1).
The pathwise part of the argument is the loss bound for the weighted average (Lemma 5.3, posed in the companion mission on WMC). The new difficulty is probabilistic. The predictions, labels and weights are random and may depend on each other across trials, so the mistake indicator cannot be replaced by pointwise. The replacement holds only after conditioning on the -algebra , and requires that is -measurable and binary, so that the indicator is affine in . A reading that conditions on less (dropping the current label) or uses unconditional expectations does not support this step when the label depends on earlier randomness.
A second difficulty is that may be infinite: the weights can become arbitrarily small with positive probability.
The pool is Fin n; trials are indexed from to , so totalWeight … 0 is and totalWeight … t is . The probability space is a measure P with IsProbabilityMeasure P. Predictions, labels and master predictions are real-valued measurable random variables; pool predictions lie in and labels and master predictions in on every sample path. Initial weights are deterministic and positive. The update factor of member in trial is a measurable function of the member's prediction and the label, satisfying (5.1) on every sample path; the weights are computed from it, so they are random variables determined by the predictions and labels. is the supremum of the -algebras generated by the pairs , , and the weak independence condition is stated with Mathlib's conditional expectation P[λ j | 𝓕 j].
Expectations in the goal are lower Lebesgue integrals in , so the right-hand side may be and no integrability of the logarithm is assumed. The hypothesis almost surely excludes the case where the paper's bound is infinite and Lean's would make the literal statement false. A formalization that replaces the conditional expectation by the unconditional one, takes the logarithm's Bochner integral (which is when the logarithm is not integrable), or restricts to deterministic instances and labels does not state Theorem 6.1.
A complete development needs the pathwise loss bound of Lemma 5.3 for this weight model, the pull-out property of conditional expectations for bounded measurable factors, and the exchange of expectation and finite sums. The weight model and the filtration are reusable for Theorem 6.3 and for the lazy variant of the Appendix. Proofs of the milestone and of the goal are welcome, as are formalizations of Corollary 6.1.
In prediction with expert advice, a master algorithm predicts a binary label in each of a sequence of trials, after seeing the predictions of a pool of other algorithms (the "experts"), and is charged one mistake whenever its prediction differs from the label. No probabilistic assumption is made on the sequence: the goal is a bound on the master's mistakes, valid for every sequence, in terms of the mistakes of the best pool member. The Weighted Majority Algorithm of Littlestone and Warmuth (Inform. and Comput. 108, 1994) achieves this for a finite pool of members with mistakes, where is the number of mistakes of member .
Many natural pools are infinite: all programs in an enumeration, all hypotheses of a countable class, all values of a discretised parameter. Section 4 of the paper asks whether a master can compete with every member of a countably infinite pool , making at most mistakes for every , while keeping only finitely many weights at any time. Running the Weighted Majority Algorithm on infinitely many weights would give such a bound, but cannot be implemented.
Timeline. Barzdin and Freivalds (1972, 1974) studied prediction of a sequence by an enumerable family of functions and gave an essentially optimal bound for the case of a pool containing a member consistent with the whole sequence ( below). Littlestone and Warmuth's earlier versions of the paper (1989) introduced an algorithm WMI for infinite pools; the journal version (1994) replaced it by , which matches the Barzdin–Freivalds bound when and a consistent member exists, and extends it to pools in which every member may err.
Fix a parameter with and put . Fix two real functions and on the positive integers with
is the initial weight of the pool member , and bounds the weight of the tail .
A sequence of trials gives, for each trial , the prediction of every pool member and a label . Member makes at most mistakes: for at most trials .
The master keeps an active pool and a weight for each active member. With the number of its own mistakes so far, let
Initially, and after each trial in which it errs, raises (starting from ) to the least value with ; a newly activated gets weight . In a trial it computes the active weight predicting and predicting ; it predicts if , predicts if , and may predict either otherwise. After a mistake, every active member that disagreed with the label has its weight multiplied by . The weights of the analysis are the current weight of an active member and for an inactive one.
The goal is Theorem 4.1, part 3 (p. 227). Let be the total number of mistakes of on the sequence.
If , then
and if and for some , then .
At the beginning of any trial, is the minimum with , where counts the mistakes made in prior trials.
After any initial sequence of trials in which mistakes have been made,
The result. The bound holds simultaneously for every pool member, so the master competes with the best member of an infinite pool, paying for the position of that member in the enumeration. With and (the paper's Corollary 4.1) this is mistakes, with an active pool that grows exponentially in the number of mistakes but is finite at every time. Different choices of trade the mistake bound against the growth of the active pool. The same analysis shows how the predictions can be computed from finite-precision approximations of the weights, which is the reason for the slack band in the prediction rule. Its case recovers the Barzdin–Freivalds bound.
Formalizing it. The theorem is proved in the paper; no machine-checked version is known to exist, and there is no formalization of the Weighted Majority Algorithm on infinite pools on Prove2Me. The work is to formalize the paper's proof: the size statement for the active pool, the inductive invariant for the total weight, and the final logarithmic bound. The definition of a run of , with free predictions in the slack band and lazily activated weights, is reusable for other lazy-activation algorithms on countable pools, and the paper's Corollaries 4.1–4.3 are direct instances once the goal is proved.
The ordinary Weighted Majority analysis tracks the total weight of the whole pool, which shrinks by the factor after each mistake. For that argument does not apply as is: the master only sees the active weights, and the inactive tail, whose weight is unknown to the algorithm and charged at its initial value, may vote with the label. The obvious bound on the tail is too weak if applied with a fixed slack; it must shrink with the number of mistakes at the right rate so that the accumulated overhead stays below a constant factor. The slack band in the prediction rule interacts with this: when the master errs inside the band, the active majority may not have been wrong by much, and the shrinkage factor must be recovered from the band's width. The factor is where these effects are balanced.
The pool is indexed by ℕ+ and trials by Fin T; false encodes the prediction , true the prediction . IsWMI2Run is a relation between the input sequence and the master's predictions, the weights and the active-pool sizes at every trial boundary ; a prediction inside the slack band is unconstrained, so the theorems hold for every run. Only active weights are constrained; the analysis uses omega, which counts inactive members at . The bound is any upper bound on the mistakes of . The tail hypothesis is stated with a tsum together with Summable W, and the milestone on the total weight asserts summability of in its conclusion, so it cannot hold through the value that Lean assigns to a divergent series. The infimum in the goal is stated as a bound for every , which is equivalent. Logarithms in the ratio are natural logarithms (the base cancels); the bound uses Real.logb 2. The paper requires and to be computable; this only makes the algorithm implementable, and the formal statements hold for arbitrary real functions with the stated analytic properties.
A statement for an algorithm whose runs do not exist would be vacuous; runs of exist for every sequence under the hypotheses (this has been checked locally in Lean), because and keep the active pool finite.
Needed infrastructure: finite sums over the active pool, tsum manipulations for sequences that agree with outside a finite set, and real logarithm inequalities. Contributions welcome: proofs of the two milestones and the goal, and the Corollaries 4.1–4.3 as follow-up statements.
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.
Scheduling unrelated parallel machines to minimize the makespan, written , is one of the basic NP-hard problems of scheduling theory. A set of jobs must each be run on one of several machines, and the time a job takes depends arbitrarily on the machine; the goal is to finish all jobs as early as possible. Before the work formalized here, the best polynomial algorithm known guaranteed only a schedule within times the optimum (Davis and Jaffe, 1981), a factor that grows with the number of machines .
Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714, 1987; Math. Programming 46, 1990) gave a polynomial algorithm with guarantee , independent of . Their tool is a rounding theorem: a vertex of a natural linear-programming relaxation can be rounded to an integral schedule that exceeds each machine's budget by at most one job. The rounding theorem and the binary-search framework around it became standard material in approximation algorithms.
There are jobs and machines. If job is scheduled on machine , it takes time units, a positive integer. A schedule assigns every job to one machine . The load of machine is , the makespan of is the largest load, and is the minimum makespan over all schedules.
For deadlines and a threshold , let and . The linear program (LP) has variables for and constraints
The integer program (IP) replaces by and requires . A vertex of (LP) is an extreme point of its feasible polytope. The support graph of a point is the bipartite graph on machines and jobs with an edge whenever .
A -relaxed decision procedure answers, for a deadline , either 'no' or a schedule, such that (1) every schedule it returns has makespan at most , and (2) if it answers 'no', no schedule has makespan at most . The binary search of Lemma 1 starts from the greedy schedule (each job on a machine where it runs fastest), whose makespan is an upper bound , with lower bound , queries the procedure at , moves to on a schedule and to on 'no', and outputs the best schedule found once .
The LP rounding procedure answers, on deadline , by solving (LP) with : 'no' if it is infeasible, and otherwise a 0-1 solution of (IP) obtained by rounding a vertex chosen by the LP solver, supported on .
For every LP solver (every rule choosing a vertex of (LP) when it is feasible), an LP rounding procedure exists, and for every such the output of the binary search satisfies
Theorem 2 gives a constant-factor approximation for that does not depend on . The same rounding theorem drives the paper's second algorithm, a -approximation for a fixed number of machines using polynomial space, and the paper's lower bound shows that no polynomial algorithm achieves a factor below unless . The Rounding Theorem, in its later form for generalized assignment by Shmoys and Tardos (1993), is a standard tool for LP-based scheduling and assignment.
The result is proved; it has, to our knowledge, no machine-checked proof. The platform contains Matoušek and Gärtner's textbook version (MatousekLP.Scheduling.lst_two_approximation, Theorem 8.3.4 of Understanding and Using Linear Programming), which uses a different relaxation: one bound minimized parametrically over , optimal solutions with linearly independent columns, and no per-machine deadlines. This mission formalizes the report's own route: deadlines , arbitrary vertices, binary search over a relaxed decision procedure. A formal proof would also yield reusable statements about extreme points of transportation-type polytopes and matchings in pseudoforests.
The obvious rounding, putting each job on a machine where is largest, can overload a machine by many jobs at once: nothing in feasibility alone prevents many jobs from each placing a small fraction on the same machine. The bound requires that each machine receive at most one job that the vertex treats fractionally, and this fails for general feasible points; it holds only because is a vertex. The step that carries the weight is therefore a statement about the combinatorial structure of the support of an extreme point, which must be derived from the linear independence of the tight constraints, followed by a matching argument on the resulting graph. Neither step is available in Mathlib in the form needed.
On the algorithmic side, the binary search must be shown to return a schedule within although the decision procedure is only approximately correct; the invariants (the lower bound stays below , the stored schedule stays within times the upper bound) have to be tracked through a recursion.
Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive in Lemma 1 and Theorem 2 (the paper's model, p. 2). Loads, makespans and optimal schedules are the published MatousekLP.Scheduling.Schedule definitions applied to the real matrix ; is the makespan of a schedule σopt with IsOptimalSchedule.Set.extremePoints) correspond exactly. Theorem 1 and its steps are stated for real deadlines and real , more general than the paper's integers; the paper's proof does not use integrality, and mission 2 of this series needs non-integral .The assignment problem asks how to assign men to jobs, one man per job, so that the total cost (or, equivalently, the total rating) is optimal. It is the simplest combinatorial optimization problem with a nontrivial polynomial-time algorithm, and it appears as a subroutine across operations research: in transportation and network-flow methods, in tracking and data association, in scheduling, and as the relaxation behind branch-and-bound methods for the travelling salesman problem.
The algorithm studied here is the one now usually called the Hungarian method or Kuhn–Munkres algorithm.
The mission formalizes Munkres' correctness proof for §1 of that paper.
Let be a real matrix, being the cost of assigning man (row ) to job (column ). A set of entries is independent if no two of them lie in the same line (row or column). An assignment is a permutation , with the man doing job . Its cost is , and is an optimal assignment if this cost is at most that of every permutation . Choosing independent entries of minimum sum is the same as choosing an optimal assignment.
The algorithm. A state of the algorithm holds the current matrix, a set of starred zeros , a set of primed zeros , a set of covered rows and a set of covered columns. An entry is non-covered, once-covered or twice-covered according as it lies in zero, one or two covered lines.
The quantity , the maximal number of independent zeros of the matrix , measures progress.
For every real matrix :
The four clauses are needed together: optimality at final states alone holds for an algorithm that never stops.
Correctness of the Hungarian method is the basis of a standard algorithm for the assignment problem and, through it, of methods for transportation problems, minimum-cost bipartite matching and weighted bipartite matching. Its refinements remain in practical use. The invariants of the proof are the primal–dual structure of the problem: the row and column constants subtracted along the way form a dual solution, and the starred zeros at the end are a primal solution satisfying complementary slackness.
The result has been proved since 1957 and is in every textbook on combinatorial optimization. A machine-checked version of Munkres' specific procedure, as a transition system with all its free choices, with finiteness for real (not only integer) matrices, is not available on this platform; Mathlib has no assignment algorithm. The mission produces a verified specification of the algorithm, reusable invariants about covers and independent zeros, and a termination argument that does not rely on integrality.
Optimality at termination is short once the invariants are known. The work lies in two places.
First, the invariants hold only along runs. "Each is covered by precisely one line", "no column contains more than one " and "no row contains more than one " fail for arbitrary marked matrices, so they must be carried as an inductive invariant through every move, including the Step 3 transformation, which keeps the primes.
Second, termination. The obvious measure, the sum of the entries, decreases by at each Step 3, but for real entries can be arbitrarily small, so the decreasing sum gives no bound on the number of steps. The page replaces this argument by the stronger result of p. 35 (milestone 8), which holds for real entries. Turning it into a proof that every run of the nondeterministic move relation is finite, including the moves inside Step 1 and Step 2, is the core of the formalization.
Fin n × Fin n (row, column).HeldWolfeCrowder_Assignment_Setting: σ r is the row assigned to column r, the starred positions are , and optimality is IsOptimalAssignment A σ with respect to the original input matrix.Step. The order in which the Preliminaries consider the zeros, and the non-covered zero primed in Step 1, are free choices. Every claim holds for every run.Acc) of each start state for the reversed move relation.Not formalized: the operation count of pp. 35–36, whose cost model is informal; the argument that returning to the standard input after Step 3 is unnecessary (pp. 34–35); König's theorem (Remark (1), cited); and §2 on the transportation problem, which is stated without proof.
Welcome contributions: proofs of the milestones, a general library of lines and independent zeros in matrices (reusable for König–Egerváry), and an executable refinement of the move relation.
A firm that sells a product line of different qualities cannot see how much each customer values quality. It can only post a price for every quality and let customers choose. Mussa and Rosen's 1978 paper solves the monopolist's problem in this setting and compares the result with the competitive outcome. Their model is, together with Mirrlees' optimal income tax and Maskin and Riley's later treatment of nonlinear pricing, one of the founding examples of screening: the seller designs a menu so that customers sort themselves. The model's main qualitative prediction, that a monopolist degrades the quality sold to every customer except the one who values quality most, is the origin of the phrase "no distortion at the top". Textbooks on contract theory and mechanism design still teach it in this form.
Timeline. Mussa and Rosen (1978) give the first-order analysis, including "bunching" of customers at a common quality when marginal revenue is not monotone. Maskin and Riley (1984) treat the same problem for nonlinear quantity pricing. Myerson (1981) introduced the "ironing" procedure for non-monotone virtual valuations in auction design, which later became the standard way of describing the bunching conditions of this paper.
Consumer types are numbers with , distributed with a density that is positive and differentiable on the whole interval; . A consumer of type buys at most one unit, and from quality at price gets utility . Producing one unit of quality costs , where , is twice differentiable, and , for .
Under competition, price equals unit cost and type buys the quality with , or nothing when .
The monopolist chooses an assignment , the quality bought by type . It must be nondecreasing, nonnegative and piecewise differentiable on ; such assignments are called admissible. Incentive compatibility and participation fix the consumer surplus at , so the monopolist maximizes
An assignment is optimal if it is admissible and maximizes among admissible assignments. The marginal revenue of quality sold to type is
The paper's analysis runs through the marginal profit of a uniform quality increase for all types ,
For every optimal assignment :
and, if , the limit exists and satisfies (if , then ). In words: for every type below the top that buys under competition, types that do not buy under competition do not buy from the monopolist, and .
The paper's own chain of claims, in order: except at (p. 308); the first-order condition (9), for every admissible deformation; the identity (10) = (12), ; condition (13), ; condition (15), where ; at a jump; the absence of jumps; (17), where ; the bunching conditions (18)–(19); and the absence of a bunch at the top. Companion items state the two-type case of footnote 4, the uniform–quadratic example of §5, and the loss of consumer surplus (§6, "Second").
The result. The goal says how the monopolist differs from competition: it lowers every quality except the top one, and it never serves a type that competition leaves out. The distortion comes from the gap , which closes only at . The same comparison underlies results on second-degree price discrimination, regulation of product lines, and versioning of information goods. The bunching conditions (18)–(19) are an early statement of what is now called ironing.
Formalizing it. The result has been proved since 1978 in the economic literature, under the paper's smoothness assumptions and by a variational argument. As far as is known, it has not been machine-checked: no formal library contains the monopoly quality problem, its first-order conditions or the bunching conditions. The mission produces a checked version with the hypotheses made explicit, including the conventions at the endpoints that the paper leaves implicit. The uniform–quadratic example gives a concrete optimum that certifies the hypotheses are satisfiable.
The obvious argument sets pointwise and compares with . This fails when is not increasing: the pointwise solution is then decreasing somewhere and not admissible. The optimal assignment is constant on some intervals, and on such a bunch pointwise. The comparison with there needs the boundary conditions (18)–(19) and the fact that no bunch reaches . All of these come from one-sided deformations that respect monotonicity, so the first-order conditions are inequalities and need a separate argument for equality. The paper also asserts without a separate step that optimal assignments have no jumps, and later steps use continuity.
Types and assignments are real functions on ; only their values on matter. The type distribution and are the published MechanismDesign.Screening.TypeDistribution and virtualValuation. The standing assumptions are hypotheses of every main statement: is differentiable on (positivity and total mass 1 are part of the distribution), , and are differentiable on , and , on . is an added normalization: quality 0 means not buying. "Piecewise differentiable" means differentiable on outside a finite set. The competitive assignment is never formed; every comparison with is written through . Admissible deformations in (9) are required to keep .
The value does not affect , so a statement about itself would be false; the top-type claim is stated as a left limit. Optimality ranges over admissible assignments only. Any reading under which no optimal assignment exists makes the goal vacuous; the §5 companion rules this out, since its optimal assignment has a kink and uses the same notion of optimality.
Needed infrastructure: interval integrals of monotone functions, first variations under monotonicity constraints, and fundamental-theorem-of-calculus arguments for . The incentive-compatibility reduction (monotonicity and the envelope formula) is not posed here, because it is posed on the platform in Börgers' screening chapter. Related platform item: Börgers' Proposition 2.6 (MechanismDesign.Screening.nonlinear_pricing_optimal) treats a linear-cost, concave-valuation model under regularity, which is a different statement. Contributions to any milestone, and reusable lemmas about monotone deformations, are welcome.
Semiconductor burn-in ovens can process several jobs at once. A group placed in one oven must remain together until the longest job has finished, so increasing batch size saves oven starts but can delay short jobs. When several ovens are available, a scheduler also has to decide which oven receives each batch. Lee, Uzsoy, and Martin-Vega studied this setting and gave guarantees for a simple rule that first groups an arbitrary job list into batches and then sends those batches to the next available oven (Lee, Uzsoy & Martin-Vega 1992, §§2 and 5). Their bounds give a way to assess this easily specified rule against the best possible schedule, even when finding that schedule is difficult.
The paper treats both makespan, the time when all jobs have finished, and maximum lateness, the largest difference between a job's completion time and its due date. These objectives respond differently to batching. The makespan ignores which particular job finishes late; maximum lateness depends on each job's due date. Proposition 4 relates the lateness guarantee to the makespan guarantee of Proposition 1, making the two results a natural formalization unit (Lee, Uzsoy & Martin-Vega 1992, pp. 772–773).
There are jobs, indexed by , with processing times and due dates . All jobs are available at time zero. There are identical batch machines, each able to process at most jobs at once. A batch cannot be interrupted or enlarged after it begins, and its processing time is the largest among its members. A schedule partitions the jobs into nonempty batches, chooses a machine for each batch, and orders the batches on each machine. Batches assigned to a machine run one after another from time zero. Every job in a batch finishes when that batch finishes (Lee, Uzsoy & Martin-Vega 1992, p. 766).
For a set of jobs , write for the least makespan over all valid batchings and machine assignments. Write for the least possible value of , where is job 's completion time. For the full job set, abbreviate these by and . The maximum due date over all jobs is .
Batch list scheduling (BLS) begins with any ordering of the jobs. It divides successive entries into full batches of jobs, apart from a possibly smaller final batch. It then assigns each next batch to a machine that becomes available first. Denote the resulting makespan by and its maximum lateness by . The guarantee applies to every initial list; it does not require an earliest-due-date or longest-processing-time order (Lee, Uzsoy & Martin-Vega 1992, p. 771, Algorithm BLS).
Proposition 1 asserts, for every BLS list,
The milestone list includes the paper's processing-volume lower bound, , and Proposition 1 itself. The latter is stated for arbitrary job subsets as well as the full instance, because the paper applies it to a prefix sub-instance in the proof of Proposition 4 (Lee, Uzsoy & Martin-Vega 1992, p. 772).
The mission's goal is the printed ratio of Proposition 4:
The denominator is positive under the stated conditions, even if the optimal maximum lateness is negative. The remaining milestones record the paper's lower bound for a nonempty sub-instance and its reduction from the full instance to the BLS prefix containing a maximum-lateness job (Lee, Uzsoy & Martin-Vega 1992, p. 773).
The makespan result controls the cost of using an arbitrary initial list and simple next-available-machine assignments instead of optimizing both the batching and machine allocation. At , its factor becomes , the ordinary list-scheduling factor noted by the authors. Proposition 4 gives a corresponding bound for maximum lateness, normalized in a way that remains meaningful when (Lee, Uzsoy & Martin-Vega 1992, pp. 772–773).
These are proved results in the 1992 paper. The formalization work is to give their batch model, sub-instance optima, and the printed inequalities machine-checked statements and eventually proofs. The imported library already has definitions of least-loaded list scheduling and optimal assignment makespan for ordinary items on identical machines. This mission adds the batch layer, its lateness objective, and the comparison between the batch algorithm and unrestricted batch schedules. The Lean declarations here compile as open theorem targets; this proposal does not claim completed machine-checked proofs.
The processing time of a batch is a maximum, while its contribution to the volume of jobs is a sum. Treating each batch as an ordinary job gives a list-scheduling instance, but it does not by itself compare that instance's optimum with the optimum over all ways to form batches. That gap is central to the makespan bound. The lateness goal has a second obstacle: the job that determines the BLS maximum lateness may sit in a batch that is not the last to finish, and due dates prevent a direct substitution of a makespan bound for a lateness bound. Moreover, may be negative, so dividing by it would not give a valid relative error. The stated normalization and its positivity require explicit attention (Lee, Uzsoy & Martin-Vega 1992, proof of Proposition 4).
Jobs are Fin n and machines are Fin m; the paper's first job is Lean index zero. Processing times and due dates are real numbers. The paper's integer-data convention is sufficient for these inequalities but is not needed for their statements. Processing times are positive, all jobs are available at time zero, and the lateness goal requires nonnegative due dates. This last condition makes explicit what the paper's final inequality uses: allowing negative due dates makes Proposition 4 false. The full job set is nonempty. Prefix jobs are the first batches of the given arbitrary list, and the optimal values for a prefix range over every valid batching and assignment of those jobs.
The BLS implementation chunks the list into full batches and a final remainder. A batch is sent to a least-loaded machine, which is the first machine to become free when no idle time is inserted. The published list-scheduling definitions of NumStochOpt.ListScheduling supply this rule and the ordinary assignment optimum. They select the lowest machine index on a tie; identical-machine labels do not affect the resulting completion times. Machine schedules are represented by an ordered batch list and an assignment, with each machine processing its own batches back to back. No bound is obtained by defining the optimum over BLS-shaped consecutive batches, and no theorem fixes a favorable job list.
The mission covers correctness inequalities, not the paper's running-time claims or its later BLPT rule. Useful contributions include proofs of the four milestones, finite-schedule facts showing the optima are attained, and reusable links between batch completion times and least-loaded list scheduling. The parallel batch model can also support other objectives and scheduling rules.
Burn-in is the final testing stage of semiconductor manufacturing: finished integrated circuits are loaded on boards and held in an oven at high temperature for a prescribed minimum time, so that weak devices fail before shipment. An oven holds many boards at once, a load cannot be interrupted, and a board may stay in the oven longer than its specified time but never shorter. Because burn-in times are long compared to the other test operations, the ovens are frequently the bottleneck of the test facility, and the order in which lots enter them determines whether customer due dates are met.
Lee, Uzsoy and Martin-Vega (Operations Research 40(4), 1992) modelled an oven as a batch processing machine and gave polynomial algorithms for several due-date objectives. This mission covers the first of them: one machine, jobs with release times and a common processing time, and the question whether every job can be completed by its due date. Ikura and Gimple (Operations Research Letters 5(2), 1986) had already given an algorithm for this feasibility question when release times and due dates are agreeable; the paper replaces it by a simpler dynamic program, DP1, and uses DP1 with a bisection search to minimize the maximum tardiness.
There are jobs, indexed . Job has a release time (it cannot be processed earlier), a due date , and the common processing time ; all data are natural numbers. One machine processes up to jobs simultaneously.
A batch schedule of a set of jobs is a sequence of batches : nonempty, pairwise disjoint sets of at most jobs whose union is , processed in this order. A batch cannot be interrupted, and no job joins it once it has started. It starts as soon as the previous batch is finished and all its jobs are released, and it takes time :
Job completes at for the batch ; the makespan is . A schedule is feasible (has ) if for every job, and its maximum tardiness is .
Release times and due dates are agreeable if implies . A schedule is in batch-EDD order if no job of an earlier batch has a larger due date than a job of a later batch.
Algorithm DP1. With the jobs indexed in nondecreasing order of due dates, let and, for ,
For an index order nondecreasing in both and , and every ,
The minimum ranges over all batch schedules of the prefix: every batching and every batch order. The case is the paper's statement that DP1 "will find a feasible schedule with minimum makespan if a feasible schedule exists" (p. 768).
DP1 decides feasibility of and, when the instance is feasible, returns the minimum makespan of an on-time schedule. Applied to due dates augmented by a trial value , it decides whether is achievable, which together with the bound of Lemma 2 gives the paper's polynomial procedure for minimizing . The consecutive-partition structure behind it recurs in the paper's later dynamic programs (DP2 for agreeable processing times and due dates, DP3 for the number of tardy jobs), and in much of the later literature on batch scheduling with release dates.
The results are proved in the paper; none of them has a machine-checked proof. The mission formalizes the known proofs. Its formal statements also make explicit two assumptions that the printed text leaves loose: the tie-break of the index order, without which DP1 returns a wrong value, and the hypothesis of Lemma 2, without which the lemma is false.
The obvious argument for the goal is "by Lemma 1 the batches are consecutive, and DP1 enumerates consecutive partitions". Lemma 1 orders the batches by due dates, but it does not make the batches intervals of the index order: jobs with equal due dates may still be split across batches in an order that is not the index order, and when equal due dates are indexed against the release order DP1's value underestimates the start of the batch . The step from batch-EDD order to consecutive batches, and the fact that the exchange never increases the makespan, are the content of the justification milestone. The goal also asserts two directions at once: that the DP value is attained by some feasible schedule, and that no feasible schedule, consecutive or not, finishes earlier.
Jobs are Fin n, 0-based (the paper's job is i - 1); a prefix "jobs " is a prefix length . Data are natural numbers, as the paper assumes ("all data to be integers", p. 769). A batch schedule is a List (Finset (Fin n)); schedules are semi-active, starting every batch as early as possible, which loses nothing for the regular objectives here. DP1 is a def written as printed, with values in ℕ∞ and ; the minimum in the goal is an infimum in ℕ∞ over all valid feasible schedules, so its value on an infeasible prefix is .
Explicit readings of loose phrases:
Not formalized: the running time of DP1, Algorithm 1 (bisection over ) and Corollary 1, whose content is a running time. A formalization that restricts the minimum in the goal to consecutive or batch-EDD schedules would assume the milestones and is excluded; so is a DP value defined as the optimum itself.
The development needs list-based schedule recursions and ℕ∞ arithmetic only; the exchange lemmas for batch schedules (moving a job between batches without delaying later batches) are reusable for the paper's other dynamic programs. Proofs of any milestone, and of auxiliary lemmas on finish, jobCompletion and permutations of batch lists, are welcome.
In semiconductor manufacturing, finished chips go through burn-in: they are loaded on boards and held in an oven at high temperature to expose early failures. An oven holds a bounded number of boards, a load cannot be interrupted once started, and a chip may stay in the oven longer than its specified burn-in time but not shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model the oven as a batch processing machine and give polynomial algorithms for several due-date objectives. The model has since become a standard one in scheduling theory; the survey of Potts and Kovalyov (2000) traces the batching literature that grew from it.
This mission formalizes the part of the paper's §3 on minimizing maximum tardiness when all jobs are available at time and processing times and due dates are agreeable. That is the problem the paper writes . The paper's own route is a feasibility test by dynamic programming, Algorithm DP2, which a bisection over due-date shifts turns into a minimizer.
There are jobs . Job has a processing time and a due date , both natural numbers. The machine has capacity . A batch is a nonempty set of at most jobs processed together. It occupies the machine for the processing time of its longest job,
A batch schedule of a job set is a sequence of pairwise disjoint batches covering , processed in this order and back to back from time . Batch and all of its jobs complete at . The makespan is , and the maximum tardiness is
A schedule is feasible when , that is, when every job meets its due date.
A sequence is in batch-EDD order (Definition 1) if no job in an earlier batch has a strictly later due date than a job in a later batch. Processing times and due dates are agreeable if implies . A schedule is consecutive when every batch is a block of indices and the blocks appear in increasing order.
Algorithm DP2 computes values :
Index the jobs so that and . Then for every ,
with . The minimum ranges over all schedules: any batching, any order. This is the paper's reading of as "the minimum completion time of jobs if they can be scheduled feasibly, and infinity otherwise".
DP2 is the paper's feasibility test for with agreeable data. With a bisection over the common shift of the due dates, it yields a polynomial algorithm for minimizing . A correct statement of what DP2 computes is therefore the core of that result. The same consecutive-partition structure underlies the paper's DP1 (release times, equal processing times) and DP3 (number of tardy jobs), which are separate missions of this series.
No machine-checked proof of any of these statements is known. The dynamic program's correctness is argued in the paper only by reference ("the justification of this algorithm is similar to that of algorithm DP1"), and the index order it needs is left implicit. A formal proof pins down exactly which ordering of the jobs makes the recursion correct.
The recursion charges for the last batch and checks only . Both shortcuts rely on the jobs being sorted by due date and by processing time at the same time. Lemma 3's exchange argument sorts a feasible schedule by due date, but it does not by itself produce consecutive blocks of a fixed index order. With ties in due dates the indexing also has to be compatible with processing times. Without that, the recursion is wrong: for , , it gives , while every schedule takes at least . The goal compares the DP with the optimum over all schedules, so the exchange arguments have to bridge arbitrary batchings and the consecutive ones the recursion enumerates. That bridge is the main step left to prove.
Fin n (job of the paper is index ); jobs are jobsUpTo n j. Data are natural numbers; the paper assumes integral data (p. 769).List (Finset (Fin n)); validity requires nonempty batches of size at most inside the job set, pairwise disjoint, covering the set. Batches start as early as possible. Batch time is the maximum processing time in the batch.⊤ : ℕ∞, and the goal's minimum is the infimum in ℕ∞, which is ⊤ exactly when no feasible schedule exists. DP2 is defined by the printed recursion, not as an optimum.Monotone d ∧ Monotone p for DP2 and its justification, and Monotone d for FBEDD;Minimizing the weighted number of tardy jobs on a single machine, written in later scheduling notation, is one of the basic due-date objectives: each job either meets its deadline or pays a fixed penalty, and the question is which jobs to sacrifice. Moore (Management Sci. 15, 1968) solved the unweighted case with a greedy procedure. Lawler and Moore (Management Sci. 16, 1969) handled arbitrary weights by recasting the problem as a knapsack problem with nested prefix constraints and solving it by a recursion, their Equation (3). This is the classical pseudo-polynomial algorithm for the weighted problem; Lenstra, Rinnooy Kan and Brucker (Ann. Discrete Math. 1, 1977) showed that the weighted problem is NP-hard, so a pseudo-polynomial method is the expected kind of exact algorithm.
The paper's Sections 5 and 6 state the reduction in a few sentences: on-time jobs can be taken in deadline order, the problem is "equivalent" to the prefix-constrained knapsack, and (3) solves the latter. This mission turns those sentences into precise statements.
There are jobs, processed by a single machine one immediately following the other from time . Job has a nonnegative integer processing time , a nonnegative integer deadline and a penalty . A sequence is an ordering of all jobs; job completes at time , the total processing time of job and the jobs before it. Job is tardy in if , and the total loss of is
the loss being for and for .
The jobs are numbered by deadline, . A 0–1 vector (: job on time; : tardy) is prefix-feasible if
Equation (3) defines for and integer :
with for and for .
With and , is finite and
This is the paper's claim that the problem "is solved by" its recursion, with the evaluation point made explicit.
The goal follows from milestones 2 and 3 at , .
The result is the exact algorithm for with running time proportional to , and the reduction behind it (on-time jobs in earliest-deadline order, then a knapsack over the on-time set) is the template reused by later work on due-date objectives, including the two-agent and batching variants. The prefix-constrained knapsack itself reappears whenever a set of jobs must be feasible under nested capacity limits.
On formalization: the paper's argument is three sentences long and leaves several points implicit: the base cases of (3), the role of the deadline numbering, the sign of the penalties, and what "equivalent" means. A machine-checked development fixes each of them and yields a verified pseudo-polynomial algorithm for an NP-hard scheduling problem. To our knowledge none of these statements has a machine-checked proof; the platform's SchedComplexity.OneMachine.* items (Lenstra, Rinnooy Kan and Brucker) state the NP-hardness of the same problem in another model, MooreLateJobs.NumLate.* covers Moore's unweighted case, and TwoAgentSched.LateLate.lemma_7_1 is a two-agent analogue of milestone 1.
The obvious argument works with the set of on-time jobs and asserts that this set can be sequenced on time iff its earliest-deadline order is. That step is Jackson's rule, an exchange argument on lists that is not in Mathlib; it is where both milestone 1 and the first half of milestone 2 sit. The second half of milestone 2 needs the deadline numbering: for a job that is tardy, the prefix constraint at is not a completion-time constraint of any job, and only the monotonicity for the last on-time job bounds it. Milestone 3 is a dynamic-programming correctness proof in which the cap for and the base cases must be tracked through a well-founded recursion on .
Jobs are Fin n, 0-based: Lean job is the paper's job , and the paper's uses Lean job ⟨j-1, _⟩. Sequences are lists in the published model MooreLateJobs.Shared (IsSchedule Finset.univ l, completionTime, no idle time, start at ), which replaces the paper's permutation ; tardy jobs are the published MooreLateJobs.NumLate.lateSet (strictly ). Processing times and deadlines are natural numbers, penalties real. Vectors are Fin n → Bool. takes values in WithBot ℝ, with and ; never occurs.
Explicit readings of the paper's loose phrases:
Monotone d on the job index; assumed in the goal and milestone 2 only.IsLeast over all schedules); only so that exists.Section 5 literally applies Equation (1) with , , , ; read literally, that leaves the deadlines unenforced, so the mission formalizes the paper's own corrected form (3) instead. Trivializing formalizations are ruled out: the weighted number of tardy jobs is defined from completion times, not through ; the optimum is a minimum over sequences, not defined as ; (3) keeps its cap ; the goal assumes and sorted deadlines, without which it is false.
Infrastructure: an exchange lemma for earliest-deadline order on lists (Jackson's rule, posed on the platform as MooreLateJobs.NumLate.jackson) and well-founded-recursion lemmas for WithBot ℝ maxima are reusable beyond this mission. Proofs of any milestone, and of Jackson's rule, are welcome.
Many single-machine scheduling problems have a structure that is easy to describe: the jobs must be processed in an order that is already known, and the only decisions are how and when to process each one. Lawler and Moore, in A Functional Equation and Its Application to Resource Allocation and Sequencing Problems (Management Science 16(1), 1969, 77–84), isolate this situation in its simplest form: each job has two processing modes, and each mode has its own processing time and loss as a function of the completion time. They solve it with a single functional equation, Eq. (1), closely related to the recursion for the knapsack problem.
The point of the paper is that Eq. (1) solves more than this fixed-order problem. Later sections apply it to resource allocation in critical-path scheduling and to several sequencing problems with deadlines, including minimization of the weighted number of tardy jobs, often written . Everything in those applications rests on the claim checked in this mission: that the recursion computes the minimum loss it is said to compute.
There are jobs, performed one at a time in the fixed order . Job can be performed in one of two modes. In the first mode it takes time units, and a loss is incurred if it is completed at time . In the other mode it takes time units, with loss . Times are nonnegative integers.
A mode assignment picks a mode for each job, which fixes its processing time . A feasible timing of the first jobs is a vector of completion times with
so each job starts at time or later and after its predecessor has finished; idle time between jobs is allowed. The total loss is the sum of over the jobs in the first mode and of over the others. The problem asks for the mode assignment and timing of all jobs that minimize .
The paper's recursion is defined for and integer , with values in :
For and every integer , let be the set of total losses of the first jobs over all mode assignments and feasible timings with . Then
meaning: exactly when is empty, and otherwise is an element of and a lower bound for it. No assumption is made on the losses.
If every and is monotone nondecreasing and
then is finite and equals the minimum of over all mode assignments and all feasible timings of the jobs, with no deadline. This is the paper's sentence "The problem is solved by the calculation of , where is a sufficiently large number. For example, if all of the 's and 's are monotone nondecreasing, we may choose ."
The milestone is the correctness of a dynamic program: the value table computed by (1) coincides with the optimum of a combinatorial problem whose feasible set is infinite (timings are unbounded because of idle time). The goal turns that into a finite certificate for the unconstrained problem, with an explicit horizon. Downstream, the same equation with and suitable losses is the paper's algorithm for the weighted number of tardy jobs (§5–6), and the other sequencing applications are specializations of (1) as well; a formal version of this mission is the base on which those reductions can be stated.
The result is classical and its proof is short on paper. It has not been formalized: no item on Prove2Me states a two-mode fixed-order recursion. The work this mission asks for is a machine-checked proof of the two statements above, from the paper's own definitions.
The paper gives no argument beyond "the usual dynamic programming argumentation". The recursion is in two variables: refers to itself at as well as to , so the correspondence with timings is not a plain stage-by-stage principle of optimality. The edge cases are where a careless reading fails: , where ; zero processing times or , where is evaluated at the same ; and , where the deadline constraint degenerates to . The goal is harder than the milestone: the problem's feasible set is unbounded, and the horizon is only sufficient under monotone losses. Without monotonicity the goal is false: one job with , , for and has optimum , attained only at completion time , while .
Fin n and 0-based: Lean job i is the paper's job . The recursion f takes the number of jobs done; for its value is and is never used.Bool, with true the first mode (, ). Processing times are natural numbers and may be . Losses are real-valued functions of the natural-number completion time.⊤ : WithTop ℝ, so as in the paper.Monotone on the completion time; it is a hypothesis of the goal only.The optimum is defined from the scheduling problem itself (lossesBy, IsFeasible, totalLoss), never as ; statements in which the optimum is again, timings forced to have no idle time, an -valued with an arbitrary value for , or monotone losses assumed in the milestone are all ruled out by this choice of definitions.
Related platform items: GilmoreGomory61.CuttingStock.knapsack_dp_recursion (an unbounded-knapsack recursion) and the CriticalPath.CostCurve items (Kelley's continuous time–cost model) treat neighbouring recursions and models; neither states this problem. Proofs of the milestone and the goal, and reusable lemmas about the value function, are welcome.
Exponential bounds for the tails of the binomial distribution are among the most frequently used tools in probability, statistics and the analysis of algorithms: they control the number of successes in independent trials, the deviation of an empirical frequency from its mean, and, through counting arguments, the empirical distribution function itself. The two classical bounds are Hoeffding's inequality, which ignores the variance, and Bernstein's inequality, which uses the variance but loses accuracy for large deviations. Both are recorded in Shorack and Wellner, Empirical Processes with Applications to Statistics (1986), p. 440.
In his 1990 paper establishing the tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, P. Massart obtained, as a by-product of the proof, a binomial tail bound that implies both classical inequalities and, in his words, "does not seem to be known" (Massart 1990, p. 1271). Its ingredient, a lower bound for the Cramér transform of the Bernoulli law (Lemma 1), is also used in the proof of the main DKW result. This mission formalizes that by-product: Theorem 2, Lemma 1 and the Cramér–Chernoff bound (Comment 3) through which they are combined.
Fix an integer and a success probability , and write . A random variable has the binomial distribution if it counts the successes in independent trials, each succeeding with probability : for . Its mean is . The quantity of interest is the upper tail for a deviation with (for the event is empty).
Two auxiliary functions appear in Lemma 1. For (so that ),
which is the Cramér transform of the Bernoulli law with parameter at the point , i.e. the relative entropy between the Bernoulli laws with parameters and . For ,
In the Lean development these are MassartDKW.Binom.h and MassartDKW.Binom.phi.
If has the binomial distribution and , then for every with ,
The result. Theorem 2 has the shape of Bernstein's inequality with the variance proxy replaced by the smaller ; the second factor shrinks as approaches , so the bound is sharper in the large-deviation range, and it implies both Bernstein's and Hoeffding's inequalities for binomial tails. Lemma 1(ii) is a quantitative lower bound on the Bernoulli relative entropy, with an explicit nonnegative correction term , which is reusable wherever Chernoff bounds for Bernoulli sums are converted into closed-form exponents. In the paper, the same lemma is a step of the proof of the tight Dvoretzky–Kiefer–Wolfowitz inequality.
Formalizing it. The result is proved on the page, by a short calculus argument for Lemma 1 and the classical Cramér–Chernoff computation for Comment 3. To our knowledge none of the three statements has a machine-checked proof. The work this mission asks for is formalizing that known proof: the analysis of (signs of derivatives, the limit at infinity), the inequality between and the explicit quadratic term, the exponential-moment computation for the binomial law in Mathlib's measure-theoretic setting, and the bookkeeping of the boundary cases , and .
The obvious route to Theorem 2 is to bound the binomial moment generating function and optimize; this reproduces Comment 3, and the exponent it gives is the transcendental function , not the rational expression in the theorem. The step that needs care is the comparison of with uniformly in : a second-order Taylor expansion of in gives only the local behaviour near , and a bound proved by Taylor expansion alone does not survive up to , where the second logarithm of degenerates and blows up. The endpoint therefore has to be treated as a limit.
The binomial law is Mathlib's ProbabilityTheory.binomial n p : Measure ℕ with p : unitInterval; is an -valued map on a probability space with HasLaw S (binomial n p) P. Probabilities are values of the measure in , compared with real bounds through ENNReal.ofReal. The event is the strict upper tail . The goal assumes only , as on the page: and are allowed, and the denominator is positive on the whole range.
Conventions and added hypotheses ( is written out as throughout):
A formalization that states the goal with the exponent , or assumes Lemma 1 or Comment 3 as hypotheses, or restricts to , is not this theorem: the goal carries the explicit constants and the full range .
Needed infrastructure: elementary real analysis of (derivatives, monotonicity from derivative sign, limits at infinity), the moment generating function of the binomial law (or of a sum of independent Bernoulli variables) and Markov's inequality. The bound on the Bernoulli relative entropy and the binomial Chernoff bound are reusable beyond this mission. Contributions welcome: proofs of the three milestones, and helper lemmas computing for Mathlib's binomial.
In a flow shop every job passes through the same machines in the same order. Choosing the order in which jobs enter the shop so that the last job finishes as early as possible (minimizing the makespan) is one of the oldest problems of scheduling theory. For two machines Johnson (1954) gave an exact sorting rule; for three machines his rule is exact only in special cases, and the general problem was later shown to be NP-hard (Garey, Johnson and Sethi, 1976). Exact methods for three or more machines therefore enumerate sequences, and the question is how to enumerate as few of them as possible.
Ignall and Schrage (1965), at the same time as Lomnicki (Operational Research Quarterly, 1965), introduced branch and bound for the three-machine permutation flow shop. Their lower bound, which adds to the time each machine becomes free the work that remains on it and the least work that must follow on later machines, became the template for the machine-based bounds used in flow-shop branch and bound ever since.
Timeline. 1954: Johnson proves the two-machine rule and shows that for three machines a common job order on all machines loses nothing for the makespan. 1960: Land and Doig introduce branch and bound for integer programs. 1965: Ignall–Schrage and Lomnicki apply it to the three-machine flow shop. 1976: Garey, Johnson and Sethi prove the three-machine makespan problem NP-hard, so exact enumeration with good bounds remains the method for exact solutions.
There are jobs and three machines , , . Job needs time on , then on , then on . Following Johnson, only permutation schedules are considered: a full sequence is a permutation of the jobs, processed in that order on all three machines, each operation starting as early as possible. Its makespan is the time machine finishes the last job.
A node is a partial sequence: an ordered list of distinct jobs. Its unscheduled set is the set of the other jobs. The attributes , , are the times at which machines , , finish the jobs of processed in order. A full sequence begins with when its first positions are . The lower bound of a node with is
The branch-and-bound procedure keeps a list of nodes ranked by , starting from the root (no job scheduled). At each step it removes the first node, creates one child per unscheduled job by appending that job, and inserts the children ranked into the list, a new node going before old nodes of equal bound. It stops when the first node of the list is terminal, i.e. has scheduled jobs, so that its last job is forced.
where is followed by its one unscheduled job. This is the paper's "the problem is solved: that node's sequence is an optimal one" (p. 402), for any real processing times.
The goal is the correctness theorem of the Ignall–Schrage algorithm: best-first search over partial sequences, with a machine-based bound, returns an optimal permutation. Milestone 1 is the bound's validity, which every later machine-based flow-shop bound generalizes; milestone 4 is the dominance rule that justifies discarding nodes; milestone 3 brackets the effort of the search between the best case and full enumeration.
The paper's arguments are short and informal: validity of the bound is asserted with a one-line reason, and optimality at stopping is argued on the example. None of these results has a machine-checked proof. The formalization makes the procedure itself a precise object (list, insertion rule, stopping rule) and turns the paper's claims into statements about it, so that the correctness of the search is proved rather than illustrated.
Each inequality is elementary, but the goal is a statement about an iterated list-manipulating procedure. The obvious argument "the first node has the smallest bound and the bound is valid" needs an invariant that the paper does not state: at every step, every full sequence begins with some node on the list, and the list is sorted. Both must be proved to survive one step of removal and ranked insertion. Termination is likewise not stated: it needs a measure that strictly decreases, for instance the set of nodes that remain to be created, which requires showing that no node is created twice. A tempting shortcut, proving optimality only among the sequences whose nodes were created, is not the theorem.
Jobs are Fin n (the paper's job is ), processing times are arbitrary reals with no sign condition, and full sequences are Equiv.Perm (Fin n). The makespan is the machine- completion time of Johnson's as-soon-as-possible schedule, taken from the published definition JohnsonFlowShop.ThreeStage.asapSchedule. Nodes are lists of jobs, and the node attributes are the same recursion folded over the list. Minima over are Finset.inf'; on an empty set the auxiliary minimum returns a placeholder that no statement evaluates.
Explicit readings of the paper's phrases:
A formalization in which the optimality claim ranges only over sequences the run created, or one that asserts optimality without termination, would be trivial or vacuous and is ruled out by the goal's statement.
Not formalized: the reduction from general schedules to permutation schedules (Johnson's Lemma 3, proved on the platform as JohnsonFlowShop.ThreeStage.same_ordering_dominant), the dominance bookkeeping and its percentages, the two-machine mean-completion problem (a separate mission of this series), the computational tables, and the TIMEB/TIMEC columns of the example's LIST table. No platform item treats flow-shop lower bounds or branch and bound over sequences; the nearest branch-and-bound mission, BiconvexProg.BranchBound (Al-Khayyal and Falk), concerns biconvex programs and is unrelated.
The lemmas a solver will want (the invariant of the list, monotonicity of the completion recursion in its start times, validity of the bound) are reusable for the two-machine mission and for any other machine-based bound. Proofs of the milestones, and of the goal from them, are welcome in any order.
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.
A flow shop is the simplest model of a production line: every job passes through the same sequence of machines in the same order. Minimizing the time at which the last job leaves the last machine (the finish time, or makespan) is easy for two machines, where Johnson's rule gives an optimal schedule in time (Johnson 1954), and NP-hard from three machines on (Garey, Johnson, Sethi 1976; Gonzalez, Sahni 1978, §1, for preemptive schedules). For three or more machines the practical question is therefore how far a fast heuristic can be from the optimum in the worst case.
Gonzalez and Sahni (1978, §2) first show that any busy schedule, one that never leaves a processor idle while a task is available for it, has finish time at most times the optimum (their Lemma 10), and that the natural "longest job first" order does no better. They then give a heuristic, H, that uses Johnson's two-machine algorithm as a subroutine and has the better worst-case ratio (Lemma 11). This mission formalizes that bound.
A flow shop has processors and jobs. Job consists of tasks; task runs on processor and needs processing time (zero is allowed). A non-preemptive schedule gives every task a start time , and the task occupies during . It is feasible when all start times are nonnegative, when task of a job starts only after task of that job has completed (), and when no processor runs two tasks of positive length at the same time. Its finish time is the latest completion time (and if there is no task). An optimal finish time (OFT) schedule is a feasible schedule of least finish time.
Heuristic H (p. 48) divides the processors into groups: group consists of and , and when is odd the last group is alone. The flow shop on group has the same jobs, with task times only. For each group an OFT schedule of is computed (by Johnson's algorithm), with finish time . The schedule generated by H runs these schedules one after another: every task of group starts at its time in plus the offset .
For every flow shop with processors and jobs, every choice of OFT schedules of the group flow shops, the schedule generated by H, and every feasible non-preemptive schedule of the flow shop (in particular an OFT schedule ),
The paper writes this as .
The result gives a polynomial-time heuristic, running in time , whose finish time is within a factor of the optimum on every instance, half the factor that every busy schedule already achieves. The paper's Example 4 (p. 49) shows that for the factor is approached, so the analysis cannot be improved in general.
Formalizing it produces a reusable, machine-checked model of the -processor flow shop with non-preemptive schedules, its restriction to blocks of consecutive processors, and the concatenation of schedules of disjoint blocks. Lemma 11 has a short paper proof; to our knowledge it has no machine-checked proof. The model's careful treatment of zero task times, of odd , and of the restriction of a schedule to a processor group is itself part of the value: these are the points at which an informal argument is silent.
The arithmetic of the bound is short; the content lies in two structural facts about a precise model: that the concatenated object is a feasible schedule of the whole flow shop, including across the boundary between consecutive groups and for a final group of a single processor, and that the optimum of the whole flow shop is at least the optimum of each group flow shop, whose first processor has no predecessor. Informal arguments are silent on exactly these points. A naive formalization that leaves the offsets free, or that does not require the to be optimal, makes the statement false; one that lets be any schedule with the right restrictions makes it witnessed by itself.
The existence of OFT schedules for the group flow shops (milestone 1) is a separate matter: the paper takes it from Johnson's algorithm, and proving it requires an optimality argument for two-machine flow shops (or a compactness argument over finitely many processing orders).
Fin m and jobs Fin n, both 0-based; times are real numbers. A flow shop is a matrix t : Fin m → Fin n → ℝ with t ≥ 0. A schedule is a matrix of start times. Group (0-based, g : Fin ((m + 1) / 2)) contains the processors and that exist, min 2 (m - 2g) of them.max with baseline over all tasks; it is for or . The maximum of the group finish times is also a fold of max with baseline . No supremum over an unbounded or empty set is taken.(m + 1) / 2 in , cast to ; the two agree for every . The ratio is multiplied out, so a zero optimum does not divide by zero.Finset.fold max and sums over Fin; nothing beyond Mathlib. Contributions proving milestone 1 by formalizing Johnson's rule for this model are welcome and reusable.Kingman's subadditive ergodic theorem (Theorem 1 of Kingman 1973, first proved in Kingman 1968) says that for a discrete-parameter subadditive process the ratio converges with probability one and in mean. Applications in first-passage percolation, products of random matrices and longest increasing subsequences often come with a continuous time parameter, so it is natural to ask whether the theorem holds with ranging over .
Section 1.4 of the 1973 paper answers this question. Under separability alone, a continuous-parameter version would contain, as its additive special case, the claim that every separable process with stationary increments and finite expectations has a finite limit with probability one. Kingman remarks that no such theorem appears in the literature, "for the excellent reason that the conclusion is false, and in a very strong sense" (p. 888). Theorem 3 makes that sentence precise. It is the reason the continuous-parameter theorem of the paper (Theorem 4) carries an extra integrability hypothesis on the oscillation .
A real-time process is a family of real random variables on a probability space . Its joint law is the law of the path on with the product -algebra, that is, the collection of all finite-dimensional distributions.
A growth bound is a function that is increasing (non-decreasing). The event " for all sufficiently large " is the set of for which some exists with for every real .
In the Lean development these notions are IsStationary, HasStationaryIncrements, Integrable (y t) P and ContDiffOn ℝ ∞ (fun t => y t ω) (Set.Ici 0), all in the namespace KingmanSubadditive.StationaryIncrements.
For every positive non-decreasing on there are a probability space and a process with stationary increments, finite expectations and sample functions such that
The quantifiers are "for every there exists ". Because may grow arbitrarily fast, no normalization with a deterministic can converge to a finite limit almost surely.
The milestones are the four steps of Kingman's proof, stated for the explicit process of (1.4.5) built from a bump function , a uniform and independent integer-valued with a law that depends on :
The result. Theorem 3 rules out any continuous-parameter subadditive ergodic theorem whose only hypotheses are separability, stationarity of the increments and finite means, and in fact any such theorem whose hypotheses are met by smooth stationary processes with finite means. The obstruction does not come from irregular paths: the counterexample is as regular as a path can be short of analyticity. Any continuous-time ergodic theorem therefore needs a hypothesis that controls the behaviour of the process inside unit intervals, such as in Theorem 4, or the integrability of in the classical continuous-parameter ergodic theorem. The result also separates two kinds of time. Along the integers, a stationary-increment process with finite mean is an additive discrete process, so converges almost surely; Theorem 3 shows that the real-time path can still escape any envelope between the integers.
Formalizing it. The theorem is classical and its proof is complete in the paper. To our knowledge it has no machine-checked proof. A formalization requires the existence of a probability space carrying a uniform variable and an independent i.i.d. sequence with a prescribed law on the integers, the joint-law notion of stationarity for real-time processes, a stationarity argument for a randomly shifted process, an expectation computation with a change of variables, and the second Borel–Cantelli lemma. The definitions of stationarity and stationary increments for real-time processes on are reusable beyond this mission.
The natural first attempt is a process with linear or polynomial growth, such as with a heavy-tailed integrable . Every such attempt fails against a that grows faster, so the process must depend on . A process that is large on a whole interval of length one cannot have finite mean when grows fast. The difficulty is to have excursions that are taller than any prescribed envelope infinitely often, and still keep finite expectation, stationarity in real time and smoothness. In the formal proof, the stationarity step is where most of the work sits: the shifted path must be identified in law with the original one for every real shift , not only for integer shifts.
y : ℝ → Ω → ℝ, with values at ignored; lives in Type. Every with is measurable, and both stationarity definitions include almost-everywhere measurability, so Measure.map never takes its junk value.Set.Ici (0:ℝ) → ℝ with the product -algebra. Stationary increments compare the laws of and for every real .MonotoneOn Γ (Set.Ioi 0)), which gives the stronger theorem. is a total function on ; its values at are irrelevant.ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) on for every . This is , not the analytic order.Contributions welcome: proofs of the milestones, a general lemma that a uniformly shifted process built from an i.i.d. sequence of unit blocks is stationary in real time, and a proof of the goal.
Flow shops and job shops are the basic models of multi-stage production: every job passes through several machines, and each machine handles one task at a time. Gonzalez and Sahni (Operations Research 26(1), 1978) showed that minimizing the finish time of such shops is NP-complete even with preemption, and then asked how well simple heuristics do. One of the two objectives they study is the mean flow time, the average completion time of the jobs, which measures how long a job spends in the shop on average.
Their Lemma 9 analyses the most natural rule for that objective, shortest processing time first (SPT): process the jobs in order of nondecreasing total work. For a single machine SPT is optimal (Smith 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 76, which the paper cites). Lemma 9 shows that with processors the same rule loses at most a factor , and the paper's Example 2 shows that the factor is attained in the limit.
A job shop has processors and jobs. Job is a finite sequence of tasks; each task names the processor that must process it and a processing time . The tasks of a job are processed in their order: a task may start only after the job's previous task has completed. A flow shop is the special case in which every job has tasks and its -th task runs on .
A non-preemptive schedule gives every task a start time ; the task then occupies its processor during , and two distinct tasks on one processor never overlap. The finish time of job in schedule is the time at which all tasks of job have been completed, and the mean flow time is
An OMFT schedule is a feasible schedule of least mean flow time.
Let be the sum of the task times of job . An SPT order is a listing of the jobs with , ties broken arbitrarily. The SPT schedule processes the jobs in that order: each job in turn, each positive-time task starting at the later of the completion of the job's previous task and the latest completion of a task already placed on its processor. A zero-time task completes when its preceding task completes and leaves the processor available.
For every job shop, every SPT order with SPT schedule , and every feasible non-preemptive schedule ,
so that for an OMFT schedule . A separate item states the same bound for flow shops.
The milestones follow the paper's proof of Lemma 9 on p. 47:
Lemma 9 is one of the earliest performance guarantees for a shop-scheduling heuristic under a sum objective. It shows that a rule computable by one sort, plus a linear pass, is within a factor equal to the number of machines, independently of the number of jobs. This is better than the factor that Lemma 8 of the same paper gives for an arbitrary busy schedule, whenever . Example 2 of the paper shows that the factor cannot be improved for SPT. Lower bounds of the work-per-machine type used here recur in later approximation results for total completion time in shops and on parallel machines.
The result has been proved since 1978. As far as a search of the Prove2Me catalogue shows, it has not been machine-checked. This mission adds a machine-checked statement of the SPT schedule as an algorithm, not as an arbitrary schedule with a property. It also adds the guarantee for job shops with arbitrary task sequences, of which flow shops are a special case.
The arithmetic of the proof is short. The work is in two places. The SPT schedule is a concrete construction, a fold over jobs and tasks that updates processor availability, so the bound on its finish times has to be carried through an invariant of that construction. The lower bound on every feasible schedule needs a packing argument: tasks on one processor that complete by a given time have total length at most that time. That argument is not available in Mathlib in a form that applies here. The tempting shortcut of comparing the two schedules job by job fails: the optimal schedule need not finish jobs in SPT order, so the comparison must go through sums of sorted prefixes.
JobShopLTAS.Core.Instance (jobs Fin n, processors Fin m, tasks Fin (μ j), real processing times ). The local IsPaperFeasibleSchedule requires nonnegative starts, in-job order, and no overlap of positive-time tasks on the same processor. Zero-time tasks occupy no processor interval. The paper assumes , and the scheduling theorems carry that hypothesis.