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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
In quantum mechanics the energy levels of a system are the eigenvalues of a self-adjoint Hamiltonian , and for almost every Hamiltonian of interest (atoms with more than one electron, molecules) they cannot be computed in closed form. What can be computed are expectation values of explicit trial functions . The min-max principle turns such numbers into rigorous statements about the eigenvalues: every trial computation gives an upper bound, and the optimal choices reproduce the eigenvalues exactly. It goes back to Fischer (1905) for quadratic forms in finitely many variables and to Courant (1920) for differential operators; Temple (1928) added the matching lower bound. This mission formalizes the version for unbounded self-adjoint operators with essential spectrum, as stated in Chapter 4 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), where eigenvalues below the essential spectrum are characterized and estimated.
Let be a complex Hilbert space, with inner product conjugate linear in the first argument. An operator is a linear map defined on a subspace , its domain; is self-adjoint if is dense and equals its adjoint. The resolvent set is the set of for which is a bijection with bounded inverse, and the spectrum is . For self-adjoint , .
For the eigenspace is ; is an eigenvalue when it is nonzero, and its dimension is the multiplicity. The discrete spectrum consists of the eigenvalues that are isolated points of and have finite multiplicity, and the essential spectrum is .
Let ( if is empty). The numbers are the eigenvalues of below , listed in increasing order and repeated according to multiplicity; if there are only of them, for . For vectors let
Some statements involve the spectral projections of , for Borel sets : the projection-valued measure with . With the spectral measures , the form domain is , and on it means .
For self-adjoint and every ,
Both sides are extended real numbers; the infimum over an empty set is .
The min-max principle is the standard tool for comparing eigenvalues of different operators: Corollary 4.11 (monotonicity under operator inequalities) follows from it, and with it the stability of eigenvalues under perturbations, Dirichlet–Neumann bracketing and the Rayleigh–Ritz method used in computational quantum chemistry. Theorem 4.12 converts a finite-dimensional computation into a lower bound for the number of eigenvalues in an interval, and Temple's inequality supplies lower bounds on an eigenvalue to complement the variational upper bounds, which is what makes numerical eigenvalue enclosures rigorous.
All of these results are classical and proved in the literature. What is not available is a machine-checked version for unbounded operators: Mathlib has the Courant–Fischer characterization only for finite-dimensional or compact self-adjoint operators, and existing formal developments of Temple's inequality and min-max levels treat bounded operators. This mission formalizes the unbounded case, with the essential spectrum and the counting of eigenvalues by multiplicity made explicit, and with the edge cases (operators unbounded below, empty essential spectrum) covered by extended-real values.
The central difficulty is that is defined by spectral data (which points of the spectrum are isolated eigenvalues of finite multiplicity, and how many there are below a given level), while the right-hand side is defined by expectation values on the domain. Relating the two needs the spectral theorem for unbounded operators: for every level below the spectral subspace must be shown to be finite dimensional and spanned by eigenvectors, and for the level itself one needs infinite-dimensional spectral subspaces in every neighbourhood, which is where the essential spectrum enters. When the supremum and infimum need not be attained, so the finite-dimensional argument with eigenvectors does not transfer. For Corollary 4.11 and Temple's inequality the hypotheses concern only the operator and one vector, while the conclusions concern the spectrum.
The formalization uses Lean 4 with Mathlib. Operators are partially defined linear maps (LinearPMap, H →ₗ.[ℂ] H) on a complex Hilbert space; self-adjointness is Mathlib's IsSelfAdjoint, which includes a dense domain. The Hilbert space is not assumed separable. The spectrum is the resolvent spectrum defined above, not Mathlib's Banach-algebra spectrum, and for self-adjoint operators it enters through its real points. Eigenspace dimensions are cardinals (Module.rank). is defined from the spectrum, the essential spectrum and these dimensions, as an element of EReal, indexed from ; if is unbounded below its value is , and if the essential spectrum is empty and the eigenvalues run out it is . The min-max identity is stated in EReal, with entering through its real part.
A formalization that defines as the min-max expression itself would make the goal true by definition. This is ruled out: is defined only from the spectrum, the essential spectrum and the dimensions of eigenspaces.
The spectral theorem is not part of this mission. Theorem 4.12 takes a projection-valued measure on the Borel sets of as data, together with the hypothesis that (domain and ), which is the form the spectral theorem guarantees; is then , and and the quadratic form are defined from it. Nothing else the book derives is taken as a hypothesis. The goal, Theorem 2.19, Corollary 4.11 and Temple's inequality use no projection-valued measure. Corollary 4.11 states the domain inclusion explicitly, as the meaning of .
A complete development needs the spectral theorem for unbounded self-adjoint operators (or an equivalent functional calculus), the identification of with the points where spectral projections have infinite rank, and the orthogonality of eigenspaces. These are reusable across the rest of the book. Proofs of any milestone, and of lemmas connecting the resolvent spectrum with spectral projections, are welcome.
Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: an algorithm must not only compute a good solution but also pay the agents so that reporting their data truthfully is in their own interest. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001) with task scheduling on unrelated machines as the model problem. Each machine is owned by an agent who alone knows how long it takes for each task; the designer wants a schedule of small make-span.
The paper gives a truthful mechanism, MinWork, whose make-span is within a factor of optimal, and a lower bound of for every truthful mechanism. It conjectures that no truthful mechanism beats (Conjecture 4.9) and proves the conjecture for two natural classes. This mission is about one of them, additive mechanisms (Theorem 4.10, p. 180).
Timeline of the gap between and :
There are agents and tasks . The type of agent is a vector of positive reals, being the time agent needs for task ; a type vector collects all types, and denotes the types of the agents other than . An allocation is a partition of the tasks, being the set given to agent . For a set of tasks write . The make-span is
A direct mechanism maps every declared type vector to an allocation and to payments handed to the agents. An agent with true type gets utility . The mechanism is truthful if, whatever the others declare, no agent gains by declaring a type other than its true one. It is a -approximation if for every positive type vector and every allocation .
The price offered for a set to agent (Definition 12) is the payment at any declaration for which the mechanism gives agent exactly , and if there is no such declaration. For truthful mechanisms this is well defined (Proposition 4.4, Independence). The mechanism is additive (Definition 13) if
for every agent , type vector and set of tasks. MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is additive.
For agents and tasks, for every truthful additive mechanism and every real ,
The goal leaves the mechanism, its tie-breaking and completely general. It says that the ratio of MinWork is optimal among additive mechanisms.
Theorem 4.10 shows that the gap between MinWork's ratio and the general lower bound cannot be closed by any mechanism that prices tasks separately, and so any better mechanism would have to couple the prices of different tasks. It was the first class-restricted confirmation of Conjecture 4.9, which was eventually proved for all truthful mechanisms (Christodoulou–Koutsoupias–Kovács 2023). The additive case is the cleanest entry point: its proof needs only the two basic properties of truthful mechanisms, Independence and Maximization, which every later lower bound also uses.
All results here are proved on paper, and none has a machine-checked proof on Prove2Me as of this mission's drafting. The mission produces a formal model of scheduling mechanisms and prices that other lower bounds can reuse, formal statements of Independence and Maximization, and a formal proof of Theorem 4.10. Along the way the formalization corrects two points of the printed argument (see Formalization scope).
The work is to extract prices from an arbitrary truthful mechanism. Prices are defined through the attainable sets of Definition 12. A natural first idea replaces the mechanism by per-task prices that the agent maximizes against. That gives a different class, because Definition 13 constrains the price of every set of tasks, including sets the mechanism never allocates, whose price is .
Claim 4.11 is the critical step, and its printed argument does not go through for an arbitrary truthful additive mechanism. It needs the empty set to be attainable with price . For a mechanism with a bounded ratio this holds, because a very slow agent must receive nothing, but this has to be derived from the approximation hypothesis. From that, one has to show that every task of carries a single-task price of at least . The final step also needs care. The paper's "w.l.o.g. " is a further reduction, and the paper's bound has to be replaced by .
Fin n, tasks Fin k, type vectors Fin n → Fin k → ℝ, and an allocation is a map Fin k → Fin n sending each task to its agent. taskSet x i is , and the make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]). A mechanism is a pair alloc, pay of arbitrary functions; nothing about its tie-breaking is fixed.price follows Definition 12 literally: the payment at a Classical.choose witness declaration when the set is attainable, and otherwise. Additivity (IsAdditive) is required for every set of tasks, attainable or not, as Definition 13 states. It is a condition on prices, not on the payment function.The capacitated vehicle routing problem (CVRP) asks for minimum-cost routes, starting and ending at a depot, that serve every customer exactly once without any vehicle carrying more than its capacity. It is one of the central problems of operations research and logistics, and exact algorithms for it have been built on branch-and-cut for three decades: a linear programming relaxation is strengthened at every node of a search tree by adding valid inequalities that the current LP solution violates.
The most important of these inequalities are the capacity inequalities. Deciding whether an LP solution violates one of them is strongly NP-hard, so practical codes rely on heuristics, and most heuristics first shrink the support graph: groups of customers are contracted into single supervertices so that the search runs on a smaller graph. Shrinking is only useful if it is safe, meaning it cannot hide a violated inequality. Before the work of Lysgaard, Letchford and Eglese, the standard safe rule allowed shrinking a single edge whose LP value is at least one (Augerat et al. 1998; Ralphs et al. 2003). Lysgaard, Letchford & Eglese (2004), whose separation routines were released as the widely used CVRPSEP package, generalized the rule to customer sets of any size in their Proposition 1, the only numbered result of the paper.
Let be the complete undirected graph on . Vertex is the depot and are the customers. Vehicles have capacity and each customer has an integer demand with . An LP point is a vector ; and are the same variable, and LP solutions satisfy .
For a vertex set , is the set of edges with exactly one end-vertex in (edges to the depot included), and is its cut value. For a customer set :
The capacity inequalities and the rounded capacity inequalities (RCIs) are
The violation of such an inequality at is (resp. ); it is violated when this is positive.
Shrinking a customer set contracts it to one supervertex. The supervertices of the shrunk graph are then and the single customers outside , so a union of supervertices is a customer set with or . Shrinking is safe if for every customer set with whose inequality is violated, there is such a union with and at least the same violation.
For every and every customer set with
shrinking is safe for the capacity inequalities .
Proposition 1 justifies contracting whole groups of customers before running separation heuristics, which shrinks the graph those heuristics work on while preserving every violated capacity inequality up to its violation. The rule is part of the separation routines of CVRPSEP and of later branch-and-cut and branch-cut-and-price codes for vehicle routing that reuse them.
The result is proved in the paper; to the best of the platform's records, none of it is formalized. The mission produces a reusable formal layer for the two-index CVRP formulation: cut values on the complete graph with a depot, the bin-packing number, the rounded capacity bound, and the notion of safe shrinking. Submodularity of the cut function (target 2) is a classical fact that the paper cites rather than proves; the platform already has a related statement for symmetric weight matrices on Boolean regions (EmergentGeometry.cutWeight_submodular), in a different representation. Target 5 records a claim of the paper that it asserts without proof.
When the violated set contains or misses it, itself is a union of supervertices and there is nothing to show. The difficulty is a set that crosses : no union of supervertices is obviously as violated as , because enlarging can raise its cut value — can be smaller or larger than depending on the edges leaving — and the hypotheses on say nothing about directly. Both hypotheses on and the sign condition matter here; for signed the statement fails. A violated strictly inside is not a crossing set in the paper's sense and has to be handled as well.
On the formal side, the bin-packing number is an optimum of a combinatorial problem; its properties must be derived from a definition by assignments to bins, and it is well defined only because every demand fits in one vehicle. Target 5 needs a structural understanding of integer points satisfying the degree equations, which the paper does not supply.
Vertices are Fin (n+1), the depot is 0, and a customer set is a Finset (Fin (n+1)) not containing 0. The edge vector is a function x : Sym2 (Fin (n+1)) → ℝ on unordered pairs, and the cut value is ∑ i ∈ S, ∑ j ∈ Sᶜ, x s(i, j), which includes the edges to the depot. The capacity is real (the paper does not say it is an integer) and demands are natural numbers with for customers. The bin-packing number is the least number of bins over assignments of the customers of to bins of total demand at most ; under this minimum exists. Of the LP point only is assumed in Proposition 1 and targets 1–4, which is at least as strong as the paper's setting. The hypothesis " for all " ranges over nonempty proper subsets.
A formalization that lets in that hypothesis is vacuous, because ; one that drops the condition " or " from safe shrinking is trivial (take ); and one that defines as , as an arbitrary monotone function, or with a junk value , or that omits the depot edges from the cut, states a different result. None of these is the mission's statement.
Needed infrastructure: finite sums over cuts of Sym2-indexed vectors, a working API for the bin-packing number, and, for target 5, connected components of the support graph (SimpleGraph.Reachable). The cut-function lemmas and the bin-packing number are reusable for any later formalization of CVRP polyhedra (framed capacity, comb and multistar inequalities). Contributions of general lemmas about cut functions on complete graphs are welcome as separate theorems.
Column generation solves linear programs with far more columns than can be written down: a restricted master problem holds a few columns, its dual multipliers are passed to a pricing problem, and the pricing problem returns a column to add. It is the standard engine behind branch-and-price for vehicle routing, crew scheduling and cutting stock, where the master problem is very often a set-partitioning problem (Lübbecke and Desrosiers 2005; Desrosiers and Lübbecke 2005).
Which column the pricing problem returns matters. The classical Dantzig rule picks the column of most negative reduced cost, but in set-partitioning masters with identical subproblems this rule tends to produce columns that are "weak" in the dual: their dual constraint is implied by the constraints of smaller columns. Sol (1994, PhD thesis, Eindhoven) called such columns redundant and studied pricing rules that avoid them. In their survey, Lübbecke and Desrosiers state the key fact as Proposition 2 (Operations Research 53(6), p. 1016): under ratio pricing, a strictly redundant column is never the optimal choice.
Let the rows of a set-partitioning master problem be . A column is a subset of the rows, with incidence vector ( iff ). Let be a finite collection of nonempty columns with costs . The master problem is
with integer in the integer program. Its dual has one free multiplier per row and one constraint per column.
A column is redundant, eq. (30), p. 1015, if
with and ranging over the columns of that are proper subsets of ; then its dual constraint is implied by those of its subcolumns. It is strictly redundant if the cost inequality is strict. The pair has the subcolumn property if for all with . Given dual multipliers , the ratio pricing problem (31) is
the reduced cost per covered row. In Lean these objects are incidence, IsRedundant, IsStrictlyRedundant, SubcolumnProperty and pricingRatio in the namespace Lubbecke2005.SubcolumnPricing.
Let satisfy the subcolumn property, , and let be arbitrary. If is strictly redundant, then
that is, is not an optimal solution of (31). The paper states the proposition and refers to Sol (1994) for the concept; it gives no proof.
If only holds for in , the shifted costs satisfy the subcolumn property, and on every with ,
This is the paper's remark that the shift "adds to a constant term equal to the number of rows and does not change the problem".
Proposition 2 is the paper's argument for alternative pricing rules (§5.2): it shows that dividing the reduced cost by the number of covered rows filters out a whole class of columns that contribute nothing to the dual polyhedron, whatever the current dual multipliers are. Steepest-edge pricing, Devex and the lambda pricing rule are motivated along the same lines. The cost-shift remark extends the proposition to cost structures that are only weakly monotone under inclusion, which covers the frequent case of costs that do not decrease when rows are added to a column.
The result is published and elementary once stated precisely, but the paper leaves the definition of redundancy informal (no sign on , no index set of the sum), and those choices decide whether the proposition is true. A formal statement pins them down. To our knowledge neither the proposition nor the vocabulary of redundant columns and ratio pricing has a machine-checked formalization; the definitions here are reusable for other statements about pricing rules in set-partitioning column generation.
The mathematical difficulty is modest; the difficulty is in the reading. With multipliers of arbitrary sign in (30), the proposition is false: on rows take , , , with costs , , , and ; then , , the subcolumn property holds, and has the unique smallest ratio. The empty column is a second trap: its denominator is zero. The formal statement has to exclude both, and has to keep the minimum in (31) over only.
Conventions committed to in Lean:
Fin m (indexed from ); a column is a Finset (Fin m), and its incidence vector is the real 0/1 vector incidence s : Fin m → ℝ. The collection is a Finset (Finset (Fin m)); costs are a function Finset (Fin m) → ℝ, of which only the values on matter.1 ⬝ᵥ incidence a, which equals .A trivializing formalization — a redundancy witness not tied to the proper subcolumns of in , signed multipliers, or an empty column with ratio — is ruled out by the definitions above.
Needed infrastructure is only finite sums of vectors in and the identity . Contributions welcome: proofs of the goal and the milestone, and further statements from §5 (for example the redundancy characterisation of Sol 1994) built on the same definitions.
Many problems in statistics, signal processing and machine learning have the form
where is smooth (a least-squares loss, for instance), is a nonsmooth regularizer or constraint, and is a linear map such as a finite-difference operator. When is nonconvex — the cardinality function , the quasi-norm, the indicator of a nonconvex set — the problem is NP-hard in general, and the realistic goal is a stationary point. The alternating direction method of multipliers (ADMM) is widely used on such problems because each iteration splits into a proximal step on and a smooth step on , but for nonconvex it was long used without a convergence theory.
Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave one of the first general analyses. Their Theorem 1 shows that, under explicit conditions on the penalty parameter and a proximal term, every cluster point of a proximal ADMM sequence is stationary, and that a suitable start is strictly improved on. Earlier, Ames and Hong (arXiv:1401.5492) proved convergence of the plain ADMM for one specific nonconvex quadratic problem with an and norm-ball term; Li–Pong's argument follows their idea of bounding the dual changes by the primal changes, together with a descent analysis of the augmented Lagrangian from Wen, Peng, Liu, Bai and Sun (Optimization Online 2013/01/3730).
Let be twice continuously differentiable with bounded Hessian , let be proper (finite somewhere, never ) and closed (lower semicontinuous), and let be linear with adjoint .
A vector is a regular subgradient of at (with finite) if . The limiting subdifferential collects all limits of regular subgradients at points with . A point is stationary if
For the augmented Lagrangian is , and for a convex function the Bregman distance is . The proximal ADMM generates, from arbitrary ,
Assumption 1 requires for some (so is surjective), Loewner bounds , with , , a strong-convexity margin , and some with . Here .
Under the standing assumptions and Assumption 1, for every proximal ADMM sequence:
and is stationary; 2. (Strict improvement) if is not stationary, and , then every cluster point satisfies
The theorem does not assert that a cluster point exists; that is the subject of Theorem 2 of the same paper.
In attack order: the robustness (3) of ; the optimality relations (11) of each iterate; the passage from (9) and (10) to (12) and stationarity; the dual-step bound (14); the one-step estimate (20) and its summed form (21) for ; the vanishing of the primal steps (16); the convergence (10) of ; and, for part (ii), , the first-step estimate (27) and the strict decrease after (28).
Theorem 1 turns the proximal ADMM into a method with a guarantee for a nonconvex : any limit it produces is a stationary point, and with the initialization of part (ii) — for example, a stationary point of a convex relaxation — it cannot return to a stationary point worse than its start. The conditions are checkable: Remark 1 of the paper shows that the choice turns the -update into a convex quadratic program, and that the last condition of Assumption 1 can be enforced by taking large when , , do not depend on . The estimate (20) is reused by the paper's boundedness result (Theorem 2), and its whole-sequence convergence result for semi-algebraic data (Theorem 3) starts from Theorem 1.
The result is proved in the paper; Mathlib contains neither the limiting subdifferential nor any convergence theorem for ADMM, so none of it is formalized yet. A formalization would give a verified library of the limiting subdifferential of extended-real-valued functions, its robustness and its Fermat rule with a smooth sum, and the first formally verified convergence theorem for ADMM with a nonconvex term.
The obvious argument — "the augmented Lagrangian decreases, so it converges" — fails: need not decrease, because the multiplier step increases it by . The proof has to bound this increase by primal steps, which uses surjectivity of and the squared Hessian bounds, and it produces a two-step recursion (involving ) rather than a monotone sequence. Nor is known to be bounded below; the proof uses the cluster point and lower semicontinuity to get a lower bound along a subsequence. Passing to the limit in the inclusion for requires , which lower semicontinuity alone does not give. For part (ii), the start is not an iterate at all, so the first step needs its own estimate.
Spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); is a continuous linear map and is ContinuousLinearMap.adjoint. and take values in EReal; inequalities involving are written additively ( with real ), never through EReal.toReal. The Hessian is the derivative of the gradient. is Mathlib's Loewner order on self-maps, which includes symmetry of the difference; adds positive definiteness. for every , possibly indefinite. The witnesses of Assumption 1 are explicit parameters, universally quantified. A proximal ADMM sequence is any triple of sequences satisfying the three updates (global minimizers, not necessarily unique); are free and is unconstrained. A cluster point is the limit along a strictly increasing subsequence. Stationarity is the inclusion (4) itself.
The limiting subdifferential keeps all three requirements of its definition — , and — and the domain condition ; dropping -attentive convergence or replacing by the convex subdifferential would make stationarity a different, and for nonconvex wrong, notion. Part (ii) is a strict inequality for every cluster point, and its hypotheses are exactly non-stationarity of , finiteness of the objective at and . The paper's assumption that proximal maps of exist is not a hypothesis, since no statement asserts that the iteration can be run.
Needed infrastructure: Fermat's rule and the smooth sum rule for regular subgradients, a diagonal argument for (3), Taylor bounds for functions with Loewner-bounded Hessians (the paper's (5) and (6)), strong convexity from a Hessian lower bound, and the monotonicity of the positive square root in the Loewner order. These are reusable well beyond this mission; contributions of any of them as separate lemmas are welcome.
Many problems in optimization reduce to finding a zero of a maximally monotone operator: minimizing a closed proper convex function (its subdifferential is maximally monotone), finding a saddle point of a convex–concave function, and solving monotone variational inequalities. The basic algorithm for this problem is the proximal point method of Martinet (1970) and Rockafellar (1976), which repeatedly applies the resolvent of the operator. The augmented Lagrangian method, the proximal method of multipliers, the Douglas–Rachford splitting method, ADMM and the primal–dual hybrid gradient method are all instances of it, so any speed-up of the proximal point method transfers to these widely used algorithms.
For convex minimization, Güler (1992) accelerated the proximal point method in the style of Nesterov, improving the rate of the function value from to . For general maximally monotone operators no function value exists, and the natural measure of progress is the fixed-point residual , the distance moved by one resolvent step. Gu and Yang (2020) showed that the plain proximal point method has the exact worst-case rate for the squared residual. Relaxed and inertial variants had been studied, but none guaranteed an accelerated rate for this measure. Kim (arXiv:1905.05149, Math. Program. 2021) found one using the performance estimation problem (PEP) of Drori and Teboulle (2014): a new accelerated proximal point method whose squared fixed-point residual is at most .
Let be a real Hilbert space with inner product . A set-valued operator assigns a subset to every point . It is monotone if whenever and , and maximally monotone if moreover no monotone operator has a graph that properly contains the graph of . The class of maximally monotone operators is , and is the set of zeros.
For a step size , the resolvent maps to the unique with . It is single-valued for monotone and defined on all of for maximally monotone .
The general proximal point method with step coefficients starts at and iterates
Kim's proposed accelerated proximal point method starts at and iterates
The coefficients (25) are for and .
The PEP of Section 3 bounds the worst case of over all and all starts with . A semidefinite relaxation leads to the dual problem (D): minimize over nonnegative such that . The matrices are explicit symmetric matrices built from and the canonical basis . Its optimal value is .
For every , every , every run of the proposed method, and every with for a constant ,
The constant is the paper's, and nothing is left unfixed.
Theorem 4.1 gives the first rate for the fixed-point residual of a proximal point method on general maximally monotone operators. The rate uses no strong monotonicity, no smoothness, and no finite dimension. Because the proximal point method underlies the proximal method of multipliers, PDHG, Douglas–Rachford splitting and ADMM, the paper derives accelerated versions of each (Section 6). The same analysis also accelerates the forward method for cocoercive operators (Section 7). Later work related the method to the Halpern iteration (Lieder 2021) and showed that its rate is optimal among a broad class of fixed-point methods up to a constant (Park and Ryu 2022).
The result is proved in the paper, and to our knowledge no machine-checked proof exists. Formalizing it produces a verified chain of four results: an explicit semidefinite certificate (Lemma 4.1), the weak-duality step from an SDP certificate to an algorithmic bound, the resulting rate for the general method, and the algebraic identity between two recursions (Proposition 4.1). It also produces reusable definitions of monotone and maximally monotone set-valued operators on a real Hilbert space, which Mathlib does not have.
The obvious approach would be a Lyapunov (potential) function argument, but the paper does not give one. The rate comes out of a semidefinite program. Lemma 4.1 asks for positive semidefiniteness of an matrix whose entries are double sums over , uniformly in . The passage from the dual certificate back to the iterates happens in an arbitrary, possibly infinite-dimensional Hilbert space, where each constraint matrix corresponds to a monotonicity inequality between iterates, so matrix positivity has to be turned into an inequality between inner products in . The PEP is a relaxation that discards constraints, so only weak duality is available, and a rate that holds only for (Lemma 3.1) is not what is asked. Proposition 4.1 is a two-level induction with index bookkeeping at .
is any real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with no finite-dimensional specialization. An operator is M : H → Set H. Maximal monotonicity says that every monotone A with M x ⊆ A x for all x equals M.
The resolvent step is relational: is encoded as . For monotone and this determines uniquely, and for maximally monotone such an exists for every (Minty's theorem). No function-valued resolvent with junk values off its domain is used. Sequences are indexed by ℕ. The paper's is y (0 - 1) = y 0 under natural-number subtraction. The general method has no , so its initial-distance condition is on , as in (17). The step size is written lam.
PEP matrices are Matrix (Fin (N+1)) (Fin (N+1)) ℝ, with a 1-based basis basisVec N i . is the infimum of the feasible values of computed in EReal, so an infeasible gets the value as in the paper; Eq. (28) compares it with the real bounds cast to EReal.
A formalization in which the iterate predicate cannot be satisfied, the residual is , the correction term is dropped or has the wrong sign, the initial point is decoupled (), or is only monotone on finitely many points, would state a different theorem, and none is used here.
Useful infrastructure includes a Minty-type existence lemma, uniqueness of the resolvent, and a lemma turning a positive semidefinite certificate into an inequality between inner products in (via Matrix.PosSemidef and Gram matrices). These are reusable for PEP-based rates of other first-order methods. Proofs of any milestone, and of the goal by other routes, are welcome.
One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in . It is the model behind cutting stock (cutting rolls of paper or steel to ordered widths), memory and file allocation, and batch scheduling on identical machines, and it is NP-hard. Its algorithmic study is therefore about approximation: how close to the optimum a polynomial-time algorithm can guarantee to come.
An instance is a finite multiset of piece sizes, each in the open interval . Write for the number of pieces, for the number of distinct sizes, and for the sum of all sizes. A packing of is a finite multiset of bins, each a multiset of sizes, whose union is exactly and in which every bin has total size at most . Its cost is the number of bins, and is the minimum cost.
A configuration of is a nonempty multiset of sizes occurring in with total at most . With the number of pieces of size and the number of occurrences of in configuration , the fractional bin-packing problem is the linear program
whose optimal value is . A basic feasible solution is an extreme point of its feasible region.
For instances , write if there is a one-to-one map from the pieces of into the pieces of with . Linear grouping with parameter sorts non-increasingly, cuts it into groups of consecutive pieces (the last possibly shorter), rounds every piece of up to the largest size of to get , and outputs and .
ALGORITHM 1 takes and : (1) discard the pieces of size , leaving ; (2) apply linear grouping to with , giving and ; (3) put each piece of in its own bin; (4) obtain from a Fractional Bin-Packing subroutine a basic feasible solution of the LP of with ; (5) round to a packing of with at most bins; (6) shrink the pieces back to obtain a packing of ; (7) insert the discarded pieces, opening a new bin only when a piece fits nowhere. is the cost of the resulting packing.
The additive term depends on only, so ALGORITHM 1 is an asymptotic approximation scheme. The paper prints the factor , which fails for ALGORITHM 1 as printed (see Formalization scope); running the algorithm with gives the paper's main result (4), , stated as a separate corollary with the explicit term .
The result showed that the configuration LP, of exponential size in general, can be used for a guaranteed approximation: its value is within of the integer optimum, and grouping reduces at small cost. The same template (eliminate small items, group, solve the configuration LP, round a basic solution, reinsert) underlies later schemes for bin packing, cutting stock, bin packing with cardinality constraints and scheduling, and the LP-based analysis is the starting point of the Rothvoß and Hoberg–Rothvoß improvements.
The theorems are proved in the literature; none of them has a machine-checked proof on the platform or, to our knowledge, in Mathlib. This mission produces a checked analysis of the algorithm, including a correction: the printed approximation factor is not valid for the algorithm as printed, and the checked statement records the factor its proof yields. The definitions (instances, packings, the configuration LP, basic solutions, the order , any-fit insertion) are reusable for the second mission of the series and for other bin-packing results.
The Lean statements are short, but several proofs need linear-programming structure that is not in Mathlib in this form. Lemma 2 and Corollary 1 use that an extreme point of has at most as many nonzero coordinates as there are rows of ; the configuration LP is indexed by a finite but implicitly described set of multisets. Monotonicity of under ("clearly" in the paper) requires transporting a fractional solution across a piece-to-piece matching whose images are types, not pieces. The existence of a run requires an optimal basic feasible solution of the configuration LP. Lemma 3 concerns an insertion process with unrestricted order and bin choice, so its bound has to hold for every execution, not for one greedy rule.
Multiset ℝ; packings are Multiset (Multiset ℝ) with join equal to the instance, bin loads at most , empty bins allowed and counted. is a natural-number infimum over a set that is always nonempty.Multiset ℝ →₀ ℝ supported on configurations. is a real infimum over a set that is nonempty (singleton configurations) and bounded below by . "Basic" is the extreme-point property; the bound on the number of nonzero coordinates is a consequence, not the definition.Alg1Run ε I P: is a possible output. Every open choice is quantified: the subroutine's output, the packing of Step 5 (any packing within the stated bound), the size reduction of Step 6 (bin by bin), and the insertion of Step 7 (any order, any fitting bin). The goal holds for every run, and a separate item states that a run exists, so the goal is not vacuous.Proofs of any item are welcome; Lemma 2, Corollary 1 and the monotonicity display are the most reusable.
A process on a shared-memory multiprocessor that finds a lock held must decide what to do while it waits. It can spin, repeatedly testing the lock and occupying its processor, or it can block, giving the processor to another process and paying a fixed context-switch cost to be descheduled and later restored. Spinning is cheap when the lock is released soon; blocking is cheap when the wait is long. The waiting time is not known in advance, so the choice has to be made on-line. This is the spin-block problem, studied by Karlin, Manasse, McGeoch and Owicki in Competitive Randomized Algorithms for Nonuniform Problems (Algorithmica 11, 1994, doi:10.1007/BF01189993), §4. Mathematically it is the continuous form of the ski-rental problem, and the same rent-or-buy structure recurs in power-down policies and in TCP acknowledgement (Karlin, Kenyon, Randall, STOC 2001).
Timeline:
Fix a context-switch cost . A lock wait is described by its release time . An algorithm handling the wait chooses a blocking time : it spins until time and then blocks (: never block). The cost of the wait is
so a lock released exactly at the blocking time costs . The optimal off-line algorithm, which knows , pays .
An input is a finite sequence of lock waits. A deterministic on-line algorithm chooses the blocking time of wait as a function of , the release times it has already observed. Its cost is the sum of the wait costs, and the off-line cost is .
A randomized on-line algorithm is a probability distribution over deterministic on-line algorithms: a probability space and a deterministic algorithm for each , with measurable for every . Its expected cost is . Following §1 of the paper, is -competitive against an oblivious adversary if there is a constant with
The adversary is oblivious: it fixes before the algorithm's random choices are made.
The paper's algorithm blocks at a random time with cumulative distribution
where is the probability of blocking before time .
For every :
Theorem 10 settles the randomized competitive ratio of the continuous ski-rental problem: is achievable and cannot be improved by any on-line algorithm, randomized or not, against an oblivious adversary. The same constant is the limit of the paper's snoopy-caching ratios as the block size grows, and it recurs in randomized rent-or-buy problems and in on-line primal-dual analyses.
The result is proved in the literature, and the mission's work is to formalize it. The platform has related material but not this statement: Primal-Dual Online Algorithms I: Fractional Ski Rental proves a deterministic, fractional, discrete-day bound (PrimalDualOnline.SkiRental.fractional_competitive), which is a different model and contains no lower bound. A complete formalization produces a reusable model of randomized on-line algorithms with history-dependent decisions and an exact lower bound for them.
The upper bound per lock wait is an explicit computation. The difficulty lies elsewhere. First, the on-line algorithm is allowed to adapt to the release times of all previous waits, so a bound for a single wait does not by itself bound a sequence: the randomized algorithm must be assembled so that each wait is handled with the right blocking law, whatever happened before. Second, the lower bound is a statement about every randomized algorithm and must survive the additive constant : a single hard lock wait proves nothing, because absorbs any bounded loss. It has to be shown that on long sequences of waits every algorithm loses a factor on average. The natural first idea, to exhibit one bad release time for each algorithm, fails for randomized algorithms facing an oblivious adversary.
All objects live in the namespace NonuniformCompetitive.SpinBlock. Release times are ℝ≥0, blocking times ℝ≥0∞, wait costs ℝ≥0∞, and the off-line cost is real. Committed conventions:
Infrastructure a complete development needs: Lebesgue integrals of functions of a random variable (the layer-cake formula), interval integrals of the exponential, the construction of a probability measure on with a prescribed continuous distribution function, and a Yao-type averaging argument over finitely supported input distributions for the lower bound. The model of randomized on-line algorithms with history-dependent decisions is reusable for other rent-or-buy problems. Contributions welcome: proofs of the milestones, and intermediate lemmas such as the discretised lower bound for a fixed step .
A quantum particle on a line or half-line, and the radial part of a particle in a spherically symmetric potential, are described by a Sturm–Liouville expression
on an interval . The expression alone does not define a Hamiltonian: a self-adjoint operator needs a domain, and on a general interval the choice of domain is a choice of boundary conditions at and . Whether a boundary condition is needed at all depends on the behaviour of near the endpoint. H. Weyl settled this in 1910 (Math. Ann. 68, 220–269) with his limit circle / limit point dichotomy: at each endpoint either all solutions of are square integrable near it and a boundary condition must be imposed, or they are not and no condition is possible. This mission formalizes Sections 9.1–9.2 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), which develop the theory for coefficients that are only locally integrable, and culminate in Theorem 9.9, the Weyl alternative.
Let and . The coefficients satisfy: with ; real-valued; with . The Hilbert space is with .
A function is locally absolutely continuous, , if it is an indefinite integral of a locally integrable function on . The equation means that and its quasi-derivative both lie in and almost everywhere. A solution of , , is a complex-valued with in this sense. The maximal domain is
The modified Wronskian is , with no complex conjugation, and , likewise.
is limit circle (l.c.) at if there is a with and for some ; otherwise it is limit point (l.p.) at . The same holds at . A function is square integrable near if for some .
For every Sturm–Liouville expression as above,
and if is l.c. at , then for every all solutions of are square integrable near . The same two statements hold at .
The Weyl alternative turns a question about operators into a question about an ordinary differential equation. Whether a Schrödinger operator on a half-line needs a boundary condition at infinity, or whether with a radial potential is essentially self-adjoint on smooth functions, reduces to checking square integrability of solutions for a single value of . Combined with Theorem 9.6 it classifies the self-adjoint realizations with separated boundary conditions: none at an l.p. endpoint, a one-parameter family at an l.c. endpoint. The Green function of Lemma 9.7 is the starting point of the spectral theory of one-dimensional Schrödinger operators: Weyl–Titchmarsh -functions, spectral transformations, and oscillation theory in the rest of Teschl's Chapter 9.
The results are classical and proved in many textbooks. The formal content is new: Mathlib has unbounded operators (LinearPMap) and their adjoints, but no Sturm–Liouville theory, no quasi-derivatives, no ODE existence theorem for measurable, locally integrable coefficients (its Picard–Lindelöf theorem needs Lipschitz right-hand sides), and no self-adjoint realizations of differential operators on general intervals.
The definition of limit circle refers only to and boundary limits of Wronskians, while the conclusion is about all solutions of an ODE for all . The two sides are linked only through self-adjoint operators: the passage from boundary Wronskians to square integrable solutions goes through the resolvent of a self-adjoint realization, which exists only for , and so only for nonreal in general. Extending the conclusion to real , where no resolvent is available, needs an argument of a different kind. On the ODE side, the coefficients are only locally integrable, so solutions are merely locally absolutely continuous, equations hold only almost everywhere, and every boundary quantity is a limit whose existence must itself be established.
SLData bundles EReal with (infinite endpoints allowed), , and the standing hypotheses (i)–(iii) of p. 181; pointwise on . is Lp ℂ 2 for the measure on .Classical.choose (it is unique on ). is with a local integrability clause. No smoothness of the coefficients and no solutions are assumed.Filter.limUnder along , inside . They are used only on , where milestone (9.7) states that the limits exist. In Lemma 9.7, where need not lie in , the boundary condition is stated as a convergence.LinearPMaps; self-adjointness is Mathlib's IsSelfAdjoint. Theorem 9.6 asserts that an operator with graph exists (i.e. is well defined) and is self-adjoint. and follow Teschl (2.66): a bounded two-sided inverse of . No projection-valued measure or functional calculus is used.A complete development needs a Carathéodory-type existence theorem for linear first-order systems with coefficients, the Lagrange identity with its boundary limits, Lemma 9.3 (a linear-algebra fact about functionals) and the computation of the closure and adjoint of the minimal operator (Lemma 9.4). The ODE layer and the operator layer can be reused for the Weyl–Titchmarsh theory, oscillation theory (Sec. 9.7) and one-particle Schrödinger operators (Ch. 10). Contributions that build them as general lemmas are welcome.
Approximate policy iteration and policy gradient methods are the two classical families of reinforcement learning algorithms that work with approximate, sampled information instead of an exact model. Kakade and Langford (ICML 2002) observed that neither family answers three basic questions: is there a performance measure that is guaranteed to improve at every step, how hard is it to verify that an update improves it, and what performance is reached after a reasonable number of updates. Greedy approximate policy iteration can make the policy worse when the value estimates are slightly wrong at a few states, and policy gradient methods can stall on plateaus where estimating the gradient needs an enormous number of samples.
Their answer is conservative policy iteration: instead of jumping to a greedy policy, move only a controlled fraction of the way toward it, with a step size chosen from an estimate of how much the greedy policy helps. The paper proves that this update improves a restart-distribution performance measure monotonically, terminates after a number of iterations that depends only on the reward range and the target accuracy, and stops at a policy that the greedy oracle can no longer improve by much. The idea is the direct ancestor of trust-region and proximal policy optimization methods (TRPO, Schulman et al. 2015; PPO, Schulman et al. 2017), whose improvement bounds are refinements of the paper's Theorem 4.1.
A finite Markov decision process has a finite nonempty set of states , a finite nonempty set of actions , transition probabilities (for each state and action , a probability distribution over next states ), a reward function with , and a discount factor . A stochastic policy gives, for each state , a probability distribution over actions.
The normalized value of from is , where , , ; it lies in . The state-action value is and the advantage is .
For a state distribution (a restart distribution), the discounted future state distribution is (eq. (2.1)), and the performance measure is .
The policy advantage of a policy with respect to and is
and . The conservative update (4.1) is with . An -greedy policy chooser (Definition 4.3) returns, for every policy , a policy with .
Conservative policy iteration (§5) starts from any policy and repeats: call to get ; form an -accurate estimate of from -restarts; if , stop and return ; otherwise apply (4.1) with and repeat.
With probability at least , conservative policy iteration (i) strictly improves with every policy update, (ii) stops after at most policy updates, and (iii) returns a policy with
The estimation step is represented by its guarantee: each reached loop's estimate fails to be -accurate with probability at most , .
Lemma 6.1 (p. 6), the performance difference identity:
Theorem 4.1 (p. 4), with and all :
Corollary 4.2 (p. 5): if , the step size gives
Theorem 4.4 is the first guarantee of its kind for approximate reinforcement learning: the number of iterations is bounded by , independent of the number of states and of the restart distribution, and every iteration provably helps. Lemma 6.1 is the standard performance difference lemma, used throughout the analysis of policy optimization, including natural policy gradient and trust-region methods; Theorem 4.1 is the prototype of the "surrogate objective minus a penalty" bound that TRPO refines.
These results are proved in the paper. As far as a search of the platform shows, none is formalized: the platform's finite-horizon performance difference lemma (Foster and Rakhlin's Lemma 13) is a different statement, for episodic problems with non-stationary policies. This mission produces machine-checked versions of the discounted performance difference identity, the conservative improvement bound with its exact constants, and the high-probability termination and quality guarantee of the algorithm, all on top of an explicit infinite-horizon model rather than an assumed Bellman equation.
The obvious argument for the improvement bound expands to first order in ; that only gives with an unspecified constant, which cannot fix a step size. The exact bound needs control of how far the state distribution of the mixed policy drifts from that of the old policy, uniformly in time, and the performance difference identity is only useful once the states are weighted by the new policy's distribution. On the formal side, and are infinite discounted series, so summability, exchanges of sums and the identities and must all be established from the definitions. For Theorem 4.4, the algorithm is a random process whose policies depend on all earlier estimates; the argument has to be made pathwise on the event that every reached loop is accurate, together with a union bound over the loops that can be reached.
Policies are functions π : S → A → ℝ with π s a the paper's , and P s a s' is ; both are constrained by the published predicates IsPolicy and IsTransitionKernel. is times the published series PolicyValue, so values are normalized as in the paper. is a real supremum over all stochastic policies; the set is nonempty and bounded, and the maximum is attained. Every theorem carries the standing assumptions of §2: finite nonempty and , a transition kernel, rewards in with , , and a state distribution . In Corollary 4.2, is any upper bound on the rewards rather than necessarily the attained maximum.
In Theorem 4.4 the run is formalized pathwise, driven by arbitrary real random estimates on a probability space; the conclusion bounds the probability of the failure event by . Two deviations from the printed statement are disclosed. First, (ii) is stated for policy updates: the proof bounds updates, and the algorithm calls once more than it updates, so "at most calls" is off by one. Second, the per-loop failure budget is , which covers the loops that may be reached. The Hoeffding estimate (5.1) is not formalized: as printed it concerns the -biased target, and its role is taken by the accuracy hypothesis. The step size is clipped at , which never binds when the estimate is accurate. No trivializing reading is available: the accuracy hypothesis is satisfied by a perfect estimator and a -greedy chooser exists, so the theorem is not vacuous, and strict improvement at every update is required, not merely nonnegative change.
Pages are PDF pages; the paper has no printed page numbers.
A complete development needs summability and algebra of discounted occupation measures, the performance difference identity, and a union bound over the loops of a random process; the first two are reusable for any discounted policy-optimization result. Proofs of the milestones in any order are welcome.
A two-machine flow shop is the simplest multi-stage production system: every job visits machine 1 and then machine 2, each machine works on one job at a time, and the goal is to finish all jobs as early as possible. S. M. Johnson's 1954 paper (Naval Research Logistics Quarterly 1(1):61–68, doi:10.1002/nav.3800010110) answered this question, posed by R. Bellman, with an exact rule, now called Johnson's rule. It is one of the first exact results in machine scheduling. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) the problem is written . The rule is the standard polynomial case against which the NP-hardness of the three-machine flow shop (Garey, Johnson and Sethi 1976) is contrasted, and it is still used inside heuristics for larger shops.
Timeline:
There are items . Item needs units of time on machine 1 and then units on machine 2. Each time is setup time plus work time, and the times are otherwise arbitrary. A schedule assigns start times and . It is feasible when all start times are nonnegative, the intervals of distinct items do not overlap on machine 1, the intervals do not overlap on machine 2, and for every item. The total elapsed time is the time at which the last item leaves machine 2.
An order is a permutation , where is the item in position . The as-soon-as-possible schedule of an order processes the items in the order on both machines, with no delay on machine 1. Each item starts on machine 2 as soon as it has left machine 1 and machine 2 is free.
Relation (II). Item is definitely preferred to item when
and the two items are indifferent when equality holds. An order is consistent with all the definite preferences when no item is definitely preferred to an item placed earlier.
For an order the paper uses the quantities
For positive :
The comparison is against every feasible schedule, including those whose two machines follow different orders.
The theorem reduces an optimization over a continuum of start-time vectors, and over orders, to sorting with respect to a pairwise relation. The paper's working rule computes an optimal order in time. The two-machine rule is the building block of Johnson's three-machine result, of the Campbell–Dudek–Smith heuristic for machines, and of lower bounds in branch-and-bound methods for flow shops. The closed form reappears across flow-shop theory as a longest-path formula.
The result is classical and proved. This mission contributes a machine-checked proof in Lean 4 against Mathlib. As far as a search of the platform shows, no formal statement of the flow-shop model or of Johnson's rule exists there. The mission also fixes a reusable Lean model of a two-machine schedule: start times, feasibility, total elapsed time and the as-soon-as-possible schedule of an order.
The paper's argument leaves two steps informal, and a formal proof must supply both. First, Lemma 1 is justified by a picture and the phrase "successive interchanges". The page does not show that each interchange keeps the schedule feasible and does not delay the last completion on machine 2, and this is where most of the modelling work sits. Second, relation (II) is not a strict weak order when there are ties, so the obvious sorting argument fails. Consistency on adjacent pairs does not imply optimality: the items , in that order, satisfy (II) non-strictly on both adjacent pairs, yet take 13 units against an optimum of 10. Lemma 2's exception is exactly this case.
Items are Fin n (0-based) and times are real numbers. Positivity , is a hypothesis of the goal and of Lemma 1, the as-soon-as-possible step and the closed form, as on p. 61. Lemma 2 and the interchange statements are pure min/sum algebra and carry no positivity. An order is σ : Equiv.Perm (Fin n) with σ k the item in position k. Interchanging positions is σ * Equiv.swap j (j+1). The total elapsed time is Finset.univ.fold max 0 of the machine-2 completion times, so it is when . is indexed by 0-based positions (Lean's is the paper's ), and requires .
Conventions made explicit or corrected:
Measuring the objective by , or comparing only against schedules that follow one common order, would drop Lemma 1 and change the theorem. The goal compares against every feasible start-time schedule. The working rule of p. 64 (a procedure) is not formalized.
Proofs of any milestone are welcome, as are further lemmas about the as-soon-as-possible schedule and a formalization of the working rule. The schedule definitions are the basis for the three-machine mission of this series.
A Markov-renewal program is a sequential decision model in which a system moves among finitely many states, the time between transitions is random and may depend on both the current and the next state, and a reward accrues during each sojourn. It generalizes the Markov decision process, where every transition takes one time unit, and is the standard model for maintenance, inventory and queueing control problems in which decisions are made at irregular epochs. W. S. Jewell introduced the model in two companion papers in Operations Research in 1963 (Part I, Part II).
Part II studies returns over an unbounded planning horizon. When the horizon is measured in number of transitions and rewards are not discounted, the expected return of a stationary policy grows linearly, and the paper's policy-improvement algorithm for this model rests on the precise form of that growth: a rate, the gain, and a state-dependent offset, the bias. Appendix A of Part II derives this asymptotic form from the Kemeny–Snell theory of finite Markov chains. This mission formalizes that derivation.
The result is the transition-counting counterpart of Howard's gain–bias analysis for Markov decision processes (R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960), and the fundamental matrix it uses is that of J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
Fix a stationary policy. Only the embedded chain and the mean one-step rewards matter for the infinite-step undiscounted model (the paper, p. 961: these processes "depend only on the means"). The data are:
The chain is ergodic (assumption 2, p. 951): is irreducible, meaning every state can be reached from every other state with positive probability. may be periodic. A stationary probability vector is with , and ; denotes the matrix every row of which is .
The -step return of the policy is the recursion (I 16) without the maximization:
The system gain is (A 6), the bias after steps is , and the fundamental matrix is (A 7).
For every irreducible row-stochastic , stationary , rewards and terminal rewards : the matrix is invertible, and
This is (A 4) with (A 5)–(A 7), in the form that is true for every ergodic chain and every terminal-reward vector.
In order: the stationary vector exists, is unique and positive, and (Appendix A); the increment identity (A 1) for constant ; the Cesàro limit of the increments (A 2); invertibility of and the relations , , ; the Cesàro summability of to ; the finite- bias formula (A 3) for constant ; the relative-value equations (4) for the limiting bias; and the paper's two-state machine example, where the four stationary policies have gains , the policy is optimal for every with , the limiting biases are , and the relative values of (5) are and .
If is moreover primitive (aperiodic), itself converges to . This is included as a supporting statement.
The asymptotic is what makes average-reward policy improvement work: substituting it into the recursion yields the linear equations (4), whose solution (the relative values) is the test quantity of the paper's algorithm. The gain identifies which stationary policy earns most per transition in the long run, and the bias separates policies of equal gain. The same gain–bias decomposition underlies average-cost dynamic programming, the analysis of Markov reward processes, and the deviation matrix used in sensitivity analysis of Markov chains.
The result is classical and proved on paper. Formalizing it adds, first, a machine-checked account of the fundamental matrix of an irreducible, possibly periodic, finite chain: invertibility of , its algebraic relations and its Cesàro characterization. Mathlib has irreducible and primitive nonnegative matrices and row-stochastic matrices, but no stationary-vector uniqueness for irreducible chains, no Cesàro ergodic theorem for finite chains, and no fundamental matrix. Second, it fixes two slips of the printed appendix (below) with an exact statement. No machine-checked proof of this result is known.
The obvious argument writes and passes to the limit term by term. This fails for periodic chains: does not converge, does not tend to zero, and the series does not converge. The paper's own example ( swaps two states) is of this kind, and there oscillates forever. What survives is Cesàro convergence, and establishing it needs control of all eigenvalues of of modulus one (they are simple roots of unity for an irreducible stochastic matrix) or an equivalent combinatorial argument. Invertibility of requires that be a simple eigenvalue of with left eigenvector , which is the Perron–Frobenius uniqueness statement for irreducible matrices; positivity of all entries of , or a one-step Doeblin condition, is not available.
States are a finite type with decidable equality and at least one element; vectors are S → ℝ, matrices Matrix S S ℝ, column vectors act by P *ᵥ v, the row vector by π ᵥ* P. Ergodicity is P ∈ Matrix.rowStochastic ℝ S ∧ P.IsIrreducible. The stationary vector is a hypothesis-constrained parameter (nonnegative, summing to one, ), which is unique by the first milestone. , and are definitions computed from , and , never free variables. Cesàro means are , equal to at . Mathlib's matrix inverse is on singular matrices, so the goal asserts invertibility of explicitly.
Two printed slips are corrected, and the milestone texts are kept verbatim:
The printed uses for the number of states .
A trivializing formalization is ruled out: is not a junk inverse (invertibility is part of the goal), is a genuine stationary probability vector of rather than an arbitrary vector, is computed from and , and the hypotheses are met by the paper's periodic two-state example.
Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, positivity, uniqueness), the Cesàro ergodic theorem , and the fundamental matrix. These are reusable for any finite-chain average-reward result. Contributions proving any milestone, or the aperiodic variant, are welcome.
In quantum mechanics an observable is a self-adjoint operator on a complex Hilbert space , and the dynamics is the Schrödinger equation . In finite dimensions the solution is the matrix exponential , computed by diagonalizing . The operators of physics (the Laplacian, Schrödinger operators with Coulomb potentials, position and momentum) are unbounded, defined only on a dense subspace, and have no eigenbasis in general. The spectral theorem is the substitute for diagonalization in this setting: it expresses every self-adjoint operator as an integral of the identity function against a family of orthogonal projections, and so gives meaning to for every Borel function , in particular to and to the spectral projections .
The theorem goes back to Hilbert (bounded symmetric forms, 1906) and was extended to unbounded self-adjoint operators by von Neumann (1929/30), Stone (1932) and Riesz. This mission follows the treatment in G. Teschl, Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), Section 3.1: projection-valued measures, their functional calculus for bounded and unbounded functions, and the spectral theorem obtained from resolvents through the Herglotz representation of Borel transforms.
Let be a complex Hilbert space, with inner product conjugate linear in the first argument, and let be the bounded operators on it. An (unbounded) operator is a linear map defined on a subspace ; means extends . is self-adjoint if is dense and , domains included.
The resolvent set of is the set of for which is a bijection with bounded inverse, and the spectrum is its complement, .
A projection-valued measure assigns to every Borel set an orthogonal projection such that and, for pairwise disjoint Borel sets , for every vector (strong, not norm, -additivity). Each gives the spectral measure , a finite Borel measure of total mass , and by polarization the complex measures .
For a bounded Borel function the operator is the bounded operator with for all . For an arbitrary Borel function it is the operator with domain
and for . An operator is normal if it is densely defined, and on .
For every self-adjoint operator in there is a unique projection-valued measure with
an equality of operators including their domains. Uniqueness is among projection-valued measures, compared on Borel sets.
A further supporting statement (not a milestone) records that is a finite measure with .
The result itself. The spectral theorem is the foundation of the rest of the book and of mathematical quantum mechanics generally. Stone's theorem and the time evolution , the min-max principle, the RAGE theorem, the decomposition of the spectrum into absolutely continuous, singular continuous and pure point parts, Weyl's theorem on essential spectra and scattering theory are all statements about or . Theorem 3.8 identifies the spectrum with the support of , which is what makes spectral questions accessible to measure theory.
Formalizing it. The result is classical and fully proved in the literature. Mathlib has the continuous functional calculus for bounded normal elements of -algebras and the finite-dimensional spectral theorem, but no projection-valued measures, no spectral integral of unbounded functions, and no spectral theorem for unbounded operators (LinearPMap). On Prove2Me the related published material is bounded or finite-dimensional (for example diagonalization of self-adjoint endomorphisms and the Fuglede–Putnam theorem). A formal proof here supplies the object that every later mission of this series currently has to take as data.
The obvious route through the bounded case fails. For bounded self-adjoint one can build from polynomials by the sup norm on and extend by monotone limits; for unbounded there are no polynomials in defined on a common useful domain and no sup-norm estimate. The standard reductions (the Cayley transform , or the bounded resolvent ) produce bounded normal operators whose spectral measures must then be transported back, and the domain must be recovered exactly as ; getting the domains right, not just the formulas on a core, is where unbounded arguments usually break. Beyond the domain issue, the projections are not given by any formula in that Mathlib can evaluate: they have to be recovered from resolvent data, which in the book's development requires the Herglotz representation of Borel transforms and the Stieltjes inversion formula for finite measures, neither of which is in Mathlib. Uniqueness is also not automatic: it requires that a projection-valued measure is determined by the operator alone.
is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since none of the stated results or their proofs in the book need it. Operators are LinearPMaps H →ₗ.[ℂ] H; self-adjointness is Mathlib's IsSelfAdjoint, which includes density. A projection-valued measure is a function Set ℝ → (H →L[ℂ] H) constrained on Borel sets only (IsProjValuedMeasure); uniqueness in the goal compares values on Borel sets. The spectral measure spectralMeasure P ψ is built with Measure.ofMeasurable from . The spectral integral spectralIntegral P f is the operator with domain and quadratic form (the predicate IsSpectralIntegral), selected by choice; its existence for Borel is part of the milestone for Theorem 3.2, not an assumption. The bounded calculus boundedSpectralIntegral is characterized the same way in . The spectrum is the resolvent-based TeschlQM.Spectral.spectrum of Section 2.4, not Mathlib's spectrum ℂ of a Banach algebra element. In Theorems 3.8 and 3.9, enters as a projection-valued measure P with the hypothesis A = spectralIntegral P (fun x => x), which by the goal's uniqueness is exactly .
Nothing is taken as data that the book derives. In particular the goal is not stated for "a projection-valued measure with " given as a hypothesis, and is not defined by choosing such a measure: the goal quantifies existentially and uniquely over projection-valued measures, with self-adjointness of as the only hypothesis.
Lemma 3.4 (spectral bases), Lemma 3.6 (the family built from the Herglotz representation) and the results of Sections 3.2–3.3 are not stated. A complete development needs finite Borel measures and spaces (in Mathlib), the Herglotz representation and Stieltjes inversion (the subject of the next mission of this series), and the adjoint theory of LinearPMap. The projection-valued measure and spectral-integral layer is reusable by every later mission of the series. Contributions of any milestone, of general lemmas about IsProjValuedMeasure (finite additivity, , monotonicity), and of alternative proofs of the goal are welcome.
Many controlled systems do not move in unit time steps. A machine runs for a random time before it breaks down, a repair takes a random time, a queue sits in a state until the next arrival or departure. A Markov-renewal program (in later terminology a semi-Markov decision process) models such a system: the sequence of visited states is a Markov chain controlled by the decision maker, but each transition takes a random time and earns a reward that may depend on that time. When the horizon is long and rewards are not discounted, the natural criterion is the gain rate, the long-run expected reward per unit of time, not per transition.
Howard's policy-iteration algorithm (Howard 1960) finds a policy of maximal gain per transition for finite Markov decision processes. W. S. Jewell's Markov-Renewal Programming. II (Oper. Res. 11 (1963) 949–971) extends it to the time-average criterion. The paper's Fig. 2 gives the algorithm; pp. 954–955 state its claim: the algorithm "will find an optimal stationary policy for the infinite-time, undiscounted model, in the sense that the policy will have a gain rate, , which is at least as large as that obtained for any other policy". Appendix D compares Jewell's test quantity with an alternative one proposed by P. Schweitzer, and states the identity (D 3) that measures the gain-rate improvement produced by either.
Timeline. Howard (1960) introduced policy iteration for the per-transition gain of finite Markov decision processes, and sketched a semi-Markov version. Jewell (1963, Parts I and II) developed Markov-renewal programming, with the ratio test quantity of Fig. 2 for the undiscounted time-average case. Schweitzer (unpublished MIT report, cited in Appendix D) proposed the test quantity (D 1). The ratio criterion was later treated systematically for semi-Markov decision processes (e.g. Puterman 1994, Ch. 11).
There are finitely many states and, in each state, finitely many alternatives . Under alternative in state the next state is with probability (, ). The transition takes a random time with finite mean , and the transition out of earns an expected reward . The mean sojourn time is , and it is positive.
A stationary policy picks one alternative in each state. Its chain has transition matrix , and , denote the data of . The paper's standing assumption 2 is that this chain is ergodic (irreducible) for every policy. Let be the stationary probability vector of (, , ). The gain rate of is (B 7):
The value-determination equations (13) of are, in the unknowns ,
The test quantity of Fig. 2 for alternative in state is . One cycle of the algorithm solves (13) for the current policy and then chooses, in every state, an alternative that maximizes the test quantity, retaining the current alternative when it already attains the maximum. The algorithm stops when the policy does not change.
For every run of the algorithm, from any initial policy and with any choice among tied maximizers, there is with ; and whenever , is the gain rate of and, for every stationary policy ,
The result makes the time-average criterion computable: a finite sequence of linear solves and pointwise maximizations produces a policy whose reward per unit time is optimal among all stationary policies. The identity (D 3) is the quantitative content: it expresses the gain-rate change as an average of local improvements, weighted by the fraction of time the new policy spends in each state. Both test quantities, Jewell's (D 2) and Schweitzer's (D 1), are covered by it. When every the model is a Markov decision process and the algorithm is Howard's.
The result is classical and has textbook proofs for semi-Markov decision processes. The paper states the proof as "elementary" and does not write it out. None of it is machine-checked on Prove2Me, and no semi-Markov or ratio-criterion result is on the platform. The mission produces a checked account of value determination for irreducible finite chains, the improvement identity, and termination of policy iteration under ties.
The gain rate is a ratio, so the per-transition argument for Markov decision processes does not transfer by rescaling rewards: the denominator changes with the policy. Comparing two policies requires weighting local improvements by the new policy's time-stationary probabilities, and a strict improvement needs those probabilities to be positive in every state, which uses irreducibility of the new policy, not only of the current one. Termination rests on the retain-on-tie rule: without it the algorithm can cycle among tied maximizers without improving. Finally, (13) has unknowns and equations only because of the normalization ; its unique solvability is a statement about the kernel and range of for an irreducible stochastic .
States are Fin N with NeZero N; the paper's state is index (lastState N). Alternatives form a type α; the goal assumes Fintype α and Nonempty α. The model records only , and , with as a field. The transition-time distributions and reward functions of the paper enter the undiscounted infinite-time model only through these means, and every such choice of means is realized by some distributions, so nothing is lost. Ergodicity is Matrix.IsIrreducible of the policy matrix for every policy. Stationary vectors are nonnegative, sum to one and satisfy ; every statement quantifies over all of them.
The gain rate is defined by its closed form (B 7). Its identification with ((B 6), argued in Appendix B from renewal theory) is not part of the mission. (13) is stated with the full sum , equal to the paper's because . The paper states (D 3) for a policy "which led to an improved policy "; the identity holds for any two policies and is stated that way. A run of the algorithm is a relation, not a chosen argmax: the goal quantifies over every run, so the termination claim cannot be met by a particular tie-breaking. A run begins at an arbitrary policy; the "initial set of returns" entry of Fig. 2 is a run started one cycle later.
A formalization in which the improvement step already asserts optimality, or in which termination is assumed, would be trivial; here the step only asks for pointwise maximization of the test quantity, and termination is part of the conclusion.
Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, uniqueness, strict positivity), the kernel of , and finite-policy termination arguments. These are reusable for any finite Markov decision or semi-Markov model. Proofs of any milestone, and of the specialization, are welcome.
In network revenue management a firm sells products that consume capacitated resources over periods, and in each period it chooses which offer set of products to make available. When customers choose among the offered products according to a choice model, the standard planning tool is the choice-based linear program, which assigns a frequency to every offer set (Liu and van Ryzin 2008). It has variables. Its optimal solution is what the firm actually implements: a randomization over offer sets.
For the Markov chain choice model of Blanchet, Gallego and Goyal (2016), Feldman and Topaloglu (2017) show that the choice-based program is equivalent to a reduced linear program with only variables. The reduced program can be solved directly, but its solution is a pair of vectors , not a randomization over offer sets. This mission formalizes the paper's Section 7, which converts the reduced solution back into a randomization over offer sets: the Dimension Reduction algorithm, and Theorem 9, which says that the algorithm produces at most offer sets and that these sets are nested.
Products are indexed by . A customer arrives wanting product with probability . If the product she visits is offered, she buys it. Otherwise she moves to product with probability , and leaves without buying with probability . Throughout, , and for all .
For an offer set , the (Balance) equations
have a unique solution. is the probability that product is purchased, and is the expected number of visits to while it is not offered. Write and .
The set consists of all pairs with and for all . The (Reduced) linear program maximizes over subject to the capacity rows for each resource .
The Dimension Reduction algorithm starts from the optimal solution of (Reduced) and sets . At iteration it forms . It stops with if . Otherwise it sets , stops if , and if not updates
The weights are .
Let be optimal for (Reduced). The algorithm stops at some first iteration with . At that ,
In the order the proof uses them:
Theorem 9 makes the reduced program usable. Together with the equivalence of (Reduced) and the choice-based program, it produces an optimal choice-based solution that offers at most sets. By a basic-solution count the choice-based program has an optimal solution with at most nonzero offer sets. Theorem 9 bounds the number by the number of products instead, and adds a structural property: the offered sets form a chain. Each set is contained in the previous one, so the implemented policy offers a single nested sequence of assortments. The algorithm needs at most solutions of linear systems of size . It never enumerates offer sets.
The result is proved in the paper. As far as a search of the platform and of Mathlib shows, it has not been formalized. Mathlib's Carathéodory theorem (Analysis/Convex/Caratheodory) bounds the number of points in a convex combination. It does not construct this decomposition, and it does not give nestedness. Formalizing Theorem 9 therefore requires the paper's argument: a verified, terminating peeling procedure on the polyhedron whose output is a convex combination of (Balance) solutions indexed by a chain of sets.
The algorithm divides twice. Step 2 divides by , which must be positive on . Step 3 divides by , which must be nonzero whenever the algorithm continues. Both rest on nontrivial facts: the positivity of purchase probabilities, and the bound on . That bound in turn requires the comparison . The paper proves this comparison only in its online appendix; it is a monotonicity property of the inverse of restricted to the unoffered products. The update of Step 3 can make coordinates of negative unless this comparison holds, so the naive observation that " is a combination of points of " does not by itself keep the iterates in .
Termination is not a consequence of alone. It needs the strict decrease of the support, which comes from choosing a minimizing index. The weights are defined by products of the . Their sum telescopes to only because the last step has .
Everything lives in the namespace MarkovChainChoice.DimReduction. Products are Fin n and offer sets are Finset (Fin n). The model is a structure carrying , and, as a disclosed implicit hypothesis, . The pair is chosen by Classical.epsilon among the solutions of (Balance); milestone 1 is what identifies it with the paper's unique solution. Revenues, capacities and consumptions carry no sign conditions. "Optimal for (Reduced)" means feasible and at least as good as every feasible point.
The iterates are indexed from as in the paper. The value at index is an unused copy of the input. "The algorithm stops at iteration " is the first with or . Iterates after the first stop involve a division by zero, which Lean evaluates to , and no statement refers to them. The termination bound is a conclusion of the goal, not a hypothesis. The goal is about the algorithm's actual iterates, not about an arbitrary sequence that satisfies the invariants. The paper's and denote non-strict inclusion and are rendered as and .
Two milestones are stated more generally than the page. The paper states the iteration invariants for the (Reduced) optimum; the Lean requires only , which every feasible (Reduced) solution satisfies. Lemma 8's may be a set; the statement holds for every minimizer. The page contains printed slips: on p. 1332, has numerator , and the paper writes for . The Lean uses the correct forms, as in Lemma 8 and Step 3. None of these slips appears in a milestone quotation.
A complete development needs a small theory of M-matrices, in the form of nonnegativity of for substochastic , together with finite induction on supports. The comparison lemma (milestone 3) and the (Balance) existence and uniqueness result (milestone 1) are reusable across the other missions on this paper. Proofs of any milestone are welcome, as are alternative proofs of the goal.
A buyer and a seller negotiate over a single indivisible good. Each knows what the good is worth to them but not what it is worth to the other side, and each shades their offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this as a one-shot game in which both parties submit sealed offers simultaneously and a sale takes place at a weighted average of the two offers whenever the buyer's offer is at least the seller's.
The weight is a design parameter: lets the buyer set the price, the seller, and splits the difference. For values uniform on a common interval the paper computes an explicit equilibrium for every (its Example 1) and then asks the questions a designer of the rule cares about: how often does trade happen, who gains when moves, and which maximises the expected gains of the two parties together. The answers are the subject of this mission.
The example became a benchmark for bilateral trade. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) proved that no mechanism can guarantee efficient trade with two-sided private information, and that for uniform values the split-the-difference equilibrium of this game attains the largest expected gains from trade of any mechanism. The numbers and below are therefore the second-best benchmarks against which later work on the -double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) measures inefficiency.
A seller with reservation price and a buyer with reservation price each know their own value. The two values are drawn independently and uniformly on , with ; this law, written , is also each player's belief about the other's value ( in the paper).
Under the Bargaining Rule with parameter , the seller asks and the buyer offers . If the good is sold at price , the seller earns and the buyer earns ; otherwise both earn zero. Ties trade.
An offer strategy maps a value to an offer. The strategies of Example 1(a) are
A pair with these four properties is said to have the shape of Example 1(a) (IsExample1Pair k v̄ S B). On the two inequality ranges a seller asks too much, or a buyer bids too little, for any trade to occur, so the strategy there is free apart from the bound.
For such a pair, with , the trade probability is (tradeProb), and the ex ante expected profits — taken before either value is drawn, as the paper specifies on p. 843 — are
(sellerExAnte, buyerExAnte).
For , and every pair of the shape of Example 1(a),
and as a function of this total attains its maximum at . The goal is the paper's efficiency statement: among these equilibria, splitting the difference maximises expected group profit.
The goal is the sum of milestones 2 and 3 together with a one-variable maximisation; milestone 1 describes the trade region over which both profits are integrated.
The formulas answer the design question for the rule. Moving toward the buyer's offer makes the price rule look more favourable to the seller, yet milestone 2 shows the seller's equilibrium profit falls and milestone 3 shows the buyer's rises: the paper (p. 844) uses this to show that an intuition which ignores the players' strategic response is mistaken. The comparison with truthful offers, which would trade with probability and earn expected group profit , quantifies the cost of strategic misrepresentation: at best and .
The paper states these results as "straightforward computations" and prints no derivation. As far as is known, none of them has a machine-checked proof. A formalization settles the constants against the exact strategies of Example 1(a), including the non-linear no-trade branches the paper allows, and provides a worked example of computing trade probabilities and expected payoffs under a product of uniform laws, reusable for other double-auction and bilateral-trade examples.
The computation is elementary on paper, but the equilibrium strategies are only partly specified: on the seller's high range and the buyer's low range the offers are arbitrary functions subject to a bound, and need not be measurable. The obvious approach — substitute the linear formulas and integrate — is valid only after showing that these free branches never trade, so that the trade event and both integrands agree almost everywhere with their linear versions. The resulting integrals are over a product of two conditioned Lebesgue measures, not over Lebesgue measure on the plane, and the trade region depends on through both strategies. The monotonicity claims hold only on (the seller's cubic is not monotone on ), and the derivative of each profit vanishes at an endpoint of the interval.
Values are real numbers; the uniform law on is Lebesgue measure conditioned on the interval (volume[|Icc 0 v̄]), and the joint law of is the product measure, with pairs ordered . The trade probability is the real number (P {p | S p.1 ≤ B p.2}).toReal; the profits are Bochner integrals over the product. Ties trade. The results are ex ante, not conditional on a player's own value. Every theorem assumes and . Maxima are stated with IsMaxOn on plus the value at ; monotonicity with StrictAntiOn/StrictMonoOn on .
The statements do not assume that is an equilibrium; they are computations about any pair of the shape of Example 1(a). That this pair is an equilibrium is Example 1(a) itself, the goal of a companion mission. No measurability of or is assumed: the free branches never trade, so each integrand agrees almost everywhere with a bounded measurable function and the integrals are the paper's expectations. A formalization that assumes and linear everywhere, or that integrates over a single uniform variable, proves a different statement.
A complete development needs: the reduction of the trade event and the integrands to their linear versions on ; Fubini for the product of conditioned measures; evaluation of polynomial integrals over a triangle; and elementary calculus on cubics. Lemmas on integrating over products of uniform laws are reusable. Contributions of intermediate lemmas, such as the explicit trade region, are welcome.
A holomorphic function on an open set of restricts to a real hypersurface as a function that satisfies the tangential Cauchy–Riemann equations: it is annihilated by every antiholomorphic vector tangent to . Functions on with this property are called CR functions, and they are the boundary values that several complex variables studies whenever a domain is approached through its boundary. The basic question is the converse: when is a CR function locally the restriction of a holomorphic function? For smooth data the answer is "not always" (the book's Example 3.2.7 gives a smooth CR function on the hyperplane that is no such restriction). For real-analytic data the answer is "always", and that is Severi's theorem, the goal of this mission.
The mission follows Chapter 3 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026), where Severi's theorem is proved by complexification: a real-analytic function of and is treated as a holomorphic function of two independent variables restricted to the diagonal . The milestones are the steps of that route: uniqueness on totally real slices, the two complexification propositions, the fact that restrictions of holomorphic functions are CR, and the normal form of a real-analytic hypersurface.
Write with . A function on an open subset of is real-analytic if near each point it equals a convergent power series in the real coordinates. A set is a real-analytic hypersurface if near each of its points, after choosing one real coordinate among the and collecting the other as , it is the graph of a real-analytic function .
A function on an arbitrary set is smooth (respectively real-analytic) if near each point of it agrees on with a smooth (respectively real-analytic) function defined on an open neighbourhood. A defining function of at is a smooth real function on an open with nonvanishing derivative and ; is a smooth real hypersurface if it has one at every point.
With the Wirtinger derivative , the space of antiholomorphic tangent vectors of at is
A smooth is a CR function if for all and , where is computed on any smooth local extension of . A real-analytic CR function is a CR function that is real-analytic on .
In Lean, is Fin n → ℂ, and these notions are the definitions IsRealAnalyticOn, IsRealAnalyticHypersurface, IsSmoothHypersurface, IsSmoothOnSet / IsRealAnalyticOnSet, antiholTangent and IsSmoothCRFunction / IsRealAnalyticCRFunction of the namespace LeblSCV.CR.
Let be a real-analytic hypersurface, , and a real-analytic CR function. Then there are an open neighbourhood of and with
Severi's theorem identifies the real-analytic CR functions on a real-analytic hypersurface with the local traces of holomorphic functions. Together with Proposition 3.2.6 it shows that, in the real-analytic category, the tangential Cauchy–Riemann equations are exactly the obstruction to holomorphic extension. It is the model for the later extension theorems of the chapter: the Baouendi–Trèves approximation theorem (Theorem 3.3.1) and the Lewy extension theorem (Theorem 3.4.1), which replace real-analyticity with smoothness and pay for it with one-sided extension or approximation. Complexification (Propositions 3.1.3 and 3.1.5) is also a tool in its own right, used for the composition of real-analytic maps (Proposition 3.1.10) and for pluriharmonic functions.
All results here are classical and proved in the book; none of them is formalized in Lean or Mathlib as far as a search of the Prove2Me corpus and Mathlib shows. Mathlib has real and complex analyticity (AnalyticOnNhd), the one-variable and several-variable identity theorems for analytic functions, and the holomorphic implicit function theorem is within reach, but it has no notion of real hypersurface, CR vector or CR function. The mission produces that layer and a checked proof of the first extension theorem for CR functions.
The obvious idea is to take a real-analytic extension of , complexify it to a holomorphic function of variables, and substitute to remove . That produces a holomorphic function of , not of ; showing that it does not depend on requires transporting the CR equations, which hold only on , to the whole complexified hypersurface. That transport is a uniqueness statement for the complexification, and it rests on the normal form of Proposition 3.2.8, itself an application of the holomorphic implicit function theorem to the complexified defining function together with its reality symmetry. On the Lean side, the diagonal is not a complex submanifold, so identity theorems along it (Lemmas 3.1.2 and 3.1.4) do not follow from the standard identity theorem for open sets.
Fin n → ℂ, with 0-based indices; is the product type. The sup norm of Fin n → ℂ never enters a statement: no ball, norm or distance occurs.DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 there. A domain is an open connected (hence nonempty) set.AnalyticOnNhd ℝ on an open set, applied to as a real vector space, which is the book's power series in (equivalently in ).Mathlib.Analysis.Analytic.Basic (analytic functions, AnalyticOnNhd). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Analytic/Basic.htmlThe Russian option of Shepp and Shiryaev pays its holder, at an exercise time of their choosing, the running maximum of the stock price, discounted, with no fixed maturity. It is the standard example of a perpetual lookback option, and its value is a model problem of optimal stopping for a two-dimensional Markov process (the price and its running maximum). Perpetual contracts are simple to analyse but economically unrealistic: every real contract ends. Canadization (Carr, Randomization and the American put, Rev. Financial Stud. 11, 1998, https://doi.org/10.1093/rfs/11.3.597) replaces a fixed maturity by an independent exponential time . The holder must exercise before ; if they have not, they are paid the claim evaluated at . Because the exponential law is memoryless, the problem stays time-homogeneous and its value can be computed in closed form, while it approximates a contract of finite expected life .
Avram, Kyprianou and Pistorius (AKP04) solved both the perpetual and the Canadized Russian problem when the log-price is a spectrally negative Lévy process: a process with stationary independent increments whose only jumps are downward. This covers Brownian motion with drift, the Black–Scholes model, and jump-diffusions with downward jumps (crashes). Their answer is written with the scale functions , of the process. This mission is the third of three drawn from that paper, and formalizes the Canadized problem (§7, Theorem 3).
Timeline. Shepp and Shiryaev (1993) solved the Russian option for geometric Brownian motion. Carr (1998) introduced Canadization for the American put. Kyprianou and Pistorius (Ann. Appl. Probab. 13, 2003) studied perpetual options through fluctuation theory; §7 of [AKP04] builds on their calculations. Avram, Kyprianou and Pistorius (2004) solved the perpetual and Canadized problems for general spectrally negative Lévy processes.
Let be a filtered probability space with right-continuous, and let be a spectrally negative Lévy process adapted to : , paths càdlàg with no upward jumps and not monotone, increments stationary and independent of . The standing assumption is that has unbounded variation, or bounded variation and a Lévy measure .
The Laplace exponent is . Fix with , and let be the Esscher measure, .
For the -scale function vanishes on , is continuous on , and satisfies for , where is the largest root of . Further, . All scale functions in this mission are those of .
Starting from (the paper's ), the reflected process is , where and the position is . Its passage time above is .
Let , and let be an exponential random variable of rate which under is independent of . The Canadized Russian problem (32) is
over all -a.s. finite -stopping times . Write .
With
for every :
and is a -a.s. finite -stopping time attaining the supremum. The statement covers every variation regime at once.
In attack order:
The result. Theorem 3 gives the price and the optimal exercise rule of a Russian option with random (exponential) maturity, for every spectrally negative Lévy model at once. It makes three things explicit. The optimal rule is a threshold rule for the reflected process . The threshold is the crossing point of one explicit function of the scale functions. Whenever (possible only with bounded variation), immediate exercise is optimal. Because scale functions are known in closed form for many models, including Brownian motion with drift and hyper-exponential jump-diffusions (§8 of the paper), the theorem produces explicit prices.
Formalizing it. The result is proved on paper. It is not formalized in any proof assistant, and none of its infrastructure is available in Lean. This mission produces:
A machine-checked proof would also check the verification argument, which the paper states in detail only for the unbounded-variation case.
The obvious route is to compute the value of every threshold rule (Lemma 3) and optimize over . That identifies the right candidate, but it does not show that no other stopping time does better. The verification step needs two things for all regimes of : that is a supermartingale, and that stopped at is a martingale. For processes of bounded variation, is only continuous, not , at , so a smooth Itô formula does not apply directly. Computing the expected -integral up to uses excursion theory of away from , which Mathlib does not have. Eliminating is easy only if is independent of the whole filtration. If it is independent of alone, a stopping time could depend on .
ℝ≥0) and values are real. Random times take values in WithTop ℝ≥0, and the payoff is on . Expectations of nonnegative payoffs are lower Lebesgue integrals in , and is an extended-real supremum, so no expectation defaults to . Equalities with a real right-hand side also assert finiteness.The traveling-salesman problem (TSP) asks for a cheapest cycle through all vertices of a weighted complete graph. Exact algorithms for it are branch-and-bound searches, and their size depends almost entirely on the quality of the lower bounds used to prune the search. In 1970 Held and Karp introduced the 1-tree bound: a Lagrangian relaxation of the degree-2 constraints of a tour, whose value can be evaluated by one minimum-spanning-tree computation (Held & Karp, Part I, 1970). Part II (Held & Karp, 1971) replaces the ascent procedure of Part I by an iterative method related to the relaxation method for linear inequalities of Agmon and of Motzkin and Schoenberg (1954), and with it solved to proven optimality every instance presented to it, up to 64 cities. The iteration is the prototype of what is now called the subgradient method with Polyak-type step sizes, and the 1-tree bound remains a standard lower bound in exact TSP codes.
Timeline:
Let and let be a symmetric real matrix of weights on the edges of the complete graph with vertex set ; weights may be negative and need not satisfy the triangle inequality. A subgraph has weight equal to the sum of its edge weights. A tour is a cycle through every vertex exactly once; is the weight of a minimum tour.
A 1-tree is a tree on the vertex set together with two distinct edges at vertex . Index the 1-trees by ; let be the weight of the -th 1-tree, the degree of vertex in it, and the degree-excess vector with components . For define
A tour is a 1-tree with , so for every (Eq. (2)); the best bound is . For a point , denotes a minimum-weight 1-tree at , a 1-tree attaining the minimum defining . The ascent iteration (3) is
For a target value , is the polyhedron of solutions of for all (system (5)). All norms are Euclidean.
With constant step , any starting point and any choice of minimum-weight 1-trees,
with , the iterates enter or converge to a boundary point of . 6. Lemma 3, Case 2: with the iterates enter . 7. §3 bound: the restricted minimum over 1-trees containing the edges and avoiding the edges is a lower bound on every tour of the derived problem.
Milestones 1–5 are the steps of the paper's proof of Theorem 1; 6 and 7 are further results of the paper on the same objects.
Theorem 1 is the paper's justification of the step rule actually used in its computations: a fixed step loses at most times the asymptotic squared deviation of the generated 1-trees from being tours. Since is an even integer that vanishes exactly on tours, and the paper observes it is typically small in practice, the bound explains why the constant-step ascent reaches bounds sharp enough for branch-and-bound. Lemmas 1–3 are the first analysis of a subgradient-type method for a nonsmooth concave function, cast as the relaxation method for the (exponentially large) system (5).
All results are proved in the paper (except the Féjer-monotone convergence and Case 2 of Lemma 3, which it cites from Motzkin and Schoenberg). None is formalized: the platform has the 1-tree lower bound only under a metric assumption on the weights (SupplyChainTheory.held_karp_bound, SupplyChainTheory.one_tree_lower_bound), and the subtour-LP bound MetricTSP.held_karp_le_opt, a different object. This mission produces the bound for arbitrary real weights, the supergradient property of , and a machine-checked convergence analysis of the relaxation iteration.
Lemmas 1 and 2 and Eq. (2) are short once the finite minimum defining is handled. The difficulty is in Lemma 3 and Theorem 1. The iteration is not monotone in , so no descent argument applies; progress is measured by the Euclidean distance to the target polyhedron , and turning distance decrease into convergence requires the Féjer-monotonicity theorem, which in turn needs to have nonempty interior (from ). In Theorem 1 the step is constant rather than of the relaxation form (6), and the target polyhedron is not given in advance: the relevant relaxation parameters are admissible only eventually and must be kept away from zero, which requires controlling degenerate directions and the behaviour of along an iteration that is not known a priori to stay bounded. A direct argument that increases fails, since single steps can decrease .
Vertices are Fin n, the paper's vertex 1 is 0 : Fin n, and graphs are SimpleGraph (Fin n). Weights are c : Sym2 (Fin n) → ℝ, arbitrary reals. A 1-tree is a graph whose restriction to the vertices other than 0 is a tree and in which 0 has degree 2; a tour is a connected graph with all degrees 2. w(π) is the minimum of weight c G + ∑ i, π i * (deg G i − 2) over 1-trees, written as an sInf over a finite set that is nonempty for n ≥ 3; every theorem assumes 3 ≤ n. Euclidean norms and inner products are written as coordinate sums of squares and products, never Mathlib's sup norm on Fin n → ℝ. The minimum-weight 1-tree is a hypothesis at every step, and ties may be broken arbitrarily. The goal is stated as "for every and some iterate has ", which is equivalent to the printed inequality; is the limsup of a sequence with finitely many values, a genuine real.
The statements exclude trivializing readings: the 1-tree predicate rejects graphs without exactly two edges at vertex 1; w is never a minimum over an empty set under the standing hypothesis 3 ≤ n; no ⨆ of a possibly unbounded family is used; the step size and the parameter are strictly positive.
A complete development needs finite minima of affine functions (concavity, attainment), 1-tree and tour combinatorics on simple graphs, and Féjer-monotone sequences in ; the last two are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3, are welcome.
In one complex variable every open set is the natural domain of some holomorphic function. In several variables this fails: by the Hartogs phenomenon, every function holomorphic on some domains extends to a strictly larger one. The domains that are "natural", the domains of holomorphy, are characterised by a convexity condition on the domain. Since the work of Levi (1910), Hartogs, Oka and Cartan–Thullen (1932), the way to state that condition intrinsically has been pseudoconvexity. The tool that makes it work is the plurisubharmonic function, the complex analogue of a convex function.
This mission formalizes the part of that theory that needs no partial differential equations: harmonic, subharmonic and plurisubharmonic functions; smoothing of plurisubharmonic functions; the characterizations of Hartogs pseudoconvexity; and the Cartan–Thullen theorem. The source is §2.4–2.6 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026), pp. 78–103.
Timeline, as the book presents it:
Throughout, carries the Euclidean norm . A domain is a nonempty connected open set. For , means that is relatively compact in : its closure is compact and contained in .
Harmonic and subharmonic functions (one variable). A function on an open is harmonic if . A function is subharmonic if it is upper-semicontinuous and, for every disc with and every continuous on and harmonic inside it, on implies on .
Plurisubharmonic functions. For open, is plurisubharmonic if it is upper-semicontinuous and is subharmonic on for all .
Hulls and convexity. For a class of extended-real functions on and , the hull is
is convex with respect to if implies . For this is holomorphic convexity, with hull .
Hartogs pseudoconvexity. is an exhaustion function if for every . A domain is Hartogs pseudoconvex if it admits a continuous plurisubharmonic exhaustion function.
Analytic discs. A closed analytic disc is a nonconstant holomorphic that extends continuously to . Its image is and its boundary is .
For a domain with , the following are equivalent:
for every collection of closed analytic discs .
The result. Theorem 2.5.6 makes pseudoconvexity checkable. Condition (i) involves one explicitly given function of the domain's geometry. Condition (iv) involves only families of discs. Condition (ii) is the form the Levi problem and Hörmander's theory need. From these equivalences one gets, for example, that intersections and increasing unions of pseudoconvex domains are pseudoconvex, that pseudoconvexity is a biholomorphic invariant, and, with Lemma 2.5.7, that it is a local boundary property. In the smooth case that local property is Levi pseudoconvexity (Theorem 2.5.8, chapter III of this series). Cartan–Thullen supplies the other half of the picture for domains of holomorphy.
Formalizing it. All of these results are classical and proved in the book, apart from routine steps left as exercises. As far as is known, none of them is formalized in any proof assistant. Mathlib has harmonic functions (InnerProductSpace.HarmonicOnNhd) and the circle average, but no subharmonic or plurisubharmonic functions, no hulls and no pseudoconvexity. The Prove2Me corpus holds a one-variable subharmonic definition based on the sub-mean-value property and the one-directional mean-value property of harmonic functions; neither is the book's definition or statement. The mission would give Lean a first library of plurisubharmonic functions in , with the definition matching the textbook.
The obvious route to (iv) ⇒ (i) of the goal would show is plurisubharmonic by computing a complex Hessian (Proposition 2.4.9). That fails: is in general not even differentiable, so no Hessian is available. Several other steps also need measure theory with extended-real values. The sub-mean-value property requires Lebesgue integrals of upper-semicontinuous functions that may equal on large sets. Smoothing requires convolution of such functions with a mollifier, and pointwise convergence in . Suprema of families lose upper semicontinuity in general, which is why Proposition 2.4.7 carries that hypothesis. In Cartan–Thullen, holomorphic convexity alone must produce a holomorphic function on that extends across no boundary point. Nothing in the hypothesis supplies such a function directly.
EuclideanSpace ℂ (Fin n), so balls, = Metric.infDist z (frontier U), and are all Euclidean, as in the book. They are not sup-norm polydisc quantities.EReal-valued with excluded on . Upper semicontinuity is UpperSemicontinuousOn for the order of EReal.EReal, and holomorphic hulls in , so no supremum takes a junk value. Set distances are infima in (Metric.infEDist).DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 there.IsOpen U ∧ IsConnected U. Relative compactness is compact closure contained in .LeblSCV.Pseudoconvex.Several trivializing formalizations are ruled out. Plurisubharmonicity is not defined through the Hessian condition, so the mission does not reduce to functions. Nor is it defined by the sub-mean-value property, which would make Proposition 2.4.3 (ii) a tautology. is not the sup-norm distance. Suprema, infima and integrals are nowhere allowed to default to on empty, unbounded or non-integrable input.
A complete development needs:
The subharmonic and plurisubharmonic layer is reusable beyond this mission. Chapters on the Levi problem, the -problem and Bergman kernels would all build on it. Proofs of the smaller milestones, and alternative arguments for the goal, are welcome.
Two strategic levers shape the balance of power between a manufacturer and the retailer that resells its product. The first is strategic inventory: a buyer that orders more than it sells today, and carries the surplus into the next period, weakens the supplier's leverage over tomorrow's wholesale price. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period channel the buyer withholds inventory exactly when its unit holding cost is below . The second is supplier encroachment: a supplier that can sell directly to consumers competes with its own buyer. Arya, Mittendorf and Sappington (Marketing Science 2007) showed that the threat of encroachment can lower wholesale prices and benefit both parties.
Guan, Gurnani, Geng and Luo, Strategic Inventory and Supplier Encroachment (MSOM 2019), combine the two levers in one game. Their headline qualitative finding is Proposition 4.2. When the supplier's direct channel is costly, but not quite too costly to use, the buyer keeps withholding inventory at every finite holding cost. This contrasts with the cutoff of Anand et al. This mission formalizes that proposition, together with the equilibrium characterizations of Appendix A on which it rests.
There is one supplier and one buyer, two periods, deterministic demand and complete information. In each period the market price is , where is the total quantity sold in that period and is the demand intercept. The buyer pays a per-unit holding cost on inventory carried into period 2. The supplier pays a per-unit direct selling cost . All other costs and the salvage value are zero. The moves are:
The total profits are
A strategy profile assigns an action to every history at which a player moves. It is a subgame perfect equilibrium (SPE) if, at every feasible history, the mover's prescribed action is feasible and no feasible alternative, followed by the profile afterwards, raises the mover's total profit. The equilibrium path is the outcome the profile generates; the equilibrium inventory is on that path. Following the paper (§4), the goal theorem sets .
With ,
Here may depend on , and the bound applies at the same .
The thresholds , , , , are explicit algebraic functions of , given in Appendix A.
Proposition 4.2 separates the combined model from the two models it merges. Without a direct channel, inventory disappears once . With a direct channel, a threat of encroachment that is only barely credible keeps inventory alive at every holding cost. The total holding cost nevertheless stays below a constant, because the inventory shrinks as grows. Milestone 6 shows the flip side: for a fixed , a large enough removes the inventory. This is why the window must depend on .
The paper's proofs are in an online appendix that is not reproduced in the article. The article itself gives the equilibrium only as tables. A formal development would supply a checked backward-induction proof of those tables in the regions near . It would also give a machine-checked SPE framework for multi-stage pricing-and-quantity games in supply chains, which none of the following exists for: Stackelberg pricing, sequential quantity competition, or dual-channel encroachment. No part of this paper has been formalized before.
The equilibrium is found by backward induction through five stages. Each stage's value function is only piecewise smooth, because the supplier's direct-channel response switches on and off. As a result the buyer's period-2 profit has kinks, the supplier's period-2 profit as a function of has several local maxima, and the period-1 problems must compare branches whose boundaries are the irrational thresholds of Appendix A. The obvious approach, solving the first-order conditions stage by stage, fails at the kinks. At some region boundaries it also misses that the supplier is indifferent between two first-period prices, which makes the equilibrium path change discontinuously. Proposition 4.2 then needs uniform control of , and as , where the denominator of tends to .
IsSPE imposes optimality at every feasible history, including off-path ones. All actions are real numbers; wholesale prices and quantities are nonnegative, with and .Game, IsSPE and Thresholds are shared by every statement. Welcome contributions include:
Minimizing the total weighted completion time of jobs with release dates on a single machine, written in scheduling notation, is strongly NP-hard. Most constant-factor approximation algorithms for it, and for many related scheduling problems, follow one pattern: solve a linear programming relaxation, which gives a lower bound on the optimum, and round its solution into a schedule whose cost is compared with that bound. The quality of the algorithm is therefore limited by the quality of the relaxation, and the question of which relaxations are equivalent is a basic one for the method.
Two relaxations of are central. The time-indexed relaxation of Dyer and Wolsey (doi:10.1016/0166-218X(90)90104-K) has one variable per job and unit time slot, a pseudopolynomial number of variables. The mean busy time relaxation has one variable per job but one constraint per subset of jobs, the shifted parallel inequalities studied by Queyranne and others. Goemans, Queyranne, Schulz, Skutella and Wang (doi:10.1137/S089548019936223X, Section 2) show that both have the same optimal value, and that both are solved by one simple preemptive schedule. This mission formalizes that result, Corollary 2.6, together with the lemmas and theorems its proof uses.
Timeline:
There are jobs . Job has an integral processing time , an integral release date and a weight . For a nonempty set of jobs, and .
A preemptive schedule gives each job a bounded measurable set of processing times of Lebesgue measure , the sets pairwise disjoint. The mean busy time of is .
The LP schedule processes, at every moment, the available (released, unfinished) job of largest ratio , ties broken by index. With the jobs indexed so that , this is the available job of smallest index. As the data are integral, it runs one job or none in each unit slot ; records whether it runs there, and is its mean busy time of .
The preemptive time-indexed relaxation (D) with horizon has real variables for and reads
The mean busy time relaxation (R) reads
The horizon is required to bound the makespan of some feasible nonpreemptive schedule, for instance .
For every instance, every weight vector and every admissible horizon ,
No ordering of the jobs and no reference to the LP schedule appear in the goal.
The equality lets one choose, for each purpose, the more convenient of the two relaxations. (D) is intuitive and a transportation problem, but has pseudopolynomially many variables; (R) has variables and a supermodular right-hand side, which the paper uses to describe its polyhedron. Theorems 2.2 and 2.5 show that the common optimum is attained by the LP schedule, which is computable greedily; the approximation guarantees of Section 3 of the paper, and of later work on -point scheduling, are all measured against this value.
A formal development adds three things. First, a machine-checked model of preemptive single-machine schedules with release dates, of mean busy times, and of the LP schedule as a concrete recursive object, reusable by any formalization of -point methods (two companion missions of this series use the same objects). Second, a formal statement of the two relaxations with honest optimal values. Third, verified proofs of results that are proved in the paper by short interchange and averaging arguments, whose measure-theoretic details (integrals over processing sets, null sets in the equality case) the paper leaves implicit. The results are proved in the literature; to our knowledge none of them has been machine-checked.
The paper's arguments are short, and each rests on a step that is informal on the page. Lemma 2.1 cites the integrality of transportation problems, a statement about the vertices of a polytope rather than a one-line fact. Theorem 2.2 ends with the claim that a 0/1 solution admitting no improving exchange "must correspond to the LP schedule", which is a property of the greedy rule that has to be derived from its definition. Theorem 2.5 depends on how the LP schedule arranges the jobs of each prefix of the sorted order in time; this is the only place sortedness enters, and it is again a property of the concrete schedule. Lemma 2.4 is an extremal statement about integrals over sets of prescribed measure, and its equality case holds only up to null sets. Finally, the goal concerns arbitrary, unsorted weights, while the two theorems it combines are about sorted indices, so the goal is not a direct conjunction of the milestones.
Jobs are Fin n, numbered from ; , and the horizon are natural numbers and weights are real. A preemptive schedule is a family of processing sets , not indicator functions. The LP schedule is defined by recursion on unit slots with the smallest-index rule; the sortedness of is a hypothesis of Theorems 2.2 and 2.5, not part of the definition. Variables of (D) are functions required to vanish outside . and are infima of the objective over the feasible sets; under the stated hypotheses the feasible sets are nonempty and the objectives bounded below, so these are the LP values. Optimality in the milestones is stated as attaining the minimum, not through these infima.
The horizon hypothesis rules out the trivializing case in which (D) is infeasible and its infimum takes the junk value ; (D) is kept a linear program over real , since restricting to would make Lemma 2.1 vacuous. The running-time claim of Corollary 2.6 () is not formalized.
A complete development needs: integrals of the identity over finite unions of intervals; a rearrangement lemma for sets of given measure; basic properties of the LP schedule (it is a preemptive schedule, it is work-conserving and finishes by any admissible , its blocks are canonical); and a relabelling argument. The schedule model and the LP-schedule lemmas are reusable for the companion missions on -point scheduling. Contributions of any of these lemmas as separate theorems are welcome.
Chapter 10 turns from structure theory to algorithms: efficient methods for minimizing M-convex functions (via domain reduction) and submodular set functions (via Schrijver's and the Iwata-Fleischer-Fujishige scaling algorithms). Most of chapter 10's numbered results are asymptotic running-time bounds for specific procedural algorithms — a genuinely different kind of claim from the rest of this book (see Formalization scope). This mission places the results of this block that ARE ordinary mathematical propositions: correctness certificates, min-max theorems, and structural facts the algorithms rely on and produce.
For an M-convex set B ⊆ Z^V, the central part B° (the vectors of B lying away from its
boundary, defined via per-coordinate bounds ℓ°_B, u°_B) is what the domain reduction algorithm
searches from. For a submodular set function ρ : 2^V → R, the base polyhedron B(ρ) and its
extreme bases (one per linear ordering of V, via Eq. (10.12)) let any base be written as a
convex combination of finitely many extreme bases (Eq. (10.13)); a candidate minimizer W is
certified via the linear orderings representing an optimal base. The Iwata-Fleischer-Fujishige
(IFF) scaling algorithm relaxes this problem with a flow-augmentation parameter δ, maintaining
a δ-feasible flow φ and vector z = x + ∂φ; near the end of a scaling phase, no augmenting
path and no "active triple" together certify near-optimality.
If S ⊆ W ⊆ V∖T, no arc of the auxiliary network leaves W, and no active triple exists, then
z⁻(V) ≥ ρ(W)-nδ and x⁻(V) ≥ ρ(W)-n²δ; moreover W exactly minimizes ρ once δ is small
enough relative to the smallest positive gap between two values of ρ. Chosen as goal: the book
calls this "a key property of the scaling algorithm" and "a relaxation version of the min-max
relation in Proposition 10.8", its own proof is the most substantial argument among this chunk's
placed results, and Proposition 10.23 is a direct corollary of it.
Proposition 10.8 is the min-max relation underlying the whole of section 10.2 (an Edmonds-
intersection-theorem consequence, found by direct reading — the extractor's table missed it).
Proposition 10.9 gives the three-part sufficient condition for optimality, in terms of the linear
orderings representing an optimal base, that both Schrijver's algorithm and the IFF algorithm use
as their termination criterion (also found by direct reading). Propositions 10.5-10.6 establish
that the domain reduction algorithm's central part B° is always nonempty, via an explicit
vector-extension step (Proposition 10.5 likewise missing from the extractor's table). Proposition
10.23 fixes individual coordinates once a scaling phase ends, and Proposition 10.24 gives the
termination certificate for the IFF fixing algorithm's own separate graph-contraction procedure.
Chapter 10 is where this book cashes out its structure theory as algorithms with provable running times, and this mission places every result of that chapter's first two sections that is a mathematical proposition rather than a runtime bound: two min-max/optimality-certificate theorems (10.8-10.9) that are the combinatorial core making the following two strongly polynomial algorithms (Schrijver's, and Iwata-Fleischer-Fujishige's) correct, one central-part nonemptiness fact (10.5-10.6) underlying the domain reduction algorithm, and the two fixing/termination certificates (10.23-10.24) that let the scaling algorithms actually output a minimizer with a proof of optimality attached, not just a numerical answer.
None of these results are open — they are Murota's own account of submodular-function- minimization algorithms (sections 10.1-10.2). What this mission contributes is a faithful, machine-checked formal statement of each, including two results (Propositions 10.5 and 10.8) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).
Six numbered results in this block (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are
excluded as hard: each states a Big-O asymptotic bound on the running time, function-evaluation
count, or internal-procedure-call count of a specific iterative algorithm (the domain reduction
algorithm, its scaling variant, Schrijver's algorithm, the IFF scaling algorithm). Faithfully
stating "this algorithm runs in O(g(n)) time" requires a cost-tracked operational semantics for
that specific algorithm — a well-founded recursive procedure with an oracle for evaluating the
input function, threading a step/evaluation counter, instantiated over an unbounded family of
ground-set sizes n and numeric parameters (K∞, M) — which is a fundamentally different kind
of formalization task (computational complexity theory) from every one of the roughly 280 other
numbered results in this book, none of which require modeling the cost of computing them. See
HARD.md.
Ground-set elements are a Fintype V with DecidableEq. Base M-convex-set vocabulary is
redeclared from prior missions. Linear orderings of V are represented as bijections
V ≃ Fin (Fintype.card V) rather than as lists, matching this series' established preference for
order-indexed families over sequential data structures. Proposition 10.5's witness vector is
stated as an existence claim (the mathematical content of the proposition), rather than by
reconstructing the specific recursive modification procedure the book uses to produce it — a
choice consistent with how this series has always formalized "the algorithm produces X"
claims where X is a mathematical property, by asserting X's existence rather than executing the
algorithm (see, e.g., mission 33-ch09c-networkflows's cycle-cancellation theorem). Six numbered
results (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are hard; see HARD.md.
Contributions completing any of the seven sorrys are welcome; the goal and Proposition 10.9
carry the most independent proof content.
Chapters 6 through 9 characterized minimality for M-convex functions structurally (the M-optimality criterion, Theorem 6.26: a point is a global minimizer iff no local swap improves it) without saying how to find one. Chapter 10 turns that structural fact into an algorithm: the local characterization is the termination test of the simplest possible minimization procedure, steepest descent by coordinate swaps. This mission formalizes that algorithm and its two complexity bounds, plus a structural min-max identity for submodular base polyhedra that the chapter's heavier submodular-minimization algorithms build on. It is the first mission in this series whose goal names a method, not just a property of a class of functions — formalizing it faithfully means giving the algorithm itself a Lean representation that the complexity theorem then quantifies over, not just describing its output.
Let be an M-convex function (MExchangeAxiom,
chunk 06), . The steepest descent algorithm repeatedly replaces the current point
by for a pair minimizing , stopping
when no such swap improves on — at which point, by the M-optimality criterion, is a
global minimizer. This mission represents a run of the algorithm as a sequence satisfying these step and termination relations directly, so that "the number
of iterations" is a genuine property of any such run, not an informal gloss. Separately, for a
submodular set function (chunk 04's SubmodularSetFunction), the
base polyhedron (chunk 04's BasePolyhedron) is the polytope .
For an M-convex function with finite -diameter (Eq. (10.1)), the number of iterations in the steepest descent algorithm using the tie-breaking rule (10.2) — a fixed lexicographic rule for choosing among tied steepest pairs, based on an arbitrary but fixed ordering of — is bounded by .
Proposition 10.1: an unconditional warm-up — if has a unique minimizer , any run of the plain (untied) algorithm from terminates within iterations, with no tie-breaking rule needed. Proposition 10.8: a structural min-max identity, , for a submodular set function — chosen deliberately as a milestone that names no algorithm at all, in contrast to this mission's other two items.
The result itself. Proposition 10.2 is the complexity backbone of §10.1: it is what turns "steepest descent terminates" (an easy monotonicity observation) into a genuine polynomial bound, and it is the base case the chapter's more elaborate scaling and domain-reduction algorithms (not drafted here) improve on. Proposition 10.8, though algorithm-free, is the structural fact ("verifying membership in seems to need a submodular minimization procedure — but demonstrating optimality of a cut only needs a base with ") that makes Schrijver's and the IFF algorithms' correctness proofs possible, and specializes chunk 04's Edmonds's intersection theorem to the two-function case .
Formalizing it. A prior-art search (q=steepest descent, q=submodular minimization,
q=base polyhedron) found no existing platform items for any of this chapter's results. This
mission gives the first formal statement of an M-convex minimization algorithm's complexity,
and directly reuses chunk 06's MExchangeAxiom/ArgMin/CharVec/DomZ and chunk 04's
SubmodularSetFunction/BasePolyhedron — genuine cross-chunk substrate reuse spanning two
different chapters' worth of prior missions.
The chapter's own framing (quoted in BRIEF.md) is that every other chapter's theorems state a
property of a class of functions or sets, while this chapter's theorems state properties of a
named algorithm run on such an object. Formalizing "the number of iterations in the steepest
descent algorithm is bounded by ..." faithfully means giving the algorithm's steps (S0-S3) and
termination test a Lean representation that the bound then quantifies over — stating the bound
about "the minimizer" alone, with the algorithm silently dropped, would misrepresent the
theorem as a fact about minimizers rather than about a procedure that finds one. This mission
represents a run of the algorithm as an abstract sequence satisfying the book's own
step-transition relations (documented in full in MODERATION_NOTES.md), letting the complexity
theorems quantify over any valid run rather than committing to one executable implementation.
A second difficulty is scope: the chapter's recommended primary goal, Proposition 10.18
(Schrijver's algorithm's complexity), needs a scaling procedure with several auxiliary data
structures — a materially larger definitional undertaking than steepest descent's simple
greedy-swap loop. Per BRIEF.md's own explicit fallback authorization, this mission takes
Proposition 10.2 as its goal instead; see HARD.md and MODERATION_NOTES.md for the full
reasoning.
Runs of the algorithm are represented as x : ℕ → V → ℤ satisfying IsSteepestDescentRun
(plain) or IsSteepestDescentRunTieBreak (with the tie-breaking rule) — a step relation plus a
termination test, with an explicit iteration count N the theorems bound. The tie-breaking key
(Eq. (10.2)) and its lexicographic order are formalized directly (a manual
three-way comparison, not Mathlib's default componentwise Prod order). Both iteration bounds
are stated as 2 * N ≤ k rather than N ≤ k / 2, avoiding natural-number division. Not
drafted: the derived "hence ... in time" corollary of Proposition 10.2
(needs a cost-model primitive for "time" and "" this mission does not otherwise use — the
iteration-count bound itself, this proposition's genuine combinatorial content, is drafted in
full); Schrijver's algorithm and everything in §10.2.2 onward; the steepest descent scaling
algorithm, the domain reduction algorithm and its scaling variant (§10.1.2-10.1.3, structurally
different algorithms); the quasi-M-convex extension mentioned immediately after Proposition
10.2. A trivializing formalization would state the iteration bound as an unconditional fact
about "a" minimizer-finding procedure, or would drop the tie-breaking rule from Proposition
10.2 and thereby understate what the bound actually requires; neither is done.
In best arm identification with fixed confidence, a learner samples unknown distributions ("arms") sequentially and must name the arm with the largest mean, with error probability at most a prescribed , using as few samples as possible. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) showed that every -PAC strategy needs, in expectation, at least samples, where the characteristic time is the value of a max–min optimization problem over the proportions of draws allocated to the arms. The maximizer of that problem, , is the allocation any asymptotically optimal strategy must follow; the Track-and-Stop algorithm of the same paper computes at plug-in estimates and tracks it.
A strategy can only track if can be computed. This mission formalizes the part of the paper (Section 2.2 and Appendix A) that turns the abstract max–min problem into an explicit recipe: a closed form for the inner infimum, and a characterization of through the root of one increasing scalar function. The problem had been solved in closed form before only for special cases, such as Poisson rewards with all suboptimal arms equal (Vaidhyan and Sundaresan, 2015); the paper's result covers every one-parameter exponential family.
A canonical one-parameter exponential family is a family of laws , , on with density with respect to a reference measure . The law has mean ; the set of attainable means is the mean space . For means and the Kullback–Leibler divergence is
Bernoulli laws and Gaussian laws with known variance are the standard examples.
A bandit model is identified with its vector of means . is the set of models with a unique optimal arm , and is the set of alternatives. is the probability simplex. The transportation cost of proportions and the objects of the paper are
The arms are sorted so that . The parameterized Jensen–Shannon divergence is, for ,
For let for , let , and let . Finally
With : is continuous and strictly increasing on , , as , the equation has a unique solution , and
The equivalence says at once that the argmax exists, that it is a single point, and that it is given by eq. (5).
The result. Theorem 5 reduces a -dimensional non-smooth max–min problem to finding the root of one continuous increasing function on a bounded interval, each evaluation of which requires scalar inversions. It gives existence and uniqueness of , which the paper's lower bound only presupposes, and it is the computational core of Track-and-Stop: without an explicit, well-posed the tracking strategy is not defined. Lemma 3 alone gives the closed form of the inner infimum used again in the analysis of the stopping rule.
Formalizing it. The results are proved in the paper; nothing here is open. To the best of our knowledge none of them has a machine-checked proof: the platform's existing best-arm-identification rows concern Gaussian arms and state the characteristic time at the level of measures, without this characterization. The mission produces a checked reduction for general one-parameter exponential families, including the edge cases the text passes over (ties among suboptimal arms, zero weights, the behaviour of near the end of its domain).
The infimum in Lemma 3 ranges over , a set of models with a unique best arm, so it is an open condition: the minimizing configuration, in which and coincide, lies outside and is only approached. Other arms may also compete for the best position. A statement in which the infimum is taken over the closed relaxation is a lemma of the proof, not Lemma 3.
For Theorem 5, the equalization in Lemma 4 needs an argument that holds for every maximizer, not only for one found by a first-order condition, because the objective is a minimum of functions and is not differentiable. The monotonicity of needs the monotonicity of each and of each ratio in the moving point , and the limit at rests on the second-best arm(s) only, which is where the ordering enters. Finally the analytic facts about (continuity, positivity off the diagonal, monotonicity in each argument) must be derived from the exponential family itself.
Lean represents a model by μ : Fin K → ℝ with 2 ≤ K and every μ a in the mean space deriv F.b '' F.Θ. The paper's arm is index 0, arm is index 1. The exponential family is a structure ExpFamily whose parameter set is a nonempty open interval and whose b is twice continuously differentiable with on . These two conditions are added to the paper's "convex, twice differentiable" and are disclosed: strict convexity is what makes the mean parameterization unique, and openness is what lets alternatives approach the boundary of . The reference measure and normalization are part of the structure but unused here.
The transportation cost is an infimum in EReal, so it is the true infimum of the set of values rather than a default 0. is never defined by choice: " is optimal" is a predicate, and Theorem 5 characterizes the set of such . The functions are the inverse of on and are evaluated only on . "Increasing" in Theorem 5 is stated as strictly increasing, as proved in Appendix A.2. Lemmas 3 and 4 and the claim on assume only that arm is the unique best arm, which is weaker than the paper's standing ordering.
A formalization that replaces by , assumes the maximizer exists and is unique, or asserts only existence of some without the formula for , does not state these results and is ruled out.
A complete development needs: basic calculus of exponential families (the Bregman form of , its continuity and strict positivity off the diagonal, its monotonicity in the second argument), the inverse function of a continuous strictly monotone map on an interval, and compactness of the simplex. The divergence facts are reusable in every bandit mission built on exponential families. Proofs of the milestones, of auxiliary facts about and , and a sorry-free instance of ExpFamily (Bernoulli or unit-variance Gaussian) are welcome.