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?
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.In a job shop, each job has an ordered list of tasks, and each task must use a specified machine. A production planner may be able to interrupt a task and resume it later, yet still be unable to find a short schedule efficiently. Gonzalez and Sahni studied how the ability to preempt changes the difficulty of minimizing the time at which all jobs are complete. Their 1978 paper establishes complexity results for flow shops and job shops and then examines approximation schedules when exact optimization is difficult (Gonzalez and Sahni, 1978).
This mission concerns the paper's two-machine construction from 3-PARTITION. It is the reduction used for their claim that finding an optimal preemptive or non-preemptive finish-time schedule remains NP-complete when input size is measured by the sum of task lengths. The formal target isolates the decision equivalence proved for the constructed instance. It gives solvers a precise schedule statement to establish without conflating the scheduling theorem with the separate complexity-class argument.
A 3-PARTITION input comprises an integer , a positive integer target , and positive integer sizes . A valid input satisfies
It has a 3-partition when the indices can be assigned to disjoint groups, each containing exactly three indices and having total size . The strict bounds rule out groups of other cardinalities at that sum and are part of the source problem, not a convenience added for formalization. When , the input has no sizes or groups and the empty grouping is a solution.
The paper builds a job shop with machines and jobs. For , job has a task of length on , followed by a task of length on . The last job, , has tasks, each of length . Its tasks alternate between the machines, starting on . This last order matters: reversing it would produce a different construction. The source gives the decision threshold (Lemma 7, p. 44).
A non-preemptive schedule gives each task one continuous processing interval. A preemptive schedule may divide an operation into finitely many positive-length intervals. In either case, jobs obey their task order, distinct pieces on the same machine do not overlap, and processing starts at or after time zero. Write for the time at which all tasks of schedule have finished. The paper allows the same job to revisit a machine, as the final job does here.
For every valid , the main goal states both the paper's preemptive equivalence and the non-preemptive form established by its two directions:
The milestones follow the source's proof text: the schedule supplied by a solution in Lemma 7(a), the timing forced on the final job, the exclusion of short preemptive schedules in Lemma 7(b), and the preemptive equivalence stated in the proof. The final-job milestone describes the occupied time slots of the paper's Figure 4, independently of how many adjacent pieces a formal schedule uses.
The equivalence transfers the distinction between solvable and unsolvable 3-PARTITION inputs to an exact finish-time threshold in a job shop with only two machines. It also establishes the non-preemptive decision equivalence for this construction, because a solution yields a non-preemptive schedule while an unsolvable input rules out even the more permissive preemptive schedules. These facts supply the scheduling part of the paper's strong NP-completeness claim; membership in NP is handled separately by Lemma 6 (pp. 44–45).
The result is proved in the source paper. The work proposed here is a machine-checked development of its explicit reduction equivalence and the finite-piece scheduling model needed to state it. The milestone theorems expose statements that can be reused when formalizing other preemptive scheduling reductions. The shared job-shop instance and 3-PARTITION input are already published definitions; the particular reduction instance and preemptive schedule predicate are new local definitions.
Preemption makes a task's processing time distributable across intervals. Merely checking that each machine has enough total capacity does not characterize feasible schedules: every job's operations must still occur in order, and pieces of different jobs must avoid one another on each machine. The converse direction must constrain every preemptive schedule that meets the threshold, not only a schedule having the visual pattern in Figure 4. A schedule can also represent one uninterrupted interval as several adjacent pieces, so piece count alone cannot express the source's timing claim.
Machines are Fin 2, with numbered and numbered . Jobs are Fin (3t+1); the final job is index . Its zero-based operation uses machine for even and machine for odd . The definition uses the published JobShopLTAS.Core.Instance for ordered operations, machines, real processing times, and non-preemptive feasibility. It uses the published ResourceScheduling.Chain.ThreePartition for , validity, and solutions. Those objects have the same conventions as the paper here. The local preemptive model uses finitely many positive-length pieces per task, whose durations sum exactly to that task's processing time. The threshold is the explicit real cast of ; no real infimum or division by a possibly zero optimum appears.
The goal is specific to the instance the paper constructs from each valid input. A free job-shop instance, a freely chosen schedule, or an extra hypothesis that the input has a solution would erase the reduction's content. Validity carries , total , and both strict bounds on each . The case remains in scope: the constructed job has no tasks and its finish-time threshold is zero. All existing tasks have positive length whenever the input is valid, so the published non-preemptive predicate's treatment of zero-length tasks does not affect this mission.
The paper states “3-Partition preemptive JOFT with ” and connects it to NP-completeness for preemptive and non-preemptive scheduling when complexity is measured by the sum of task lengths. The Lean theorem states the proof's two decision equivalences with constant and machine count . It does not formalize as a polynomial-time many-one reduction, the unary task-length measure, NP-completeness, or Lemma 6's NP-membership argument. Contributions that establish the reduction statements, the schedule construction, or general finite-piece scheduling facts are within scope.
Shop scheduling asks how to process a set of jobs, each a sequence of tasks on prescribed machines, so that all work is completed as early as possible. The flow shop, in which every job visits the machines in the same order, is the most studied of these models in operations research. For two machines, Johnson's rule (1954) computes a schedule of minimum finish time in time, and for two machines allowing interruptions (preemption) does not help. Garey, Johnson and Sethi (Math. Oper. Res. 1976) and Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum report BW 43/75, 1975; Ann. Discrete Math. 1977) showed that the non-preemptive problem becomes NP-complete with three machines.
Gonzalez and Sahni (Operations Research, 1978) extended this picture to preemptive schedules. Their Theorem 1 shows that minimizing the finish time of a three-machine flow shop is NP-complete with or without preemption, even when every job has at most two tasks of nonzero length. When every job has only one task the problem is trivial, so this is the simplest NP-complete case of the flow-shop finish-time problem. The result explains why no exact polynomial algorithm is expected and motivates the approximation results in the second half of the same paper.
Timeline:
A flow shop has processors and a finite set of jobs. Task of job must be processed on for time units, and it can start only after task of the same job is completed. Task times may be zero. The schedule starts at time .
A preemptive schedule gives every task a finite set of pieces with : the task is processed on its processor during . Pieces on the same processor do not overlap, the pieces of a task have total length , and every piece of a task starts after every piece of the earlier tasks of the same job has ended. A non-preemptive schedule processes every task in at most one piece. For a schedule , is the time at which job is completed and the finish time is .
PARTITION. A multiset of nonnegative integers has a partition if some set of indices satisfies .
The instance FS. With , the flow shop has processors and jobs:
and the threshold is . Every job has at most two nonzero tasks.
For every and every :
The result. The equivalence shows that a polynomial-time algorithm deciding whether a three-machine flow shop (with two nonzero tasks per job) has a schedule of finish time at most , preemptive or not, would decide PARTITION in polynomial time. With membership in NP (the paper's Lemma 2) it gives NP-completeness of both versions. It also marks the boundary with the polynomial cases: (Johnson's rule), and jobs with a single task.
Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no machine-checked proof of this reduction exists, and the platform has no formal model of preemptive shop schedules. The mission produces one: a piece-based preemptive schedule with zero task times, which subsumes the non-preemptive case, together with the first formal NP-hardness reduction for preemptive flow shops on the platform.
Direction (a) asks for one explicit schedule. Direction (b) must rule out every preemptive schedule of FS, and preemption is exactly what makes this delicate: a task may be split into any finite number of pieces placed anywhere on its processor, so the naive intuition that a failed partition leaves "unusable gaps" is no longer evident, since pieces of different jobs can be interleaved to fill gaps. A correct argument must therefore be an accounting of processor time over the pieces, valid for any number and position of pieces, and it must treat zero-length tasks, which occupy no processor time but still delay the next task of their job. Finally, the non-preemptive equivalence is not a formal consequence of the preemptive one alone: it uses that (a) produces a non-preemptive schedule and that (b) holds for all preemptive schedules, which include the non-preemptive ones.
Fin 3 ( = 0, 1, 2), jobs of FS are Fin n ⊕ Fin 2 (Sum.inr 0 is job , Sum.inr 1 is job ). Task times are real numbers; the PARTITION data are a : Fin n → ℕ, and "has a partition" is in .Finset of pieces per task with the four conditions of the Setting. Non-preemptive means at most one piece per task. Zero tasks have no pieces and occupy no processor time. and are maxima with baseline .A finite Markov decision system asks how to choose actions while a changing state controls which actions are available. The choice can affect both the reward now and the distribution of future states. In a total-reward problem, the process can continue indefinitely; if transitions are substochastic, it can also terminate. Kallenberg's treatment of positive dynamic programming connects this control problem to a finite linear program and uses an optimal flow to identify a policy that is optimal from every initial state Kallenberg, Chapter 3.
The connection matters when an optimizer is easier to compute as state-action frequencies than as an infinite sequence of decisions. A policy may depend on the entire observed history and may randomize at every decision. The theorem under study says that, when the dual linear program has an extreme optimal solution, its positive coordinates identify a pure stationary policy as good as every such general policy. This assertion includes models in which the selected policy is not transient Kallenberg, Theorem 3.5.2 and Example 3.5.1.
Let be a nonempty finite state space. At state , one chooses an action from the nonempty finite set . Action earns a real reward and moves to state with probability . The sum is at most one; any missing probability represents termination. Positive dynamic programming imposes for every admissible state-action pair Kallenberg, Section 2.2 and Assumption 3.5.1.
A policy assigns an action distribution after each finite history. The history records the initial state and all states and actions observed so far. Write for this full policy class. A pure stationary policy always chooses one fixed admissible action whenever it visits .
Starting from state , let be the expected total reward of , and let . Because the rewards are nonnegative, the finite-horizon expected totals increase to ; both policy and optimal values may be . A real vector is TMD superharmonic if for each and Kallenberg, Definition 3.3.1.
For given weights , equation (3.5.2) is a linear program over nonnegative state-action flows . It maximizes subject to
The set records the states with positive flow Kallenberg, Notation 3.1.1 and equation (3.5.2).
Theorem 3.5.1 identifies as the smallest nonnegative TMD-superharmonic vector. The original superharmonic definition ranges over real vectors; the value must also be allowed to take . The formal statement gives both the extended superharmonic inequalities for and its componentwise bound by every nonnegative real superharmonic vector:
This is the numbered milestone of the mission Kallenberg, Theorem 3.5.1.
The main goal is Theorem 3.5.2. Suppose is an extreme point of the feasible region of (3.5.2) and has objective at least as large as every feasible flow. Then every pure stationary rule choosing on , with arbitrary admissible actions outside , is total optimal:
The goal records the finite-optimum case by requiring an actual optimal solution ; it makes no extra assumption that every policy is transient Kallenberg, Theorem 3.5.2.
The theorem converts an extreme optimal state-action flow into one decision rule that is optimal simultaneously for all starting states. Since includes policies that change with time, use full histories or randomize, it establishes that those freedoms cannot improve the total-reward value when the stated dual optimizer exists. The positive model also reveals when extended values matter: outside the finite-optimum case, the dual objective may be unbounded and an optimal total reward may be infinite Kallenberg, pp. 78–83.
A formal development of this result must keep the policy class and the linear program in the same model. It provides reusable definitions of a finite substochastic control system, finite-history probabilities, extended total rewards, state-action flows and superharmonic vectors. The result is proved in the book; the mission asks for a machine-checked proof of its statement, not for a new optimization theorem. The draft statements are open goals until such proofs are supplied.
A finite linear program has finitely many variables, while the value compares a flow-derived rule with every infinite, history dependent policy. A comparison restricted to stationary or transient policies would miss the main assertion. The proof also has to treat zero-flow states: the dual solution does not prescribe an action there, yet the theorem permits every admissible choice. Finally, the superharmonic milestone permits an infinite value, while the linear program itself uses real coordinates. A development must connect those representations without turning an infinite reward into an arbitrary default real value.
Lean represents states as Fin N with , and each as a nonempty finite subset of a finite action type. The transition rows sum to at most one. Histories carry past states and actions, and the first action has internal index zero, corresponding to the book's time one. Policy probabilities are nonnegative, vanish outside and sum to one. The expected reward of a finite horizon is a finite sum over histories; nonnegative total reward is its supremum in EReal. The value takes the supremum over the full policy type, not over a restricted policy subclass.
Dual flow coordinates exist only for admissible state-action pairs. Extreme points are taken in the feasible set of (3.5.2) in those coordinates, and its balance constraints retain the source's direction. The goal quantifies over every admissible pure rule satisfying the positive-flow condition. These choices exclude the vacuous shortcut of defining the value using only pure stationary policies or assuming optimality as a hypothesis.
The mathematical infrastructure includes finite policy histories, state-action occupancy probabilities, extended nonnegative reward limits, the real flow polyhedron and its extreme points. The history and flow definitions can support later work on other finite decision models. Contributions to those foundational results and to the full comparison with history dependent policies are within the mission's scope. The negative-reward regime of Section 3.6, whose claims involve average optimality and recurrent classes in an extended stochastic model, requires its own representation and is outside this positive-reward target.
Every pure integer program, once its linear programming relaxation has been solved, can be relaxed further to a problem over a finite Abelian group: the nonbasic variables must satisfy a single congruence in the group of the optimal basis. R. E. Gomory introduced this relaxation in 1965 and studied the convex hull of its solutions in Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969), 451–558, doi:10.1016/0024-3795(69)90017-2). The facets of these group polyhedra are valid inequalities for every integer program whose basis produces the same group, and they became the source of cutting planes for integer programming: Gomory's mixed-integer cut and the later theory of corner polyhedra and subadditive valid inequalities descend from them.
The number of facets grows fast with the order of the group, so a list of facets for each group is not a usable description. Section 3D of the paper, "Lifting up Faces", gives a structural tool instead: facets of the polyhedron of a small group produce facets of the polyhedron of every larger group that maps onto it. This mission formalizes that construction (THEOREM 19) and its converse (THEOREM 20).
Let be a finite Abelian group, written additively, with zero and order , and let . For a right-hand side , the group equation asks for nonnegative integers , , with
Its solution set is ; when , the zero solution is excluded, as stipulated on p. 474. Each solution is a point of , a space of dimension , and the master polyhedron is the convex hull of . Gomory reads a solution as a path from to that uses the element exactly times; with arc lengths its length is .
An inequality , written , is a face of when , every satisfies it, and the solutions on the hyperplane generate that hyperplane: every point of it is a weighted sum, with total weight 1, of such solutions. A face is therefore a facet; Gomory says "face" throughout, and so does this mission. The solutions with are the minimal paths.
Let be a homomorphism of onto a second finite Abelian group , with kernel . A coefficient vector on is lifted to by
so that every element of the kernel gets coefficient .
If and is a face of with , then
For instance, the face of lifts through reduction mod 2 to the face of (p. 488).
Conversely, a face of with and for some is the lift of a face of for some of onto a group with .
THEOREMS 19 and 20 together say that the faces of with and a zero coefficient are exactly the faces lifted from proper quotients of . A catalogue of these positive-right-hand-side faces therefore only needs the faces with all coefficients positive; the rest come from smaller groups. Gomory uses this to explain the tables of Appendix 5: for and every such face is a lift of the single nontrivial face of , and for a direct sum every face of the polyhedron of a summand not containing extends to a face for (p. 489). The same idea, sending facets of one group problem to facets of another by a homomorphism, recurs in the later theory of group relaxations and infinite group problems.
Both theorems are proved in the paper. To the knowledge of this mission, neither the group polyhedra, their faces nor the lifting theorem has a machine-checked formalization; the platform's other "lifting" results (lifted cover facets of the knapsack polytope, cone lifts of convex sets) are different notions. The mission produces a reusable definition layer for master group polyhedra and their faces, stated once for an arbitrary finite Abelian group, and a formal version of the passage between faces of a group and of its quotients.
Validity of the lifted inequality is a one-line computation (milestone 2). The content is that the lift is a facet: one must exhibit affinely independent solutions on the hyperplane, while the quotient face only supplies of them. A solution of the quotient problem does not determine a solution for ; coset representatives must be chosen and the path closed by a kernel element, and the kernel coordinates, which all have coefficient zero, must still be filled to full rank.
The obvious reduction, "a facet pulls back to a facet under a surjective map", fails here because the map from -paths to -paths is a linear projection from dimension to and does not lift independence by itself. It also fails at : with , , , the face of lifts to , which is valid but not a face of .
The formalization uses one definition file for an arbitrary finite Abelian group ([AddCommGroup G] [Fintype G] [DecidableEq G]), instantiated at both and . It commits to the following readings:
Function.Surjective ψ, and is .A formalization that proves only validity of the lift, or that defines faces without the generation condition (so that every valid inequality is a "face"), would be trivial and is ruled out by the definition of IsFace.
The development needs finite sums over fibres of , a choice of coset representatives, and a rank argument for a block matrix with full-rank diagonal blocks. The definitions of , and face are reusable for any further result on master group polyhedra. Proofs of the milestones in any order, alternative proofs of the face criterion, and a proof of THEOREM 20 are welcome.
Finite group equations arise when an integer program is expressed relative to an integer basis: the residue of a candidate solution in a finite Abelian group records whether it satisfies the original integrality requirement. Gomory's group polyhedron collects the nonnegative integer solutions with one prescribed residue. Its faces give valid linear inequalities for the group relaxation, so a description of those faces is useful to anyone studying integer programming cuts or the geometry of integer hulls. Gomory's 1969 paper develops the group equation and its polyhedra in this setting and then gives a finite system for the faces of the largest, or master, polyhedron. Gomory 1969, pp. 457–458, 474, 480–483.
The main question is how to recognize a facet inequality without ranging over every nonnegative integer solution of the group equation. The paper's Theorem 7 characterizes facets through a system with one row for each integer solution, an infinite collection in general. Theorem 18 replaces that family by rows determined by pairs of group elements and a rank condition at the candidate coefficient vector. Gomory 1969, pp. 469–470, 481–483.
Let be a finite Abelian group with zero , and let . For a subset and a right-hand side , a group-equation solution is a nonnegative integer vector satisfying
The set of solutions is , and the group polyhedron is their convex hull in the real coordinate space . The master polyhedron uses . This mission concerns ; Gomory specifies a separate convention at , excluding the zero solution from that master polyhedron. Gomory 1969, pp. 457–458, 474–475.
Gomory calls a face when , all points of satisfy the inequality, and its tight points generate the entire hyperplane by affine combinations. Thus "face" means a facet of full hyperplane dimension here. The equivalent integer-point criterion uses the tight members of , which is the representation adopted in Lean. A basic feasible solution of a linear system satisfies every equation and inequality and has tight rows whose coefficient vectors span the full variable space. Gomory 1969, pp. 468–469.
The path to the goal starts with the sign of the face coefficients, the infinite-system characterization, and the shortest-path interpretation. An integer vector represents a path whose total group displacement is and whose length is . The shortest-path statements lead to subadditivity and complementary equalities for face coefficients. For , Theorem 17 collects the row conditions needed for the final system. Gomory 1969, pp. 469–473, 480–481.
The target is Theorem 18. Fix and . With , system (13) is
The goal asserts the full equivalence
The equation rows, ordered pair rows, and nonnegativity rows all count toward basicness; is held fixed. Gomory 1969, pp. 481–483, Theorem 18.
Theorem 18 turns a geometric property defined against infinitely many integer vectors into a finite test in coefficient variables. A solver can check its displayed equations and inequalities and then check whether the tight row vectors have full rank. That gives a concrete route to enumerating the facet coefficient vectors of for a fixed finite group, the use Gomory reports immediately after the proof. Gomory 1969, p. 483.
The result was proved in the paper; the work here is to formalize that known theorem and the numbered results it uses. The group-solution model, the integer-point facet criterion, and the generic tight-row definition of basic feasibility can also support other group-polyhedron arguments. The local prior-art search found related formalizations of facets and polyhedra, but none with the same integer-point-generated hyperplane and finite-group conventions, so these definitions are stated for this paper's objects.
Validity of the rows of (13) for a face does not by itself establish Theorem 18. Basicness requires the tight rows to span all coefficient directions, and the converse must turn that rank information into enough tight integer solutions to generate a hyperplane. A supporting inequality that is tight at only a smaller face would pass a mere feasibility check while failing Gomory's face definition. The shortest-path results connect the group equations to the coefficient restrictions, but do not erase the rank requirement. Gomory 1969, pp. 468–470, 472–473, 481–483.
Lean uses a finite Abelian group and a Finset of nonzero elements. Its real vectors have coordinates indexed by itself, with no unconstrained zero coordinate. The group equation is a finite sum of natural-number multiples in ; is the real convex hull of the cast integer solutions. A face requires a nonzero normal, validity on every integer solution, and equality between the affine span of tight integer points and the entire hyperplane. This excludes the trivial reading that merely asks for one tight point. It also makes an empty solution set incapable of supplying a face. Theorem 7 assumes nonempty (), as the paper does implicitly: with no coordinates every vector would be trivially basic.
Paths are represented by their nonnegative integer arc-multiplicity vectors. The same vector can describe several arc orders, but the length and group displacement used here depend only on multiplicity. Shortestness is stated by comparison with every competing vector of the same displacement; no infimum with an empty-set default is used. The complement and subadditivity rows of (13) use , and the subadditivity rows include ordered pairs with equal entries. Basic feasible solutions use the span of tight coefficient rows, including equation rows, in the full real space of variables.
The mission includes the paper's Theorems 6, 7, 10, 17, Lemmas 1–2, and both numbered corollaries on p. 473 as milestones. Contributions that establish the affine-span and rank equivalences, or reusable finite-group shortest-path and polyhedral lemmas, directly advance the target. Theorems for and for other sections of the paper are outside this mission's stated domain.
A decision maker may choose an action whenever a system changes state, even though the time until the next change is random. Maintenance and replacement decisions are examples: a repair choice changes both the next operating state and the length of time before another choice is available. A discrete-time Markov decision model gives every decision epoch the same duration. A semi-Markov decision process allows the holding time to depend on the current state, action, and next state. Kallenberg's Chapter 7 develops discounted and average-reward versions of this finite-state model, including a characterization of optimal discounted value through inequalities and a linear program (Kallenberg 1983, Chapter 7).
The mission focuses on the discounted part of that chapter. The result is known: Kallenberg proves it as Theorem 7.2.1. The formalization task is to state and eventually prove the result for the same policy class and the same general holding-time distributions. Those details matter because a stationary-policy-only version would omit the comparison that the theorem makes with all admissible policies.
Let be a nonempty finite state set. Each has a finite nonempty set of available actions. If action is chosen, the next state is with probability , with . Conditional on , the nonnegative time until that transition has distribution . The action earns a lump reward immediately and a reward rate during the ensuing sojourn. Neither the holding-time laws nor the reward rates are required to be identical across transitions (Kallenberg 1983, pp. 210–212).
Fix a positive continuous discount rate . The factor applied after elapsed time is . Assumption 7.2.1 requires the Laplace–Stieltjes transform of each conditional holding-time law to satisfy
The assumption is strict for every triple; it does not require a particular parametric family. Define the one-epoch expected discounted reward and discounted transition entry by
A policy is a sequence of randomized decisions. At each epoch its choice may depend on every previously observed state and chosen action and the current state. It does not observe previous sojourn times when choosing. Let be the expected sum of discounted lump and rate rewards from initial state , as in equation (7.2.1). The DRD value vector is , with the supremum over this full policy class. A real vector is DRD-superharmonic when
These are Kallenberg's Definitions 7.2.1 and 7.2.2 (p. 214).
Theorem 7.2.1 states that the value vector itself satisfies the superharmonic inequalities and lies below every other vector satisfying them:
This is the mission goal. Its content includes both clauses: merely showing that every superharmonic vector bounds policy rewards would leave out the assertion that the value is superharmonic.
Lemma 7.2.1 expresses as a sum of expected discounted state-action occupancies. Theorem 7.2.2 says that a feasible action choice attaining equality in the value equation at every state yields an optimal pure stationary policy. Theorem 7.2.3 says that positive support in an optimal solution of the dual linear program (7.2.11) yields such a policy. Their statements and exact conditions are the mission's milestones (Kallenberg 1983, pp. 212, 216–217).
The goal turns a supremum over possibly history-dependent randomized policies into a finite system of inequalities indexed by available state-action pairs. The next two results explain how equality in those inequalities and an optimal linear-programming solution identify a pure stationary policy with the same value. Thus the finite programs are statements about the original semi-Markov process rather than a separate discounted matrix model (Kallenberg 1983, pp. 214–217).
Kallenberg supplies paper proofs. This mission supplies Lean statements and a shared model interface; the proposed theorem items still require machine-checked proofs. The model's arbitrary conditional holding-time measures, its distinction between the current reward and future discounted value, and its history-dependent policy class are reusable for other finite semi-Markov arguments. The average-reward section of Chapter 7 is outside this mission.
The straightforward finite-state discounted equation concerns expected one-step rewards. The source value, however, is defined from rewards earned at random physical times, and a policy can react to its entire discrete history. Identifying these two descriptions requires accounting for the joint state, action, and elapsed-time law without giving the policy access to past holding times. Holding times may equal zero with positive probability; the strict transform assumption excludes a degenerate law concentrated entirely at zero, but it does not make each holding time strictly positive. A second issue is real-valuedness: all-policy suprema and integrals must represent the finite quantities in the source rather than Lean's default values on ill-posed inputs.
Lean uses finite types for states and actions, with a nonempty available-action finset for each state. Conditional sojourn laws are probability measures on with no mass on negative times. This includes arbitrary distributions on and permits an atom at zero. The model stores stochastic transition rows, lump rewards, and rate rewards. The discounted layer stores and the source's strict per-triple transform inequality. The expected one-epoch reward uses a Lebesgue integral against each sojourn law.
Policy decision rules read a list of past state-action pairs and the current state. Finite-horizon value recursively integrates the original epoch reward and its holding-time discount; policy value is its limit. The coordinatewise supremum ranges over all such policies. The occupation sum of Lemma 7.2.1 is a separate theorem, not the definition of policy value. A proof must establish convergence and boundedness from Assumption 7.2.1 so that Lean's total limit, integral, and real-supremum operations have their intended meanings.
The dual program sums only over actions available in each state and uses strictly positive weights , equality flow constraints, and nonnegative variables as printed. Its pure stationary selector must choose an available action with positive dual mass in every state. Contributions establishing the occupation identity, value bounds, Bellman inequalities, or dual decoding all fit the mission.
An integer program in standard form, subject to , , integer, is easy to state and hard to solve. Its linear programming relaxation is solved by the simplex method, which ends at an optimal basis . The difference between the two problems is the integrality of , and R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2, 451–558, doi:10.1016/0024-3795(69)90017-2) measures that difference with a finite Abelian group. Dropping only the nonnegativity of the basic variables leaves a problem whose feasible set has a simple structure: its convex hull is the corner polyhedron, and its integer points are the solutions of an equation in the group .
The first section of the paper uses this to explain when the integer program reduces to the group problem. Its asymptotic theorem says that if lies far enough inside the cone where is LP-optimal, then an optimal solution of the group problem gives an optimal integer solution. Gomory first proved this in 1965 (On the relation between integer and noninteger solutions to linear programs, PNAS 53, 260–265, doi:10.1073/pnas.53.2.260) by a counting argument on group solutions. The 1969 paper proves it again through the geometry of the corner polyhedron. The vertices of that polyhedron are irreducible, and an irreducible point is small. This is the version formalized here.
Let be an integer matrix, with a nonsingular matrix (the first columns) and the matrix of the remaining columns . As on p. 452 of the paper, contains an unit matrix. Let and . The integer program (2) is
The relative prices are , with components . is an optimal LP basis when and every .
The group is , where and is the lattice of integer combinations of the columns of . Let be the quotient map. is finite of order . Let be the set of nonzero elements among , and put . The group equation is
and is the convex hull of its solutions in . A nonnegative integer is irreducible if any two integer vectors with and are equal.
The group costs are . Problem (8) minimizes over the solutions of the group equation. A corresponding vertex of a point (Remark 1) is a nonnegative integer with three properties: ; at most one positive per group element; and when . It uses only least cost columns when only if .
The cone is where is LP-optimal. is the set of its points at Euclidean distance at least from its frontier, and is the largest Euclidean length of a column .
If , is a vertex of minimizing (8), and is a corresponding vertex using only least cost columns, then
THEOREM 4 explains why integer programs with large right-hand sides are often easy. For outside a band of width along the boundary of the cone , the integer optimum is the LP solution plus a correction that depends only on the class of modulo the lattice of . That correction is periodic in and can be tabulated once for the group elements. The vertex form adds a structural statement: the correction can be read off a vertex of the corner polyhedron, so the faces and vertices of corner polyhedra (the subject of the rest of the paper) bear directly on integer programming. Display (10) shows such optimal solutions are small: their nonbasic parts satisfy .
All results here are proved in the paper. None of them is formalized yet. The 1965 version of the asymptotic theorem, posed as THEOREM 1 of the mission on Gomory (1965), is in the same family of statements. Its hypothesis is that the group solution is optimal; here the hypothesis is that it is a vertex of . Its counting lemma (a short optimal group solution) and its bound have counterparts in milestones 4 and 6.
An optimal solution of the group problem need not be short. Group solutions can be made longer without changing their cost (add a zero-cost cycle), and a long nonbasic part can push out of the cone , making negative. The goal must therefore use the vertex hypothesis. Vertices are irreducible (THEOREM 2), and irreducibility bounds their size through a pigeonhole count in the finite group (THEOREM 1). The formal work is spread across three settings: the convex geometry of the hull of an infinite integer set, the arithmetic of the quotient and its order, and the linear algebra connecting , the cone and its frontier.
Vectors on are functions on the subtype of a Finset of the group. Integer solutions are -valued, and is convexHull ℝ of their real images. THEOREMS 1 and 2 are stated for an arbitrary finite Abelian group and any finite not containing , as in the paper. The integer program uses the basis as the first columns, Fin m ⊕ Fin n. is the real matrix inverse, and every statement assumes . Optimality of means feasibility plus for every feasible integer ; no supremum is taken. The loose phrases of the paper are read as follows.
The printed slip on p. 462 ( for THEOREM 1's product) is corrected in the Lean. Dropping the vertex hypothesis from the goal is not a valid formalization (the statement becomes false in general), and neither is defining irreducibility with real (THEOREM 1 then fails). The existence of a minimizing vertex, which the paper takes for granted, is not posed.
A complete development needs the finiteness and order of (Mathlib's AddSubgroup.index_eq_natAbs_det), extreme points of convex hulls (extremePoints_convexHull_subset), and an argument that a closed cone with deep inside it contains the ball around . The group-polyhedron definitions and THEOREMS 1–2 apply to any finite Abelian group and are reusable beyond this mission. Proofs of any milestone are welcome independently.
A two-person zero-sum stochastic game (also called a Markov game) is a Markov decision problem with two decision makers who pull in opposite directions: at every time point both players choose an action simultaneously, one player pays the other, and the system moves to a random next state whose law depends on the current state and both actions. Stochastic games were introduced by Shapley (Shapley 1953) and are the standard model for adversarial sequential decisions in operations research, economics and computer science (pursuit–evasion, inspection, robust control against an adversarial environment).
Shapley proved that a discounted stochastic game has a value and that both players have stationary optimal policies. The value, however, is in general not computable by linear programming: it need not lie in the field generated by the data. Kallenberg's Example 6.2.1 (after Parthasarathy and Raghavan) has rational data and an irrational value in one state. When only one player controls the transition probabilities, the situation changes: the value and stationary optimal policies are the optimal solutions of one pair of dual linear programs (Parthasarathy & Raghavan, as cited in Kallenberg 1983, pp. 192 and 196; Kallenberg 1983, Chapter 6).
Timeline.
The state space is with . In state player I chooses an action from a finite nonempty set and player II an action from a finite nonempty set . Player I then receives from player II, and the next state is with probability , where .
A history at time is . A policy of player I chooses, at each time and history, a probability distribution on ; policies of player II are defined likewise. A policy is stationary, written or , if the distribution depends only on the current state. With the expected reward in period from initial state , the total reward is .
A pair is optimal if, componentwise,
and then is the value of the game.
Assumption 6.2.1 (contraction). There are and with for all , , . The discounted game is the case .
Assumption 6.2.2 (single controller). does not depend on ; it is written .
For a stationary write and . A vector is TMG-superharmonic if some stationary of player II satisfies for all , . For weights the two linear programs are
Under Assumptions 6.2.1 and 6.2.2, let and be optimal solutions of (6.2.1) and (6.2.2), and . Then
The goal fixes no constants; it states that the LP pair produces the value and optimal stationary policies.
Theorems 6.2.1 and 6.2.2 hold for the general contracting game. Assumption 6.2.2 enters only from (6.2.1) on.
The result. Theorem 6.2.3 turns a single-controller game into a finite computation, Algorithm XXVII: solve one LP pair and read off the value and optimal stationary policies of both players. A consequence (Remark 6.2.1) is that the value and the optimal decision rules lie in the field generated by the rewards and transition probabilities. Example 6.2.1 shows this fails without Assumption 6.2.2. Theorem 6.2.4 matches the feasible points of the dual program with the stationary policies of the controlling player. This is the game version of the correspondence between state-action frequencies and policies in Markov decision problems.
Formalizing it. All results are proved in the book, and Theorem 6.2.1 is classical. None of them is formalized: the platform has turn-based stochastic games with positional strategies (TBSGStrategyIteration), which do not cover simultaneous moves or history-dependent randomized policies. The mission adds a reusable model of simultaneous-move stochastic games with history-dependent policies, together with machine-checked optimality of the LP solution against every such policy.
There are two difficulties. First, optimality in (6.1.1) is against every history-dependent randomized policy of the opponent, while the LP produces only stationary policies. Fixing one player's stationary policy reduces the game to a Markov decision problem for the other player (Remark 6.1.1), and the facts needed from that problem (stationary policies suffice, and the value is the smallest superharmonic vector) are theorems about contracting MDPs, not consequences of the LP. Second, Theorem 6.2.2 rests on Shapley's existence theorem, which is not a linear-programming fact: its usual proof is a fixed-point argument for the Shapley operator built from one-stage matrix games. Remark 6.2.2 indicates a route that avoids it, through the bounded polytope of state-action frequencies of a contracting MDP. Either way, LP duality alone does not give optimality against non-stationary opponents.
Fin N with . Actions live in finite types α, β, and , are nonempty Finsets. Rows are substochastic.tsum of the period rewards, which converges absolutely under Assumption 6.2.1, and every theorem assumes it.Restricting either player's policy class to stationary policies would make the optimality claims of Theorems 6.2.1 and 6.2.3 a statement about a finite family and is ruled out: the comparison class is all history-dependent randomized policies.
Lemma 6.1.1 is Mathlib's isSaddlePointOn_value (Mathlib/Order/SaddlePoint.lean) and is not restated. The LP duality theorems of Chapter 1 are proved on the platform (LinearOptimization.lp_strong_duality, lp_complementary_slackness) and may be used. Useful contributions include: the reduction of Remark 6.1.1 (a fixed stationary opponent gives an MDP), the contracting-MDP facts it needs, and a proof of Theorem 6.2.1. The model definitions are reusable for any finite stochastic game.
A Markov decision model describes a system that repeatedly occupies a state, receives a reward when an action is chosen, and then moves according to action-dependent probabilities. Termination may occur after any action. In a model with signed rewards, a policy that continues indefinitely can have a different total-reward behavior from one that eventually leaves the active states. Section 3.3 of Kallenberg's 1983 monograph therefore asks for the best policy within the transient class. The restriction occurs naturally in stopping problems: a decision maker may continue for a while, but the expected number of visits to each active state must remain finite.
The chapter relates that policy problem to a finite linear program. The central question is stronger than finding a policy with a large average over initial states. It asks for one policy that is optimal from every initial state among all transient policies, including policies that randomize and use the entire observed history. Kallenberg's Theorem 3.3.5 says that an extreme optimal point of the program identifies such a policy, and that the policy can be pure and stationary. Theorem 3.3.5, p. 57.
Let be a nonempty finite state set. Each state has a finite nonempty set of available actions. If action is selected, the system earns the real reward and then moves to with probability . The row sum is at most one; any missing mass represents termination. Action sets can differ across states. These are the conventions of Section 2.2, pp. 19–20.
A policy selects an action distribution at each decision epoch. It may depend on the entire state-action history. A Markov policy depends only on time and the current state; a stationary policy uses the same state-dependent distribution at every time; a pure stationary policy selects one action in each state. These four classes are denoted , , , and . The first decision occurs at time in the book.
Write for the chance of being in state and choosing action at time , given initial state . A policy is transient if the expected number of visits to each state is finite from every initial state:
For such a policy, its expected total reward is finite. Section 3.3 assumes that at least one transient policy exists. Its transient value is , which can still be infinite as the policy varies. Section 2.2, pp. 21–23; §3.3, pp. 49–50.
Fix positive weights . The linear program (3.3.7) maximizes over nonnegative state-action arrays satisfying the flow equations
Its feasible set is . A transient stationary rule has an occupation vector , where is the -weighted expected number of visits to state-action pair . Theorem 3.3.3 identifies transient stationary rules bijectively with and identifies extreme points with pure rules. Theorem 3.3.4 compares the occupation sets of all four policy classes: , where the bar means closed convex hull. Theorems 3.3.3–3.3.4, pp. 54–55.
The goal is Theorem 3.3.5, p. 57. If is an extreme optimal solution of that program and is the action with , then the pure stationary policy is transient and
A stronger companion statement is Theorem 3.3.6, p. 58: under the correspondence of Theorem 3.3.3, a stationary policy is optimal transient exactly when its occupation vector is optimal for (3.3.7), in the two directions printed on the page. The milestone list follows the chapter's numbered results on the finite-value Bellman equation, the smallest superharmonic vector, the stationary-policy/LP correspondence, the four occupation sets, and the preservation of optimality. The goal itself does not assume that is finite; the existence of an extreme LP optimum is its stated premise.
An LP optimum is a vector of occupation amounts, not an implementable policy by itself. Theorem 3.3.5 converts an extreme optimum into an action choice at each state. It also upgrades a scalar objective weighted by to simultaneous optimality of the resulting policy from every initial state. This is the bridge between the finite optimization problem and the original control problem. The scope is specifically transient optimality: Example 3.3.4, p. 58 gives a policy outside that comparison class with larger total reward.
The result is proved in the book. The work here is to give its model, occupation map, linear program, and numbered supporting statements precise Lean interfaces that can later receive machine-checked proofs. The reusable parts include finite substochastic MDP data, history-dependent policy semantics, transient visit sums, and state-action occupation vectors. The theorem proofs are open in this proposal.
Optimizing a weighted sum of rewards is not, by itself, the same as optimizing every state's reward. The linear program also describes flows of expected visits, while the theorem talks about actual policies and all initial states. A solver must account for both links without assuming that all policies are stationary. The geometry of an extreme feasible point matters because the theorem selects an action from each state using a positive coordinate. Existence of a transient policy does not by itself bound the supremum of transient rewards; Example 3.3.1, p. 50 makes that distinction explicit.
Lean uses Fin N with for states and a finite action type with a state-dependent finite nonempty available-action set. Only available state-action pairs index occupation vectors and LP variables. Transition rows are substochastic, not necessarily stochastic. Rewards are real and may have either sign. A general policy is a normalized action kernel on full finite histories; its Markov, stationary, and pure stationary subclasses remain distinct. The history list is stored newest first, and Lean's time index zero corresponds to the book's time one. All state-action probabilities are finite sums over histories; transience is summability of state-visit probabilities, and occupation counts are infinite sums used under that condition.
The LP flow constraints are equalities and is strictly positive. The goal does not normalize to a probability distribution, matching (3.3.7); Theorem 3.3.4 uses the initial-distribution convention of p. 55 and hence normalizes it. Theorem 3.3.3 uses the matrix inverse only for transient stationary rules. For Theorems 3.3.1–3.3.2, nonemptiness of the transient class and boundedness above of each transient reward set make the real supremum meaningful. Theorem 3.3.5 uses neither boundedness as an extra hypothesis nor a restriction of the comparison class to stationary policies. A formalization that compares only with stationary (or Markov) policies, or that identifies the classes , , , , would make Theorems 3.3.4 and 3.3.5 much weaker or trivial, and is ruled out: the comparison class is every history-dependent randomized transient policy. Mathlib's finite sums, matrices, summability, convex hull, and extreme-point definitions provide the general library interface. Contributions establishing the policy/occupation identities and the chapter's numbered milestones are within scope.
Integer linear programming asks for the best point whose coordinates are integers, even though linear programming methods naturally search over real points. In his 1958 note, Gomory describes a systematic way to add a constraint that excludes a fractional simplex solution while retaining every nonnegative integer solution. This mission isolates that single cut and its effect on the objective value. The note announces an iterative finite algorithm, but explicitly defers a proof of finiteness to another treatment. The target here is the cut's correctness for one tableau.
The cut belongs to the history of cutting plane methods for integer programs. Related formalized objects include a Chvátal closure and intersection cuts based on lattice free sets, but their data and cut constructions differ from the row and fractional part formula in Gomory's note. The note itself contrasts its systematic row operation with earlier problem specific constraints used by Dantzig, Fulkerson, and Johnson and by Markowitz and Manne. Those comparisons explain why a reusable row formula is useful; they do not assert an identity between the different cuts.
A tableau is a finite array of real numbers . Row represents the objective variable ; rows represent . Column holds constants; columns multiply the negatives of the variables . A solution of (2) is a pair satisfying
The original integer program requires , every , and every to be nonnegative integers. The simplex solution of this tableau has and . It is a real tableau solution, whether or not any of its coordinates are integers.
Choose a row whose constant is not an integer. For each coefficient let be the greatest integer at most that coefficient, and let be its fractional part. Equation (3) defines a new variable
The augmented system (2)* adds this equation to the tableau. Feasibility now also requires ; an integer solution additionally requires . For example, the one row relation admits the integer solution , and its cut value is . At the simplex point , the same cut value is .
The main target combines exclusion of the simplex solution, exact correspondence of nonnegative integer solutions, and equality of their attained objective values. Writing and for the two sets of nonnegative integer solutions, the correspondence is
Every member of has the displayed cut value for , and the projection that drops leaves unchanged. Consequently a real is the greatest attained value for (2) exactly when it is the greatest attained value for (2*). The statement does not assume either set has a maximum.
The milestones follow the paragraphs on page 277: projection of feasible solutions, the impossibility of integer solutions when the selected row has a fractional constant but only integral other coefficients, exclusion of the simplex point, the identity proving integral, and its nonnegativity on integer solutions. These are the claims the note uses to pass from the cut formula to the correspondence and the objective statement.
The result certifies that equation (3) removes the current fractional simplex point while retaining every integer candidate and its objective value. It is the local correctness condition needed before one can safely reoptimize an integer program after adding this constraint. The note's argument is a mathematical result about one tableau, independent of whether the subsequent sequence of pivots terminates.
This mission supplies a machine checkable interface for the tableau, the fractional cut, and the projection between their integer feasible sets. The theorem statements are drafted and compile with open proofs; this mission does not claim that the paper's result already has a machine checked proof here. A completed proof would make the one cut result available for later developments about iterations, optimization, or stronger cut families.
The cut value is visibly at least when the nonbasic variables are nonnegative, but that inequality alone does not give : the right side is negative for the chosen row. The key additional statement is that the real expression for is an integer on an integer tableau solution. Formalization must preserve both facts while using the same sign convention for the tableau and the cut. Merely defining the augmented solution as a pair together with its computed cut value would make the correspondence automatic and would omit the new variable's integrality and nonnegativity requirements.
Lean uses real valued tableau coefficients and real valued variables with a separate predicate for being an integer. This lets the fractional simplex point and integer feasible points inhabit the same space. The row and column sets are finite, including the cases and ; row is , column is the constant column, and Lean's Fin n index denotes the paper's . The selected row can be row in Lean. Gomory chooses a constraint row, but the local cut argument needs only the selected row's variable to be integral, and is integral in the stated problem. Every variable, including and the added , is required to be nonnegative and integral in an integer solution.
The fractional part uses the greatest integer at most a real number, including negative coefficients. The objective comparison uses greatest elements of the sets of attained values, so empty and unbounded sets receive no artificial supremum. Nonnegative constants and objective row coefficients are features of the simplex setting, but the five local claims and goal remain valid without those extra hypotheses. The paper's loose phrases “cuts off,” “one-one correspondence,” and “can be replaced” are represented by infeasibility of the augmented simplex point, a unique extension and projection preserving , and equivalence of greatest attained values, respectively.
The mission does not formalize the derivation of (2) from (1) by simplex pivots, dual simplex reoptimization, finiteness of repeated cutting, the equation bound and deletion of re-entering variables, the suggested choice of largest fractional part, or the reported E101 runs. These concern an iterative process the note does not define fully, or empirical observations. Reusable contributions include a verified fractional part identity, the integer extension theorem, and solution set correspondence for a real tableau.
Finite Markov decision models are often described by policies that choose an action from the current state. The admissible class in a total reward problem is wider: a randomized decision may use the complete history of observed states and chosen actions. For an undiscounted infinite horizon, the expected number of visits to a state may be infinite, and the total reward may be an extended real number. It matters whether a test carried out on finitely many pure stationary policies really controls this wider class. Kallenberg's Section 3.2 answers that question for finite models whose transition rows may lose probability mass when the process terminates.
The chapter is part of a 1983 account of linear programming methods for finite Markovian control. Its Theorem 3.2.4 collects earlier characterizations of transience and relates them to a finite linear program. The historical attribution in Kallenberg's Remark 3.2.2 is precise: Veinott (1969) established the equivalence of the first three conditions for nonrandomized policies, Hordijk (1976, course notes) extended the first four to general policies, and Denardo and Rothblum (1979) established the link between pure stationary transience and the LP condition. The mission targets Kallenberg's combined five-way statement, rather than treating those partial precedents as separate conclusions. Kallenberg, pp. 42–43.
Let be a finite nonempty state space of size . For every state , let be a nonempty finite set of actions. Choosing gives the transition number to state , with . The missing mass is the probability that the system terminates before another decision epoch. This is a substochastic model; replacing the inequality by equality would change the question. Kallenberg, §2.2.
A policy specifies, at each epoch , a probability distribution on after the full history . It may be randomized and may depend on all preceding states and actions. A memoryless policy depends only on the epoch and current state. A pure stationary policy chooses a single admissible action in state at every epoch. Write for the probability of state at epoch from initial state . The policy is transient when for every pair . Kallenberg, pp. 20–23.
The finite-horizon survival recursion starts from and sets for . A model is contracting if there is a strictly positive vector and a scalar for which for every admissible . These objects are determined by the transition system; rewards do not enter the five-way characterization. Kallenberg, p. 23 and pp. 41–43.
For any fixed , Theorem 3.2.4 states the equivalence of: transience of every pure stationary policy; transience of every policy; ; contraction; and existence of a finite solution of
“Finite solution” means an attained finite optimum. The are arbitrary positive right-hand sides, not a choice that the theorem is allowed to make after seeing the model. The state count is the exponent in , and the inequality is strict. Kallenberg, Theorem 3.2.4, pp. 42–43.
The milestones follow the results the chapter uses on the way to Theorem 3.2.4, in attack order:
Assumption 3.2.1 says that every policy's expected total reward exists in ; it is a hypothesis of items 2–4 only. Kallenberg, pp. 32–33, 37–42.
The theorem gives four finite or structured ways to recognize a property quantified over all policies. The survival condition uses only recursion steps, and the contraction condition supplies a weighted geometric bound on continuation. The LP links the same property to a finite-dimensional optimization problem. Each characterization can serve a different later argument without assuming the policy class has been reduced to stationary rules. Kallenberg, Theorem 3.2.4.
The five-way theorem and its supporting results are proved in the book; this mission asks for machine-checked proofs of their stated finite-model versions. The Derman–Strauch policy result is quoted by Kallenberg without proof, so its formal proof is a separate substantial contribution. None of these results has a machine-checked proof yet. The general history and occupancy definitions can be reused by later total-reward and constrained-control missions.
Checking only the finitely many pure stationary transition matrices does not directly bound the occupation counts of a history-dependent policy. Such a policy can change its action distribution after each observed path, and it need not be a mixture of stationary policies chosen once at the start. Likewise, is a finite-horizon bound, whereas transience is a statement about an infinite series of visit probabilities. The main difficulty is connecting these different quantifiers without changing the policy class. The LP condition adds a second boundary: its constraints use , and finite value includes attainment. Kallenberg, pp. 41–45.
States are Fin N with , and actions form one finite ambient type with a nonempty admissible subset at each state. Transitions are real nonnegative numbers with row sums at most one. Epoch is Lean index zero. A history records states and earlier actions; policy decision rules are normalized and supported on the current state's admissible actions. Occupancies are finite sums of transition products, so the definition of transience is summability of a nonnegative real sequence, not a bound on an individual term.
The reward layer is separate from the transition system. It uses extended real limits under Assumption 3.2.1, while the five-way goal needs no reward hypothesis. Sums of extended reals are only asserted for p-summable , where no and meet with positive coefficients; the convention is the book's. The LP objective and constraints range only over admissible state-action pairs. Its finite-solution predicate includes a feasible optimizer. Contraction allows an arbitrary componentwise positive weight and requires ; it does not normalize to the all-ones vector. The -step test uses the cardinality of the original state space.
All-policy transience means every history-dependent randomized policy. Restricting that quantifier to Markov or stationary policies would remove the central content of the theorem. Useful contributions include finite-history probability identities, the Derman–Strauch occupancy theorem, the maximal-survival recursion, the stationary total-optimality result, and the finite LP characterization. The occupancy and policy definitions are reusable beyond this mission.
Finite Markov decision models describe repeated choices whose consequences depend on the present state. They are used when a planner needs one rule that works from every starting state, yet the rule may in principle respond to the entire observed history. Linear programming offers a different description: it records how often each state and action are used, without representing the order of decisions. Kallenberg's account connects these two descriptions for a contracting total-reward model, in which the system may terminate after a transition and all policies have finite expected occupation counts (Kallenberg 1983, §§2.2 and 3.4).
The question is whether the frequency vectors attainable by general randomized policies are already attainable through the simpler stationary classes. This matters for constrained planning: restrictions on expected total resource use are linear in frequencies, while a direct search over every history-dependent policy has no comparable finite parameterization. Kallenberg's Theorem 3.4.8 makes the exact comparison, including initial distributions that assign zero probability to some states (Kallenberg 1983, pp. 72–74).
Let be a nonempty finite set of states. Each has a nonempty finite action set . Taking earns a real reward and moves to with probability . A row may sum to less than one; the missing probability is termination. A policy specifies a probability distribution over after every finite history ending in . A Markov policy uses only time and current state, a stationary policy uses only current state, and a pure stationary policy chooses a single action in each state. These are the classes , , , and of §2.2 (Kallenberg 1983, pp. 19–21).
The standing contraction assumption supplies weights and with
It is weaker in form than fixing a common discount factor: the weights may differ across states. The assumption makes every policy transient, so expected total rewards and state-action frequencies are finite (Kallenberg 1983, Assumption 3.4.1 and Theorem 3.2.4).
For an initial probability distribution , with and , write for the expected total number of visits to state at which action is chosen, averaged over the initial state. Let , , , and collect these frequency vectors for the four policy classes. The frequency polytope consists of nonnegative vectors satisfying conservation of expected flow at each state:
These equalities are those of the dual linear program (3.3.7), and the set names follow Notation 3.3.1 (Kallenberg 1983, pp. 53–55).
The first milestones identify the total-reward value vector as the smallest TMD-superharmonic vector, establish a bijection between stationary policies and feasible frequencies when every , and show that an optimal linear-programming solution yields a pure stationary policy optimal from every state (Kallenberg 1983, Theorems 3.4.1–3.4.3).
The mission goal allows zero entries in the initial distribution and compares all four policy classes:
The overbar is Kallenberg's notation for the closed convex hull, rather than topological closure alone. Since there are finitely many pure stationary policies, is finite and its convex hull is already closed (Kallenberg 1983, Definition 1.2.1(i) and Theorem 3.4.8).
The goal says that the finite LP flow constraints characterize exactly the frequencies of arbitrary history-dependent randomized policies. It also says that every such vector is a convex combination of frequencies from pure stationary policies. A resource-constrained objective that depends linearly on expected state-action use can therefore be expressed over without losing feasible frequency vectors. Kallenberg states this constrained consequence in Theorem 3.4.9; that theorem is beyond this mission's selected milestones (Kallenberg 1983, pp. 73–74).
The results are proved in the book. The remaining work here is a machine-checked development of their definitions and proofs, including the passage from arbitrary histories to finite flow equations. The history and frequency interfaces can also be reused for other finite, terminating control models. A proof of the goal would make explicit which uses of contraction and finite action sets justify the infinite sums and the closed convex hull.
For a stationary policy, the frequency equation can be written with a finite transition matrix. A general policy has a separate decision distribution after each possible history, so there is no single stationary transition matrix to substitute into that formula. A direct identification of with therefore skips the main issue. Moreover, the stationary-policy correspondence is one-to-one only when every initial weight is positive. When , different rules at never-visited states may have identical frequencies; the set equality must survive this loss of injectivity (Kallenberg 1983, Theorem 3.4.2 and Remark 3.4.3).
States and their action sets are finite and nonempty. Actions are indexed by their state, so an illegal state-action pair cannot occur. Transition rows are substochastic; rewards, values, and frequencies are real. Histories contain the past state-action pairs and current state, and time index represents the book's period . The four frequency sets range over genuinely different policy classes. In particular, the general set permits every legal history-dependent randomized policy; defining it through stationary policies would erase the goal's content.
The initial distribution in the goal may have zero coordinates. The strictly positive weights in the bijection and LP-optimality milestones are the different convention of §3.3. Frequencies and rewards use infinite sums; contraction supplies their convergence. The value vector is a coordinatewise supremum over legal policies, bounded under contraction. The LP uses equalities, not relaxed inequalities, and the pure-policy set is convexified only in the goal's first equality. Needed infrastructure includes finite history probabilities, stationary transition matrices, inverse stationary flows, superharmonic vectors, and finite-dimensional convex geometry. Contributions that establish these interfaces and the three stated milestones are in scope.
Iterative methods for a system of linear inequalities stop at a vector that only almost satisfies the system: the violation is small but not zero. A user then needs to know that is close to an actual solution. Hoffman's 1952 paper (J. Res. Nat. Bur. Standards 49) gives the first quantitative form of this fact: the distance from to the solution set is at most a fixed multiple of the violation. The paper itself names one application: in Brown's method for solving games, the computed strategy vector approaches the set of optimal strategy vectors.
The result is now known as Hoffman's error bound and the constant as the Hoffman constant. It is a standard tool in convergence analysis, sensitivity analysis of linear programs, and the theory of error bounds.
Timeline.
Let be a real matrix with rows and let . The system (1) is for , briefly ; its solution set is , and the system is consistent if . The th half space is .
For a real number , if and otherwise; for a vector, is taken coordinatewise. So records by how much violates each inequality.
Hoffman measures sizes with a positive homogeneous function on : a continuous real function with (i) and only for , and (ii) for . Norms are examples, but need not be symmetric, subadditive or convex.
For a set of rows, is the matrix obtained from by replacing the rows outside by , and keeps the coordinates of in and zeroes the others. "Nearest" always refers to Euclidean distance. The set consists of the points outside the cone whose nearest point in that cone is the origin; is the cone spanned by the rows of with the origin removed.
Section 3 uses three norms: (largest absolute coordinate), (sum of absolute coordinates) and the Euclidean norm. With , is the largest absolute coordinate of a row in , and over probability vectors on , the value of the matrix game .
If is consistent and , are positive homogeneous, there is such that for every some solution satisfies
The constant is existential and fixed before ; no value is asserted. This is the weakest statement that carries the content and survives any later improvement of the constant.
Each is stated as in the theorem: for every there is a solution with the bound.
The result. The theorem converts a residual estimate into a distance estimate. Any scheme that drives to zero brings its iterates to the solution set at a linear rate in the residual. Linear convergence proofs for projection and first-order methods on polyhedral problems and stability results for LP solution sets build on it. Formulas (8)–(10) show that in the max and sum norms the constant can be read off the rows of through a matrix game.
Formalizing it. The theorem has been proved since 1952, and later papers give several alternative proofs. The mission formalizes Hoffman's own proof route, Lemmas 1–4, in Lean and Mathlib, and the explicit constants (8)–(10). Mathlib has Farkas-type results and projections onto closed convex sets in inner product spaces, but no error bound for linear inequality systems, and the Prove2Me library has no statement of Hoffman's theorem.
For a single , a bound is trivial: take the nearest solution and choose accordingly. The whole content is that one works for all , including far from and approaching along every direction. A compactness argument on alone fails, because the ratio is not a continuous function of on a compact set: the nearest solution and the set of active constraints jump as moves. Lemma 3 needs a positive lower bound on a set that is not obviously closed away from the origin; its closedness comes from Lemma 4, i.e. from Farkas' lemma. Since , are not norms, no argument using the triangle inequality or symmetry is available. For (8), a set can arise in Lemma 2 with (e.g. , in with ), contrary to an unnumbered remark on p. 265; the bound (8) is still true, but that remark cannot be used.
Fin k → ℝ, is Matrix (Fin m) (Fin n) ℝ, the system is A *ᵥ x ≤ b (componentwise), and is posPartVec y = fun i => max (y i) 0.IsPosHomogeneous (continuity, nonnegativity, vanishing exactly at , positive homogeneity); they are never specialised to norms in the goal or Lemmas 1, 3.dist on Fin n → ℝ is the sup distance and is not used.) Lemmas 2 and 3 take "a nearest point" as hypothesis; since the Euclidean nearest point of a closed convex set is unique, this is the page's "the nearest point".Finset (Fin m) of row indices; keeps all rows, with zero rows outside .⨆ i, |x i| and is ∑ i, |x i|; minima and maxima over finite index sets are ⨅/⨆ in ℝ, equal to the attained min/max on nonempty sets. is defined directly by (7) as a min over the simplex of a max, for nonempty , so no minimax theorem is needed. In (8), is the maximum over nonempty with and is when there is none (only when ). In , the page's summation range "" is read as ranging over the rows, since is indexed by rows.The quantifier order is part of the statement: a version with chosen after is trivially true and is not this theorem; likewise precedes and in Lemma 1 and precedes in Lemma 3.
Infrastructure a complete development needs: existence and the variational characterisation of the Euclidean projection onto a polyhedron in Fin n → ℝ; Farkas' lemma in cone form (published as LinearOptimization.farkas_cone_corollary); compactness of level sets of positive homogeneous functions. The projection and polyhedral-cone lemmas are reusable well beyond this mission. Proofs of any milestone, alternative proofs of the goal, and sharper or equivalent forms of the constants are welcome.
The restricted shortest path problem asks for a shortest route between two points of a network subject to a budget on a second additive quantity, such as travel time, cost or risk. It appears as the pricing subproblem of column generation for crew scheduling and vehicle routing, in quality-of-service routing in communication networks, and in scheduling, where Hassin's own §7 uses it for a single-machine problem. The problem is NP-hard (Garey and Johnson, 1979), so exact polynomial algorithms are not expected, and the natural question is how well it can be approximated in polynomial time.
Timeline.
Hassin's combination of an approximate decision test with a geometric search on the bounds is the pattern later schemes for resource-constrained path problems refine, which is why his first scheme is the subject of this mission.
A directed graph has vertex set , , and edge set . Following the paper, the vertices are numbered so that every edge has ; in particular the graph is acyclic. Each edge carries a positive integer length and a positive integer transition time . A path has length and transition time . For a nonnegative integer , a -path is a path from to with , and is the length of a shortest -path.
Fix . For a real , the rounded lengths are
Procedure TEST(V) deletes the edges with and answers NO if, for some integer , some – path in the remaining graph has transition time at most and rounded length at most ; otherwise it answers YES.
The Rounding Algorithm keeps bounds on OPT. Starting from initial bounds , Step 1 repeats while : with it sets if TEST(V) = YES and if TEST(V) = NO. Step 2 outputs a -path that is shortest for the rounded lengths . The bounds after passes are written .
If is a lower bound on the length of every -path, is a stage at which , and is a Step 2 output at , then
that is, . The initial upper bound is arbitrary.
The guarantee makes the Rounding Algorithm a fully polynomial approximation scheme: combined with the paper's running-time analysis, a -approximate -path is computed in time polynomial in the input size and . The two ingredients, an approximate decision test that answers "OPT " or "OPT ", and a geometric search on the ratio , are reused in later FPASs for constrained path, knapsack-type and scheduling problems; the milestones isolate them as separate statements.
The result has been proved since 1992 but, as far as a search of the platform and of Mathlib shows, none of it is machine-checked. This mission produces a checked version of the first scheme, stated for every stage at which the printed stopping test holds and every optimal Step 2 output. It also records, as a companion, that the printed Step 1 need not terminate when , and proves termination under .
The arithmetic of each step is short; the difficulty is in the combinatorial facts the page uses without proof and in the bookkeeping of a run. The rounding error of a path is at most only because a – path has at most edges, which follows from the numbering and must be derived for list-encoded paths. The YES case must cover -paths through edges that TEST deleted, which the rounding argument does not see. The bound update needs both bounds to stay positive so that is a meaningful test point, an invariant of the whole run rather than of one step. A tempting shortcut, assuming that LB is a lower bound on OPT at the stopping stage, would assume milestone 4; the goal assumes it only for .
The proximal point algorithm is a way to find a zero of a set-valued monotone operator by repeatedly solving a regularized version of that operator equation. Its classical regularizer is quadratic, so the distance from one iterate to the next is Euclidean. In convex optimization, that geometry can be poorly matched to the domain: the natural iterates may be constrained to a positive orthant, a simplex, or an open set with a meaningful boundary. Eckstein's 1993 paper studies what happens when a Bregman function supplies the regularization instead. The convergence question matters because the later multiplier methods in the same paper are instances of this general iteration. Eckstein (1993) develops the general result before applying it to convex programs.
The result considered here is Theorem 1 of that paper. It concerns an existing infinite run: it states what such a run does, while Theorems 4 and 5 address conditions under which a run can be generated. This separation keeps the convergence assertion precise. The result is known mathematically; the mission asks for a Lean proof of its stated generality, including its alternative when the operator has no zero.
Work in a finite-dimensional real inner-product space , representing the paper's . A monotone operator associates a set of vectors with each point. It is monotone when for every and , and maximal monotone when its graph has no proper monotone extension. Its domain is ; a zero is a point with .
Let be open and a real function on . At , define the Bregman distance
It need not be symmetric and is generally not a metric. Definition 1 requires to be continuously differentiable on , strictly convex and continuous on , and to satisfy boundedness of both kinds of partial sublevel sets. Two sequential conditions connect convergence in to convergence of Bregman distances, including sequences approaching the boundary of . These six requirements together define a Bregman function with zone .
A Bregman proximal-point run uses positive parameters and a sequence satisfying
This is the inclusion form (4) of the paper's recursion (3). It permits set-valued and does not assert that a next iterate exists for arbitrary starting data. The model also uses the paper's standing domain condition .
The main target is Theorem 1. Assume that the positive parameters have a common positive lower bound and that one of the following conditions holds: (C1) , or (C2) for a proper lower semicontinuous convex extended-valued function . Then
The second line retains the paper's extra (C1) requirement. The standing inclusion has a different direction and role. The milestone list follows Lemma 1 and the three labelled steps of Theorem 1's convergence proof: the resolvent inequality, boundedness of the run when a zero exists, identification of every limit point as a zero, and convergence of the full run. The no-zero alternative remains in the goal because restating that conjunct as a separate milestone would add no independent target.
Theorem 1 says that the nonlinear iteration cannot remain bounded without approaching a zero under (C1), and that when a zero exists the whole sequence converges under either (C1) or (C2). This is stronger than saying only that accumulation points solve the operator equation. It supplies a common convergence result for the paper's later proximal minimization and multiplier algorithms, where the operator is often a subdifferential and the geometry comes from a nonquadratic . Eckstein (1993) gives those applications after the general theorem.
A formalization would add a reusable interface for Bregman functions with open zones, including their boundary behavior, and for proximal-point runs of set-valued maximal monotone operators. The published platform definitions of monotone operators and extended-valued convex analysis are reused. The new proof work is the Bregman resolvent estimate and the convergence alternative at Theorem 1's level of generality. No machine-checked proof of this specific theorem is claimed here.
The usual Euclidean proximal-point theorem does not apply directly after changing coordinates by : the transformed operator need not remain monotone, as the paper observes after Theorem 1. A proof must account for the nonsymmetric , the possible boundary of , and two distinct ways to identify a limit point as a zero. Under (C1), the point lies where the gradient is continuous; under (C2), the argument uses the subdifferential structure instead. The no-zero case has its own difficulty because boundedness would have to contradict maximal monotonicity without first assuming that a zero exists. The proof cites a closed-graph result for maximal monotone operators and a zero-existence fact for operators with bounded domain; those external facts are groundwork for solvers, not invented milestones.
Lean uses a finite-dimensional real inner-product space rather than a coordinate-fixed . The total function is constrained only on ; its gradient is evaluated only on the open zone . The Bregman distance is used on . Definition 1's condition (vi) explicitly places its first sequence in , the natural domain stated immediately after the definition. The run explicitly keeps every in and encodes recursion (3) using the equivalent inclusion (4). A positive lower bound on is expressed by one with for every .
The operator is a published set-valued operator object, with its published notions of monotonicity, maximality, domain, and zeros. The proper and convex extended-valued function in (C2) uses the published epigraph and subgradient definitions, with EReal able to express . Subdifferentials are built from those definitions. A limit point means a limit along a strictly increasing subsequence, and unboundedness means that the full set of iterates is not bounded. The proof step on p. 207 prints ; the formal Step 1 uses the standing condition , which is sufficient for the Bregman distance and also covers (C2).
The run relation cannot be satisfied by an arbitrary constant sequence: its inclusion must hold at every step, and a zero-free operator under (C1) triggers the unbounded conclusion. Nor does the theorem replace convergence by existence of one convergent subsequence. Reusable contributions include properties of the Bregman resolvent and maximal-monotone graph limits. Theorem 5's separate existence and minimization claims are outside this mission's core.
Every manufacturer who makes a part in batches faces the trade-off Ford W. Harris described in 1913: large lots spread the fixed set-up cost of an order over many pieces, but they also tie up money in stock that must be carried. Harris's article "How many parts to make at once" (Factory, The Magazine of Management 10(2), 1913, reprinted in Operations Research 38(6), 1990) resolved the trade-off with a closed formula, the square-root or economic order quantity (EOQ) formula. It is the starting point of deterministic inventory theory and is still taught as the first model of every operations-management course.
Timeline. Harris published the formula in 1913, without proof ("the solution of this problem involves higher mathematics"). The same formula was popularised by R. H. Wilson in 1934 and was for decades attributed to him. D. Erlenkotter traced it back to Harris (Operations Research 38(6), 1990, 937–946), and the article was reprinted in the same issue. Later work built stochastic (Q, r) models on top of it; Zheng (1992) compared the EOQ heuristic with the optimal (Q, r) policy.
A part is used at a regular rate of units per month (the movement). Each unit costs dollars (the unit cost), and each order costs dollars to set up. Parts are made in lots of units, the lot size. Under regular movement a lot of is delivered when the stock reaches nothing and is then used up at rate , so the stock at time (months, from a delivery) is the sawtooth
with the fractional part. Interest and depreciation on stock are charged at ten per cent a year, a rate the paper fixes.
Harris prices a unit in three parts:
The cost per unit is therefore
and the economic lot size is . In Lean these are stockLevel, interestPerPiece, costPerUnit and econLotSize in the namespace HarrisEOQ.Lot.
For ,
This is Harris's claim that the value of giving the minimum value to "reduces to the square root of (240MS divided by C)": is admissible, attains the minimum, and is the only lot size that does.
These justify the objective , not its minimization; the paper gives no argument for the minimization.
The result. The square-root formula gives the cost-minimising batch size in closed form from three observable numbers. Its consequences are the ones Harris draws: lot sizes grow only with the square root of demand (so consumption must quadruple to double a lot), the cost curve is flat near the optimum and asymmetric (erring small is worse than erring large), and at the optimum the set-up cost balances the variable carrying cost. Every later deterministic and stochastic lot-sizing model reduces to this one in its simplest case.
Formalizing it. The result is classical and proved in textbooks, but Harris's paper itself contains no proof. A formalization supplies the missing argument for the paper's exact objective, which differs from the textbook EOQ by charging interest on the set-up cost ( in the stock value) and by the fixed ten per cent rate. It also makes the paper's modelling step precise: the claim that the average stock is becomes a statement about a time average of a sawtooth function. To our knowledge none of these statements has a machine-checked proof on the platform; the EOQ items of Zheng (1992) concern a different model, with backorders.
The minimization is elementary calculus; the substance of the mission is fidelity. The objective must be the display as printed, with meaning , and the claim includes uniqueness, not only that is a minimizer. The average-stock milestone needs a genuine long-run average of a discontinuous periodic function over with not a whole number of cycles, which is where the integration and limit bookkeeping lies.
All quantities are real numbers; lot sizes are not restricted to integers (the paper's own optimum is 48.5). The hypotheses are not written on the page; they are implicit in the meaning of a usage rate, a price and a cost, and are added. Every quantifier over lot sizes is over . Time is measured in months, and the interest rate is fixed at ten per cent, so the constant appears as printed; the formula is not generalized to an arbitrary rate.
A trivializing formalization is ruled out: is defined as the printed display, not rewritten around ; the average stock is an integral of the stock level, never defined as ; and the goal does not quantify over all real , where Lean's convention would make a spurious minimizer.
The manufacturing interval and the safe stock minimum play no role in the formula and are not modelled. The examples' cost figures (0.188 cents, $0.00028, and so on) are not formalized. The development needs only Mathlib's real numbers, square roots, fractional parts, interval integrals and limits; contributions of proofs of any item are welcome.
Scheduling work on several identical processors creates a plausible expectation: completing tasks sooner, removing constraints, or adding a processor should not delay the overall finish. A fixed priority-list rule defeats that expectation. When a task becomes ready earlier, it can occupy a processor that would otherwise have run another task; that decision changes later availability. Graham gives explicit schedules in which changing only the list raises the finishing time from 12 to 14, removing two precedence constraints raises it to 16, shortening every task raises it to 13, or adding one processor raises it to 15. These examples establish that the effect is a property of the scheduling rule, rather than of a change in the total set of tasks. See Graham, §2, pp. 417–419.
This mission concerns the upper limit of that effect. An operations researcher comparing a list schedule before and after a change in available processors or task data needs a bound that survives all four changes at once. The result is also a compact benchmark for formalizing algorithms whose behavior depends on changing availability: the model must describe when tasks become ready, when processors are idle, and which ready task a processor takes next. Graham's Theorem 1, proved in the 1969 paper, supplies the bound.
There are tasks and identical processors. Each task has a positive processing time . A strict precedence order specifies tasks that must be completed first: means cannot start before ends. A priority list orders all tasks once each. It may place a successor before a predecessor, because the processor skips any task that is not ready. These conventions are those of Graham's system in §2, p. 416.
A schedule gives each task a processor and a start time . Once started, the task occupies that processor continuously on . Two tasks on one processor cannot overlap, while tasks may meet at an endpoint. Precedence means whenever . The finishing time is the largest completion time . The paper's list rule starts the first currently ready task in whenever a processor can take a task. A ready task that has not started cannot coexist with an idle processor. If one task starts while another ready task waits, the started task is earlier in .
The same task set is run a second time, with processing times , order , list , processor count , and finishing time . The data satisfy for every and . Thus the second run may have shorter tasks and fewer precedence relations; both lists may differ arbitrarily. Both runs obey the same list-scheduling rule Graham, §3, p. 419.
For , positive processing times in both runs, and the two list schedules just described, the target is Graham's Theorem 1:
The numerator and denominator refer to the actual runs, with potentially different lists and processor counts. The conclusion does not require the new schedule to finish earlier. Its factor permits the anomalies shown in §2 while preventing an arbitrarily large increase for fixed . The supporting targets follow the proof's numbered displays: a precedence chain covering idle times in the second run (1), an idle-time estimate for that chain (2), a comparison of its length with the first run (3)–(4), and the work-volume bound used in (5) Graham, pp. 419–420.
The theorem places a quantitative limit on the damage caused by a list rule after simultaneous changes in task durations, precedence, ordering, and capacity. When , the factor is ; when the first run has one processor, it is . The statement applies to every finite task set and every pair of lists, so it can be reused when a scheduling method produces a list without additional structural guarantees. Graham states that the bound is best possible, citing earlier examples; this mission formalizes the inequality in this paper and does not claim to formalize those external examples Graham, p. 420.
The result is proved in the source paper. The work here is to give its objects precise Lean definitions and to supply machine-checked proofs of the bound and its supporting claims. A formal development needs to account for continuous real start times, processor assignments, half-open execution intervals, and the behavior of the list rule when several tasks or processors become available together. The resulting model of a nonpreemptive list schedule and the basic volume and chain estimates can serve later formalizations of parallel scheduling. The present proposal contains statements and definitions; its theorem bodies are open proof obligations.
Total work alone does not control the anomaly: processors can be idle while precedence keeps available work from starting, and changing precedence can alter which tasks occupy the processors later. A direct comparison of corresponding task completion times between the two runs also fails in Graham's §2 examples. The central difficulty is expressing the second run's idle periods through work on a single precedence chain and then relating that chain to the first run's finishing time. In Lean, the chain and the time intervals must be represented without silently changing endpoint conventions or treating a ready but unstarted task as running.
Tasks are Fin r and processors are Fin n, with zero-based Lean indices corresponding to Graham's one-based subscripts. Processing times and start times are real. A priority list is a bijection between positions and tasks, so it contains every task exactly once and need not respect precedence. The order is strict. Feasible schedules are nonpreemptive and use half-open running intervals. The finishing time is a finite maximum of completion times; for no tasks it is defined as zero, while the ratio theorem assumes so its denominator is positive. Both processor counts are positive. The strict positivity of both time functions is inherited from the paper's convention.
The model captures Graham's rule by no unforced idleness and list priority. It does not encode the smaller-index tie rule for identical processors, since the tie affects only processor labels and not start times or . The covering-chain milestone represents Graham's set as times before when not all processors are busy; all-idle times before the finish cannot occur under the list rule. The idle-time milestone writes the total duration of empty tasks as using display (5). Natural-number subtraction is not used in the constants: and are real differences. The companion existence statement and a concrete two-task sanity check rule out a vacuous list-schedule predicate. Contributions can address that existence theorem, the chain construction, interval accounting, the volume bound, and the final ratio.
Parallel processing poses a basic allocation question: given tasks of known lengths and several identical processors, how much time is lost when tasks are assigned by a simple list rule instead of an optimal allocation? The finishing time is the moment the last processor completes its work. For independent tasks, a list rule starts each next task on a processor that becomes free first. Such a rule is easy to execute, but the resulting allocation can be worse than the best partition of tasks among processors. Graham's 1969 paper studies precise worst-case ratios for this model. Its Theorem 3 asks what guarantee follows when the first tasks of the list are chosen among the longest and scheduled optimally before the remaining tasks are appended.
The paper also notes two endpoints of this family. With , the rule is ordinary list scheduling and has ratio at most . With , the longest tasks can start one per processor, giving ratio at most . Theorem 3 expresses these as instances of one bound, including the integer jump at each multiple of Graham, pp. 427–428.
There are independent tasks, indexed by , and identical processors, indexed by . Task takes a strictly positive time . A priority list contains every task exactly once. Its first tasks are of the longest tasks; equal lengths may be ordered either way. As a processor becomes available, it takes the next task in the list. Once started, a task runs without interruption. With no precedence constraints, every unstarted task is ready, so a processor runs its assigned tasks consecutively from time zero.
An assignment records the processor that executes each task. The load of processor is the sum of its assigned task lengths. The finishing time is the largest load, . For a list assignment, each task is assigned to a processor whose load from earlier list tasks is smallest at that step. If two processors are tied, either can be selected without changing the finishing time. For any assignment , let be the largest load contributed by only the first list tasks. The algorithm requires its own first assignments to minimize over all assignments ; the remaining tasks may occur in any list order.
Write for the smallest finishing time achievable for all tasks. The paper introduces it as the minimum over possible lists and later describes the same problem as minimizing the largest part sum over partitions of the task lengths Graham, pp. 421, 428. The formalization uses the partition or assignment form of .
For , when the first longest tasks have an optimal prefix schedule, Graham's bound is
Here is the greatest integer at most . The theorem also says the bound is best possible when is divisible by Graham, Theorem 3, p. 427. The equality examples are a separate companion statement in this mission.
The milestones state the finite-volume lower bound on , the case in which completing all tasks takes no longer than completing the first , and the paper's numbered inequalities (14), (15), and (16). They use for the greatest task length after the first positions. These are individual mathematical claims from the proof on p. 427, with their original wording and formulas recorded alongside the formal statements.
The theorem gives a quantitative tradeoff between work spent optimizing a prefix and the worst-case finishing time of the full list. Its denominator is , so the guarantee improves when the optimized prefix contains another full processor's worth of long tasks. The example at multiples of shows that the stated coefficient cannot be uniformly reduced for the algorithm as specified Graham, p. 427.
The result is proved in the paper. This mission's remaining work is a machine-checked proof of its exact statement and the source's intermediate inequalities. The published identical-machine makespan definition is reused, while the list-assignment rule, optimal prefix, and longest-remaining-task quantity are made explicit here. Those definitions can also support later work on list scheduling without precedence constraints. No machine-checked proof of Theorem 3 is claimed by this proposal.
An optimal schedule for the first long tasks does not make the entire list optimal: short tasks appended later can affect which processor finishes last. A bound based only on average total work ignores this final imbalance; a bound based only on the largest remaining task ignores how many long tasks every assignment must place together. The proof must relate both constraints to one finishing time while preserving the floor . Replacing that floor with the real quotient changes the claim, and allowing an arbitrary prefix arrangement loses the algorithm's required optimality.
Tasks and processors are finite indexed sets Fin r and Fin n; their zero-based indices correspond to the paper's one-based and . Task lengths are positive real numbers, and both and are positive. The list is a permutation, not merely a sequence that might omit or repeat a task. The condition is explicit because choosing tasks from requires it; the paper treats inside the proof and the case is covered by the theorem. There is no precedence relation in this mission.
The list rule is a predicate on assignments: each next task goes to a processor with least current load. It omits the paper's smaller-index tie convention, since tied identical processors can be interchanged without changing the finishing time. The first positions must contain longest tasks, and their assignment must minimize the prefix finishing time among all assignments of those tasks. Those conditions are part of the goal; the inequalities (14)–(16) are conclusions to establish, not assumptions of the goal. A separate existence statement and a checked concrete instance ensure the list predicate is satisfiable.
All maxima and minima range over finite nonempty processor or assignment sets. The optimum is a minimum over assignments, equivalent to the paper's minimum over lists in the independent-task model. The quantity is the largest duration outside the prefix when , and is defined as zero when none remains; statements using it require . Division is by and by . Lean's natural-number quotient represents ; real subtraction is used for coefficients such as . Contributions toward the finite load identities, the optimum-over-lists equivalence, and proofs of the listed bounds are within scope.
On one processor, the completion time of a job normally depends on how much work precedes it. In the model of Browne and Yechiali (1990), waiting also changes the job's own processing requirement: a job that starts later takes longer. The sequence therefore changes both when each job starts and how long subsequent jobs must wait. This matters when the goal is a weighted completion cost, because a delay to one job can raise the completion costs of many others.
The paper gives an expected-makespan ordering for this linear deterioration model and, in Proposition 2, a sufficient condition under which the original job order minimizes weighted expected completion cost. The latter is the target of this mission. Related platform work on Delayed SWPT and the AvgCompletionSched family treats weighted completion scheduling without this job-specific linear deterioration. Their additive processing-time models do not supply the completion-time object used here.
There are jobs, all available at time zero, processed one at a time on a single machine without idle time or preemption. A schedule is a permutation of the jobs: is the job processed in position . The paper labels positions and jobs from to ; the Lean development labels them from to . The identity schedule processes jobs in label order.
For job , is its random initial processing requirement, its deterministic growth rate, and its waiting cost rate. If the job starts at time , its actual processing time is . Deterioration stops once processing starts. Write for the time at which the first scheduled jobs have all finished. The model sets and
in the paper's one-based position notation. Thus the completion time of the job in position is . Its cost is its own rate times that completion time, giving
All of these are random quantities until an expectation is taken. Equation (2) of the paper writes as a sum of the initial requirements multiplied by the later growth factors. Equation (8) substitutes that expression into . Both equations are included as milestones, stated along an arbitrary schedule by relabelling the jobs. The third milestone is the exact change in from swapping two adjacent jobs. These three statements are pathwise identities, so their mathematical content does not depend on a probability distribution.
The principal target is Proposition 2: if both sequences of job-indexed ratios are strictly increasing,
then, for every permutation ,
The first ratio compares an initial expected requirement with its growth rate. The second couples growth and the cost rate. The conclusion is global optimality over the paper's whole class of nonpreemptive, non-idling permutations. It does not assert that the identity order is the unique minimizer; strict input ratios do not by themselves justify a uniqueness claim.
The attack path records exactly the supporting statements printed in the paper: the closed completion-time formula (2), the weighted cost formula (8), and the unnumbered adjacent-interchange identity after (8). The milestone quotations preserve the paper's printed display, while the Lean statements use an arbitrary permutation where relabelling permits it. The interchange display has a multiplication dot before its second bracket; expansion for two jobs shows that the term is added. The formal statement records that correction, and the source quotation retains the printed symbol.
The proposition identifies a directly checkable pair of ordering conditions under which the natural job-label order solves a weighted stochastic scheduling problem. A condition involving only , enough for the paper's expected-makespan target, does not determine this weighted objective. The cost rates introduce another ordering requirement. The result gives a sufficient rule, not a characterization of every optimal schedule or of every parameter choice.
The mathematical result was published in 1990; this mission asks for its machine-checked formalization. A complete development will connect the processing-time recursion, the pathwise cost identities, and the expected optimality statement in Lean. The recursion and cost definitions can be reused for other finite single-machine problems in which a job's processing time depends on its start time. The milestone identities are also useful independently of the final sufficient condition, including for studying other choices of weights and ordering indices.
Sorting by expected initial requirement alone cannot settle the problem, because processing a job changes later start times and hence later processing times. Even sorting by the expected-makespan index leaves the cost rates unaccounted for. The value of an adjacent swap depends on the elapsed time before the pair and on the completion costs of jobs after the pair. It is not enough to compare the two jobs' own completion costs in isolation.
The source states the sufficient condition after its interchange display but does not present a full proof of the global claim. Closing the Lean goal requires connecting local comparisons to every schedule and handling the expected value of the recursively defined cost. The identities are finite, but their indices change between zero-based Lean positions and the paper's one-based display, especially at the first position and at an empty suffix.
Jobs are , and a policy is an equivalence permutation with equal to the job in position . Completion time is defined by the processing rule , not by the closed form (2). At positions beyond the jobs it stays constant, and theorems about the closed form restrict to . The total cost is defined from job-weighted completion times, not from equation (8). This keeps both identities substantive.
The proposition uses a probability space and the Bochner integral of the real-valued cost. Every is integrable, so its expectation and the finite linear combinations appearing in the cost are meaningful. Initial requirements are nonnegative at every outcome, reflecting the paper's standing positive-processing convention; strict positivity is unnecessary for the claim. Growth rates and cost rates are strictly positive. Those two assumptions make the printed ratios well-defined and support the ordering rule. The paper's common independence convention is not required for these expectations and is not assumed.
The two strict orderings are over the labels of jobs in , not positions of an arbitrary schedule. The conclusion compares with every permutation, not only with schedules obtained by one adjacent swap. The and cases are allowed: the order conditions have no pair to compare, and there is only one permutation. Solvers may contribute the finite-sum, interchange, and integrability facts needed to link the milestones to Proposition 2. The pathwise identities require no probability assumptions and can support later variants.
Fitting a statistical model usually means solving a convex problem of the form
where holds one training example per row and one feature per column, is the response, is a convex loss and a convex regularizer. Least squares, the lasso, logistic regression and the support vector machine are all of this form. When either dimension is very large, or the data are stored on many machines, the problem has to be solved by processors that each see only a block of .
Chapter 8 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) shows how ADMM does this in two ways: by splitting by rows (splitting across examples, §8.2), which turns the problem into a global consensus problem, and by splitting it by columns (splitting across features, §8.3), which turns it into a sharing problem. In both cases the method is only practical because the individual updates have closed forms or reduce to small standard problems. This mission formalizes those closed forms, culminating in the update for the group lasso.
Vectors are in with the Euclidean norm ; . Throughout, is the ADMM penalty parameter and a regularization weight.
Splitting across examples. Partition and by rows into blocks , . With scaled dual variables and averages , , the consensus ADMM iteration is
followed by . For the lasso, and .
Splitting across features. Partition with and with , so . Introducing gives a sharing problem; its ADMM -update minimizes . Writing and for the average of the , this reduces to a single problem in , all dual variables coincide, and each block update minimizes
for a vector assembled from the previous iterate. For the group lasso, (not squared).
Soft thresholding is for , for , for .
Let on and . Then
and then is the only minimizer; if , there is exactly one with , the point minimizes , and every minimizer is of this form.
The goal result says that a group-lasso block either switches off entirely, which is how group sparsity arises, or solves a ridge regression whose ridge parameter is the unique root of a scalar monotone equation; this is what makes the distributed group lasso implementable with one cached factorization per block and a bisection. The milestones are the remaining closed forms that turn the two distributed schemes of Chapter 8 into concrete algorithms, and the reduction of milestone 3 is the structural fact that lets feature splitting carry a single dual variable.
The book derives these facts in running text and states them without proof. None of them is formalized on Prove2Me, and the book's printed zero test for the lasso (p. 69) uses the wrong norm; a machine-checked collection of the correct updates removes that kind of error from the record and gives later ADMM missions a verified library of update formulas.
Each statement is a characterization of all minimizers of a nonsmooth convex function, not a check that a formula satisfies a stationarity equation. For the goal, the nonsmooth term has a kink at , need not be strictly convex when has a nontrivial kernel, and the existence and uniqueness of the parameter is part of the claim rather than an assumption: the obvious move of assuming a suitable and checking the formula proves nothing about the case split or about uniqueness, and the singular case of is exactly where naive arguments break. Milestone 3 must handle an arbitrary convex loss , with no closed form at all.
Vectors are EuclideanSpace ℝ (Fin n); matrices are Matrix (Fin m) (Fin n) ℝ acting through Matrix.toEuclideanLin; blocks are indexed by Fin N (0-based); the regularization weight is lam; the eigenvalue vector the book also calls (p. 70) is μ. " minimizes " is Mathlib's IsMinOn F Set.univ x. Iteration superscripts are dropped: each statement is about one update with the previous iterate given. Explicit choices:
A statement that only checks that satisfies the optimality equation, or that assumes the parameter exists, does not capture the goal; the goal asserts existence and uniqueness of and describes every minimizer of .
Contributions welcome: subgradient calculus for and in EuclideanSpace, first-order optimality for convex quadratics plus a convex nonsmooth term, and the monotonicity of for positive semidefinite ; these are reusable for every proximal and ADMM update.
Minimizing a smooth function over a closed convex set is the basic problem of constrained continuous optimization. When the constraint set is simple enough that the nearest point of the set to any given point can be computed (a ball, a box, an orthant, an affine subspace), the most direct method is the gradient projection method: take a gradient step and project back onto the set. The method is the ancestor of the projected gradient and proximal gradient algorithms used today in signal processing, machine learning, and optimal control, where the variable is often a function, so that the natural setting is an infinite-dimensional Hilbert space rather than .
A. A. Goldstein's 1964 note in the Bulletin of the AMS (Goldstein 1964) is one of the two founding papers of the method, alongside the independent work of Levitin and Polyak (1966). It states, in a Hilbert space and with an explicit step-size window, that the iterates stay in the initial level set, that the objective values converge, and that under convexity they converge to the optimal value, with weak and strong convergence of the iterates under further hypotheses. Goldstein motivates the method by applications to control theory (Balakrishnan 1963; Goldstein, Minimizing functionals on Hilbert space, 1964).
Timeline.
Let be a real Hilbert space with inner product and norm . Let be closed and convex, and let be the projection onto : is the point of closest to . In Lean, IsProjection C P says that and for all .
Let , , and let
be the level set (levelSet f C x0). Let be an open set containing the convex hull of . Write for the Fréchet derivative of at applied to , for the gradient (so ), and
for the directional second derivative in the sense of Gâteaux (d2 f x h). The curvature hypothesis is that for some , at every and for every , these derivatives exist and
Choose and step sizes . The method is
A point is stationary if for every .
Assume is bounded below and continuous on . There is such that
The goal is the whole theorem, because its five parts share one limit and one standing setting.
The projection inequality for ; the Lipschitz property of ; the characterization of stationarity for convex at a differentiability point; the one-step Taylor estimate; the step lemma (for the new point stays in and the decrease is at least ); parts (i) and (ii); the strong-convexity bound on ; the supporting-hyperplane inequality of the proof of (iii); parts (iii), (iv) and (v). A companion item states the last clause of (ii) under convexity of on .
The result. The theorem gives a step-size rule that needs only a curvature bound near the level set, not a global Lipschitz constant of the gradient, and it covers the infinite-dimensional case directly: (iii) gives convergence of the objective values to the optimal value without assuming that a minimizer exists, (iv) yields minimizers as weak cluster points when the level set is bounded, and (v) gives strong convergence of the iterates under strong convexity on the level set. These are the prototypes of the convergence statements now proved for projected and proximal gradient methods.
Formalizing it. The result is classical and proved on paper; it has no machine-checked proof. The note is two pages long and its proof is terse ("The proof of (ii) being straightforward"), and checking it in Lean exposes two places where the printed statement needs repair (see Formalization scope). A complete development also produces reusable infrastructure: the variational inequality and Lipschitz property of the metric projection in a Hilbert space, a one-dimensional Taylor estimate from a Gâteaux second derivative along a segment, and weak lower semicontinuity of convex continuous functions on closed convex sets used through cluster points in WeakSpace.
The obvious argument for (i) applies a quadratic upper bound for along the segment from to . That bound is only available where the curvature hypothesis holds, on , and nothing guarantees in advance that , or the segment, lies in . Ruling this out requires control of up to the boundary of the level set, which the printed hypotheses do not give; this is where the added continuity hypothesis enters. In (iii) the iterates may be unbounded and no minimizer need exist, so compactness arguments are unavailable. In (iv) the cluster points are weak, so norm-closedness arguments do not apply directly.
[NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. The inner product is ⟪x, y⟫_ℝ, and is Mathlib's gradient f.IsProjection C P; there is no chosen projection and no junk value.SecondDerivBound) states both differentiabilities before the bound, so the bound is never on a junk zero.IsGLB (f '' C) L. Weak cluster points are cluster points in WeakSpace ℝ H.Contributions welcome: proofs of any milestone, in particular the projection inequality and Lipschitz property (independent of the rest), the Taylor estimate from the Gâteaux second derivative, and the weak-closedness argument of (iv).
Many estimation problems in statistics, machine learning and signal processing minimize a smooth loss plus a nonsmooth ℓ1-type regularizer: the lasso, basis pursuit, least absolute deviations, Huber fitting, the group lasso, and ℓ1-penalized maximum likelihood for Gaussian graphical models. Chapter 6 of Boyd, Parikh, Chu, Peleato and Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers (Found. Trends Mach. Learn. 3(1), 2011), shows that the alternating direction method of multipliers (ADMM) splits each of these problems into a step that touches only the loss and a step that touches only the regularizer, and that each step has a closed form. The practical value of ADMM on these problems rests entirely on those closed forms: an iteration is one cached linear solve, one projection, or one thresholding.
The capstone is sparse inverse covariance selection (§6.5), the ℓ1-penalized Gaussian maximum-likelihood problem of Banerjee, El Ghaoui and d'Aspremont (2008), also solved by the graphical lasso of Friedman, Hastie and Tibshirani (2008). Its ADMM X-update minimizes a log-determinant objective over positive definite matrices, and the book shows that it is solved exactly by one symmetric eigenvalue decomposition.
All vectors are real and is the Euclidean norm. For the soft thresholding operator is if , if , and if , applied componentwise to vectors and entrywise to matrices. The vector soft thresholding operator on is , with . The Huber penalty is for and for , summed over components for vectors.
In scaled-form ADMM for minimizing subject to , with penalty and scaled dual variable , the updates are
followed by . "The update is given by formula " means is the unique minimizer of the corresponding subproblem.
For sparse inverse covariance selection, is symmetric (the empirical covariance), is the regularization weight, , , and is the set of symmetric positive definite matrices, the domain of . ADMM alternates
and .
Let and be symmetric, , and with . Then
is positive definite and is the unique minimizer of over .
The closed forms are what make ADMM competitive on these problems. For the lasso the x-update is a ridge regression whose factorization is computed once; for basis pursuit it is a cached projection; the ℓ1 step is a componentwise threshold. For covariance selection the X-update costs one eigenvalue decomposition, and the book (p. 46) cites Scheinberg, Ma and Goldfarb (2010) as showing that ADMM outperforms state-of-the-art methods on this problem. The goal also yields that is always positive definite, so the iterates remain in the domain of without a line search.
All statements here are classical and their proofs are elementary convex analysis and linear algebra. A search of the platform found no machine-checked version of any of them. Formalizing them produces verified proximity operators (soft thresholding, vector soft thresholding, Huber, projection onto an affine set) and a verified matrix-function argument for that later missions on ADMM, proximal methods and Gaussian graphical models can import.
The vector updates reduce to separable one-dimensional problems or to a normal equation, and the difficulty there is bookkeeping: uniqueness, the case of vector soft thresholding, and the three regimes of the Huber prox.
The goal is harder. The book's argument says that satisfies the gradient equation "and thus minimizes the X-minimization objective". Checking the equation is algebra; the claim to be proved is minimality over the open cone , which needs the convexity (indeed strict convexity, for uniqueness) of on positive definite matrices and the identification of its gradient with along symmetric directions. Mathlib has determinants and positive definiteness; a usable convexity statement for on is not among the platform's published results. Showing that satisfies (6.5) alone does not establish the goal.
EuclideanSpace ℝ (Fin n), matrices Matrix (Fin m) (Fin n) ℝ acting by Matrix.toEuclideanLin. The Frobenius norm and the entrywise ℓ1 norm are written as explicit sums, not through Mathlib's matrix norm instances. The vector ℓ1 norm is the platform definition HighDimStat.SparseLinear.l1Norm.IsUniqueMinimizerOn). Iterates are not defined; the subproblem's data (, , ) are arbitrary.Matrix.PosDef only. Singular or indefinite matrices are never competitors, so Real.log of a nonpositive determinant plays no role.lam and μ.Real.log of nonpositive determinants, is not the book's claim; the goal states unique minimality over .Contributions welcome: convexity and strict convexity of on and its derivative; a general "prox of a separable function is componentwise" lemma; and the projection onto an affine set.
The cutting stock problem asks how to cut standard stock rolls of length into pieces of demanded lengths so that the demands are met at least cost. Gilmore and Gomory solved its linear programming relaxation by column generation (Part I, Opns. Res. 9 (1961)): every cutting pattern is a column, and the column to bring into the basis is found by solving an integer knapsack problem whose objective is given by the current dual prices. In Part II (Opns. Res. 11 (1963)) they replaced the dynamic-programming knapsack solver of Part I by a lexicographic enumeration with a bound test, the Knapsack Method, and reported it to be about five times as fast as dynamic programming on their problem set (p. 866). The method is an early enumeration-with-bounds (branch-and-bound type) procedure for the integer knapsack, and the same pricing problem remains the inner loop of column generation for cutting stock, bin packing and their many variants.
There are demanded lengths with linear programming prices , and standard stock lengths with costs . A column for is a vector of nonnegative integers with . The knapsack problem (1) for is
and the quantity to compute is : a column improves the linear program exactly when .
For a prefix write and . Step (1) sorts the data, and , and appends a slack item with , . The method then generates vectors in decreasing lexicographic order:
In Lean the method is a transition system Step on states (a, s, t, M, phase). Reachable means reachable from the start state of Step (2).
Under Step (1)'s ordering, with and :
and at the end every is or the price of a column for , with . With one stock length () this is the paper's correctness claim in full: the method solves the knapsack problem (1).
The goal certifies the pricing oracle of the Gilmore–Gomory column-generation method: the knapsack solver it calls returns the true optimum. The pricing step is exact only if that holds, and so is the conclusion "no improving column exists, the LP is solved". Milestones 1–4 are reusable on their own. They are the textbook ingredients of lexicographic and depth-first branch-and-bound for the integer knapsack: the greedy completion, the density-ordered LP bound, and the pruning rule.
The paper's argument is a short paragraph, "clear from the order in which the -vectors are generated". Writing it out shows that the claim is false for several stock lengths as the steps are printed. With , , and , the method tests . The test of Step (5) at then fails for only because , Step (6) stops, and the run ends with while the column has price 2. This mission therefore states what the printed algorithm does achieve. The result is the full claim for and for the longest stock length in general. A sorry-free Lean proof of the counterexample run accompanies the mission. No part of the method or its correctness has been formalized before, as far as a search of the platform shows.
The method skips large parts of the lexicographic order in three ways:
Each skip has to be justified by a bound that holds for every vector skipped, and the justifications interact. A skipped vector may fit a longer stock length but not , and the bound for must cover exactly those vectors. The invariant that survives all three moves is not the naive "every vector above the current one has been examined": the vectors are not examined, only bounded. Termination needs the lexicographic decrease together with finiteness of the fitting vectors, and progress needs the reachability invariants and that make Step (5) meaningful.
Items are Fin m from 0. The paper's level is a natural number, and the prefix is the coordinates with index < s. Stock lengths are Fin k, and is index 0. The slack item enters only through and at . The lexicographic order is Mathlib's Pi.Lex, and is Nat.floor.
is the predicate IsKnapsackMax, never a real supremum, which would be 0 on an empty set. The algorithm's output is never defined as the maximum. The goal includes termination and progress, so its correctness clause is not vacuous. Every invariant is stated for reachable states only.
The goal adds two disclosed hypotheses:
Step (1) is a hypothesis on the data, not a step.
The goal also makes these corrections:
Not formalized:
Contributions welcome: proofs of the milestones, and a corrected multi-length variant of the method with a proof that it computes every .
Many large optimization problems arising in statistics, machine learning, signal processing and resource allocation have an objective that is a sum of terms, each depending on data held by a different processor, or a coupling term that depends on the sum of the agents' decisions. Chapter 7 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) introduces two templates that turn such problems into distributed algorithms: consensus and sharing. Nearly every distributed application in the rest of the monograph (distributed lasso, distributed logistic regression, splitting across examples and across features in Chapter 8) is an instance of one of the two. Consensus problems in the context of ADMM go back to Bertsekas and Tsitsiklis (Parallel and Distributed Computation, 1989).
The value of the templates lies in a handful of exact algebraic facts about the ADMM subproblems: the global update is an average, the dual variables average to zero, and the sharing update, which looks like a problem in variables, is really a problem in variables. These facts are what this mission formalizes.
There are agents. Vectors live in with the Euclidean inner product, and an overline denotes an average over agents, . Each local cost and the shared cost are functions into . The penalty parameter is .
Global variable consensus (§7.1) is the problem
with local variables and a global variable . ADMM alternates a parallel -update, an averaging -update and a dual update of the multipliers . With a regularizer added (7.2), the -update (7.4) becomes a minimization involving .
General form consensus (§7.2) lets local variable copy only some entries of : entry of corresponds to entry , and is defined by . The number of local entries copying is .
Sharing (§7.3) is the problem
written for ADMM with copies of the (7.12). In scaled form, with , its -update is
followed by .
For every : solves the -variable -update iff solves
and
and along every run of sharing ADMM,
so all scaled dual variables agree after one step.
The reduction is what makes sharing ADMM scale: the central step needs only the averages , and one -dimensional proximal problem, regardless of the number of agents, and the dual state collapses to a single vector. The same reduction underlies exchange ADMM (§7.3.2) and the splitting-across-features algorithms of §8.3. The consensus facts explain why the fusion center only averages and why the dual variables can be dropped from its update.
All results of the chapter are proved, informally, in the monograph; they are elementary. To our knowledge none has a machine-checked proof. The mission produces checked statements of the update formulas that later chapters of the series and distributed-optimization developments can cite instead of re-deriving.
The statements are exact identities between minimizer sets of nonsmooth problems in which may be any extended-real-valued function: there is no first-order condition to use, so each step must be argued by comparing objective values, and the iff requires producing, for an arbitrary competitor, a competitor of the reduced problem with no larger value. The index bookkeeping is the other half: averages of sums of sequences indexed by agents and by iterations, the off-by-one in "after the first iteration", and in §7.2 sums over the fibres of an index map between local vectors of different dimensions.
EuclideanSpace ℝ (Fin n); agents are indexed by Fin N, so the book's is Lean's ; components are 0-based as well.lam), for every global index in §7.2, and the index ranges for and for (the starting is arbitrary).