Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many 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).In two-stage optimization under uncertainty, a first-stage decision is taken before the data are known, and a second-stage decision is taken after a scenario is revealed. The fully adaptive formulation lets depend on and minimizes the worst-case cost. It is the natural model of recourse, but it optimizes over policies, one decision per scenario, and is computationally hard in general. The static robust formulation fixes one in advance that must be feasible in every scenario. It is a single deterministic mixed integer program and is the standard tractable surrogate (Ben-Tal, Goryashko, Guslitzer, Nemirovski 2004; Bertsimas & Sim 2004).
The question is how much is lost by the surrogate. Bertsimas and Goyal (2010) bound the gap by against the stochastic problem and by against the adaptive problem when the uncertainty set is symmetric. Their §5.3 identifies a case with no gap at all: when the uncertainty set is a hypercube (a box), the static robust optimum equals the adaptive optimum, and this holds even when the constraint matrices themselves are uncertain. Box uncertainty is the simplest and most common uncertainty model in practice (interval data on every coefficient), so the result says that for it, adaptivity buys nothing.
This mission formalizes that theorem, Theorem 5.4, together with Theorem 2.4, which shows that under right-hand-side uncertainty the robust problem is a single deterministic problem with the coordinatewise worst right-hand side.
Fix dimensions and sets of integer coordinates. The decision domains are
which is up to relabelling coordinates, .
A scenario set is given. In scenario the data are a constraint matrix , a recourse matrix , a right-hand side and a second-stage cost . The first-stage cost is fixed.
The uncertainty set is , a subset of with . Following Definition 1.1, is a hypercube if for some .
For Theorem 2.4, , and are fixed and only varies; (1.2) is the robust problem above, and is the deterministic problem with right-hand side .
If is a hypercube, then
The integer coordinates are arbitrary, and nothing is assumed about the signs of , , .
The result. Theorem 5.4 says that for interval uncertainty on every coefficient, the static robust program, whose size does not grow with the number of scenarios, solves the adaptive problem exactly. Combined with Theorem 2.4 for right-hand-side uncertainty, the adaptive problem collapses to one deterministic mixed integer program with worst-case data. It marks the boundary case of the paper's adaptability-gap bounds: the gap is at most for symmetric sets, and exactly for boxes.
Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a Lean model of two-stage robust and adaptive mixed integer programs with uncertain constraint matrices, with values as extended-real infima, which other formalizations of adjustable robust optimization can build on.
The mathematics is elementary; the care is in the statement. The step that fails for a general uncertainty set is the existence of a single worst scenario that is simultaneously entrywise smallest in , and entrywise largest in , . For a set that is only contained in a box, the box's worst corner need not be realized. With two scenarios and , , , the adaptive value is and the robust value is . A formalization therefore has to state the hypercube hypothesis as an equality of sets. A second point is the arithmetic of extended reals: the paper argues from optimal solutions, which need not exist, so the inequalities must be transported through infima over feasible sets that may be empty and through suprema that may be infinite.
Fin n → ℝ; matrices are Matrix (Fin m) (Fin n) ℝ; constraints use Mathlib's componentwise order and mulVec.EReal infima over the feasible set, when infeasible; worst-case costs are EReal suprema over . No optimal solution is assumed.IsHypercube (uncertaintySet A B b d), i.e. the realized data are exactly a box. Assuming only that the data lie inside a box would make the statement false (example above); assuming fixed , would state Corollary 5.1 instead of Theorem 5.4.Contributions welcome: proofs of the milestones and of the goal, and lemmas on monotonicity of mulVec for nonnegative vectors and on EReal infima over feasible sets, which are reusable across the other missions of this series.
In just-in-time scheduling each job has a preferred time, and finishing it early is as undesirable as finishing it late. Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988), 330–348) study the one-processor version in which task has a length and a preferred starting time , and the discrepancy of a task started at time is . The penalty is symmetric: earliness and tardiness cost the same. The paper shows that minimizing the total discrepancy is NP-complete, gives an algorithm for a fixed task order, and, in §3, gives an efficient algorithm for minimizing the maximum discrepancy : a linear-time test for a given bound after an sort, combined with a search over .
This mission formalizes the structural core of §3: the normal-form theorems (Theorem 4, Corollaries 1 and 2) on which the paper's algorithm for maximum discrepancy is built. The two companion missions of the series cover the NP-completeness result (THEOREM 1) and the fixed-order algorithm (THEOREMS 2 and 3).
Fix a bound . A schedule has maximum discrepancy at most exactly when every task starts no earlier than its release time and finishes no later than its deadline (p. 342). These release times and deadlines are in special form: with , for every task
From here on the data are arbitrary reals , , in special form for some .
A schedule is an execution order ( is the task in position ) with starting times , such that a task finishes no later than any later-positioned task starts: for . It is feasible if and for every . Its makespan is , and it is optimum if it is feasible and no feasible schedule has a smaller makespan.
Let be a task of largest deadline. A schedule has the release time property if every task executed after has release time strictly later than the starting time of . When the tasks are indexed with , a schedule is in standard form with split index , , if it begins with an optimum schedule of , followed by started at the maximum of and the completion time of that first part, followed by in this order without idle time.
Two companion items state the reformulation of the maximum-discrepancy bound as release times and deadlines, and the special form with .
Corollary 2 reduces the search for an optimum schedule of to candidates, one per split index, each assembled from an optimum schedule of a shorter prefix. This is the dynamic program of §3.2, which the paper implements in time after an sort; combined with a search over it minimizes the maximum discrepancy. Without the special form, deciding whether one processor can meet arbitrary release times and deadlines is NP-complete (reference [4] of the paper, Garey and Johnson 1979), so the normal form is what separates the tractable case from the general one.
The results are proved in the paper; no machine-checked proof of them is known on Prove2Me. A formal proof of Corollary 2 would certify the correctness of the split-index recursion and, together with the companions, of the reduction from maximum discrepancy to this release-time/deadline problem.
The obvious argument fails in Theorem 4. Exchanging a straggler (a task after released no later than starts) with shifts the tasks between them, and for general release times and deadlines those tasks can become infeasible. The paper's argument uses the special form at every step: a task released after starts has , hence exactly, and this equality is what bounds how far tasks may move. It also needs an extremal choice of the optimum schedule (fewest tasks after , then fewest tasks between and the first straggler), which requires showing that optimum schedules exist over the reals. The passage to standard form then combines this with an earliest-deadline exchange for the tasks after and the replacement of the first part by an optimum sub-schedule without losing feasibility of the later tasks.
Tasks are indexed by Fin N (0-based: the paper's are ; the paper's in Corollary 2 is the index ). All data are real. A schedule is a permutation σ : Fin N ≃ Fin N with starting times s : Fin N → ℝ; "executed before/after" refers to σ, not to a comparison of starting times, because zero-length tasks may share a starting time. Execution intervals meet at most at endpoints. The makespan is a supremum over Fin N; "optimum" quantifies over all feasible schedules, not only standard-form ones.
The standing hypotheses on every structural item are , , (from , the in , and nonnegative lengths); since , start times are nonnegative, as the paper assumes throughout. The special form is a hypothesis of every structural item and cannot be dropped. The paper's dummy task () is not a task; an empty first part completes at time . Corollary 1's "the set of all tasks with deadline or less" is read as excluding , the only reading under which it is true. The page's "(which can be assumed optimum)" is part of the standard form. The deadline-split and release-before-finish milestones are stated for every feasible schedule, as their arguments allow.
A trivializing formalization is excluded: the standard form pins 's start to and the later tasks to consecutive positions in index order, so the goal is not Corollary 1 restated with an unconstrained split.
Running times (, ) and the algorithm of §3.2 are out of scope. The development needs only finite permutations, finite suprema and the exchange arguments of §3.1; the existence of an optimum schedule (minimum makespan over finitely many orders, earliest-start schedules) is reusable for other single-machine problems with release times and deadlines. Proofs of any milestone, and a sorry-free proof of the existence of optimum schedules, are welcome.
The residual life time of a lifetime at age is the remaining life given survival past . Its distribution at great age is a basic object in reliability, insurance and the statistics of extremes: excess-of-loss reinsurance prices the part of a claim above a retention level, and peaks-over-threshold methods fit a model to the observations exceeding a high level. Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974), 792–804, doi:10.1214/aop/1176996548) determined every possible limit law of the suitably normed residual life time as and the domains of attraction of these laws; Pickands (1975) obtained the continuous part of the same picture, which is the probabilistic basis of the generalized Pareto approximation used in practice.
Limit theorems describe the behaviour only as . Section 4 of the paper gives approximation results for finite . In extreme-value theory, von Mises (1936) gave a sufficient condition for attraction to the Fréchet law : . Theorem 6 of the paper is a non-asymptotic, two-sided counterpart for the residual life time: two-sided bounds on the scaled hazard rate give two-sided bounds on the residual life distribution at every age past a threshold. This mission formalizes Theorem 6 (p. 801).
Let be a real random variable with law and distribution function . For an age with , the residual life distribution function is
which is for . For the residual life scaled by the age has distribution function .
For the Pareto-type law is
It is the law of when for . has a positive density for if is differentiable at every with derivative . The quantity is the hazard rate of at , and is the hazard rate scaled by the age.
Let have a positive density for , and let satisfy for . Then for all and all real ,
The smaller constant gives the lower bound: a smaller scaled hazard rate means a heavier tail and hence a larger chance that the remaining life is long. For a Pareto tail one may take , and both inequalities are equalities.
For and ,
The theorem turns a pointwise condition on the hazard rate, which can be checked on a density, into a bound on the whole conditional distribution of the residual life, valid at every age rather than only in the limit. If moreover , then can be taken arbitrarily close to for large , which recovers the convergence with an explicit error at finite ages. Such bounds are what a practitioner fitting a Pareto tail above a threshold needs to quantify the approximation.
The result is classical and its proof is short; it is not open. As far as is known, no machine-checked version exists, and Mathlib has no theory of residual life distributions or of the limit laws of Balkema and de Haan. A formal proof would provide reusable pieces: the identity between the integrated hazard rate and for a distribution function with a density, and the comparison of a residual life distribution with a Pareto law. The other missions of this series formalize the paper's limit theorems, for which this mission's objects (the residual life distribution and ) are shared.
The mathematics is elementary; the work lies in the regularity bookkeeping that the printed proof leaves implicit. The density is only assumed to exist pointwise, so the fundamental theorem of calculus must be applied to with a derivative that is not assumed continuous, and its integrability on has to come from the hazard bounds themselves. That stays positive, that , and that the case is trivial all have to be derived from the hypotheses rather than assumed. Finally, the conditional probability must be identified with , where , through the measure of intervals.
The law of is a probability measure on , and is Mathlib's ProbabilityTheory.cdf μ. The probability is residualLife μ t (x * t) . is a real function defined by cases, with Real.rpow for the power. The density is an explicit function with having derivative at every , the derivative taken within . This is a right derivative at and the ordinary derivative for . It is the weakest reading of "positive density for ", and it admits the exact Pareto law with , whose distribution function has no two-sided derivative at . The bounds are stated for with Lean's real division.
No hypothesis is added to the printed theorem, and no printed slip was found. The conditions and follow from the hypotheses: for the ratio is not , and a positive derivative on makes strictly increasing there. Lean's convention therefore never acts at the ages concerned. The conclusion is stated for all real , as printed; for all three quantities are . The milestone does not assume the hazard rate integrable: it is bounded and measurable on , and a non-integrable integrand would make the inequality false rather than trivially true. A formalization that dropped the density hypothesis, replaced by deriv without differentiability, or let the bounds hold only on a set not containing every would not be this theorem; all three are excluded by the statement.
A proof needs the fundamental theorem of calculus for derivatives within a half-line (in Mathlib), the identity , and the chain rule for . Proofs of the milestone and the goal are welcome, as are sorry-free lemmas showing that is a distribution function and that the Pareto law satisfies the hypotheses with .
PERT (Program Evaluation and Review Technique) and the critical path method model a project as a directed acyclic network whose arcs are jobs and whose nodes are events; the duration of the project is the length of a longest path from the origin to the terminal. When job durations are random, the quantity a planner wants is the expected duration. Computing it exactly requires solving one longest-path problem for every joint outcome of the job durations: with jobs each taking two values, deterministic problems. Classical PERT practice replaced every random duration by its mean and reported the longest path for the mean durations. That figure is known to be optimistically biased.
D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks (RAND Memorandum RM-3075-PR, 1962; Operations Research 10(6):808–817, 1962, doi:10.1287/opre.10.6.808), proposed a second estimate, computed node by node with work exponential only in the size of a single node's bundle of incoming arcs, and proved that it lies between the classical mean-length figure and the true expectation.
A project network has events with , origin and terminal . Its arcs are ordered pairs with , at most one per pair, and every event lies on a directed path from the origin to the terminal. Fulkerson numbers his nodes ; his node is event here. The bundle of an event is the set of arcs entering , and the set of their tails; the origin's bundle is empty.
For arc lengths , let be the length of a longest (critical) path from the origin to ; equivalently and .
The lengths of the arcs of each bundle form a random vector with a finite distribution: a finite set of bundle vectors , where is the length of arc , with probabilities summing to . Arcs within a bundle may be correlated; distinct bundles are independent, so an assignment of one bundle vector per event has probability . Three numbers are attached to each event :
In the order of Fulkerson's induction (pp. 10–12):
The chain (4.4) says that the classical PERT estimate never overstates the expected project duration, and that the numbers are a lower bound at least as tight. The computation visits each node once and sums over the support of that node's bundle only, so its cost grows exponentially with bundle size rather than with network size, while the exact expectation requires the whole product space. The Fig. 4.2 example shows that the bundle-independence hypothesis cannot be dropped for the upper inequality, while the lower inequality survives arbitrary dependence.
The result has a complete published proof. This mission seeks a machine-checked proof of (4.4) for finite distributions, with the longest-path characterisation of the earliest-event-time recursion and the locality of critical path lengths as reusable lemmas, and machine-checkable versions of the paper's numerical examples, including the counterexample showing the role of independence.
The left inequality compares an average of maxima with a maximum of averages. The right inequality requires more: averages over the bundle entering , while averages over assignments to every bundle. Taking expectations in yields , which gives the weaker bound . Fig. 4.2 shows that can fail when the bundles are dependent. In Lean, is a sum over a dependent product of finite supports (Fintype.piFinset); its interaction with the local recurrence for is the central technical difficulty.
CriticalPath.Events.ProjectNetwork (Kelley–Walker 1959): events Fin (n + 1), arcs a Finset of ordered pairs with strictly increasing labels, origin preceding and terminal following every event. This requires . Fulkerson's numbering condition "" on p. 3 is read as the strict (arcs join distinct nodes of an acyclic network). There is one arc per ordered pair, Fulkerson's own convention in (3.13).CriticalPath.Events.earliest, a recursion with Finset.sup' over the nonempty set of incoming arcs. This is the paper's convention that terms of missing arcs are ignored. Nothing uses a default value of or .Finset and a weight function per bundle) plus a predicate IsProb (nonnegative weights on the support, summing to , for every event including the origin). Bundle vectors are functions on all events, and coordinates outside are never read.Infrastructure that a full development needs, and that is reusable elsewhere, includes the longest-path characterisation of the earliest-event-time recursion, the locality lemma, and the factorisation of sums over Fintype.piFinset along one coordinate. Proofs of any milestone or companion are welcome. Out of scope here: §5 (computational examples) and the general-network analogues of §6.
A task may have a preferred execution time because a material delivery, external event, or downstream operation is timed to it. Starting early can be as costly as starting late. Garey, Tarjan, and Wilfong study this situation on one processor, where tasks cannot overlap but idle time between tasks is permitted. Their total-discrepancy problem is hard when the execution order is free; fixing the order leaves a substantial timing problem because each start can still move and can force changes to earlier starts. The paper gives an explicit scheduling procedure for that case and proves that it minimizes the sum of deviations from preferred starts (Garey, Tarjan, and Wilfong, 1988, §§1–2).
This mission targets that procedure and its correctness theorem. It also records the paper's equal-length result: when task lengths are identical, a minimum-cost schedule exists in preferred-start order, so the fixed-order procedure applies after sorting. These are two precise claims about total discrepancy, distinct from the paper's separate maximum-discrepancy problem.
There are tasks, indexed . Task has a nonnegative length , a nonnegative preferred starting time , and an actual starting time . Once started, it occupies the one processor until . Each start must be nonnegative. For the fixed-order problem, task must finish before task starts, so . This permits idle time when the inequality is strict. The task's discrepancy is ; because its preferred completion is , this is also its absolute completion-time discrepancy. The total discrepancy is
A block is a maximal consecutive set of tasks with no idle time between neighboring tasks. Within a block, Decrease counts tasks whose actual starts are later than preferred, and Increase counts tasks whose actual starts are no later than preferred. These names describe the effect of moving the entire block earlier: the discrepancy of a Decrease task falls initially, whereas that of an Increase task rises. The algorithm's state is a schedule for the first tasks. It inserts the next task at its preferred start when the previous task has finished, and at that finish time otherwise. In the latter case it may move the final block earlier until one of the paper's stopping events occurs: the block reaches time zero, a late task reaches its preferred start, or the block meets its predecessor (§2.2, p. 337).
For the equal-length result, schedules may execute tasks in any order. Two distinct tasks are feasible together when one completes before the other starts; meeting at endpoints is allowed. The objective remains the same sum of absolute discrepancies.
The main target is the paper's Theorem 2. For all nonnegative task data and every , the actual schedule produced by the block-shifting algorithm is feasible and satisfies
This includes the empty schedule and schedules with idle time. The milestone list follows the paper's own assertions: a balanced final block can move earlier without changing cost; every block of has more Increase tasks than Decrease tasks or begins at zero (Lemma 7); and the two claims in Case 2 of the proof record the cost of adding a late task and the comparison with schedules that place it earlier (Theorem 2 and Lemma 7, p. 338).
The companion target is Theorem 3. If every task has a common length and the preferred starts are indexed so that , then among all feasible schedules, including those with another task order, at least one minimum-cost schedule starts the tasks in index order:
The paper uses this statement to connect free-order equal-length scheduling to its fixed-order procedure (Theorem 3, p. 340).
Theorem 2 certifies an explicit schedule, not just the existence of an optimum. It fixes the objective value for a prescribed execution order and gives a baseline against which any other legal timing of the same tasks can be compared. Theorem 3 supplies the ordering fact needed to use that result when all lengths agree. Together they explain why a problem that is difficult for unrestricted task lengths still has these structured solvable cases (Garey, Tarjan, and Wilfong, 1988, abstract and §2.5).
The paper proves both theorems on paper. The work here is to formalize its schedule construction, cost, block boundaries, and comparison classes in Lean, then obtain machine-checked proofs of the stated targets. The draft theorem declarations compile with proof placeholders; this proposal does not claim that they are already machine-checked results. A completed development would make the model and the algorithm available for later formal work on scheduling with idle time and symmetric earliness and tardiness penalties.
Moving a task closer to its preferred start can move neighboring tasks farther from theirs. A simple task-by-task choice therefore does not establish global optimality. Nor does a count of late and early tasks in one block, by itself, justify arbitrary earlier movements of individual tasks. The difficult comparison in the paper is between the algorithm's schedule and a competing feasible schedule whose new task starts earlier: the whole final block and its constrained relative movements matter. The proof also has to account for the boundary at time zero and for blocks that merge when shifted. These are the reasons the explicit procedure and its block invariant need careful statements (§§2.2–2.3, pp. 337–338).
The Lean development represents task data and starts as functions from natural-number indices to real numbers; only indices below count. Task in Lean is the paper's . Preferred times, lengths, and legal starting times are nonnegative. The start-time condition is a standing convention used by the paper's algorithm, especially its zero-boundary stopping rule. Fixed-order feasibility requires successive tasks to be separated by at least the earlier task's length; unrestricted feasibility uses pairwise nonoverlap. An empty schedule is legal and has cost zero. The representation allows zero-length tasks, as does the paper's model.
The algorithm is defined by its stated insertion and single-block-shift operations. Defining as a chosen minimizer would erase the content of Theorem 2; the goal also explicitly asserts feasibility so that an illegal low-cost function cannot qualify. Theorem 3 compares with every feasible unrestricted-order schedule, not just schedules already in preferred-start order. The core definitions, the block invariant, and the cost comparisons are useful beyond this particular proof. Formalizing the paper's running-time bounds and heap implementation is outside this mission.
3SUM asks whether three distinct positions in a list of integers contain values summing to zero. It is a central problem in fine-grained complexity.
This mission formalizes a deterministic algorithm for 3SUM on polynomially bounded integers, on a word RAM with -bit words. Alman and Vassilevska Williams's 2026 breakthrough gives a truly subquadratic bound, refuting the integer 3SUM hypothesis in this model.
The mission uses the accompanying Lean specification and shares the Exact Triangle milestone with Truly Subcubic APSP on a Word RAM.
Theorem_22_3SUM.Many network optimization algorithms spend most of their time in a heap (priority queue): a set of items with real keys that supports inserting an item, finding and deleting an item of minimum key, melding two heaps, decreasing the key of an item, and deleting an arbitrary item. Dijkstra's shortest-path algorithm performs at most one delete min per vertex and may perform a decrease key for each edge, so on a graph with vertices and edges its running time is governed by how cheap decrease key is. Binomial queues support the heap operations in worst-case time.
Fredman and Tarjan (J. ACM 34 (1987)) introduced Fibonacci heaps (F-heaps), in which delete min and delete take amortized time and every other operation, decrease key included, takes amortized time. This brings Dijkstra's algorithm to and improves the best bounds then known for all-pairs shortest paths, weighted bipartite matching (the assignment problem) and minimum spanning trees. F-heaps descend from the binomial queues of Vuillemin (1978) and use the potential technique of amortized analysis of Sleator and Tarjan. This mission formalizes the paper's §2 analysis, culminating in THEOREM 1 on p. 604.
An F-heap is a list of heap-ordered rooted trees: every child's key is at least its parent's key. Each node holds an item, the item's real key and a mark bit; the children of a node are kept in the order in which they were linked to it, earliest first. The rank of a node is its number of children. A collection is a list of heaps, named by position; a run starts with no heaps.
Linking two trees with roots and makes the last child of if the key of is smaller, and otherwise makes the last child of ; the root that becomes a child is unmarked. The operations act as follows:
The actual time of an operation is one unit, plus one per linking step, plus one per cut, plus for delete min the scan of the rank array (the largest rank involved). The potential of a collection is the number of trees plus twice the number of marked nonroot nodes, and the amortized time of an operation is its actual time plus the increase of .
There is an absolute constant such that for every sequence of operations started from no heaps, with the number of items in the heap that operation acts on, just before it acts,
The paper's wording is "the total time is at most the total amortized time, where the amortized time is for each delete min or delete operation and for each of the other operations"; the goal pins the to one constant and does not name the potential.
THEOREM 1 is the data-structure fact behind the paper's algorithmic results: Dijkstra's algorithm in , all-pairs shortest paths and the assignment problem in , and minimum spanning trees in .
The result has been proved since 1987. What the mission adds is a machine-checked version of the paper's own analysis on an operational model with arbitrary linking order, unmarking on link, marking or cascading on every cut, and the paper's unit costs. The proposal states the theorem and its supporting claims; their proofs remain to be formalized.
The obvious argument, that every tree is a binomial tree and so every rank is at most , fails as soon as cuts are allowed: decrease key and delete remove subtrees arbitrarily, and the trees of an F-heap need not be binomial. The rank bound has to come from an invariant of the whole history (LEMMA 1), which only holds because a node loses at most one child before it is cut itself; without cascading cuts a node of rank can be left with only descendants, and no logarithmic rank bound holds. A second difficulty is that the actual cost of one decrease key is unbounded, since a single operation may trigger arbitrarily many cascading cuts; a per-operation worst-case argument cannot give THEOREM 1, and the bound holds only for whole sequences started from no heaps.
All declarations sit in the namespace FibHeap.Amort. Trees are a nested inductive FTree with item ℕ, key ℝ, a mark bit and a list of children in linking order; a heap is List FTree (its roots) and a collection is List Heap. Operations are a step relation Step s op s' d whose data d records linking steps, cuts, cascading cuts and the scan, so that cost d = 1 + links + cuts + scan is determined by what the operation did. The linking loop allows every order of linking; a link tie makes the first root a child of the second, while delete min may choose any minimum-key root. Runs start from no heaps; reachable collections consist of heap-ordered trees with each item in at most one heap. LEMMA 1, COROLLARY 1 and the delete-min bound are stated for reachable collections only, as the paper's "a node in an F-heap" intends. The paper's standing assumption that an item is in only one heap at a time is enforced by the precondition of insert and is not a hypothesis. The minimum pointer and returned items are not stored in the step relation; find min is a state-preserving step charged one unit. A heap destroyed by meld remains as an empty heap at its index.
Logarithms in the goal are base 2 (footnote 1, p. 600), with a so that one-item heaps have positive budget. The paper's constant "" on p. 604 is a rounding slip (); milestones use the exact .
The goal is not trivialized: the cost counts every linking step and every cut as fixed by the step relation, is quantified before the run, and a companion theorem (step_exists) shows that every valid operation can be performed, so runs containing delete min, decrease key and cascading cuts exist. A further supporting statement gives an explicit form of the delete potential bound. A complete development needs facts about the nested inductive (sizes, subtree lists, marked counts under list edits), an invariant for LEMMA 1 recording when each child was linked, and the Fibonacci inequality; contributions of any of these as separate lemmas are welcome.
A postal route that must traverse every street and return to its starting point is a Chinese postman tour. In a street network, crossings are nodes, streets are edges, and the cost of a route is the sum of the lengths of the streets it traverses, counted with repetition. The practical question is which streets must be repeated, and how often. Edmonds and Johnson's 1973 paper separates that question from constructing the resulting tour: choose the repeated edges first, then find an Euler tour of the resulting multigraph. This mission concerns their reduction of the first question to a minimum-weight matching of the odd-degree nodes.
The reduction matters because it turns a route problem with arbitrary repeated edge traversals into a finite pairing problem. The graph of odd nodes is complete, with the weight of a pair given by its shortest-path distance in the original network. A matching chooses which odd nodes to pair, and paths realizing those pairs identify edges to repeat. The paper also explains why overlapping paths can be replaced so that no edge needs to be repeated by this construction more than once (§3, pp. 92–93).
A graph has finite node and edge sets. Each edge has two distinct endpoints. Different edges may join the same pair of nodes, so parallel streets remain distinct. The graph is connected when every pair of nodes is joined by an edge-labelled walk. A walk records both its node sequence and its edge sequence; a tour is a closed walk. An Euler tour uses each edge exactly once, while a postman tour uses each edge at least once. Edge lengths are real and nonnegative, as in §2, p. 89.
The degree of is the number of named edges meeting it. Let be the set of nodes of odd degree. For every edge , let be the number of additional traversals. The parity equations require a nonnegative integer at each node such that
Their objective is . These are the paper's (3.1)–(3.4), with natural-number values encoding integrality and nonnegativity (§3, pp. 90–91). The equations express the even-degree condition after adding copies of each original edge.
For nodes , write for the length of a shortest path in . This distance is backed by an attaining edge-simple path and is a lower bound on the length of every walk from to . Connectivity and nonnegative edge lengths make that specification meaningful. Let be the complete graph on , with edge of weight . A 1-matching pairs every node of with exactly one distinct node. Its length is , equivalently half the sum of over for the pairing involution (§3, p. 92).
The goal asserts the existence of a 1-matching of the odd nodes and both directions of the cost comparison:
The existence conclusion and these comparisons identify the two attained minimum values. The goal does not prescribe a particular matching algorithm. Its supporting targets are the paper's uncrossing of overlapping shortest paths, parity of their union, reduction of multiplicities to zero or one, and decomposition of a parity solution into paths between odd nodes (§3, pp. 92–93).
The companion target relates a tour's edge counts to the parity equations. A postman tour traverses edge exactly times, and its length is
Conversely, positive integer edge counts with even incidence at every node can be ordered into a postman tour of a connected graph. The supporting Euler theorem handles a connected even multigraph (§2, p. 89).
The matching result characterizes the optimal additional cost of an undirected postman route. It says that the parity correction can be chosen from paths pairing odd nodes, and that no feasible choice of repeated traversals can beat the best such pairing. The companion identifies how that correction becomes an actual tour. The distinction is useful when one wants to change the matching method while retaining the mathematical guarantee on route length.
A formal development would provide a reusable account of finite multigraph walks whose edge names distinguish parallel edges, of shortest-path distances with explicit attainment, and of parity subgraphs decomposed into odd-to-odd paths and even-degree residual tours. These pieces support later formal work on route inspection, -joins, and matching-based graph algorithms. The paper proves the mathematical result. The exact multigraph and cost statements drafted here are open formalization targets; the local prior-art search found related results for simple graphs and metric traveling-salesman models, but no published statement with this paper's objects and conclusion.
A direct shortest-path construction can assign the same original edge to two matching pairs. Simply setting for the union then loses the additivity of path lengths, and setting loses the promised zero-or-one form. The uncrossing claim must control both the matching cost and the number of times each original edge appears. In the converse direction, an arbitrary feasible may contain repeated edges and cycles; the argument must account for these without assuming that every supported edge belongs to a path between odd nodes (§3, pp. 92–93).
Lean uses the published EdmondsMatching65.Polyhedron.Graph for : finite node and edge types and an endpoint map into unordered node pairs. A proof field excludes loops; distinct edge names may have identical endpoints. Walks use lists of nodes and named edges with zero-based indices, and the one-node, zero-edge walk is allowed. Edge multiplicities and parity witnesses are natural numbers. Costs and shortest-path lengths are real. The distance relation requires both an attaining edge-simple path and a bound against all walks; no real infimum over a possibly empty family is used. The matching is a fixed-point-free involution on the odd nodes, extended by the identity elsewhere, and each pair contributes half of its two directed distance terms.
The goal assumes a connected graph and nonnegative edge lengths, exactly as the section does. The tour-only results require a nonempty node type because a list-based tour must have a starting node; without it an edgeless graph on no nodes would satisfy connectivity and even degree vacuously. The path-decomposition statement permits unused even-degree cycles. No independent set of “odd nodes” is accepted as input: it is computed from the degree of .
The development needs finite multigraph incidence, edge-labelled walks, shortest paths, finite matchings, parity arithmetic, path uncrossing, and Euler tours. Proofs or useful intermediate results for these objects are welcome, including results applicable to multigraphs beyond the postman setting.
The Chinese postman problem asks for a shortest closed walk in a graph that traverses every edge at least once. Edmonds and Johnson (Math. Programming 5 (1973) 88–124) reduce it to two subproblems: choosing, by matching, which edges to duplicate so that every node has even degree, and then actually finding an Euler tour of the resulting even graph, a closed walk using every edge exactly once. Euler's theorem guarantees such a tour exists in a connected even graph, but an algorithm has to produce one and represent it compactly.
Section 5 of the paper gives two such representations and two algorithms. This mission formalizes the next-node representation: for each node , a list of the nodes the tour goes to when leaving . Theorem 5.1, which the paper attributes to its reference [1] (van Aardenne-Ehrenfest and de Bruijn, 1951) and to Berge's textbook, characterises exactly which lists describe an Euler tour; Theorem 5.2 shows the paper's next-node algorithm produces such lists. The same correspondence between Euler tours and arborescences is the combinatorial core of the BEST theorem on counting Euler tours of directed graphs (van Aardenne-Ehrenfest and de Bruijn, 1951).
A graph is a finite set of nodes and a finite set of edges, each edge meeting two distinct nodes; several edges may meet the same pair of nodes. The degree counts the edges meeting , and counts the edges meeting both and . A tour is an alternating sequence in which meets and ; an Euler tour contains every edge exactly once. is connected when every two nodes are joined by such a sequence, and even when every degree is even.
Next-node lists assign to each node a list of nodes. Given a starting node , the lists specify a walk: start at ; the first time a node is reached (for , at the start), leave it to ; the second time, to ; and so on, so the lists are read from the last entry to the first. The walk stops at the first node whose list is used up. The lists describe an Euler tour when this walk uses every entry of every list and its node sequence is the node sequence of an Euler tour of . With parallel edges, the lists name nodes only, and the edge used at each step is chosen so that every edge is used once.
An arborescence with root is a tree whose edges are directed so that every node has exactly one edge directed away from it, and has none.
For any node of an even, connected graph , next-node lists describe an Euler tour from if and only if
The printed condition (iii) names the edges ; the paper's own proofs of Theorems 5.1 and 5.2 use , the last exit from , and the printed version is false on a five-edge example. The goal states .
The proof on pp. 112–113 splits into five claims, each a milestone:
The lists produced by any complete run of the next-node algorithm of §5.2 satisfy (i), (ii) and (iii); together with Theorem 5.1, they describe an Euler tour.
Theorem 5.1 replaces a global property, that a walk uses each edge exactly once, by three local checks: list lengths, pair counts, and a tree condition on one distinguished entry per node. That is what makes the next-node representation usable. An algorithm only has to build lists with (i)–(iii), and Theorem 5.2 shows the paper's algorithm does so for every nondeterministic choice it makes. The same arborescence condition counts Euler tours in the BEST theorem: each arborescence and each ordering of the remaining exits gives a distinct tour.
The results have been proved since 1951. What this mission proposes is a Lean formalization on multigraphs with parallel edges, which is the setting the Chinese postman reduction needs, since duplicated edges are parallel. A search of Mathlib and of the platform finds no formalization of Theorem 5.1, of next-node lists, or of arborescences in this form. Mathlib has Eulerian walks only for simple graphs, and the existing platform statements of Euler's theorem (for example SupplyChainTheory.euler_tour_iff) are about simple graphs and existence only.
The necessity of (i) and (ii) is counting. The substance is in two places.
First, necessity of (iii): the last exits must be shown to leave every set avoiding . The tempting choice of the first exits , which is what the theorem's printed text says, is wrong: on an Euler tour the first exits can form a cycle, so any argument that does not distinguish first from last exits cannot work.
Second, the converse: a walk that follows lists satisfying only (i) and (ii) can return to early and leave edges untraversed, so (iii) is indispensable, and the statement depends on exactly which list entries have been used when the walk stops. Making that bookkeeping precise for a walk defined by a counter per node, and turning the used entries into an actual edge sequence in a multigraph, is the main formal work. For Theorem 5.2 the difficulty is the invariant of a nondeterministic algorithm: every trail it starts closes at its starting node because the graph is even.
All declarations live in the namespace ChinesePostman.NextNode. A graph is a local ChinesePostman.NextNode.Graph V E structure on finite types: ends : E → Sym2 V and a proof that no edge is a loop, so parallel edges are distinct elements of E with the same ends. Walks are pairs of a node list and an edge list. A list is a Lean List V, so is the entry at index and is the length. The walk specified by the lists is computed by follow L r, a fuel-bounded iteration whose state is the current node and the number of departures made from each node. It returns the node sequence and the final counters. DescribesEulerTour G r L requires every counter to reach the list length and some edge list to make the node sequence an Euler tour. Condition (ii) is quantified over all pairs including , where it forbids a node in its own list. Condition (iii) requires every list of a node to be nonempty, its chosen exit to be an edge of , and requires the iterates of the parent map (with ) to reach from every node. The next-node algorithm is an inductive step relation on states, and "produced" means reachable termination from the Step 0 state.
Added hypotheses: Theorem 5.2 and its corollary assume an edge meeting , which Step 0 needs; a one-node graph without edges satisfies Theorem 5.1 trivially and is not excluded. Milestones drop the hypotheses their claims do not use (connectivity, evenness), which makes them stronger.
A trivializing formalization is ruled out explicitly: the lists are read backwards, from to , and must all be used up. Reading them forwards, dropping the "uses every entry" clause, or stating (iii) with an empty-list default for the parent would each make a different, and in some cases false, statement.
The development needs walks on multigraphs, counting arguments for closed walks (in-degree equals out-degree along the walk), and a finite pigeonhole/orbit argument for the arborescence. The arborescence lemma (milestone 3) is graph-free and reusable. Proofs of any milestone, and of the multigraph walk lemmas they need, are welcome.
A matroid abstracts the dependence structure of the columns of a matrix: which sets of columns are linearly independent, forgetting the numbers themselves. Graphs are the special case of incidence matrices over the integers mod 2, where a set of edges is independent exactly when it contains no cycle. A natural combinatorial question in this setting is the minimum partition (or covering) problem: how few independent sets are needed to cover all the elements? For a graph this is the least number of forests that cover its edges, its arboricity.
J. Edmonds answered this question for every finite matroid in Minimum partition of a matroid into independent subsets (J. Res. NBS 69B, 1965, doi:10.6028/jres.069b.004). The answer is a good characterization in Edmonds's sense: there is a short certificate both that a partition into independent sets exists (the partition itself) and that it does not (a single subset that is too large for its rank). The paper is also the source of the matroid partition algorithm, which together with matroid intersection became a basic tool of combinatorial optimization.
Timeline:
Let be a finite set of elements and call some subsets of independent. Edmonds's two axioms are:
A matroid is a system satisfying both. The rank of is the largest cardinality of an independent subset of ; in a matroid every maximal independent subset of has exactly elements.
A circuit is a minimal dependent set. A span (closed set) is a set such that no circuit has exactly one element outside , and the span of is the minimal span containing . A partition into independent sets is a family of mutually disjoint independent sets whose union is ; any number of the may be empty.
For every finite matroid and every integer , the elements of can be partitioned into independent sets if and only if there is no with
The condition ranges over all subsets of , as printed.
The milestones follow the paper's own lemmas and the claims of its main proof, in order.
A further item states the paper's COROLLARY (Nash-Williams): the edges of a loopless finite graph can be colored with colors so that no circuit is one color if and only if no nonempty node set has , where is the set of edges with both ends in .
THEOREM 1 is the base case of matroid union: the sets coverable by independent sets form a matroid whose rank is , and the paper's proof is the origin of the polynomial-time matroid partition algorithm and of Edmonds's later matroid intersection theory. Its graphic case gives the arboricity formula of Nash-Williams, used for sparse-graph decompositions and orientation problems. The criterion is a certificate: a single set with proves that no partition exists.
The theorem has been proved since 1965 and appears in every matroid textbook. As far as the platform and Mathlib record, it has no machine-checked proof: Mathlib has matroids, circuits, closure and strong circuit elimination for its own Matroid structure, but no matroid union or partition theorem. This mission produces a formal proof from Edmonds's own axioms (Axiom 2 as an equal-cardinality condition, not an exchange axiom), together with the equivalences between his axiom systems, which are themselves standard results.
The "only if" direction is a three-line count. The difficulty lies in the converse: a greedy procedure that fills the sets one after another fails even for matroids, so an element that fits in no current set must be accommodated by moving other elements between sets. Such a chain of exchanges must keep all sets independent and disjoint at every step and must terminate; stating it with sets whose contents change while their labels persist is the part that needs careful bookkeeping in a formal proof. A second, smaller difficulty is the translation between the paper's equal-cardinality Axiom 2 and the circuit and span language its proof uses (PROPOSITIONS 1–5).
Finset.univ, subsets are Finset α, and the independent sets are a predicate Indep : Finset α → Prop.IndepI1 and rankOfIndep (WhitneyMatroid.RankIndep.Postulates). The rank is integer-valued, and every inequality versus is compared in with .Matroid.Fin k → Finset α of pairwise disjoint independent sets covering , with empty parts allowed and included.ends : E → Sym2 V (parallel edges allowed, loops excluded), with independence as linear independence of incidence columns over . It quantifies over nonempty : as printed, makes the statement false.Contributions welcome: proofs of the axiom equivalences (reusable for any work with Edmonds-style or circuit-axiom matroids), the span lemmas, the augmentation step, and bridges to Mathlib's Matroid that would let its circuit and closure library be reused.
Truncated-Newton methods minimize a smooth function by taking, at each iterate , a search direction obtained by solving the Newton equation only approximately, with the linear conjugate gradient (CG) method. Here is the gradient and the Hessian of . The approach was analysed by Dembo and Steihaug (Math. Programming 26, 1983), building on the inexact Newton framework of Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19, 1982), and Newton–CG with curvature tests remains a standard large-scale method (Nocedal and Wright, Numerical Optimization, Ch. 7).
Away from a minimizer the Hessian need not be positive definite, and CG on an indefinite system can produce directions along which curves downward. The Dembo–Steihaug method stops CG when it meets such a direction. A practical question follows: started at or near a stationary point that is not a local minimizer, will the method ever notice the nonpositive curvature? Theorem 2.4 of the paper answers it for exact CG: it does, except in a degenerate case described by the eigenspaces of .
Fix a symmetric linear operator on , with the Euclidean inner product and norm , and a vector . In the paper these are and at the current iterate.
The TNCG minor iteration (p. 194) runs CG on from . Its state at iteration is :
and, writing ,
At iteration the method first applies the curvature test (2.1), , and stops if it holds; otherwise it computes and applies the truncation test (2.2), , and stops if it holds. With , (2.1) reads and (2.2) reads . The method exits through (2.1) at when no test fired at any iteration and (2.1) holds at .
For the eigenspace is (A.21). The span of vectors is written ; the Krylov space of is .
Let . If is not positive definite, then either the minor iteration exits through (2.1) at some iteration , so that
or
The theorem is the theoretical justification, given in the paper on p. 197, for using the direction of negative curvature produced in case (ii) of the minor iteration: with exact arithmetic and no truncation, CG either produces a direction of nonpositive curvature or the gradient lies entirely in the span of eigenvectors with positive eigenvalues. The paper draws the consequence that if and the method terminates through (2.2), then, outside this rare case, is a strong local minimizer. Theorem A.5 is a self-contained statement about conjugate families in Krylov spaces, usable in any analysis of CG on indefinite systems.
The result is proved in the paper (Appendix, pp. 206–211), with the CG relations of Theorem A.1 cited from Hestenes and Stiefel. No machine-checked proof of these statements is known to this mission. Formalizing them produces a Lean development of CG on a symmetric, possibly indefinite operator, with its conjugacy and Krylov-span relations, which classical treatments state only for positive definite systems.
The CG relations of Theorem A.1 are usually proved for positive definite , where every denominator is positive. Here is indefinite, and the relations hold only as long as the curvature along the directions has stayed positive; the induction must carry that hypothesis and must also show the residuals do not vanish early. The passage from "CG ended with " to a statement about all eigenspaces is the second obstacle: the CG run sees only the Krylov space of , so one must relate that space to the eigenspaces that meets, using symmetry of and a count of distinct eigenvalues. A direct argument via "the directions span " fails, because when misses an eigenspace the Krylov space is a proper subspace.
is EuclideanSpace ℝ (Fin n); is a continuous linear map that is self-adjoint (IsSelfAdjoint H), as the paper's is a Hessian. Positive definiteness is for all . The CG recursion is total and carries no stopping test; division by zero returns in Lean, so states after a would-be stop are junk, and the statements read the iteration only through first-exit predicates. The test (2.2) is encoded in the product form .
Theorem 2.4 is stated for an arbitrary symmetric and vector rather than at an iterate of a run of the full algorithm. It uses nothing else about or the run, and every such pair occurs as the Hessian and gradient of an admissible objective. The paper's (A.5) prints as the last Krylov vector; the correct is used.
A trivializing formalization exists and is ruled out: the first alternative is not " for some " over the unstopped recursion, which holds automatically once a residual vanishes (the recursion then continues with ); it requires that iteration is reached with no earlier exit. The goal does not assume conjugacy, the Krylov span identity, or the hypotheses of Theorem A.5.
A complete development needs the spectral theorem for self-adjoint operators on finite-dimensional spaces (in Mathlib), finiteness of the set of eigenvalues, and the CG invariants. The CG lemmas are reusable for any Newton–CG or trust-region CG analysis. Proofs of the milestones, and of auxiliary CG invariants such as (A.3)–(A.4), are welcome.
A Markov decision process describes repeated choices whose costs and subsequent states depend on the current state. Such models are used when a decision affects both today's expense and the options available tomorrow. Papadimitriou and Tsitsiklis studied how the computational difficulty of finding an optimal policy changes between stochastic and deterministic transitions. Their general finite-state problems are P-complete, while their deterministic cases admit highly parallel algorithms Papadimitriou and Tsitsiklis, 1987. The contrast makes the deterministic case a useful setting in which to isolate the precise graph problem hidden inside long-run optimization.
This mission concerns their infinite-horizon average-cost case. When transitions are certain, every decision is an arc in a directed graph. The long-run cost of a policy can be related to the mean cost of a cycle reachable from the initial state. That relation is the mathematical claim supporting the algorithm in the paper's Theorem 3, whose headline says that the deterministic average-cost problem is in NC Papadimitriou and Tsitsiklis, p. 446.
Let be a finite set of states and the initial state. At each there is a finite, nonempty decision set . A decision has a real cost and moves the process with certainty to . All of these data are stationary: they do not change with time. A policy chooses a decision for each state and each time . It generates a trajectory by . The corresponding directed graph has a state for each node and a decision for each arc. It may contain loops and parallel arcs, since different decisions can lead to the same next state.
The paper prints the finite average with cost terms and denominator :
A time-dependent policy's averages may fail to converge. We use the upper limit and optimize over all policies, . A state is reachable if some finite walk of decision arcs goes from to . A simple cycle is a positive-length closed sequence of decision arcs with distinct states before it returns to its start; its mean cost is . A loop is a one-arc simple cycle.
For states , the min-plus adjacency entry is the least cost of a decision arc from to , or when no such arc exists. A min-plus product uses addition in place of multiplication and minimum in place of addition. Thus represents the least cost of a -arc walk from to , when such a walk exists Papadimitriou and Tsitsiklis, pp. 445–446.
The first target identifies the value of the original policy optimization problem:
It also states that a policy attains this value with convergent finite averages. The milestone for following a reachable cycle gives the attainable direction; the milestone saying that no policy can improve the least mean gives the reverse direction. The latter is formulated with , so it applies even when a policy's averages oscillate.
The second target identifies the finite graph calculation used in the paper:
The milestones establish what a min-plus power says about decision walks and why closed walks of lengths from through recover the least simple-cycle mean. The restriction to reachable is essential: a cheap cycle in a disconnected component cannot be used from .
The result reduces optimization over infinitely many decision times and all state-and-time policies to finitely many closed-walk calculations. It also guarantees that an optimal long-run value is realized by a trajectory with a genuine limiting average, despite the nonconvergence possible for other policies. The finite formula lets one determine the value by comparing graph quantities indexed by states and lengths; it is the correctness statement beneath the paper's parallel algorithm Papadimitriou and Tsitsiklis, p. 446.
Formalizing the identity creates a reusable bridge between deterministic decision processes, weighted directed walks and min-plus powers. Related proved tropical-algebra results on maximum cycle means use dense matrices and a max-plus convention, rather than the reachable, possibly missing-arc, minimum-cost process here; for example, the platform's TropicalLA.tpow_isGreatest concerns greatest walk weights. The present mission keeps the policy optimum and reachability explicit. The paper proves the result mathematically; these Lean statements are open proof targets in the proposal.
An arbitrary policy can keep changing its choices at repeated visits to the same state. Its averages can oscillate, so one cannot simply assume that its infinite trajectory becomes periodic or that its printed limit exists. The lower-bound claim must apply to every such trajectory. There is a second distinction between a closed walk and a simple cycle: a diagonal min-plus entry allows repeated states, whereas the cycle characterization is stated using simple cycles. Finally, an unrestricted matrix calculation would include cycles unreachable from the chosen initial state.
Lean represents the general finite stationary deterministic process in its own definition, then defines policies, finite walks, simple cycles, average costs and min-plus powers on top of it. Decisions are arcs, so parallel arcs remain distinguishable; takes their least cost and uses WithTop ℝ for a missing arc. Decision sets are explicitly nonempty because a policy has to make a choice at every state. The finite state set is automatically nonempty once is supplied. Policy time starts at zero. The printed terms divided by are retained; Lean's quotient is zero and has no effect on the limit. The optimum is the infimum over all policies , not a quantity defined by cycles or by stationary policies. Finite states and finite decision sets bound the one-step costs and hence the averages; this gives real limsup and infimum their intended values.
The paper's Theorem 3 asserts membership in NC. This mission formalizes the exact optimization identity that makes that algorithm correct. Its processor count and parallel-time bound are outside the scope, as are membership in P, log-space computability of reductions, PSPACE membership and the paper's Corollaries 1–2. Contributions to the finite-walk and min-plus lemmas, the lower bound for arbitrary policy paths, and the cycle-attainment statement are all needed; the graph definitions can be reused in other deterministic control problems.
All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph. It is a fundamental problem in graph algorithms and a fundamental problem in fine-grained complexity.
This mission formalizes a deterministic algorithm for APSP on directed -vertex graphs with polynomially bounded integer edge weights and no negative cycles, on a word RAM with -bit words. This is a truly subcubic bound and refutes the integer-weight APSP hypothesis in this model.
Theorem_22_APSP.Minimum makespan scheduling on unrelated parallel machines, written , is one of the basic models of scheduling theory: jobs must each be run on one of machines, and the time a job takes depends arbitrarily on the machine. Lenstra, Shmoys and Tardos (CWI Report OS-R8714, 1987; journal version Math. Programming 46, 1990) gave a polynomial 2-approximation algorithm for this problem and, in the same paper, a matching limit from below: no polynomial algorithm can guarantee a factor smaller than unless (their Corollary 2).
The two bounds have stood for more than three decades. Closing the gap between and for is listed among the central open problems of approximation algorithms (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, open problem on unrelated machines; Schuurman and Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 1999). The lower bound of is the subject of this mission.
Timeline:
3-dimensional matching. There are three disjoint sets , , and a family of triples, each with one element of , one of and one of . A matching is a subfamily with whose union is . In Lean an instance is a map , and HasMatching T says that a matching exists.
The scheduling model. Machines are , jobs are , and is the positive integer processing time of job on machine . A schedule assigns each job to one machine; the load of machine is and the makespan is the largest load. These are the published definitions MatousekLP.Scheduling.load and makespan.
The instance of Theorem 5. The triples containing are the triples of type ; let be their number. From the paper builds a scheduling instance with machines, machine corresponding to , and with
If , machine processes the element jobs of and in time , each dummy job of type in time , and every other job in time . In Lean the processing-time matrix is P T.
A -approximate schedule of an instance is a schedule with for every schedule of the same instance.
For every instance , every , and every -approximate schedule of the instance of Theorem 5 built from ,
This is the mathematical content of "for every there is no polynomial -approximation algorithm unless ": a -approximate answer on the reduced instance decides 3-dimensional matching.
For every instance ,
The result. Theorem 5 shows that is NP-hard already when every processing time lies in and the target makespan is . Corollary 2 turns this into the best known inapproximability bound for the problem, , which sits opposite the paper's own factor-2 algorithm. The same reduction pattern (machines as triples, dummy jobs that pin machines down) is reused in many later hardness proofs for scheduling and assignment problems.
Formalizing it. The result is proved on paper; no machine-checked version is known to exist. A formal proof requires the full combinatorial argument behind the reduction, including the counting of machines per type and the case where some element of lies in no triple, which the paper does not discuss. Together with mission 1 of this series (the factor-2 algorithm), it fixes both ends of the gap in one formal library.
The construction is short, but the converse direction carries the weight: from an arbitrary schedule with makespan at most one must recover a matching, although nothing in the schedule singles out the triples that form it. The obvious first idea, to read the matching off the machines that receive unit-time jobs, fails as it stands: a machine may receive one unit-time job or none, and the argument must exclude this for every schedule, including the degenerate instances in which some lies in no triple or triples repeat. For Corollary 2, the passage from the real-valued approximation guarantee to the threshold depends on the strict inequality ; at the statement is no longer implied by Theorem 5.
Fin m; 3DM elements are Fin n; a 3DM instance is T : Fin m → Fin n × Fin n × Fin n, so a triple may repeat. A matching is a set of triple indices covering every , , (the covering form of the paper's definition, which forces disjointness).MatousekLP.Scheduling.makespan applies. All statements quantify over every schedule, so the choice of bijection is irrelevant.Assortment optimization asks which products a retailer should offer when customers choose among the offered products according to a probabilistic choice model, so as to maximize expected revenue. Under the nested logit model the products are grouped into nests: a customer first picks a nest, then a product inside it. The model is the standard relaxation of the independence of irrelevant alternatives property of the multinomial logit, and it is used throughout revenue management and transportation demand modelling.
Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) classify the complexity of the assortment problem under four variants of the nested logit model, according to whether the dissimilarity parameters are at most one and whether a customer who picks a nest always buys there. The problem is NP-hard as soon as some dissimilarity parameter exceeds one (their Theorem 5), and also when the nests have positive no-purchase weights (Theorem 8), so for the general variant approximation is the realistic aim. §6.2 of the paper gives an approximation scheme for the most general variant: for any it restricts each nest to a short list of candidate assortments indexed by the powers of , solves a small linear program, and loses at most a factor of the optimal revenue. This mission formalizes the guarantee behind that scheme, Theorem 12.
There are nests and products in each nest. Product of nest has revenue and preference weight ; the products are ordered so that . Nest has a no-purchase weight and a dissimilarity parameter , and is the weight of leaving without choosing a nest. Offering in nest gives
The optimal expected revenue is the optimal value of the linear program (3): minimize subject to and for every nest and every . Problem (4) keeps the second family of constraints only for a candidate collection of assortments in each nest.
Let , assumed throughout §6, and fix . Put , , and let , be the least integers with , . For each level , problem (15) maximizes over the assortments with ; its value is . An assortment is feasible for (15) and satisfies . The candidate collection of nest is .
If is an optimal solution of problem (4) over the candidate collections , then
Theorem 12 is the analytical half of the approximation scheme. Together with the paper's Theorem 1 it shows that a linear program with variables and at most constraints yields an assortment within a factor of the optimum, for the most general variant, which is NP-hard, and Proposition 15 makes the candidate assortments computable. Letting trades accuracy for running time, so the result is the paper's answer to how well the general problem can be approximated by this LP approach.
The result is proved in the paper; the work here is to formalize the known proof. To the best of a search of the Prove2Me library (local index and platform mirror, October 2026), no nested logit approximation result, and no knapsack lemma matching Proposition 15, has a machine-checked statement or proof. The definitions of the shared model (the instance, , , , the linear programs (3) and (4)) are common to the six missions of this series.
The obvious argument compares an arbitrary assortment with the candidate of its level and uses the candidate's constraint in (4). This fails as a direct comparison because the nest weight enters twice with different exponents, in front of the revenue and in front of , and within one level may vary by a factor . When and when the monotonicity of goes in opposite directions, so the losses must be tracked separately by and , and they are absorbed by the common factor only because . The other half, Proposition 15, concerns a knapsack with both a lower and an upper bound on the total weight, where a feasible solution must be produced as well as a good objective value.
Products are Fin n ( for ), nests a finite type, powers real powers, and , which gives . The shared model carries the standing assumptions of §1 with the disclosed pins , and (the page allows and zero-weight padding products, under which its convention and its proofs fail). Every statement of the mission also assumes (for ), is the greatest of the (so at least one nest exists) with , and . Integer powers are zpow, and , are written , , which equal the minima of the paper. An optimal solution of (4) is a feasible pair whose is minimal among feasible pairs. The companion guarantee adds , the pin of Theorem 1. In Proposition 15 the capacity row of (33) includes , correcting a printed slip, and the running-time claim is not stated.
The assortments enter Theorem 12 as an arbitrary family with the two properties of p. 28; the theorem is stated for every such family. A level at which (15) has no feasible assortment imposes nothing on , as on the page. Requiring to lie in its level unconditionally would make the hypothesis unsatisfiable for most instances and the goal vacuous; that encoding, and any goal that assumes displays (34)–(36) or the exponent bounds, is ruled out.
Contributions welcome: proofs of the real-power milestones (3)–(5), which are self-contained, of the two cases (6)–(7), and of Proposition 15, whose fractional knapsack lemma (the greedy solution of a continuous knapsack sorted by ratio is optimal) is reusable beyond this mission.
A firm may know salary bounds and the ranking of positions without having a reliable sample of individual salaries suitable for least-squares estimation. Charnes, Cooper and Ferguson used that kind of partial information to estimate a salary formula from ratings assigned to job factors. Their 1955 paper gives a model in which weights respect the job hierarchy while the implied salaries approach specified salary levels as closely as possible. It then turns the sum of absolute deviations into a linear program that can be handled by the methods available for constrained optimization. The setting and transformation are in §§4–6 of the published paper.
The question here is a precise one: does the transformed program have the same optimal value and the same optimal salary weights as the original absolute-deviation problem? This matters because a linear-program solution should answer the compensation-estimation problem stated before the transformation, even though the transformed program has additional variables and a different feasible set. The mission also records the paper's seven-position numerical example, where the reported salary formula can be checked directly against the table of factor ratings.
There are rated factors and job levels ordered from highest to lowest. The rating is the amount of factor required at level , and is the nonnegative weight assigned to that factor. The estimated salary at level is
The salary formula applied to a person's factor amounts is . For the ranked positions, feasible weights satisfy the four parts of the paper's system (2): each ; the top-level salary is at most the ceiling ; successive salaries descend, ; and the bottom-level salary is at least the floor . These are one-sided ceiling and floor bounds. They do not force the fitted salaries to equal the bounds.
The firm specifies target salaries at a finite set of levels, which includes the ceiling and floor levels in the examples and may include intermediate levels. The absolute-deviation objective of (3) is
The original problem minimizes over the feasible weights. At a specified level, let . The split-variable program of (4)–(5) introduces with and minimizes . The split variables are constrained only for levels in . The salary constraints (2) continue to apply to . This is the paper's transformed linear program, with a feasible set that contains many choices of above the same weight vector Charnes, Cooper and Ferguson, §§4–5.
The main target is the paper's claim that the two problems have equal minimal values and that minimizers correspond §6, p. 143. In the formal statement, equal values are expressed by equality of attainable objective thresholds:
The goal also says that minimizes exactly when the triple formed from and the positive and negative parts of minimizes . Every LP minimizer projects to a minimizer of . These clauses give the value and solution correspondence the authors use when they call the two problems equivalent.
Three milestones follow the paper's exposition. First, every feasible weight vector has a split-variable lift with the same objective. Second, every transformed feasible point projects to an original feasible weight vector with no larger original objective. Third, the minimal values agree §§5–6, pp. 141–143. Each is recorded under the unnumbered sentence from which it was extracted; the paper has no numbered lemmas.
Two companion statements record other claims: opposite coefficient columns cannot both occur among selected independent simplex columns, and the Table I data have the reported optimum. For the latter, targets are 16 at , 10 at , and 4 at , measured in thousands of dollars. Equation (7) assigns weights , yielding the minimum deviation §7, pp. 145–148. A further companion checks the redundant ranking row.
The equivalence justifies using a linear-program output as an estimate for the earlier salary problem: the transformed objective reaches the same value, and its optimal weight vectors solve the original problem. The numerical claim supplies a fully specified instance with seven job levels and nine factors, including the exact fitted salaries. Without the correspondence, optimizing the enlarged variable set could give no assurance that its weights minimize the deviations the firm intended to measure.
The mathematical result was argued in the 1955 paper; this mission asks for a machine-checked formulation and proof of that known result. The statements compile as open Lean theorems, so compilation alone does not establish their truth. Closing them would add a reusable treatment of absolute-deviation objectives under finite linear inequalities and an exact certificate for the paper's worked example. The consistency claim in the appendix is a separate mission because it concerns perturbations of another linear program, not this transformation.
The split-variable program permits and to be simultaneously positive even when their difference is fixed. Consequently, simply identifying the two feasible sets would misstate the transformation: one has extra degrees of freedom. A proof must relate their objective values and then account for optimal solutions on both sides. The numerical example has a separate difficulty. Substituting the reported weights verifies a feasible objective of , but does not by itself rule out another feasible weight vector with a smaller deviation. The global lower bound is part of the companion theorem.
The Lean development represents factor and level vectors by functions on Fin n and Fin L, and sums explicitly over finite indices. Paper level 1 is Lean index 0; paper level is the final Fin L index. The assumption is explicit because both the top and bottom level are named. No sign, monotonicity, or boundedness assumptions are imposed on the ratings beyond what the paper states. The weights are componentwise nonnegative. Intermediate target salaries enter the objectives through but add no constraints to (2), matching the paper's treatment of .
A minimizer is a feasible point whose objective is no larger than that of every feasible point. The equality of minimal values uses the threshold formula above, so an empty feasible set cannot inherit a spurious real infimum. The transformed feasible set is exactly the split-variable system of (4)–(5); defining it as only the image of a chosen lift would make the principal comparison empty of content. The Table I constants are exact rational values in units of . The paper rounds some displayed salaries, while Lean records their exact fractions. The generic column-independence companion is stated for an arbitrary finite matrix, with the basis and zero nonbasic coordinates explicit.
The shared definition module provides the salary map, feasibility predicates, objectives, minimizers, and example data. A full development can contribute proofs of the three milestones, the main equivalence, the column claim, the numerical lower bound, and the redundant-row fact. The finite absolute-deviation and split-variable statements can also serve later formalizations with other linear constraints.
Minimum makespan scheduling on unrelated parallel machines asks for an assignment of jobs to machines, where job takes time units on machine , so that the largest machine load is as small as possible. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) it is . It models load balancing across heterogeneous processors, workers or production lines, and it is a standard test case for linear-programming rounding.
Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714; Mathematical Programming 46, 1990) gave a polynomial 2-approximation algorithm for and showed that no polynomial algorithm achieves a ratio below unless P = NP. They also asked which restrictions on the processing times keep the problem hard. Their Section 5 answers this when only two distinct processing times occur:
Theorem 7 is the paper's last result and closes this classification. Its proof generalizes the reduction of Theorem 4, which handles the case , from 3-dimensional matching to -dimensional matching.
Machines are indexed by and jobs by . A schedule assigns every job to exactly one machine. The load of machine is , and the makespan is the largest load.
-dimensional matching. An instance is a ground set of elements and a family of -element subsets of . A matching is a subfamily with and ; its members are then pairwise disjoint.
The instance of Theorem 7. Fix natural numbers that are relatively prime. Build a scheduling instance with machines, machine corresponding to , and two kinds of jobs:
Every processing time lies in .
The instance of Theorem 4. For disjoint sets , , of the same size and triples , , there are element jobs, one per element of , and dummy jobs. Machine processes the element jobs of , , in one time unit and every other job in three time units. A 3-dimensional matching is a subfamily of triples covering .
For relatively prime and a family of -subsets of a -element set, the instance above has all processing times in , and
The result. Theorems 6 and 7 together say exactly which two-valued restrictions of are tractable. Up to scaling, the polynomial case is , and every other pair with is NP-hard. Theorem 4 is the base case. It also yields Corollary 1 of the paper: no polynomial -approximation with exists unless P = NP. Reductions of this "no idle time" kind are a standard template for hardness of restricted-assignment and two-value scheduling, a line still active in the study of the restricted assignment problem and of the "graph balancing" special case.
Formalizing it. The result is proved, in two short paragraphs. The proof leaves to the reader the construction of the schedule from a matching and the "easy number theoretic argument" behind the converse, and both become explicit here. The development also produces reusable pieces: a -dimensional matching definition over an arbitrary family of -sets, and two reduction instances built on the published load and makespan of MatousekLP.Scheduling.Schedule. To our knowledge no machine-checked proof of these reductions exists.
The forward direction is a direct construction. The converse is where care is needed. A schedule with makespan at most may a priori place an element job on a machine whose tuple does not contain it, at length , and may mix element and dummy jobs on one machine. Looking at one machine at a time does not exclude either: a single machine can carry such a mixed load below . What excludes them is a property of the whole schedule together with the arithmetic of and . The hypotheses are sharp for this step: for element jobs are cheaper on foreign machines, and for a load with becomes possible.
Fin m. Schedules are maps from jobs to machines. Load and makespan are those of the published MatousekLP.Scheduling.Schedule, with natural-number processing times cast to . The jobs are enumerated as Fin (q * n + p * (m - n)) (Theorem 7) and Fin (3 * n + (m - n)) (Theorem 4), element jobs first, through finSumFinEquiv.Fin (q * n) and the family is indexed by machines, so repeated tuples are allowed. The -partite structure of -dimensional matching is not imposed: the reduction does not use it, and statements over all families of -sets contain the -partite case. Theorem 4 keeps the tripartite structure, with triples of indices in Fin n × Fin n × Fin n.MatousekLP.Scheduling.Schedule (it bounds every load; it is attained when ), which are reusable across scheduling reductions.A manufacturer launching a new product often depends on a single supplier for a critical component, and the supplier must build capacity before demand is known. The manufacturer usually knows more about demand than the supplier does: her sales force, market research and order history give her a forecast the supplier cannot verify, and she has a reason to inflate it, since more capacity costs her nothing if the supplier pays for it. Whether contracts can make forecast sharing credible, and at what cost to the supply chain, is the subject of Cachon and Lariviere, "Contracting to assure supply: how to share demand forecasts in a supply chain" (Management Science 47(5), 2001, doi:10.1287/mnsc.47.5.629.10486). Section 6.10 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents a simplified version of that model, and this mission formalizes it from the author's January 2003 draft.
The section separates two regimes. Under forced compliance the supplier must build exactly the capacity the contract specifies; under voluntary compliance he may build less. The section's conclusion is that forced compliance allows both coordination and credible forecast sharing, while voluntary compliance allows forecast sharing only at the price of under-investment in capacity.
Demand has one of two types with distribution function . The page assumes for , for (so demand has an atom at ), increasing and differentiable, and stochastic dominance for all . The supplier builds capacity at cost per unit; after demand is observed he produces at cost per unit; the manufacturer earns per unit of demand satisfied; unused capacity is worth nothing.
Expected sales with units of capacity are , and the supply chain's expected profit is
An optimal capacity maximizes over , and .
In an options contract buys options at each and pays for each option exercised. With her profit is and the supplier's is . The contract with share sets and . Under a wholesale price contract with price the supplier earns ; the price inducing capacity is with , and the manufacturer then earns .
With asymmetric information only observes . Let be the supplier's minimum acceptable profit, and define the shares
The low type offers the options contract with share and initial order , the high type the one with share and initial order . Assuming and :
the supplier earns from the low type and at least from the high type, and each initial order maximizes both firms' profits. The profit comparisons are stated between the contract profit functions, not between shares.
The goal shows that with forced compliance a high-demand manufacturer can share her forecast credibly through the terms of a coordinating contract rather than its form: both types use the same contract family, the supply chain is coordinated in every state, and the only cost of asymmetric information is that the high type may be unable to push the supplier down to his reservation profit. The voluntary-compliance milestones show the other side: once the supplier may under-build, only the wholesale price affects his capacity, and the resulting capacity is strictly below the integrated optimum. Together they explain why compliance regimes matter in capacity contracting.
The results are established on the page with short arguments; none has a machine-checked proof. Formalizing them requires the derivative of expected sales for a distribution with an atom, the first-order characterization of a concave maximizer on a half-line, and careful bookkeeping of the incentive constraints. The demand and profit definitions are reusable for other capacity-procurement and newsvendor-type models.
The incentive constraints look like arithmetic on shares, but the strict inequality needs : the low type's chain profit at the high type's capacity must be strictly below its optimum. The obvious argument via uniqueness of the maximizer is not available, because the page does not assume strictly increasing, so need not be strictly concave and may have a whole interval of maximizers. Likewise needs a strict comparison of integrals of distribution functions. In the voluntary-compliance part, the derivative of needs the density at , and fails when that density is .
Each demand law is a probability measure on and is Mathlib's cdf. is required to be differentiable only on , because the page's makes it jump at . is defined by the expectation , whose integrand is integrable because almost surely. Optimal capacities are passed as arguments characterized as maximizers over , never chosen; is footnote 46's assumption. Derivatives are HasDerivAt statements.
Hypotheses added relative to the page, all disclosed in the items: and in the goal (the page divides by and needs ); for the voluntary-compliance derivative (at it vanishes); and for the non-coordination result. The page's assumption is not needed and not imposed; its strict-concavity claim on p. 101 is not stated, because it would need strictly increasing. The prior does not enter any statement. The page's "separating equilibrium" is formalized by its defining incentive and participation conditions, not by a general signalling-game solution concept; a predicate that holds by construction of (for example ) is not an acceptable substitute for the profit inequalities. The fixed-fee condition of p. 105 is pure algebra on four numbers and is not included.
All definitions are local to the namespace CachonCoord.CapacityForecast. No platform theorem formalizes this model; the Snyder–Shen newsvendor definitions (SupplyChainTheory_contracts) and the revenue-sharing model of Cachon–Lariviere 2005 (RevShareCoord.*) concern different games and are not reused. Proofs of any milestone, and a sanity instance showing the model's hypotheses are satisfiable (for example demand with an atom at and an exponential tail, ), are welcome.
In most contracts of the supply chain coordination literature the transfer payments are fixed when the contract is signed: a wholesale price , a buy-back rate , a revenue share . Some settings need payments that respond to information arriving after signing, such as realized demand at several retailers and realized production output. Fixing the per-unit price in advance then fails twice: for some output realizations the retailers do not buy everything that was produced, and for others they want more than exists, so the supplier must ration, which invites strategic ordering and misallocation (Cachon and Lariviere, 1999).
Section 6.9 of Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003) studies an alternative after Kouvelis and Lariviere (2000): the supplier commits to hold an internal market for output after demand is observed, and pays her own production manager a fixed amount per unit of realized output. The model is a variant of Porteus and Whang (1991), who studied incentives between manufacturing and marketing managers in a firm. The section shows that this pair of mechanisms coordinates both the production decision and the allocation decision without the supplier observing either the demand shocks or the manager's effort.
This mission is part IX of a series formalizing the capstone results of that chapter.
One supplier employs a production manager and sells to two independent retailers. The constant demand elasticity is .
If retailer one receives the share of , total retailer revenue is
The optimal share is (Eq. (44)), and is revenue under it. The expected supply chain profit is , and the optimal effort solves the first-order condition (45).
In the decentralized system, if the per-unit price is , retailer 's profit is . The contingent price is
The manager is paid a fixed amount per unit of realized output. With , the payment is
and his expected utility is .
The goal has two parts.
The result shows that one mechanism handles two separate information problems. The market price is the shadow price of output. Charging it makes the retailers' independent orders add up to exactly the output and split it as the integrated firm would, and the supplier never needs to observe . Paying the manager the output-weighted expectation of that shadow price, a single number fixed in advance, aligns his marginal incentive with the supply chain's, and the supplier does not need to observe . The supplier breaks even on the market. Kouvelis and Lariviere (2000) show that in more general settings she breaks even or loses money, so any profit must come from fixed fees. The section therefore illustrates a general design principle: market-based transfer prices inside a firm, combined with linear output-based pay.
The derivations are short calculus on the page. Formalizing them pins down what the page leaves implicit: the range of efforts and allocations; the role of and of the integrability of the shock; the fact that each retailer's problem has a unique interior optimum only at a positive price; and how the realized output enters the expectation . To our knowledge none of these statements has been machine-checked before.
The deterministic part requires real-power calculus with a non-integer exponent . Strict concavity of has to be used on the closed interval , where the derivative blows up at the endpoints. The retailer's optimum has to be shown to be interior even though the profit at is defined.
The stochastic part requires pulling the effort out of the expectation, , pointwise in the shock, including at realizations with . The natural first idea, to differentiate under the expectation sign, is unnecessary but tempting. The obstacle it hides is that is undefined where , so the identity (46) only holds once is read as its limit at . Uniqueness of the manager's optimum depends on strict convexity of alone, since his payment is linear in .
All objects live in the namespace CachonCoord.InternalMarket. The deterministic file Revenue defines , (as the printed formula, not as an argmax), , and with real powers (Real.rpow). The file Model bundles a probability space with measurable and , the elasticity , and the cost . The cost is strictly convex and increasing on and has derivative at every . On top of these, Model defines , , the payment (46) (by its printed left side, not as the ratio it is claimed to equal), expected output and market revenue, and the manager's utility (from the payment scheme, not by the printed formula). Derivatives are HasDerivAt statements and optima are IsMaxOn over or .
The standing assumptions are those of the model paragraph on p. 92: risk neutrality and the distributional assumptions above. Added hypotheses, each disclosed in the item's Formalization Note:
The existence of an effort satisfying (45) is a hypothesis, as on the page. Clauses 1 of the goal are stated for fixed realizations, not as random variables.
A trivializing formalization would define as an argmax, or define the payment (46) as ; neither is done here. Outside and , Lean's real power returns junk values, and every statement restricts to that range. The companion claim that is the unique market-clearing price is not posed.
The formalization needs no infrastructure beyond Mathlib's real powers, convexity and Bochner integral. The concavity and first-order-condition lemmas for with may be reused for other constant-elasticity models. Contributions are welcome at any milestone; each is independent of the others except through the closed forms.
In a supply chain with stock at two locations, a supplier holds inventory that replenishes a retailer, and the retailer serves customers. Each firm sets its own inventory level to minimize its own cost. The retailer bears only part of the cost of customer backorders, and the supplier bears none of the retailer's holding cost, so their incentives differ. The resulting equilibrium generally differs from the policy that minimizes total cost. Cachon and Zipkin (Management Science 45(7), 1999) studied this game and proposed linear transfer payments that align the firms' incentives. In the chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003, doi:10.1016/S0927-0507(03)11006-7), Cachon re-derives that analysis, adds a parameter that divides the retail-level costs between the firms, and answers two questions the original paper left open: whether the contracts allow an arbitrary division of cost, and whether the optimal policy is the unique equilibrium under the contracts. This mission formalizes the second answer, together with the analysis of the decentralized game and of the optimal policy that it rests on (§6.8 of the 2003 chapter, read in the author's January 2003 draft).
Two firms, a retailer and a supplier , each use a base stock policy: firm keeps its inventory position equal to its base stock level . A negative supplier base stock means planned backorders. Let and be the demands during the retailer's and the supplier's lead times. They are nonnegative with finite means , , and their distribution functions , are continuous, zero at , strictly increasing on and differentiable on . Holding costs are and , with . Each backorder at the retailer costs the retailer and the supplier per unit time. Write .
At retailer inventory level the expected on-hand stock is and the expected backorders are . The retail-level cost rates are , and . Because the supplier may stock out, the retailer's actual inventory level is , and every retail-level quantity is averaged accordingly:
With the supplier's inventory and backorders , the firms' costs and the chain's cost are
A pair minimizing is an optimal policy. A Nash equilibrium is a pair from which neither firm can lower its own cost by a unilateral change of its base stock.
Under a linear transfer the supplier pays the retailer (a negative amount is a payment the other way). The Cachon–Zipkin contracts with parameter are
If is optimal with and , then under the contracts
is a Nash equilibrium, and it is the only one. The goal contains no numerical constants. It holds for every demand distribution in the class and every in the range.
The goal says that a contract built from quantities both firms can measure, namely the retailer's inventory and backorders and the supplier's backorders, makes the system-optimal policy the only equilibrium. The firms therefore reach the optimum without coordinating on an equilibrium. The parameter splits the retail-level costs between the firms in any proportion up to . Milestone 2 shows the contract is needed: without transfers, decentralization is always strictly suboptimal when the supplier is charged for retail backorders. The transfers and are those of the single-location model (§6.7), even though the retailer's target fractile changes from to .
The results are proved in the source and in Cachon and Zipkin (1999), with informal derivative arguments. No machine-checked version is known. Formalizing them requires differentiating expectations of piecewise-linear convex functions of a random lead-time shortfall. The page's argument also assumes densities, which the formal statements avoid, and contains several printing slips (see below). These would be settled by a complete development.
The firms' costs are compositions: a convex single-location cost evaluated at the random level , which is concave in . The supplier's cost is therefore not obviously convex in ; its convexity at depends on the value of and on . Uniqueness is the hard part. Under the contracts the retailer's best response decreases, but the supplier's marginal cost along that best response, , is not monotone in general when is small, contrary to a literal reading of p. 84. A uniqueness argument has to show that it has at most one zero, not that it increases.
Demand laws are probability measures on with no mass below , finite means, and continuous distribution functions, zero at , strictly increasing on and differentiable on . These are the section's standing assumptions, together with and (footnote 34 excludes the zero cases). Expectations are Lebesgue integrals: , , and the two-location averages are defined by expectation, and the page's integral forms are consequences. Integrals against are written against the law of , so no density hypothesis is made. Base stocks range over all of , and "optimal" means minimizing over ; the existence of an optimum is a hypothesis, as on p. 77. Derivatives are stated with HasDerivAt. Independence of and , implicit on the page, enters only through the convolution of their laws in (38).
The contracted costs are defined from the firms' original costs and the transfer payment. Defining them by the closed forms (42)–(43) would make the identities trivial and is ruled out.
Corrected slips: (42) is stated with where the page prints (the difference does not depend on ). The retailer's single-location fractile on p. 79 is stated as , not the printed . The garbled display after (43) and the / slip in the best-response derivative are not reproduced. Not included: the contraction condition (34), the case split for the optimal policy (p. 84), the case , and the alternative schemes of §6.8.5 (Lee–Whang, Chen). Contributions of those, or of a reusable library for derivatives of , are welcome. The platform's Clark–Scarf items (InventoryControl_clarkScarf, ClarkScarf.Serial.*) concern periodic-review echelon policies and are not reused.
In 1983 H. W. Lenstra, Jr. proved that integer linear programming with a fixed number of variables is solvable in polynomial time (Lenstra 1983). The algorithm became one of the founding results of algorithmic geometry of numbers: it introduced the strategy of making a convex body "round" by a linear change of coordinates, and then either finding a lattice point in it or showing that the body is covered by few parallel lattice hyperplanes, which reduces the dimension by one.
The algorithm rests on two geometric facts, each with its own proof. The first (§1 of the paper, the companion mission Integer Programming with a Fixed Number of Variables 1) says that a round body that misses the lattice meets few lattice hyperplanes. This mission is the second (§2): an explicit construction of the rounding transformation. Starting from a simplex inside the polytope, the algorithm repeatedly swaps a vertex for a point of the polytope as long as this increases the simplex's volume by more than a factor . When no such swap exists, a linear map that makes the simplex regular also makes the polytope round, with an explicit roundness ratio .
Short timeline. Khachiyan's ellipsoid method (1979) made linear programming polynomial and supplied the subroutine that Lenstra uses to maximize linear functions on . Lenstra's algorithm (preprint 1981, published 1983) combined it with the lattice basis reduction of Lenstra, Lenstra and Lovász (1982). Remark (c) of the paper notes that rounding with a maximal-volume inscribed ellipsoid achieves the better ratio , but not by a polynomial algorithm for varying ; later work (Kannan 1987, Grötschel–Lovász–Schrijver 1988) refined the rounding step with ellipsoid methods.
Work in with the Euclidean length , and write for the closed ball. For points , the simplex volume is
where has column vectors .
Let be convex, and let with linearly independent. Choose linear functions with
Thus measures the height above the facet opposite . The stopping condition of the second stage is
The ratio is the factor by which the volume changes when is replaced by , so (16) says that no such swap enlarges the simplex by more than .
Let be a nonsingular linear map of such that span a regular simplex, meaning that all distances , , are equal. Let be its centroid and its convex hull. For , the paper defines
The proof of the LEMMA works in model coordinates. There is the hyperplane of , the are the standard basis vectors, , and .
Under (15) and (16), with making the simplex regular and its centroid, there are positive reals with
These are conditions (3)–(4) of §1 with .
The paper's own proof derives the goal from milestone 1 and the LEMMA at . At the constant cannot be improved by this argument.
The result. The theorem is the only place in the paper where the roundness constant is computed, and enters the bound on the number of lattice hyperplanes that the algorithm branches over. Remark (c) of the paper uses the exact LEMMA for other values of to obtain ( even) and ( odd). The LEMMA itself is a self-contained fact about the regular simplex. In Euclidean geometry it says how far the "volume- neighbourhood" of a regular simplex extends.
The formalization. The result is classical and proved in the paper. Nothing in it has been machine-checked: there is no regular simplex in Mathlib, and no formal result relates simplex volumes to barycentric coordinates in this form. The platform has the related ellipsoid rounding ConvexOptimization.lowner_john_polytope_rounding (the John-ellipsoid version with factor , by Shuze Chen) and its definition ConvexOptimization_IsLownerJohn. That is the alternative construction of Remark (c). It has a different constant and is not used here. This mission and its companion together give a formal account of the geometry behind Lenstra's algorithm. The algorithm itself is not formalized: its running time needs a machine model and an encoding that the paper does not fix.
There are two separate difficulties. The first is the translation in milestone 1. It needs the volume of a simplex with one vertex replaced to be identified with a barycentric coordinate, through a determinant identity, and it needs this identification to survive the linear map . The second is the transfer to the model. The paper's "similarity transformation" identifies with a hyperplane of and sends the regular simplex to the standard one. In Lean the vertex description (milestone 2), the radii (milestones 3–4) and must all be carried across this isometry up to scaling. The LEMMA is stated in , not in the model. The "straightforward analysis" behind milestone 2 is a vertex enumeration of a cube cut by a hyperplane, and its parity split is where sign errors appear.
EuclideanSpace ℝ (Fin n) and the model is EuclideanSpace ℝ (Fin (n+1)). Distances are Euclidean, never the sup norm. Vertices are indexed by Fin (n+1), matching .A supplier that sells through many competing retailers usually worries that competition among them pushes orders too high, because each retailer ignores the demand it takes from the others. Deneckere, Marvel and Peck (1997) identified the opposite failure. When the retail price is set by the market after demand is realized, retailers who hold too much stock in a weak market bid the price down, and anticipating this, perfectly competitive retailers order too little. The supplier then needs a contract that raises orders, and the classical justification for resale price maintenance (a price floor imposed on retailers) comes out of this model. G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents the model in §6.5.2 as a closed-form example. In it the supplier's best wholesale price contract is computed explicitly and compared with two contracts that recover the monopoly profit: resale price maintenance and a full-refund buy-back.
This mission is volume V of a series that formalizes the section capstones of that chapter, read in the author's 3rd draft (January 2003), pp. 53–58.
Fix . Industry demand is low or high, each with probability . If the retailers hold a total stock , the market clearing price is
Leftover inventory has no salvage value, and the supplier's production cost is zero.
Perfect competition means the retailers keep ordering until expected profit is zero. The competitive order is the with and on . The supplier earns .
The page's notation , , and is kept in Lean under the names q1, q2, supplierProfit, wStar.
With
the goal states four things:
The goal shows that in this model a wholesale price contract always falls short of the integrated profit, whatever . It also shows where the shortfall comes from: at the optimal wholesale price the low-state market price falls below the monopoly price (milestone 4). Restoring the monopoly profit therefore requires a mechanism that holds the low-state price at . Resale price maintenance and a full-refund buy-back both do this, so the section gives a closed-form efficiency argument for vertical restraints that are often treated as anticompetitive. The section also contrasts the buy-back with revenue sharing, which coordinates the single newsvendor (§6.2) but not this model.
The results are proved on the printed pages by elementary algebra. None of them has a machine-checked proof, and nothing on Prove2Me covers this model. The mission produces checked versions of the case analysis, including the tie and the two regimes of the competitive order. It also adds a reusable encoding of "perfect competition" as the first zero of aggregate expected profit.
Every statement reduces to one-variable inequalities, but the case structure is easy to get wrong.
All quantities are real numbers and throughout. The continuum of retailers enters only through the total order. No measure space of retailers is formalized, and footnote 26's multiplicity of individual equilibria is not stated. The sales rules under resale price maintenance (proportional allocation) and under the buy-back (price floor ) are written into the contract definitions, as the page describes them in words. The theorems use only .
The formulas , , and are definitions transcribed from the page. That they are the competitive order and the optimum is the content of the theorems. Defining or the competitive order by its closed form would trivialize the mission, so the competitive order is defined only by the zero-profit property and as a greatest element of the monopolist's feasible profits. The goal is stated over all real wholesale prices, so it also rules out profitable prices outside . Uniqueness of is not asserted at .
The chapter's standing assumptions used here are risk neutrality and full information, together with the model paragraph of pp. 53–54 (two equally likely states, zero salvage value, zero production cost). No platform definition is referenced: no published item formalizes this model.
A supplier selling through a retailer earns more when the retailer works harder at selling. Examples are a better shelf position, more knowledgeable sales staff, local advertising and keeping the display in order. These activities cost the retailer, raise demand, and usually cannot be observed or verified by the supplier, so no contract can be written on them directly. Chapter 6 of the Handbook of Operations Research and Management Science, Vol. 11: Supply Chain Management (G. P. Cachon, Supply Chain Coordination with Contracts, 2003) surveys contracts that align a retailer's decisions with the interest of the whole supply chain. Its §6.4 asks which of these contracts survive when the retailer also chooses such an unverifiable effort level.
The question goes back to the marketing literature on retail effort (Chu and Desai 1995, Desai and Srinivasan 1995, Desiraju and Moorthy 1997, Lal 1990, Lariviere and Padmanabhan 1997). It was taken up for newsvendor contracts by Taylor (2000), who showed that a sales rebate combined with a buy back restores coordination, and by Krishnan, Kapuscinski and Butz (2001), who let effort be chosen after demand is observed. This mission is the third in a series that formalizes the chapter's section capstones. It covers §6.4.1.
One supplier sells to one retailer for a single selling season. Before the season the retailer chooses an order quantity and an effort level . Effort costs him , where , and . Demand given effort has distribution function on , with and strictly increasing. Demand is stochastically increasing in effort: for . Units sell at the retail price and cost to produce. Goodwill costs, the salvage value and the retailer's own unit cost are zero. Expected sales and the integrated channel's profit are
Let maximize . A contract fixes the transfer the retailer pays the supplier, as a function of what the supplier can verify: the order and, for some contracts, sales or leftover units, but never effort. The contracts compared are the buy back , quantity flexibility , revenue sharing , the sales rebate and the quantity discount . Under each, the retailer's profit is his revenue less the transfer and .
The goal combines the section's negative and positive results.
the following hold for every . The retailer earns and the supplier earns . The retailer's marginal profit of effort equals the channel's. His optimal efforts are the channel's. 3. The optimal order. If maximizes , both firms' profits at effort are maximized by .
The milestones follow the section's own claims: the integral form of (p. 41); the first-order condition (18) for the chain-optimal effort; (19); the analogous strict inequalities for quantity flexibility () and revenue sharing (), and the reverse inequality for the sales rebate (, ); the two displays of under the quantity discount; and the fact that decreases in .
The result separates two jobs a contract does. To coordinate the order quantity, buy backs, quantity flexibility and revenue sharing all shield the retailer from part of the demand risk or take part of his revenue. The same shield dulls his incentive to raise demand, so each one leads him to under-invest in effort. The sales rebate pushes the other way, toward too much effort. The quantity discount works because the retailer keeps every unit of realized revenue and bears all of his own effort cost. The schedule then prices the order against expected revenue at the optimal effort, so the order is coordinated without touching the effort incentive. Because with free in , any split of the channel's optimal profit is attainable. The chapter extends this observation to retailers that also set price (p. 43).
The section's claims are proved on the page only in outline; several are introduced with "it can be shown". To our knowledge none has a machine-checked proof. Formalizing them requires differentiating expected sales in a parameter of the demand law. That step recurs throughout stochastic inventory and pricing models.
Most of the algebra is short. The substance is in the derivatives. is a differentiation under the integral sign. The strict inequalities need this integral to be strictly negative. That in turn needs to be integrable and negative on a set of positive length, which is why (and for the sales rebate) matters.
The natural reading "the quantity discount makes the retailer's joint optimum" is not what the page shows, and it fails in general. The page gives two partial statements: for each fixed the retailer's effort incentive is the chain's, and at his best order is . Since , the retailer can gain by moving and together when is small. The goal states exactly the two partial claims.
The Lean namespace is CachonCoord.EffortNewsvendor. A structure Model collects the data: and with ; a family of demand laws indexed by effort (probability measures on with finite mean, no atom at , strictly increasing distribution function); the effort derivative , negative for , ; and with and positive first and second derivatives for . is defined as an expectation, and its integral form is a milestone. Derivative claims are HasDerivAt statements at interior efforts . The inequalities assert that both derivatives exist.
The following hypotheses are standing assumptions or disclosed additions:
Revenue sharing and the sales rebate use §6.2's profit functions (pp. 21, 27) with this section's zeros, less .
The page prints the last term of as . With that sign the page's own displays and fail by . The formalization uses , under which both hold. is the explicit printed schedule with this correction. It is not defined as "a schedule with ", which would make the goal empty.
Not covered: the price-and-effort schedule at the bottom of p. 43, for which the page gives no argument. The cachon-2005 revenue-sharing effort results (RevShareCoord.Effort.*, deterministic revenue ) are a different model and are not referenced. Proofs of any milestone, and a reusable library for differentiating newsvendor expectations in a parameter, are welcome.
Strictly convex quadratic programs — minimize a positive definite quadratic subject to linear inequalities — are the subproblems solved at every iteration of successive quadratic programming (SQP) methods for nonlinear optimization, and they arise directly in least-squares estimation with constraints, portfolio selection and model predictive control. In SQP the unconstrained minimizer of the quadratic model is available at no cost, while a feasible point is not.
D. Goldfarb and A. Idnani (Math. Programming 27 (1983) 1–33) proposed a dual active-set method that exploits this asymmetry. It starts at the unconstrained minimizer, which is optimal for the problem with all constraints removed, and adds violated constraints one at a time while keeping the current point optimal for the subproblem defined by the current active set. No phase 1 is needed. The method, usually called the Goldfarb–Idnani algorithm, is the basis of widely used solvers (for example the quadprog package in R and QuadProg++), and the paper proves that it terminates finitely with a correct answer.
Earlier dual methods for quadratic programming include the modified-simplex methods of Lemke (Management Science 8 (1962) 442–453) and of Van de Panne and Whinston (1964), which the paper compares with its own in Section 7.
Fix , a vector , a symmetric positive definite matrix , an matrix with columns , and . The quadratic program (1.1) is
The gradient is . For , the subproblem keeps only the constraints indexed by ; is solved by . A set is linearly independent if the normals , , are.
For an independent , let be the matrix with columns , , and define
The multipliers are ; for a constraint with normal the infeasibility multipliers are ; a superscript denotes the same objects for .
An S-pair is an independent active set with for and optimal for . A V-triple has , independent, , for , and .
The dual algorithm starts from . In Step 1 it stops if is feasible; otherwise it picks any violated constraint . In Step 2 it moves along the primal direction and the dual direction with step , where is the largest step that keeps the multipliers nonnegative and makes constraint active. If both are infinite it reports infeasibility. A full step () adds and returns to Step 1. A partial step (), or a dual step (), drops a constraint attaining and repeats Step 2.
For every choice of the violated constraint and of the dropped constraint :
Theorem 3 is the correctness certificate of the Goldfarb–Idnani method: whatever rule an implementation uses to choose the entering and leaving constraints, it cannot cycle and its answer is right. In particular the infeasibility verdict is a proof that (1.1) has no feasible point, which matters in SQP where infeasible subproblems trigger a different branch of the outer method. The intermediate results (the operator identities, Lemma 1, Theorems 1–2) are the standard analysis of dual active-set methods for quadratic programming.
The result is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces verified projector identities for and , a verified KKT characterization for equality-active subproblems, and a verified finite-termination proof for a nondeterministic algorithm with an explicit step relation. The platform already has a proved KKT sufficiency theorem for general convex programs (ConvexOptimization.kkt_sufficient_for_convex), stated over EuclideanSpace with general convex functions and gradient fields; it can serve as background for the sufficiency half of milestone 2, but it is not stated in this mission's matrix objects.
The obvious termination argument is that increases strictly at every iteration and there are finitely many active sets. It fails as stated: partial steps may leave unchanged (the dual steps of Step 2(c)(ii)), so is only nondecreasing between consecutive states. A termination proof therefore needs a measure that also decreases along steps that do not move . Any such argument relies on invariants (independence of , nonnegativity of the multipliers, along partial steps) that hold only on reachable states, and the operators and are meaningful only while those invariants hold. Correctness of the infeasibility verdict requires the dependent case (Theorem 2), not only Theorem 1.
Vectors are Fin n → ℝ, is Matrix (Fin n) (Fin n) ℝ with G.PosDef, is Matrix (Fin n) (Fin m) ℝ, and active sets are Finset (Fin m). Multiplier vectors are indexed by constraint index (Fin m → ℝ, zero off the active set), not by position in . Lean's matrix inverse returns for singular matrices, so every statement about and assumes and an independent active set (directly, or through an S-pair or V-triple).
The algorithm is the inductive relation Step on states step1 x A u, step2 x A p u⁺, stopOptimal x, stopInfeasible, with one transition per admissible choice of and . Infinite step lengths are separate transitions; a tie takes the full step, as the paper tests first. The running value of and the factorizations of Section 4 are not part of the state.
Explicit readings of the paper's words:
Step transitions from the Step-0 state, and every reachable state without a successor is a STOP whose verdict is correct (optimal for (1.1), or (1.1) infeasible);Property (2.10), printed , is false unless and is not formalized. Equality constraints (1.2), Section 4 (numerically stable implementation), Sections 5–6 (computations), Section 7 (comparisons) and the Appendix example are out of scope.
A trivializing formalization is ruled out: the goal quantifies over every run of the relation (not one selection rule, not "some run terminates"), the infeasibility verdict is about (1.1) itself, and the algorithm is a relation that always has a successor until a STOP, so correctness cannot hold because a run gets stuck.
Needed infrastructure: Schur-complement and projector identities for and ; first-order optimality for convex quadratics on affine subspaces with inequality multipliers; well-foundedness arguments for a nondeterministic relation. The operator identities and the KKT characterization are reusable for other active-set and SQP analyses. Contributions of proofs of any milestone, and of reusable lemmas about and , are welcome.