Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
An airline sells the seats of one flight leg at several prices. Low fares fill seats that would otherwise fly empty; high fares are bought by passengers who book late and cannot be predicted exactly. Seat inventory control decides how many seats each fare class may sell. Peter Belobaba's 1987 MIT dissertation (MIT Flight Transportation Laboratory Report R87-7) gave the probabilistic treatment of this problem that became the expected marginal seat revenue (EMSR) method, which was in use across the airline industry for decades.
This mission formalizes the first, simplest model of the thesis: distinct (non-nested) fare-class inventories on a single leg, where a seat assigned to a class may be sold only in that class or not at all. The thesis surveys this model in Sect. 4.2 (pp. 84–94), where an integer-programming formulation from McDonnell-Douglas and its solution by ranking marginal values are described (p. 90), and develops it probabilistically in Sect. 5.1 (pp. 102–107).
A leg has capacity seats (the thesis also writes ). There are finitely many fare classes . Class has an average fare and receives a random number of requests , with law . The seats are split into allocations , one per class.
With seats, a class books requests until its seats run out, so its bookings and spill (refused requests) are
The expected revenue of class is with , and the leg's expected revenue is (Eq. (5.9)). Write
the expected marginal seat revenue of the -th seat of class . The value of the -th seat of class in the integer program of p. 90 is , .
Let be any set of pairs , , such that every with is at least every with , and let . Then and
The goal fixes no distribution, number of classes or fare ordering, and it holds for every tie-breaking among equal marginal values.
The goal is the reason distinct-inventory allocation is computationally easy: a revenue-maximising allocation is obtained by sorting numbers, with no search over allocations. The same marginal-value principle underlies the EMSR rules for nested classes in the rest of the thesis, and the identity (5.11) is the link between an expected-revenue function and its marginal seat values used throughout revenue management. Milestone 5 is the integer form of the Lagrangian condition of Eq. (5.13); the thesis states it only for a continuous relaxation, and its equality form is generally unattainable with integer seats.
These results are classical and their proofs are elementary; to our knowledge none of them has been machine-checked. The mission produces a reusable formal model of a single-leg, distinct-inventory allocation problem with integer demand (bookings, spill, revenue and marginal values of a PMF ℕ), and checked statements of the marginal-allocation principle for it.
The thesis argues with continuous densities and derivatives, setting equal across classes. That argument does not transfer to integer seats: the derivative of a step-shaped expected-revenue function does not exist, equality of marginal values across classes generally fails at every integer allocation, and the tail probability must be rather than the of Eq. (5.2) for the marginal identity to hold. The integer statements need their own exchange argument. A second subtlety is ties: "the largest values" is not unique, and the goal must hold for every admissible choice, including choices in which a class's selected seat numbers are not an initial segment .
All declarations live in the namespace SeatInventory.Distinct. Conventions:
d i : PMF ℕ; expectations are series over . The thesis's continuous densities are replaced by this discrete model, which the thesis itself requires for seat allocations (p. 103).The expected revenue in the goal is computed from the booking rule ; it is not defined as a sum of marginal values, and the optimal allocation is not defined as an argmax of . Either shortcut would make the goal a tautology and is ruled out.
Needed infrastructure: tail sums of a PMF ℕ, telescoping of , and a finite exchange argument for sums of the largest values of a function on a finite set; the last two are reusable for any separable concave resource-allocation problem. Contributions of proofs of any milestone, and of a verified sorting routine that produces a set of largest values, are welcome.
Thompson Sampling (TS) is the oldest heuristic for the stochastic multi-armed bandit problem: it was proposed by Thompson in 1933 (Biometrika 25) and is used in practice for online advertising and recommendation, where it often performs as well as or better than upper-confidence-bound methods (Chapelle and Li, NIPS 2011; Scott 2010). Until 2012 its theoretical guarantees for the frequentist regret were weak: earlier analyses gave only regret in time (Granmo 2010; May, Korda, Lee and Leslie 2011).
Agrawal and Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem (arXiv:1111.1797v3, COLT 2012), gave the first logarithmic finite-time bound on the expected regret of TS. This mission formalizes their two-armed result, Theorem 1. A companion mission covers the -armed bound, Theorem 2.
Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least . Auer, Cesa-Bianchi and Fischer (2002) gave UCB1 with an finite-time bound. Agrawal and Goyal (2012) proved for two-armed TS. Kaufmann, Korda and Munos (ALT 2012) and Agrawal and Goyal (AISTATS 2013) later proved asymptotically optimal bounds for Bernoulli TS.
There are two arms. Arm has a fixed, unknown reward distribution supported in , with mean . Plays of an arm give i.i.d. rewards, independent of the other arm. Arm 1 is the unique optimal arm, , and is the gap.
Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm , a success count and a failure count , both starting at . In each round it
is the number of plays of arm before round . The expected regret in time is
the expectation being over the rewards and the algorithm's randomness.
The analysis uses the Beta cdf , the binomial cdf , and the random variable : the number of independent draws made before one exceeds .
There is an absolute constant such that for every two-armed instance with rewards in and , and every ,
The constant is not fixed numerically: the paper states the theorem in form (footnote 1), and the explicit display it reports on p. 8, , is not the formal claim.
The result. Theorem 1 shows that TS, a randomized Bayesian heuristic with no explicit confidence bonus, has regret logarithmic in on every two-armed instance, matching the order in of the Lai–Robbins lower bound. The proof introduced a way to control the optimal arm's waiting time between plays through the Beta–Binomial duality, and later analyses of TS reuse that device.
Formalizing it. The result is proved on paper and has no machine-checked proof that we know of. The platform's existing TS results concern Gaussian TS (Lattimore and Szepesvári, Ch. 36) and Bayesian regret, which are different algorithms or regret notions. A formalization adds a reusable Lean model of Algorithm 2 on -valued rewards, Beta–Binomial facts (Fact 1, Lemma 1), a binomial-median theorem, and binomial Hoeffding bounds. It also produces a proof with a constant that has been checked, since the printed constants contain an arithmetic slip.
The standard UCB argument does not transfer to TS. For UCB, the optimal arm's index exceeds its mean with high probability however often the arm has been played, because the exploration bonus is deterministic; the analysis then only has to count plays of the suboptimal arm until its own index concentrates, after plays. Under TS the optimal arm's sample is random and, if the arm has been played rarely or its early rewards were poor, it falls below with constant probability. The optimal arm may then wait a long, random time between plays, and the length of that wait depends on the arm's posterior, which in turn depends on how long it has waited. Counting plays of the suboptimal arm with a union bound over rounds, under the assumption that the optimal arm is already concentrated, therefore does not work; controlling these waiting times is the central difficulty and is where the dependence enters.
StochasticBandit 2 (a probability measure on per arm, mean banditArmMean), with the hypothesis that each reward law gives mass to . Lean arm 0 is the paper's arm 1 and Lean arm 1 the paper's arm 2. Lean rounds are indexed from .In a short 1997 letter, Max Tegmark argued that, given the other laws of physics, a spacetime with space and time dimensions can host observers who understand and predict their world only when (Tegmark 1997). The argument is physical and anthropic, but each step rests on a precise mathematical fact: the classification of second-order linear PDEs into elliptic, hyperbolic and ultrahyperbolic type, the well-posedness (or ill-posedness) of the corresponding initial-value problems, the potential theory of , the stability of Kepler orbits, and the algebra of curvature tensors in low dimension. This mission collects those mathematical facts as formal targets.
Timeline of the ingredients cited by the letter:
A second-order linear PDE on has the form
with symmetric. Following the paper, at a point it is elliptic if all eigenvalues of are positive or all are negative, hyperbolic if one eigenvalue is positive and the rest negative (or vice versa), and ultrahyperbolic if at least two are positive and at least two negative. Eigenvalues are counted with multiplicity; the Lean development counts them as the positive/negative real roots of the characteristic polynomial (numPosEigenvalues, numNegEigenvalues, IsElliptic, IsHyperbolic, IsUltrahyperbolic).
A spacetime of dimensionality carries a metric with positive (time-like) and negative (space-like) eigenvalues, so that has signature . The covariant field equations (wave) and (Klein–Gordon) have coefficient matrix . The Laplacian on is (laplacian).
For a symmetric with positive and negative eigenvalues,
The goal makes precise the paper's central new observation: the hyperbolicity needed for a well-posed initial-value problem singles out exactly one time dimension (or, in the tachyonic mirror case, one space dimension). The milestones supply the mathematical content behind each of the paper's other claims, namely instability for and the absence of gravity for , as well as the well-posedness and ill-posedness facts behind the "predictability" argument. All of these are classical results; none of them is new mathematics. The value of the mission is a machine-checked record of exactly which mathematical statements the argument uses, under which hypotheses, and with which caveats (for instance the critical coupling in four dimensions).
The goal is linear algebra. The difficulty lies in the milestones: Ásgeirsson's theorem and the Klein–Gordon energy estimate need integration over spheres and balls, a divergence theorem or spherical-mean calculus, and differentiation under the integral sign, and Mathlib supports these only partially. The four-dimensional hydrogen case sits exactly at the Hardy-inequality threshold, where the outcome depends on the coupling constant.
Fin d; eigenvalue counts are root counts of the characteristic polynomial with multiplicity. Classification is pointwise: one constant coefficient matrix.EuclideanSpace ℝ (Fin n); derivatives are Fréchet derivatives, and the Laplacian is the sum of pure second derivatives along the standard basis.Reusable infrastructure: PDE type via eigenvalue signs, spherical means, and local energy estimates for wave-type equations.
The subgradient method for a convex function moves from against a subgradient , and everything hinges on the step length. Divergent-series stepsizes guarantee convergence but are slow and need no information about . When the optimal value , or any level that is known to be attainable, is available, B. T. Polyak proposed in 1969 the step
which uses the current gap to scale the move. This Polyak stepsize is still the reference adaptive rule in nonsmooth convex optimization, in the solution of convex feasibility problems, and in the Lagrangian relaxation heuristics of integer programming (Held–Wolfe–Crowder, Camerini–Fratta–Maffioli), where it is known under the name "relaxation step".
Section 2.4 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) places Polyak's rule in the framework of Fejér-type approximations developed by I. I. Eremin: an iteration whose map strictly decreases the distance to every point of a target set. It then proves convergence of the rule, linear rates under growth conditions, its behaviour when the level is set too low, and a property of the conjugate-subgradient direction of Camerini, Fratta and Maffioli (1975).
Timeline:
is the -dimensional Euclidean space with inner product and norm . A vector is a subgradient of at if for all . A subgradient selection is a map with a subgradient at every ; nothing else is assumed about it, in particular not continuity.
For a nonempty set , a map is -Fejér if and for all and .
For a convex with and a level , let . Polyak's method (2.32) is the iteration with the map displayed above for and on ; the factor is fixed in .
The conjugate-subgradient procedure (2.38), for a convex with minimum point and , is
If and , then for any
The goal fixes no constant and no rate; it asserts only that the method finds a point of the level set, in finite time or in the limit.
Theorem 2.11 is the convergence guarantee of the most widely used adaptive step rule for nonsmooth convex problems. With it yields a minimizer; with it solves the convex inequality , and applied to it solves consistent systems of convex inequalities. The linear rates of Theorems 2.12–2.13 are the prototype of the "sharpness implies linear convergence" results of modern first-order methods, and Theorem 2.14 quantifies the loss when the level is underestimated, which is the situation of every practical variant that estimates on the fly. Theorems 2.15–2.16 are the justification of the conjugate-subgradient directions used in Lagrangian relaxation.
All results are classical and proved on paper. None of them is formalized on Prove2Me: the platform has a smooth, strongly convex Polyak gradient-descent bound (a different theorem) and Fejér-monotonicity statements for polyhedral relaxation methods, but no Polyak subgradient step, no -Fejér map and no conjugate-subgradient procedure. The mission produces machine-checked versions of the whole section, with the page's misprints corrected where the proof and the statement disagree.
The obvious argument for the goal is to observe that is -Fejér, by (2.33), and invoke Theorem 2.10. That argument fails: Theorem 2.10 needs a continuous map, and depends on an arbitrary subgradient selection, which is discontinuous wherever is not differentiable. The book says so explicitly. Fejér monotonicity gives boundedness and a limit of each distance , but convergence of the whole sequence to a single point of , and the fact that an accumulation point cannot lie outside , have to be obtained without continuity of the map.
For Theorem 2.14 the level lies strictly below the minimum, so , the target set of the iteration as run is empty, no Fejér property is available for it, and the theorem controls only the best value found, not the iterates.
EuclideanSpace ℝ (Fin n); is real-valued on all of and ConvexOn ℝ Set.univ f.x : ℕ → E_n with the recursion as a hypothesis; the first term is arbitrary.Real.sqrt.A formalization in which may be empty, the selection is assumed continuous, or the step divides by zero through Lean's conventions would be a different theorem; these are ruled out above.
Needed infrastructure: Fejér monotone sequences in finite dimensions (bounded, with convergent distances), the subgradient inequality, and the fact that a zero subgradient characterizes a minimum. These are reusable for every subgradient-type method. Contributions of general lemmas on Fejér-monotone sequences are welcome.
The simplex method is the standard algorithm for linear programming, and its correctness rests on one question: does it stop? Each pivot of the method moves from one dictionary to another without decreasing the objective value, but a pivot can leave the objective unchanged. When that happens repeatedly, the method can return to a dictionary it has already visited and loop forever. This behaviour, cycling, is not hypothetical: Vanderbei's Chapter 3 exhibits a problem with four decision variables and three constraints on which the "largest coefficient" entering rule with a natural tie-breaking rule cycles through six dictionaries (Vanderbei 2014, pp. 26–27).
The chapter answers the question with two pivoting rules under which the simplex method provably terminates, and then draws the consequence that makes linear programming a finite theory: the fundamental theorem of linear programming. This mission formalizes the chapter's four numbered theorems in Vanderbei's own setting of standard-form problems with slack variables.
Timeline. Hoffman (1953) and Beale (1955) gave the first examples of cycling. The perturbation and lexicographic methods go back to Charnes (1952) and to Dantzig, Orden and Wolfe (1955). Bland (1977) introduced the smallest-index rule and proved that the simplex method terminates under it (Bland 1977).
A linear program in standard form has constraints and decision variables:
A solution is feasible if it satisfies every constraint, and optimal if in addition it maximizes the objective among feasible solutions. The problem is infeasible if no feasible solution exists, and unbounded if it has feasible solutions with arbitrarily large objective values.
The slack variables are appended to the list of variables as , so that the constraints become the linear system with in . A dictionary is given by a set of basic indices whose columns of are linearly independent; the remaining indices are nonbasic. Solving for the basic variables gives
The basic solution of the dictionary sets the nonbasic variables to zero. The dictionary is feasible if for every , and degenerate if for some .
The simplex method (Phase II) starts at a feasible dictionary and repeats a pivot: an entering variable is chosen among the nonbasic variables with , and a leaving variable among the basic variables with that minimize the ratio ; then becomes basic and nonbasic. The method stops when no is positive (the dictionary is optimal) or when the entering column has no positive (the problem is unbounded). A pivoting rule resolves the remaining choices. Bland's rule chooses both the entering and the leaving variable as the candidate with the smallest index. The lexicographic rule perturbs the right-hand sides by symbols all data and chooses the leaving variable by the perturbed ratio test.
From every feasible dictionary , there is no infinite sequence of pivots
in which both the entering and the leaving variable follow Bland's rule; and a finite sequence of such pivots reaches a dictionary at which the method stops, optimal or exhibiting unboundedness.
The result. Termination under Bland's rule is what turns the simplex method from a heuristic into an algorithm. Combined with Phase I, it yields the fundamental theorem of linear programming, which reduces the search for an optimum to finitely many basic solutions and underlies the duality theory of the following chapters. Bland's rule also needs no perturbation or extra bookkeeping, and it is the anticycling rule used in many correctness proofs of simplex-type and combinatorial pivoting algorithms, including oriented-matroid programming.
Formalizing it. All four theorems are classical and proved. The Prove2Me library has the lexicographic rule and a nondegenerate termination theorem in the tableau setting of Bertsimas and Tsitsiklis (equality form , , full row rank), and the existence of basic feasible and optimal solutions in that form. It has no statement of Bland's theorem, and none of Vanderbei's dictionary formulation over . This mission produces a machine-checkable model of dictionaries and pivoting rules in that formulation, and targets Bland's theorem, whose proof is a genuine combinatorial argument rather than a monotonicity argument.
The natural argument for termination is monotonicity: each pivot increases the objective, so no dictionary repeats. It fails exactly at degenerate pivots, where the step length is zero and the objective and the basic solution do not change. Bland's rule gives no potential function that strictly increases along degenerate pivots, so the proof has to reason about a hypothetical cycle as a whole: which variables enter and leave the basis within it, and how two dictionaries of the cycle, in which the same variable leaves and later enters, constrain each other's coefficients. Relating the coefficients of two different dictionaries of the same problem is the step that has no counterpart in the model's definitions and has to be developed.
For Theorem 3.2, the symbols cannot be replaced by a fixed small real number: the method treats them as formal quantities on separate scales, and the statement is about that symbolic rule.
Vectors are Fin n → ℝ, Fin m → ℝ, and the constraint matrix is Matrix (Fin m) (Fin n) ℝ. The variables are indexed by Fin (n + m) with the decision variables first and the slacks after them, which is the order that Bland's rule compares. A dictionary is a structure holding its basic set, a proof that it has elements and a proof that its columns of are linearly independent; the coefficients are computed as coordinates in the basis of basic columns. A dictionary is therefore determined by its basic set, as the proof of Theorem 3.1 uses. "Basic solution" is defined through such a dictionary, not as a support condition.
Termination is stated as the nonexistence of an infinite run from a feasible dictionary, for Theorems 3.2 and 3.3. The goal adds that a finite Bland run reaches a stopping dictionary, so that it cannot hold because pivots fail to exist. The lexicographic rule is encoded by lexicographic comparison of the coefficient vectors of the perturbed ratios; the symbol is attached in the starting dictionary to its -th basic variable in increasing index order, which for the initial dictionary is the -th constraint. Unboundedness in Theorem 3.4 is "for every a feasible solution with objective ", as defined on p. 7. The statements carry no explicit constants.
A formalization that stated Theorem 3.3 for arbitrary pivot sequences with pairwise distinct bases would be Theorem 3.1's counting argument, not Bland's theorem; the goal is stated for pivots that follow Bland's rule and only those.
A complete development needs: the pivot update of a dictionary and the invariance of the solution set under it, feasibility preservation by the ratio test, the relation between the objective rows of two dictionaries, and finiteness of the set of bases. These are reusable for any later formalization of simplex-type algorithms. Proofs of the milestones, alternative proofs of Theorem 3.3, and Phase I (to connect Theorem 3.4 with the algorithm) are welcome.
The subgradient method for a nonsmooth convex function converges, but slowly: when the level sets of the objective are elongated, the subgradient is nearly orthogonal to the direction towards the minimum, and the method zigzags. For smooth functions the remedy is a change of metric (Newton and quasi-Newton methods); for nonsmooth functions no Hessian exists to supply one. N. Z. Shor's answer was to learn a metric from the subgradients themselves: after each step, stretch the space along the latest (transformed) subgradient, so that components of future subgradients parallel to it are damped. These subgradient methods with space dilation along the gradient (SDG methods) are the ancestors of Shor's r-algorithm and of the ellipsoid method, which the book (p. 49) describes as a special case of the same family and which Khachiyan later used to show that linear programming is solvable in polynomial time.
Section 3.4 of Shor's monograph (Springer 1985, translated by K. C. Kiwiel and A. Ruszczyński, doi:10.1007/978-3-642-82118-9) proves that, under a two-sided condition on the objective, a suitable SDG method decreases function values at the speed of a geometric progression whose ratio is invariant under nonsingular linear changes of variables. This mission formalizes that chain of results.
Let be the -dimensional Euclidean space with inner product . For a unit vector and a coefficient , the operator of space dilation along is
which multiplies the component of along by and leaves the orthogonal complement fixed.
Let and let be a generalized gradient: a subgradient of when is convex, an almost-gradient when is almost differentiable. The SDG method starts from and a nonsingular operator . At step : if it stops; otherwise it forms the transformed gradient , the direction , and
with a stepsize and a dilation coefficient . So is the accumulated space transformation, , and each step is a subgradient step for in the variables .
The quantitative results assume, for a point and the ball , the two-sided condition
For a convex function the lower inequality holds with ; the upper one bounds how far is from a positively homogeneous function around .
Under (3.18), with , , stepsizes , a constant coefficient , and a bound for on : there are and indices with
and for every
The result shows that one fixed rule, depending only on , and , yields linear convergence of function values for every objective satisfying (3.18), at a ratio that does not deteriorate when the problem is badly scaled: the method, and hence its rate, is invariant under nonsingular linear changes of variables. This is the property the ellipsoid method inherits (Section 3.8 of the book), and the same space-dilation machinery drives the r-algorithm (Section 3.7), still used for large nonsmooth problems such as Lagrangian duals of integer programs.
The theorems are proved in the book; none of them, and no space-dilation method, has a machine-checked proof to our knowledge, and the platform has no statement about variable-metric subgradient methods. The mission provides a reusable formal model of the SDG iteration, the eigenvalue-growth arguments behind Theorems 3.1–3.2, and the one-step invariant of Theorem 3.3. The formalization also corrects two points of the printed text (see Formalization scope).
Theorem 3.3 is a one-step computation, but Theorems 3.1 and 3.2 are not: they relate the size of the transformed gradients to the growth of the singular values of , whose determinant is . A bound on at a single step says nothing, since the dilations can concentrate in few directions; the argument has to control the largest singular value of over many steps against the geometric-mean lower bound . The dimension enters the rate exactly through this comparison. Theorem 3.4 then needs the invariant of Theorem 3.3 to keep every iterate inside , where (3.18) and the bound are available.
EuclideanSpace ℝ (Fin n) with in the rate statements. Operators are continuous linear maps; is a continuous linear equivalence and its inverse. The state is produced by a defined recursion sdg, not assumed; is gTilde.α (k+1). When the state is repeated, which encodes the book's stop; no division by zero is used.Useful infrastructure, reusable for the r-algorithm and ellipsoid chapters: identities for , determinants and singular values of products of rank-one dilations, and the invariance of the SDG iteration under a linear change of variables. Proofs of any milestone, and alternative arguments for Theorem 3.1, are welcome.
Many optimization problems in operations research have objectives that are convex but not differentiable: the maximum of finitely many linear or smooth functions, the value function of a Lagrangian dual, the cost of a two-stage linear program as a function of the first-stage decision. Gradient methods do not apply to these directly. N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer Series in Computational Mathematics 3, 1985; translated by K. C. Kiwiel and A. Ruszczyński from the 1979 Russian edition) develops the algorithms that replace the gradient by a subgradient, and its first chapter sets up the calculus of subgradients these algorithms rely on.
This mission is the first of a series formalizing the book. It covers §1.2 (convex functions and the concept of subgradient) and §1.3 (rules for computing subgradients), printed pages 7–16. Every later mission in the series (the subgradient method, space dilation, the ellipsoid method, decomposition) assumes that a subgradient of the objective can be computed, and §1.3 is where the book explains how: by combining subgradients of simpler pieces.
Write for -dimensional Euclidean space with inner product and norm . A function with domain a convex set is convex if its epigraph is convex, equivalently for and .
Let be an interior point of . A vector is a subgradient (or generalized gradient) of at if
The set of all subgradients is the subdifferential, written or . For differentiable at it is the single gradient; for on it is at .
The one-sided directional derivative of at in direction is
A direction is a direction of steepest descent at if .
For convex on and , the function is convex and, at every ,
Both inclusions are part of the goal.
The result. Theorem 1.12 is the finite-dimensional, finite-valued case of the Moreau–Rockafellar sum rule. With Theorem 1.13 it is the book's recipe for computing subgradients of functions assembled from simple pieces by nonnegative combinations and pointwise maxima, the two operations that produce most nonsmooth convex objectives in practice (Lagrangian duals, penalty functions, piecewise-linear costs). Theorem 1.8 identifies the directional derivative with the support function of the subdifferential; the Corollary and Theorem 1.11 give the optimality condition and the steepest-descent direction that every descent method for nonsmooth convex functions starts from.
Formalizing it. These results are classical and have been proved many times in textbooks (Rockafellar, Convex Analysis, 1970, §23). Mathlib at the pinned revision has convexity, separation theorems and Carathéodory's theorem, but no subdifferential of a convex function on and no max formula. The mission builds that layer: a subdifferential with the book's inequality (1.3), a one-sided directional derivative defined as a right-hand limit, and the calculus rules above. The platform has a Clarke-gradient analogue of Theorem 1.8 for locally Lipschitz functions and a Banach-space sum rule for ; neither states the convex, finite-dimensional results here.
The inclusion "" in Theorem 1.12 is immediate from (1.3). The inclusion "" is the content: a subgradient of the sum is a global object, and nothing in (1.3) splits it into subgradients of the pieces. Adding the inequalities of the pieces only produces vectors of the right form; it does not show every subgradient of arises this way. Any argument has to use the finite dimension and the interior-point setting, which is where Theorems 1.7 and 1.8 (existence of subgradients, compactness of , existence of one-sided derivatives) come in.
Theorem 1.8 in turn needs the existence of a finite right-hand limit of the difference quotient, which requires both monotonicity of the quotient and a lower bound, and the existence of a subgradient attaining the maximum, which is a separation statement. Theorem 1.9's "if" direction must rebuild convexity from one-sided derivative information alone, with no differentiability assumption.
EuclideanSpace ℝ (Fin n) and is inner ℝ x y. A function is f : EuclideanSpace ℝ (Fin n) → ℝ; the domain is a set, convexity on it is ConvexOn ℝ M f (which includes convexity of ), and interior points are x₀ ∈ interior M. Theorems 1.9, 1.10, 1.12 and 1.13 are stated on all of (Set.univ), as the book proves them.subdifferential M f x₀ is the set of with for all . It is defined for any ; the interior-point assumption is a hypothesis of each theorem that needs it.HasOneSidedDirDeriv f x₀ η d is the right-hand limit Tendsto … (𝓝[>] 0) (𝓝 d), not Mathlib's two-sided lineDeriv. Maxima and minima are stated with IsGreatest/IsLeast (attained), never with sSup/sInf.Fin k; and zero coefficients are allowed, as in the book. Theorem 1.13's maximum is Finset.sup' over Fin m with , and it asserts only the inclusion the book states.geometric_hahn_banach_*, Carathéodory and Krein–Milman, ConvexOn.continuousOn_interior) and are not restated.Contributions welcome: proofs of any milestone, a reusable lemma that the difference quotient of a convex function is monotone in , and a general max formula; these are reusable in the later missions of the series, which define subgradients the same way.
Optimal control of queueing systems leads to Markov decision problems whose state space is countably infinite (buffer contents, numbers of customers) and whose costs are unbounded (holding costs grow with the queue). Such a problem cannot be solved on a computer as it stands. The standard remedy is to truncate: solve a finite problem on the states and hope that its value and its optimal policy approximate those of the original problem as grows. Linn Sennott's approximating sequence method (ASM) makes this hope precise. For the expected discounted cost criterion, Sections 4.6–4.7 of Sennott's book (Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999) identify a single condition, Assumption DC(), that is necessary and sufficient for convergence of the truncated values, and give checkable sufficient conditions for it.
The method matters because naive truncation can fail. The book's Example 4.6.1 has a chain whose value at state is finite, yet a natural truncation produces values . How the probability that would leave the truncated set is redistributed decides whether the computation is meaningful.
Earlier truncation schemes (Fox 1971; White 1980, 1982; Hernández-Lerma 1986; Cavazos-Cadena 1986; Whitt 1978–79; see the bibliographic notes on p. 81 of the book and Puterman 1994) require bounded rewards or pass directly to an algorithm. The ASM instead produces a sequence of finite Markov decision chains that can be studied in their own right; the material of Sections 4.6–4.7 is presented in the book as new.
A Markov decision chain (MDC) has a countable state space ; for each state a finite nonempty action set ; nonnegative finite costs ; and transition probabilities with . A policy chooses the action at time at random from a distribution on that may depend on the entire history . A stationary policy always chooses in state . Fix a discount factor . The discounted cost of and the discounted value function are
both in , the infimum over all policies. A policy is discount optimal if .
An approximating sequence consists of finite nonempty sets increasing to and, for and , probability distributions on with as . The finite MDC has state space and the same actions and costs; is its value function and a stationary policy attaining the minimum in its discount optimality equation
An augmentation type approximating sequence (ATAS) keeps the original probabilities inside and redistributes the excess probability , , according to augmentation distributions on : .
Assumption DC(): for every , and .
The following are equivalent:
Under either, every limit point of (a stationary with eventually along a subsequence, for each ) is discount optimal for .
Theorem 4.6.3 turns the question "does truncation work?" into the verification of one inequality between a lim sup and the true value, and it delivers both the value and an optimal stationary policy from finite computations. Propositions 4.7.4–4.7.6 give conditions that hold in the queueing models of the book with unbounded holding costs, and Corollary 4.7.5 supplies the computational form used for the inventory model of Chapter 5. The discounted theory is also the stepping stone to the average cost ASM of Chapter 8, which is built on discounted approximations.
All results are proved in the book. None of them is formalized: the platform has no statement about approximating sequences or state truncation of countable-state MDPs, and Mathlib has no Markov decision processes. The mission produces machine-checked versions of the convergence theorem and its sufficient conditions, for general history-dependent randomized policies and -valued costs.
The value functions are infima over uncountably many history-dependent policies and may be infinite, so no contraction argument applies: costs are unbounded and is only the minimal nonnegative solution of its optimality equation. Passing to the limit in inside is an interchange of limit and infinite sum under a moving probability measure, with no dominating function in general; Example 4.6.1 shows that the interchange genuinely fails. The upper bound of Proposition 4.7.4 requires comparing with along a coupled first passage out of , which needs the taboo-probability estimates of Lemmas 4.7.2–4.7.3. The obvious idea of bounding by works only for bounded costs (Proposition 4.7.1).
The state type S is countable ([Countable S]); actions live in a type Act, with a finite nonempty Finset of admissible actions per state. Costs are ℝ≥0, transition probabilities and all value functions are ℝ≥0∞, so infima over policies are lattice infima and is a legitimate value. A general policy is a function of the history, encoded as the list of past state–action pairs (most recent first) and the current state; the expected cost at time is the -valued sum over histories. is the infimum over all such policies; a stationary policy enters as the policy putting mass one on . The discount factor is α : ℝ≥0 with (the chapter's standing assumption). is an MDC on the subtype ; is extended by when or , a convention that affects finitely many for each fixed and hence no limit in . Limits, lim sups and lim infs are along Filter.atTop in ℝ≥0∞. Taboo probabilities and the first passage quantity (so ) are defined combinatorially from the transition probabilities.
A trivializing formalization is ruled out: is not an infimum over stationary policies only (which would make optimality of limit points close to definitional), DC() keeps both of its conditions, and statement (i) of the goal includes finiteness of .
A complete development needs the minimality of among nonnegative solutions of the discount optimality equation (Theorem 4.1.4, chunk II of this series), Fatou-type lemmas for sums against converging distributions (Appendix A, chunk XI), and compactness of stationary policies (Proposition B.5). Contributions of these as reusable lemmas about countable-state MDCs are welcome.
The solution concept of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944) is defined from two ingredients: a set of imputations and a domination relation between them. A solution is a set of imputations that is internally stable (no member dominates another) and externally stable (every non-member is dominated by some member). In §65 of the book the authors observe that this definition never uses what imputations and domination actually are. They abstract it to an arbitrary set and an arbitrary relation on , and ask which properties of guarantee that exactly one solution exists.
The abstract notion is what graph theory now calls a kernel of a directed graph: draw an arc whenever ; a solution is a set of vertices that is independent and absorbs every vertex outside it. Kernels appear in combinatorial game theory (the losing positions of a finite impartial game form a kernel of its move graph) and in the theory of preference and choice.
Timeline.
Let be an arbitrary set and an arbitrary relation on ; is read " dominates ". A solution (in for ) is a set with
For , an element is a maximum of if and no has ; the set of maxima is .
For , condition says: never with and all . The relation is acyclic if it satisfies every , ; in particular never . It is strictly acyclic if there is no infinite sequence in with for every . Property (65:K) says that every non-empty has . A partial ordering (65:B) is a transitive relation for which at most one of , , holds.
For the main theorem the book constructs a candidate solution by induction (65.7.1): ; ; is the set of elements of dominated by some element of ; . With the first index for which ,
In Lean the elements live in a type α, D V : Set α, and S : α → α → Prop with S x y meaning ; the predicates are IsSolution D S V, maxima E S, IsAcyclic, IsStrictlyAcyclic, HasMaximaProperty, IsPartialOrdering, ConditionG, and the construction stageA, stageB, stageC, V0.
If is finite and is acyclic on , then
The result itself. (65:X) is the most general of the book's three existence-and-uniqueness theorems for solutions (complete ordering, partial ordering, acyclic relation; 65.8.1). For games proper it has no direct application: the set of imputations of an essential game has no maxima, so (65:K) fails (65.9.1). Its role is to isolate a sufficient condition for a unique solution. With (65:Z), and applied to every subset of , it characterizes the finite relations for which every subset has exactly one solution: exactly the acyclic ones (65.8.2). In graph language it is the statement that a finite directed acyclic graph has exactly one kernel. In combinatorial game theory this is the partition of the positions of a finite impartial game into P- and N-positions. The complete- and partial-ordering results (65:E)–(65:I) are the special cases the book treats first.
Formalizing it. The results are classical and fully proved in the book; to the best of our knowledge none of them is on the Prove2Me platform, and Mathlib has well-foundedness (WellFounded, RelEmbedding of ℕ) but no kernel or von Neumann–Morgenstern solution notion for an abstract relation. The mission produces machine-checked proofs of the book's §65 chain: the equivalence of (65:K) with strict acyclicity for arbitrary sets, the finite equivalence of acyclicity and strict acyclicity, the explicit construction of , and the characterization of 65.8.2.
Most of the individual steps are short. The work is in making the book's finite induction precise. The sets are defined recursively and refers to the first empty stage . The uniqueness proof (65:V) is a minimal-counterexample argument over the stage index, which moves between "smallest with " and the disjoint decomposition (65:U) of into the and . A tempting shortcut, taking an arbitrary well-founded rank function instead of the book's construction, proves existence and uniqueness but not that the solution is the of (65:2), which is part of the goal. For (65:P) and (65:O:c) the difficulty is the passage between finite cycles and infinite chains. Going from a chain in a finite set to a repetition needs a pigeonhole argument, and going from a set without maxima to a chain needs dependent choice.
α; D, E, V are Set α; the relation is S : α → α → Prop and is only ever consulted on elements of the set under consideration, so it is the book's relation on (or its restriction to ). Finite and infinite sequences are functions ℕ → α.IsSolution D S V is the set equation (65:1) literally; it forces . Uniqueness in the goal is ∃! over all V : Set α, not over a subtype; there is no degenerate reading in which the solution is fixed by construction.IsAcyclic D S requires for every , all cycle elements in . The case is excluded, as in the book (it would be unsatisfiable). This is equivalent to the absence of a Relation.TransGen loop inside , but the book's form is stated.stageA D S k is the book's . V0 D S is the union of all , which equals because every later is empty.D.Finite and IsAcyclic D S. (65:H) and (65:I) carry the partial-ordering hypothesis (65:B:a), (65:B:b) of 65.5.1, and (65:I) also finiteness of . (65:O:c), (65:P) and (65:Z) are for arbitrary and , as 65.6.2 and 65.8.2 state. The empty is allowed everywhere; there the unique solution is .Set.Finite, dependent choice for (65:P). The definitions are reusable for any later work on kernels of digraphs and on abstract stable sets. Proofs of any milestone, and alternative proofs of the goal, are welcome.The theory of Theory of Games and Economic Behavior (von Neumann and Morgenstern, 1944; 3rd ed. 1953) rests on one object: the characteristic function , the amount a coalition of players can secure for itself whatever the other players do. For zero-sum -person games, Chapter VI defines and proves (25.3.1 and 26.1.1) that the set functions arising this way are exactly those with , and superadditivity. Economic applications, however, are rarely zero-sum: exchange and production create value. Chapter XI extends the theory to general (non-zero-sum) games by adding a fictitious player who absorbs the total gain, and §57 answers the question that decides the scope of this extension: which set functions are characteristic functions of general games?
The answer, that these are exactly the superadditive set functions vanishing on the empty set, is the reason why the cooperative game theory that followed could take "a superadditive with " as its primitive object, usually without any underlying strategic game.
A general -person game in normalized form has players . Player chooses with , without knowing the choices of the others, and receives the real amount . No condition is imposed on . The game is zero-sum if .
The zero-sum extension (56.2.2) adds a fictitious player , who has no move and receives
Write . For , the coalition and its complement play a zero-sum two-person game. The pure strategies of are the tuples of choices of its real members. A mixed strategy of is a single probability distribution over these tuples, so the members of a coalition randomize jointly, and likewise for . The payoff to is . Then
where is the expected payoff to . The function on all is the extended characteristic function; its restriction to is the restricted characteristic function (57.1). For a zero-sum game the restricted function is the characteristic function of Chapter VI.
For every and every set function on the subsets of ,
and for every set function on the subsets of ,
In each direction a single game realizes on every set simultaneously; is not constrained.
The characterization fixes the domain of Chapter XI: every statement about solutions of general games is, by 57.3.4, a statement about superadditive set functions with , and conversely every such function is attained by a strategic game. That converse justifies studying cooperative games abstractly. (57:G) separates the zero-sum and constant-sum subclasses inside this domain. (57:B) and (57:C) quantify how much of a player's strategic role survives when his moves are removed, which is the book's justification for the fictitious player.
Status: all results are proved in the book (1944). To our knowledge none of them is machine-checked; the Prove2Me catalog has superadditive and convex cooperative games, but none tied to a strategic game, and no characteristic function built from a minimax value. The work here is formalizing the known proofs.
Necessity reduces to the zero-sum theory applied to , but still requires the minimax theorem for the coalition's two-person game and a careful treatment of joint mixing when two disjoint coalitions merge. Sufficiency requires building one finite game whose coalition values equal an arbitrary superadditive exactly, for all coalitions at once. The obvious attempt, choosing payoffs coalition by coalition, fails because the payoffs are shared: a construction that gives the right value can change the value of every set that overlaps . The difficulty is to obtain the upper bound for every simultaneously. For the extended function there is a further difficulty. The fictitious player has no move, so the values on sets containing are forced by the others, and they must be reconciled with (57:1:b).
For (57:B), the target game must reproduce an arbitrary zero-sum characteristic function while one prescribed player's choice has no effect on any payoff.
Players are Fin n (book indices become ); sets of players are Finset (Fin n). The extended domain is Fin (n + 1) with the fictitious player Fin.last n, and is the complement in Fin (n + 1). A game (GeneralGame n) has strategies Fin (β k) per player and real payoffs; zero-sum is the predicate IsZeroSum. The fictitious player's single strategy is left out of the coalition's strategy tuples, which does not change the two-person game. Max and Min are ⨆/⨅ over Mathlib's stdSimplex on the coalition's strategy tuples (one joint distribution per coalition). Both simplices are nonempty and the payoff is bounded, so these are attained values and no junk value from an empty or unbounded supremum occurs.
Standing hypotheses and their instantiation:
GeneralGame;Γ.IsZeroSum and the requirement that the replacement game is zero-sum;No normalization is imposed: is arbitrary and nothing is reduced. Every statement is made for all ; the book's is not needed, so this is a strengthening.
A trivializing formalization is ruled out: the characteristic function is defined from the game through the coalition's minimax value, so it is never a free parameter, and the existence claims must produce one game for all coalitions at once.
Needed infrastructure: finite zero-sum two-person games with joint mixed strategies over dependent product types; the minimax theorem ((17:6), on the platform as AGT.zero_sum_minimax for matrices); and product decompositions of coalition strategy tuples. The coalition-value API is reusable for any mission built on characteristic functions (Chapters VI, IX–XI). Contributions of this API as separate lemmas are welcome.
Not stated: (57:E*), (57:F*) (given without proof on p. 535), the open question (57:D), and (57:H), because the notion of a "dummy" it uses (from 46.9 and 56.3) is not defined on these pages.
Many collective decisions are taken by coalitions that either carry the vote or do not: committees, legislatures, shareholder meetings, councils with weighted votes. In such a situation the only aim of a participant is to be part of a coalition that wins, and nothing is left to bargain about except the division of the prize inside the winning coalition. Chapter X of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) isolates exactly this class of zero-sum -person games, the simple games, and studies their numerical description by weighted majorities and their finite main simple solutions.
The chapter is the origin of a large later literature: simple games and weighted voting games are the standard model of voting bodies in political science and social choice (for instance the Shapley–Shubik power index, 1954). The characterization of which simple games admit homogeneous weights, and the solutions they carry, starts here.
A zero-sum -person game with players is represented by its characteristic function , a real function on the subsets of with , ( the complement) and for disjoint . An imputation is a vector with and ; dominates if some nonempty has and for ; a solution is a set of imputations none of which dominates another and which dominates every imputation outside it (30.1.1). The game is inessential when its reduced form vanishes identically, essential otherwise.
A coalition is flat if . The losing coalitions are the flat sets, and the winning coalitions are the sets whose complement is flat. The game is simple if it is essential and every coalition is winning or losing. denotes the minimal winning coalitions, those of which no proper subset wins.
Weights define the winning system , and under the conditions (50:B) (non-negative weights, no player with half the total weight, no ties) this is the weighted majority game . The weights are homogeneous if the advantage is the same for all in .
In §50 the game is taken in reduced form with , so . For numbers and a coalition let give to the players outside and to player in . When the satisfy for every , the set of all , , is a main simple solution.
namely the set of , , with , , the common advantage. Conversely, if solve on , then are homogeneous weights for the game if and only if
The result links two descriptions of a simple game. One is numerical: a vector of weights, normalized by homogeneity. The other is game-theoretic: a finite solution in which each minimal winning coalition forms and divides a fixed total among its members. When the weights are homogeneous they are, up to scale, the shares in the main simple solution. When a main simple solution exists, its shares are homogeneous weights exactly under the inequality (50:20). The criterion (50:J) behind it is the chapter's general tool for deciding which systems of "profitable" minimal winning coalitions yield a finite solution. It is used again in the enumeration of simple games in §§51–55.
All of the results are proved in the book. As far as a search of the Prove2Me library shows (queries on simple game, weighted majority, winning coalition and stable set, 2026-09-28), none of them has been machine-checked. The only stable-set statements on the platform concern feasible payoff vectors of convex games, which is a different domain. The mission therefore asks for a formal proof of the known results, including the case analysis of §50.5–50.6, and in doing so it produces a reusable Lean theory of simple games and their winning systems.
The characterizations of §49 are set-theoretic, but they depend on superadditivity to show that subsets of flat sets are flat, and on the strategic-equivalence description of essentiality. The substantial part is (50:J). Deciding whether is a solution means classifying every imputation by the set where it meets the shares .
The natural first attempt is to check only the minimal winning coalitions. It fails, because domination can be exercised through any winning coalition. The book's argument has to exclude sets of with by producing infinitely many undominated imputations against a finite . It also has to handle indifferent players with , whose presence makes larger than the coalition that generated . For the converse half of the goal, the obstacle is the strict inequality : the equations (50:17) are linear and say nothing about it.
Players are Fin n (the book's player is index ), coalitions are Finset (Fin n), and characteristic functions are Finset (Fin n) → ℝ. Imputations are vectors Fin n → ℝ, and systems of coalitions are Set (Finset (Fin n)). A game is identified with its characteristic function (by 26.1 every satisfying (25:3:a)–(25:3:c) arises from a game). The theory is the "old" one of 30.1.1 (49.1.1), with no excess. The definitions of imputation, domination and solution are the same as in mission V of this series and are restated here, because a draft cannot import another draft.
The standing hypotheses, stated in each theorem where the book has them in force:
The numbers are given for every player. Players in no minimal winning coalition, for whom the book defines no , do not affect any . In the converse of (50:K) the derived weights are for every player.
The goal is not the bare solvability of (50:17). A statement that only asserted " exists with (50:7), (50:17)" would reduce to linear algebra. The goal asserts that the set of is a solution in the sense of 30.1.1, with domination requiring a nonempty effective set, and it adds the converse equivalence with (50:20). The set is built from only, never from all of .
Welcome contributions: proofs of the §49 milestones, which form a small reusable library on winning and losing systems; a proof of (50:G) and (50:J); and lemmas connecting of a simple reduced game with the explicit formula (49:2), on and on .
Chapter VI of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) opens the general theory of zero-sum games with more than two players. The authors propose to describe everything that can be said about coalitions, compensations between partners and fights between coalitions through one numerical object, the characteristic function : the amount a group of players can secure for itself against all the others (25.2.1). The whole later theory of the book (imputations, domination, solutions, simple games, decomposition) is built on this set function, and the same object, under the name "coalitional game" or "TU game", is the starting point of cooperative game theory as a field (cores, Shapley value, nucleolus).
§§25–27 settle two foundational questions about it. First, which set functions arise as characteristic functions of actual games? Second, which characteristic functions describe the same strategic situation, and how is a canonical representative chosen? The answers (a complete characterization by three conditions, and the reduced form under strategic equivalence) are what later chapters, and much of the cooperative literature, use when they take "a characteristic function" as a primitive without reference to any game.
A zero-sum -person game in normalized form (11.2.3, 25.1.3) has players . Player chooses a pure strategy , , uninformed about the others' choices, and then receives the real amount , subject to (25:1)
Let and, for , . The book defines in 25.1.3 through a fictitious two-person game: all players of form one composite player , all players of another, . The pure strategies of are the aggregates (one choice for each ), those of are the aggregates , and receives (25:2)
A mixed strategy of is a probability vector on the set of all aggregates , and one of is a probability vector on the aggregates . With ,
The coalition therefore randomizes jointly: is one distribution over its members' strategy tuples, not a product of independent mixtures. The empty set and are coalitions too (footnote 2, p. 241).
The three conditions of 25.3.1 on a set function are
From 26.2 on, every set function satisfying them is called a characteristic function.
Two such functions are strategically equivalent (27.1) if for numbers with ((27:1), (27:2)). A function is reduced if all one-element coalitions have the same value, (27:3); with that common value written , (27:5). A game is inessential if the reduced form of its characteristic function is , and essential otherwise (27.3).
The "only if" half is 25.3.1; the "if" half is 26.1.1, which requires a single game realizing on every coalition simultaneously.
The characterization makes the three conditions (25:3:a)–(25:3:c) the complete axiomatics of zero-sum characteristic functions. Every later result in the book that is stated "for a characteristic function" (the solutions of the three-person game in §32, the simple games of Chapter X, the decomposition theory of Chapter IX) is thereby a result about zero-sum games, and conversely no further constraint on is hidden in the game model. The reduced form of §27 cuts the parameter space of characteristic functions by and turns essentiality into a sign condition, which is used throughout the rest of the book.
These results are proved in the book. As far as a search of the Prove2Me catalog shows (queries on characteristic function, coalition, strategic equivalence, inessential, superadditive), none of them is formalized there; the existing cooperative-game definitions on the platform use other normalizations ( only, no complementarity condition) and are not this object. The mission produces a machine-checked link between the non-cooperative model of an -person game and the cooperative set function, including the book's explicit game construction behind 26.1.1.
The "only if" direction requires comparing values of different two-person games: (25:3:c) asks that the coalition can guarantee as much as and separately, which rests on the coalition mixing jointly, and (25:3:b) needs the minimax theorem, since is a Max-Min for the opposite side. The "if" direction is an existence claim: from an abstract one must produce one finite game whose characteristic function matches on all coalitions at once. Producing, for each separately, a game with the right value is easy and proves nothing. The §27 results are finite linear algebra over set functions, but the uniqueness in (27:A) and the boundary equalities in (27:7) depend on using all three conditions.
Players are Fin n (the book's are ), coalitions are Finset (Fin n), is the complement Sᶜ, and set functions are Finset (Fin n) → ℝ. A game is a structure ZeroSumGame n with strategy sets Fin (β k), a field β k > 0 (finitely many and at least one pure strategy per player), real payoffs H τ k, and the zero-sum condition (25:1) as a field. An aggregate is a dependent function on the members of ; mixed strategies are elements of Mathlib's stdSimplex, and the coalition's is a single distribution on aggregates, as in 25.1.3. The Max and Min in are written as ⨆/⨅ over the simplices; these are nonempty and the bilinear form is bounded on them, so no junk value arises. No lower bound on is imposed: the book's statements remain true for and , so dropping the implicit is a harmless strengthening.
Standing hypotheses instantiated in the statements: finiteness of the strategy sets and (25:1) (25.1.3) are part of ZeroSumGame; the §27 results carry (25:3:a)–(25:3:c) as a hypothesis, the book's standing assumption from 26.2 on ("characteristic function"); (27:7) carries reducedness (27:3) and the definition (27:5) of ; strategic equivalence includes (27:1). The reduced form is the explicit function of (27:2), (27:4), with as a real division that only matters for .
A trivializing reading of the goal, "for every there is a game with ", is excluded: the statement asks for one game with as functions. The coalition value is not the value under independent mixtures of the members, which is smaller in general and for which (25:3:c) can fail.
A complete development needs the minimax theorem for finite matrix games (the platform's AGT.zero_sum_minimax covers it for matrices indexed by Fin (m+1), and can be transported to the aggregate types), bookkeeping for splitting and joining strategy profiles along and , and the construction of 26.1 with its zero-sum check. The profile-splitting lemmas and the value facts for coalition games are reusable for the book's Chapter XI (general games) and for any work on coalitional values of strategic games. Contributions welcome: the §27 milestones, which are self-contained, and the two directions of the goal.
A zero-sum two-person game in normalized form is a real matrix : player 1 chooses a row , player 2 simultaneously chooses a column , and player 2 pays player 1 the amount . Matrix games are the base case of non-cooperative game theory, the prototype of every minimax statement in optimization, statistics (Wald's decision theory) and online learning, and, through their equivalence with linear programming, a standard tool of operations research.
Chapter III of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; third edition 1953) gives the book's complete solution of these games. Timeline:
Player 1 has pure strategies , player 2 has pure strategies , and is an arbitrary real matrix (14.1.1). A mixed strategy of player 1 is a probability vector in the simplex
and similarly for player 2. The pure strategy is the coordinate vector . The expected payoff is the bilinear form (17:2)
The good strategies of player 1 form the set of those at which assumes its maximum; those of player 2 form the set of those at which assumes its minimum ((17:B:a), (17:B:b)). A saddle point of is a pair with for all . With pure strategies alone one has and ; the game is specially strictly determined when .
For a general real function (§13) the same notions are , , saddle points, and the sets (maximizers of ) and (minimizers of ), always under the book's standing hypothesis that these maxima and minima exist.
For all and : and if and only if
The statement fixes no value and no constant; it says which pairs of mixed strategies are optimal.
AGT.zero_sum_minimax, proved).After the goal: (17:E) the game is specially strictly determined iff each player has a pure good strategy.
(17:D) is the complementary-slackness description of the optimal strategy pairs of a matrix game: a good strategy puts weight only on pure strategies that are best replies to the opponent's good strategy, and conversely any pair of mutually supported best replies is optimal. It is the basis of support-enumeration methods for matrix games, of the equalizing arguments used to solve small games by hand (the book's Chapter IV applies it to Matching Pennies, Stone–Paper–Scissors and Poker), and of the rectangular structure of the set of optimal pairs. (17:E) connects the mixed-strategy solution to the pure-strategy theory of §14 and to the perfect-information games of §15.
The results are classical and proved in the book. The minimax theorem itself is already machine-checked on the platform (AGT.zero_sum_minimax), and Mathlib contains Sion's minimax theorem and the basic saddle-point lemmas for extended-real functions on sets. This mission adds the book's own chain: the §13 saddle-point calculus under its standing attainment hypothesis, the theorems of the alternative (16:C) and (16:F) in the simplex-normalized form the book uses, the reduction (17:A) to pure strategies, and the characterizations (17:C:f), (17:D), (17:E) of good strategies, which are not on the platform in any form.
The "if" direction of (17:D) cannot be proved from the support conditions alone by local reasoning: that a pair of mutual best replies consists of good strategies uses that the value equals , i.e. the minimax theorem. Without that equality the "if" direction of (13:D*) fails (points of exist but are not saddle points), so the calculus of §13 alone does not suffice. Likewise (16:C) is not a direct instance of the Farkas lemma forms on the platform: its alternatives are normalized to the simplex and the second one is strict, and both the existence and the mutual exclusion must be shown.
Lean conventions, fixed throughout:
Fin β₁, Fin β₂ (numbered from ), the matrix is H : Fin β₁ → Fin β₂ → ℝ, and is Mathlib's stdSimplex ℝ (Fin β).0 < β₁, 0 < β₂, or mixed strategies , , which force it. The theorems of the alternative assume (a matrix with rows and columns).MaxMinAttained φ, which says that , , and are attained. (13:D*) also carries the hypothesis of 13.5.2 that saddle points exist, stated as .⨆, ⨅; they are the book's attained values under the hypotheses above (compactness of the simplex and continuity of for the mixed game). (17:A) asserts attainment explicitly (IsLeast, IsGreatest). "Does not assume its maximum at " in the goal is written without any Max operator.A trivializing formalization is ruled out: and are not taken as hypotheses or defined through the support conditions, strategy sets cannot be empty, and no Max over an empty or unbounded set occurs.
Contributions welcome: proofs of the milestones, especially (16:C) (from Mathlib's convex separation or from a platform Farkas lemma) and the bridge from AGT.zero_sum_minimax to (17:C:f). The §13 lemmas and the (17:A) reduction are reusable by any mission about matrix games or bilinear saddle points.
Game theory as von Neumann and Morgenstern built it measures every outcome by a single number, the utility a player attaches to it, and combines those numbers linearly when an outcome is uncertain: a lottery that yields with probability and with probability is worth . Every later chapter of Theory of Games and Economic Behavior uses this without comment, from the value of a zero-sum game to the characteristic function of a coalition. Section 3 of the book justifies it: it states axioms on preferences and on the combination of alternatives with probabilities, and claims that they force utility to be a number, unique up to the choice of a zero and a unit. The proof, announced in 3.6.1 as "somewhat lengthy", was added as the Appendix The Axiomatic Treatment of Utility in the second edition (1947).
The result, the expected utility theorem, is the foundation of decision theory under risk and of expected-payoff reasoning in game theory, statistics and operations research. The axiomatics were later recast by Marschak (1950), Herstein and Milnor (1953) in the language of mixture spaces (Herstein–Milnor). This mission formalizes the original statement and its original proof structure.
A system of utilities (3.6.1) is an abstract set of entities , together with
The axioms are:
All weights lie strictly between and , and is identity. The expression is notation for an abstract operation: carries no linear structure. The Appendix mostly writes the operation as , and writes for " or ". In the Lean development the system is the structure UtilitySystem U with fields gt and mix; S.cmb γ u v is .
A numerical utility (3.5.1) is a map with
For every system of utilities satisfying (3:A)–(3:C):
The constants are chosen before . No assumption on the size of is made.
The milestones follow the Appendix's own chain:
The theorem turns an ordinal preference over uncertain prospects into a cardinal scale on which expectation is meaningful. It is what licenses replacing a player's preferences by numerical payoffs whose mixtures are averaged, which the rest of the book, and most of game theory and stochastic optimization after it, assumes. The uniqueness part (A:W) states exactly how much freedom the scale has: a positive linear transformation, i.e. zero and unit may be fixed at will and nothing else.
The theorem has been proved many times since 1947, in textbooks and in the mixture-space literature, but the book's axiom system differs from the later ones (it uses a strict order with identity, strict monotony, and the two algebraic axioms (3:C) only). As far as the curators know, neither this axiom system nor the Appendix's derivation has a machine-checked proof, and Mathlib has no mixture-space or expected-utility module. The mission produces a checked proof of the original theorem under its original hypotheses and a reusable abstract mixture-space layer.
The obvious argument treats as a convex set and as a convex combination, then reads the utility off the segment between two reference points. None of that is available. The operation is formal, so identities that hold in a vector space, idempotence included, must be derived from (3:B) and (3:C) alone; only one associativity rule (3:C:b), for a repeated right argument, is given. The correspondence between a utility interval and a numerical interval requires the continuity axioms (3:B:c), (3:B:d) and the completeness of the reals. The local scales on different intervals have to be fitted into one global function, and the linearity for pairs and has to be recovered from the case .
Type*); the relation is gt : U → U → Prop and the operation mix : OpenUnit → U → U → U, where OpenUnit is the subtype of . mix α u v stands for . The operation is not defined at (3.6.1, footnote 4) and is not extended there.UtilitySystem. The items from (A:E) on assume fixed or as explicit hypotheses, as the book does "from now on until we get to (A:V) and (A:W)"; the goal does not, since (A:V), (A:W) hold for every .A complete development needs only order theory and the completeness of the reals from Mathlib. The mixture-space layer (the structure, (A:A)–(A:C), (A:T)) is reusable for any later work on expected utility, including the generalization in §66 and 67 of the book. Proofs of any milestone, alternative routes to the goal (for instance through the Herstein–Milnor axioms, once shown to follow from (3:A)–(3:C)), and statements of the omitted intermediate results (A:G)–(A:Q) are all welcome.
A cellular automaton over a group with a finite alphabet is a map on configurations that updates every cell by the same finite local rule, read off from a finite neighbourhood of that cell. Cellular automata over go back to von Neumann and Ulam and are a standard model in symbolic dynamics; replacing by an arbitrary group links the theory to geometric group theory.
In 1973 Gottschalk asked which groups have the property that every injective cellular automaton over is automatically surjective, and called such groups surjunctive. For a finite group this is the pigeonhole principle, since is then a finite set. For infinite groups the configuration space is an uncountable compact space and the pigeonhole principle is no longer available. Gottschalk's surjunctivity conjecture states that every group is surjunctive. It is open.
Fix a group and a finite nonempty set (the alphabet). A configuration is a function ; the set of configurations is . It carries the product topology, where has the discrete topology; this makes compact.
The left shift of by is the configuration
written shift G g x in the Lean development. A map is shift-equivariant (IsShiftEquivariant) if for all and .
The group is surjunctive (IsSurjunctive) if, for every finite nonempty alphabet , every map that is continuous, shift-equivariant and injective is also surjective.
A map is a cellular automaton (IsCellularAutomaton) if there are a finite memory set and a local rule with
Three classes of groups appear in the milestones:
IsResiduallyFinite) if every lies outside some normal subgroup of finite index.Garrido.IsAmenable).IsSofic) if for every finite and every there are a finite nonempty set and a map such that for at least a fraction of the points whenever , and for at least a fraction of the points whenever .The result itself. A positive answer would make the implication "injective surjective" for cellular automata hold unconditionally, extending the pigeonhole principle from finite sets to all shift spaces . Surjunctivity is also tied to Kaplansky's direct finiteness conjecture: for a surjunctive group and any finite field , the group ring is directly finite (). A counterexample would be the first known non-sofic group, since sofic groups are surjunctive.
Formalizing it. Milestones 4–7 are proved results in the literature; milestones 1–3 are standard facts of the theory. At the time of writing, none of milestones 1–3 and 5–7 is known to exist as a machine-checked proof on this platform. Formalizing them requires building the basic theory of cellular automata over groups (memory sets, local rules, induced automata on subgroups), which can be reused by other work in symbolic dynamics. The goal theorem itself is open.
For infinite the space is infinite, so no counting argument applies directly. All known proofs approximate by finite objects: finite quotients (residually finite case), Følner sets with an entropy count (amenable case), or approximate finite permutation models (sofic case). No such approximation is known to exist for every group, and it is not known whether every group is sofic. A proof of the full conjecture therefore needs either a proof that every group is sofic or an argument that does not go through finite approximations.
Type (universe ). Alphabets are finite (Fintype) and nonempty; their topology is an arbitrary topology assumed to be discrete, and carries Lean's product topology.shift, not a MulAction instance, to avoid a clash with Mathlib's pointwise action on function types.Garrido.IsAmenable (finitely additive invariant probability measure on all subsets). Residual finiteness and soficity are defined in GottschalkSurjunctivity_Defs.Contributions welcome: the Curtis–Hedlund–Lyndon theorem, restriction and induction of cellular automata along subgroups, and the residually finite case are natural first steps.
Two-stage stochastic integer programs combine the two hardest features of mathematical programming: uncertainty in the data and integrality of the decisions. Even evaluating the objective of such a program at a single first-stage decision requires the expected optimal value of an NP-hard combinatorial problem. Chapter 8 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by A. H. G. Rinnooy Kan and L. Stougie, argues that for many such problems the way forward is probabilistic analysis: the random optimal value of the second-stage problem often converges, after normalization, to a simple function of the problem parameters, and that function can replace the intractable expectation.
The chapter illustrates this on the machine investment problem: first buy identical machines at cost each, knowing only the distribution of the processing times of jobs, then schedule the jobs once their processing times are revealed so as to minimize the makespan. This mission formalizes the chapter's analysis of that example: the almost sure asymptotics of the optimal makespan (8.13), its expectation version, and the asymptotic clairvoyance of the resulting two-stage heuristic.
Let be processing times: independent, identically distributed, nonnegative random variables on a probability space with mean and finite second moment . The instance with jobs uses the first of them.
An assignment of the jobs to identical machines is a map . The load of machine is and the makespan of is its largest load. The minimum makespan is
and the machine investment problem is to minimize over integers (8.9).
List scheduling takes the jobs in the order and assigns each to the first available machine, a machine of least current load (lowest index on ties). Its makespan is . Write and .
For §8.3, the estimate is minimized over integers by the heuristic first-stage decision , the better of and . A clairvoyant decision maker who sees the processing times first chooses minimizing .
For machine counts with ,
The machine count is allowed to grow with ; this is the regime the first-stage heuristic lives in, since is of exact order .
where is the list-scheduling makespan.
Result (8.13) says that the optimal value of an NP-hard problem, rescaled, is almost surely asymptotic to the elementary function of the data and the first-stage decision. Its expectation version replaces the intractable term in (8.9) by , and the clairvoyance statement shows that the heuristic built on that replacement loses asymptotically nothing, not even against a decision maker with full information. The chapter presents the example as the template for vehicle routing and location problems preceded by an investment decision.
All results here are classical and proved in the literature cited by the chapter (Lemma 8.1 is quoted from Feller without proof; the chapter refers to Dempster et al. for the asymptotic optimality of the two-stage heuristic and to Lenstra et al. for the notion of asymptotic clairvoyance). None of them has, to our knowledge, a machine-checked proof. The mission produces a formal model of identical-machine makespan scheduling and of list scheduling, the extreme-value estimates of Lemma 8.1 for square-integrable i.i.d. sequences, and the full chain from the strong law to (8.13).
The deterministic part is elementary on paper, but list scheduling is a recursively defined procedure, and its makespan bound has to be established for that recursion rather than for a picture like the chapter's Figure 8.3. The probabilistic core is Lemma 8.1: the strong law controls , but the error term is of order once grows like , and the strong law says nothing about maxima. With a fixed number of machines the whole statement would reduce to the strong law; the growth is exactly where the second moment is needed. For the clairvoyance statement, the clairvoyant choice is a random, unstructured minimizer, so its value must be bounded below without knowing where the minimum is attained.
Processing times are one sequence p : ℕ → Ω → ℝ, 0-based (the book's is p (j-1)), with each p j measurable, the family mutually independent (iIndepFun), identically distributed with p 0, pointwise nonnegative, p 0 ^ 2 integrable and ∫ p 0 = μ with μ > 0. Nonnegativity and are not printed in the book; they are implicit in "processing times" and in the division by . Machines are Fin m; a schedule is an assignment Fin n → Fin m, which is faithful because jobs are non-preemptive, machines identical and there are no precedence constraints.
The book writes ""; this is read as a function of with and (fun n => (m n : ℝ)) =O[atTop] (fun n => √n). Stating (8.13) for a fixed would trivialize it into the strong law and is ruled out. "" means that almost surely the limit exists and equals . Expectations are Bochner integrals of functions that are measurable and bounded by , hence integrable. List scheduling uses the index order and breaks ties towards the lowest machine index; both are admissible instances of the book's "arbitrary fixed order" and "first available machine". In the clairvoyance statement the minimum is over (the book writes ; no machine cannot process any job, and the Lean value is an empty-infimum convention). No explicit constants replace an O(·): the statements are limits and the O-hypothesis is carried as stated.
Out of scope: (8.14) and the p. 210 expectation statement, which need a positive density at and whose proof the book calls "far from easy", and the dynamic programming recursion of §8.3.
Needed infrastructure: finite maxima and minima of measurable functions, extreme-value estimates for square-integrable i.i.d. sequences (Lemma 8.1), and Mathlib's strong law. The makespan and list-scheduling definitions are reusable for other identical-machine scheduling results; alternative proofs of Lemma 8.1 and sharper forms of the clairvoyance statement are welcome.
Many engineering and economic planning problems must meet random requirements with a prescribed reliability: a reservoir must satisfy demand with probability at least , a power system must cover load except on rare days, an inventory must avoid shortage with high probability. Probabilistic constrained programming (also called chance-constrained programming) models this by requiring that a system of random inequalities hold jointly with probability at least .
The first obstacle to solving such problems is structural. The probability that random constraints are satisfied is, in general, neither concave nor convex in the decision, so the feasible set need not be convex and local search can stall. Prékopa's theory of logarithmically concave measures (1971–1973) removed that obstacle for a large class of distributions, and it is the basis of the numerical methods of Chapter 5 of Ermoliev and Wets, Numerical Techniques for Stochastic Optimization (Springer 1988). This mission formalizes the structural theorems of that chapter.
Timeline:
Let be a random vector in on a probability space and let . The chapter studies problem (5.1):
The function is the probability function (chanceProb in Lean). In the special case it equals , where is the joint distribution function of .
A function is logarithmically concave on a convex set if
Where this is concavity of ; the power form also makes sense where . Nondegenerate normal densities, uniform densities on convex bodies and exponential densities are log-concave.
Section 5.7 introduces the polynomial distribution (5.19) on the cube :
(polyDistF in Lean).
If are jointly concave on and has a log-concave density on , then
Its immediate consequence is that the feasible set is convex for every .
The platform theorem ConvexOptimization.prekopa_marginal_log_concave (Prékopa's marginal theorem, proved) is included as a reference item.
Theorem 5.1 turns a probabilistic constraint into a convex constraint after taking logarithms. This is what makes convergence proofs for nonlinear programming methods (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) applicable to (5.1) and to the reliability maximization problem (5.4); without it, those methods have no guarantee of finding a global optimum. Theorems 5.2.1 and 5.2.2 are the two facts that make the SUMT method of §5.2 well defined and convex on the interior of the feasible set. Theorem 5.7.2 shows that probabilistic constraints under the polynomial distribution define convex sets, so they can be added to geometric programmes.
On status: Theorem 5.1 is a classical result, proved in Prékopa's papers (the chapter itself refers to Prékopa's survey for the proof). Prékopa's marginal theorem and the Prékopa–Leindler inequality are already machine-checked on this platform; Theorem 5.1 and the §5.2 and §5.7 theorems are, as far as a search of the platform shows, not formalized. The work is formalizing known proofs, in the log-concavity predicate the platform already uses.
The obvious argument for Theorem 5.1, "the constraint set is convex and the density is log-concave, so the probability is log-concave", hides the real content: log-concavity of a probability as a function of a parameter is a statement about integrals, and it does not follow from pointwise properties of the integrand without a Prékopa–Leindler-type inequality. Concavity of each separately in and in is not enough; joint concavity in is used essentially. The probability function vanishes on large regions in typical examples, so any argument that takes logarithms pointwise fails at the boundary of its support.
For Theorem 5.2.2 the naive argument fails at the index : nothing about is assumed directly, and log-concavity of is exactly Theorem 5.1. For Theorem 5.7.1 the difficulty is a sign condition on a covariance; without the ordering hypothesis the mixed derivative can be negative.
and are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin q); the constraint functions take pairs in the product, and concavity is ConcaveOn ℝ Set.univ on that product (joint concavity). A "continuous probability distribution with density " is stated as P.map ξ = volume.withDensity (ENNReal.ofReal ∘ f) with and measurable and a probability measure. Log-concavity is the platform definition ConvexOptimization.LogConcaveOn (nonnegativity plus the power inequality), imported as a reference item; concavity of Real.log ∘ h₀ would be a different, wrong property because Lean's Real.log 0 = 0. Indices are 0-based (Fin r, Fin m, Fin N, Fin n); the probabilistic constraint of Theorem 5.2.2 is stated separately from . The polynomial distribution is a formula on Fin n → ℝ with real powers, used only on the cube.
No constant of the book is replaced by an explicit value: every result of this chapter is qualitative.
Corrections of the printed text, recorded in each item's Formalization Note:
deriv.Theorem 5.2.2 carries all six assumptions of §5.2, including compactness of the feasible set and the Slater point; it does not assume log-concavity of , which must be derived from the density and concavity hypotheses. A trivializing formalization, such as one with a density hypothesis that no probability law satisfies or a log-concavity predicate that holds for every function vanishing somewhere, is ruled out: the density hypotheses are satisfiable (checked locally) and LogConcaveOn is the multiplicative inequality at every pair of points.
Needed infrastructure: Prékopa's marginal theorem (available), log-concavity of indicators of convex sets and of products, measurability of the constraint set, and Artin's theorem that a sum of log-convex functions is log-convex (for Theorem 5.7.2). Artin's theorem and closure properties of LogConcaveOn are reusable beyond this mission, and contributions of them are welcome.
In a two-stage stochastic linear program a decision is taken before random data are observed, and a corrective recourse decision is taken afterwards at a cost. The objective contains the expectation of an optimal value of a linear program, , and for continuous or high-dimensional that integral cannot be evaluated exactly. Practical methods therefore replace by a discrete random vector and control the error by computable lower and upper bounds on the expected recourse cost. Chapter 2 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by P. Kall, A. Ruszczyński and K. Frauendorfer, surveys these bounds as they were used in the codes of the time: Jensen's inequality from below, the Edmundson–Madansky inequality from above, and the special structure of simple recourse, where the expected cost is available in closed form.
Timeline. Jensen's inequality (1906) gives the lower bound for a convex integrand. A. Madansky, "Bounds on the expectation of a convex function of a multivariate random variable", Ann. Math. Statist. 30 (1959), and H. P. Edmundson (RAND report, 1956) gave the upper bound by the two-point law on the endpoints of an interval, and its product version for independent components. Kall and Stoyan (1982), Huang, Ziemba and Ben-Tal (1977), Frauendorfer and Kall (1988) developed partition refinement of both bounds, the scheme this chapter describes; Frauendorfer (1988) extended the upper bound to dependent data on boxes.
The two-stage problem (2.11) is: minimize subject to , . The recourse cost is the optimal value of the second-stage problem (2.12),
with a deterministic matrix (fixed recourse), and when (2.12) is infeasible. Throughout the chapter the book assumes complete recourse, , and dual feasibility: for every realization of some satisfies . Under these assumptions is finite. The expected recourse function is .
The Edmundson–Madansky law of an interval , , with mean puts mass at and at (2.32). For a box and means , the vector with independent components of these two-point laws sits at the vertex with probability .
Simple recourse is the case , with , deterministic and random only. With the recourse cost splits into one-row costs if , and otherwise.
If has independent components with means , and is convex on , then
The book applies it to ; the goal is stated for every convex , with the explicit weights of (2.32).
The upper bound is the half of the bounding scheme that is not automatic. Jensen's inequality needs only a mean; an upper bound on the expectation of a convex function needs a bounded support and, in the product form, independence. Together they give a certified interval for the optimal value of a two-stage problem, and repeated partitioning of the support shrinks that interval; this is the basis of the sequential approximation methods of §2.2.4 and of later codes. The dual-multiplier bound and the simple-recourse formulas are the pieces that make those intervals cheap to compute.
The results are classical and proved in the literature cited on the page. The one-dimensional Edmundson–Madansky inequality and the general extreme-point form of the upper bound (a measure on the extreme points reproducing the barycentre) are already formalized on Prove2Me in the Introduction to Stochastic Programming series, as is the partition Jensen bound. The product form for independent components is not: deriving it from the extreme-point form requires constructing the product kernel, which is the content of this mission. The recourse properties (b), (d), (e) for a general distribution with finite second moments, the dual-multiplier bound and the simple-recourse formulas are not formalized anywhere known to this mission.
The obvious argument inducts on the dimension, applying the one-dimensional inequality in one coordinate while the others are held fixed. That step needs the conditional law of the remaining coordinates given the first to be their unconditional law, i.e. independence expressed as a product decomposition of the joint law, and it needs with one coordinate replaced by an endpoint to remain convex on the lower-dimensional box and integrable. For dependent components the inequality is false with these weights: on with means and , the product law gives while mass at and at gives . The book's remark that the product law is extremal among all laws on with the given mean fails for this reason when , and is not part of this mission.
For the recourse properties the difficulty is bookkeeping: is an extended-real optimal value, and finiteness, measurability in and integrability must be derived from complete recourse, dual feasibility and the moment hypothesis rather than assumed.
Vectors are functions from finite index types to (ι → ℝ), matrices are Mathlib Matrix, and random data live on a probability space (Ω, P). The recourse cost is an EReal infimum over the feasible set, so infeasibility gives and unboundedness exactly as on p. 39; theorems that integrate it carry complete recourse and dual feasibility, which make it finite. The expected recourse function integrates the real part of the recourse cost. Independence of the components is ProbabilityTheory.iIndepFun; the box is Set.pi univ (fun j => Icc (a j) (b j)), with , and values in the box are required almost surely. The upper bound is the explicit sum over Boolean vertex labels of products of the weights (2.32); no abstract extremal measure is used.
Conventions fixed where the page is silent or ambiguous:
recourseCost, expectedRecourse and dualLowerBound.A goal stated for affine (where it is an equality), or with allowed to be any discrete law with the right mean, would be trivial or a different theorem; the weights are the products of (2.32), and independence of the components is a hypothesis.
A complete development needs: finite-dimensional LP duality with extended-real values (reusable across all recourse missions), measurability and integrability of optimal-value functions, the conditional-independence step for product measures, and the one-dimensional chord inequality. The partitioned upper bound (2.37) and the discrete reformulation (2.21), (2.28) are natural follow-up statements on the same definitions.
One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in . Deciding whether two bins suffice is NP-hard (it contains the partition problem), so no polynomial-time algorithm guarantees a ratio below unless P = NP. The natural question is therefore asymptotic: how small can the additive error be made, as a function of the optimum ?
Its main device, geometric grouping followed by rounding a linear program over bin configurations, recurs in later additive results and in cutting-stock problems.
An instance is a finite multiset of piece sizes in the open interval . Write for the number of pieces, for the number of distinct sizes, for the total size and for the smallest size. A packing is a multiset of bins whose union is and in each of which the sizes sum to at most ; its cost is the number of bins, and is the least cost.
A configuration is a nonempty multiset of sizes occurring in that fits in one bin. The fractional bin-packing problem is the linear program
with one variable per configuration, where counts the pieces of size in configuration and the pieces of size in . Its value is . A basic feasible solution is an extreme point of the feasible region.
Geometric grouping with parameter sorts the pieces in non-increasing order and cuts them into consecutive groups , each the shortest run of pieces of total size at least . Within each group () only as many of the largest pieces as has are kept; they are rounded up to the largest size in , giving . The rounded pieces form , and together with the unrounded leftovers form .
ALGORITHM 2 with a positive integer and a positive real :
Its cost on is written .
For every instance with , every packing that ALGORITHM 2 with and can output is a packing of with
This is the paper's , with the constants that its proof yields.
For integers , and :
In attack order: Lemmas 1–3; Theorem 2 (items 1–3, the bound on , item 4 corrected); the per-iteration shrinking of ; the bound on the number of iterations; the telescoping of ; the bin count after Step 3; the general bound.
The bound gives a polynomial-time algorithm whose additive error is polylogarithmic in the optimum, hence a fully polynomial asymptotic approximation scheme (). Varying and trades running time for error, as the paper notes after Theorem 4. The scheme of solving the rounded LP, keeping its integer part and re-grouping the residual is reused by later additive results, including the bound of Hoberg and Rothvoss.
The result has been proved since 1982. No machine-checked proof of it, or of any bin-packing approximation guarantee of this kind, is known to exist in Lean or Mathlib. The mission produces a formal version whose hypotheses and constants are explicit. It also corrects two printed statements whose published forms are false: Theorem 2, item 4, and the chain of inequalities in the analysis that relies on it. The corrections are disclosed in the statements.
Rounding a single LP solution does not suffice. A basic solution of the configuration LP has at most fractional variables, and after rounding down, the leftover pieces form an instance of size at most . With linear grouping that leftover is of order and costs a constant factor. The difficulty is making the residual shrink geometrically. Geometric grouping must produce an instance with distinct sizes while discarding only in . The residual must then be re-grouped and re-solved. Each step must be accounted for simultaneously in , and , with an additive loss per iteration; the harmonic-sum estimate behind and the telescoping of across iterations carry most of the weight.
Multiset ℝ with sizes in the open interval ; real sizes generalize the paper's rationals, and the interval is open because a group of size at least must contain more than pieces. Packings are Multiset (Multiset ℝ). and are infima over nonempty sets. LP solutions are finitely supported functions on configurations; "basic" means extreme point.Alg2Run k g I P, witnessed by a trace. Every bound holds for every run: every admissible subroutine output, every packing at Steps 2 and 3 within the prescribed counts, every choice of pieces for the principal bins (which must fill every available slot), and every order of the Step 4 insertion. A separate well-definedness item states that a run exists, so the bounds are not vacuous.Real.log and is Real.logb 2.Contributions welcome: milestone proofs; a harmonic-sum bound ; extreme-point facts for (at most as many nonzero coordinates as rows; an optimal extreme point exists), reusable beyond bin packing; monotonicity of and under the piecewise order.
The free Schrödinger operator is the Hamiltonian of a quantum particle, or of non-interacting particles, moving in without external forces. Every Schrödinger operator studied in quantum mechanics is a perturbation of it, and each standard tool of the theory refers back to : the Kato–Rellich theorem asks that be relatively bounded with respect to , Weyl's theorem compares essential spectra with that of , and scattering theory compares the dynamics with the free dynamics . Knowing exactly what is (its domain, its self-adjointness, its spectrum and its time evolution) is therefore the base case of the spectral theory of Schrödinger operators.
All of this is obtained from one tool, the Fourier transform, which turns differentiation into multiplication. This mission follows Chapter 7 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), doi:10.1090/gsm/099. The chapter first develops the Fourier transform on the Schwartz space, on and on , and then applies it to . The same material appears in Reed–Simon (Vol. II, Sec. IX.1 and IX.7).
Write for Euclidean space with and . For an integrable the Fourier transform and its inverse are
The Schwartz space consists of the smooth functions all of whose derivatives decay faster than any polynomial. and are the usual Lebesgue spaces, and denotes the continuous functions vanishing at infinity. The convolution of is .
The Sobolev space is . The free Schrödinger operator is
in units with and mass . Its time evolution is . For a linear operator with domain , the resolvent set is the set of for which maps bijectively onto the Hilbert space with a bounded inverse , and the spectrum is . For self-adjoint and a vector , the spectral measure is the finite Borel measure on with for all . The absolutely continuous, singular continuous and pure point spectra are the spectra of restricted to the vectors whose spectral measures are of the respective type. A subspace is a core if the closure of is .
For , is self-adjoint and
In the Lean statement the spectral-type part is the equivalent assertion that every spectral measure of is absolutely continuous with respect to Lebesgue measure.
The result. Theorem 7.8 says that a free quantum particle has no bound states and that its energy spectrum is purely absolutely continuous and fills . Combined with the RAGE theorem this gives the escape of every free wave packet from bounded regions, and Lemma 7.10 makes the escape quantitative: at large times the position distribution is the momentum distribution rescaled by . The self-adjointness of on and the core are the inputs to the Kato–Rellich treatment of atomic Hamiltonians, and is the reference spectrum of Weyl's theorem and of the HVZ theorem.
Formalizing it. The results are classical. Mathlib contains the Fourier transform on , Schwartz space and in the normalization (including Fourier inversion, Riemann–Lebesgue and the isometry), and the Prove2Me corpus holds several of these as FamousTheorems in that normalization. What is missing is Teschl's normalization with its constants, the spectrum of the Fourier transform, the operator as an unbounded self-adjoint operator, its resolvent spectrum and spectral type, and the free dynamics. This mission produces these objects in a form the later chapters (Kato–Rellich for atoms, Weyl, HVZ, scattering) can build on.
The Fourier-analytic milestones are close to Mathlib but not in it: every constant has to be transported from the -in-the-exponent convention to Teschl's convention, including the branch of in Lemma 7.3 and the phase in Lemma 7.10. The lower bound in Theorem 7.5 needs an eigenfunction for each fourth root of unity, which the book defers to the Hermite functions of Section 8.3.
For the goal, self-adjointness and require working with the resolvent spectrum of an unbounded LinearPMap, which Mathlib does not provide, and transporting self-adjointness and resolvents through the unitary Fourier transform. The spectral-type statement requires identifying the spectral measure of an unbounded operator from its resolvent alone, without a spectral theorem in the library, and showing that it has a density for every , not only for nice . Lemma 7.9 is a statement about the graph norm of , which is not controlled by the norm alone.
is EuclideanSpace ℝ (Fin n), so that and are the Euclidean ones, and is Lp ℂ 2 volume. fourier and fourierInv are Teschl's integrals (7.3) and (7.8) with the prefactor . The transform (fourierL2) is Mathlib's unitary transform rescaled by , and Theorem 7.5 asserts that it is the unitary extension of (7.3). (freeHamiltonian) and (timeEvolution) are defined as Fourier conjugates of the maximal multiplication operator by the symbol of and of multiplication by , written with Mathlib's transform, where the symbol is . These are the same operators as Teschl's, and the domain is exactly . Unbounded operators are Mathlib LinearPMaps, self-adjointness is Mathlib's IsSelfAdjoint, and the resolvent and spectrum are the bijective-with-bounded-inverse notions of Teschl, p. 73, not Mathlib's Banach-algebra spectrum, which is used only for the bounded operator in Theorem 7.5. Statements that need it carry , which the book leaves implicit.
No projection-valued measure or functional calculus is taken as data. The spectral types in (7.25) are expressed through the spectral measures , and these are pinned down intrinsically by their Borel transforms .
A trivializing formalization is ruled out: is the resolvent spectrum of the operator, not the essential range of , so is not a computation on a multiplication symbol. The absolutely continuous measure in the goal must reproduce the actual resolvent matrix elements, so it cannot be chosen freely, and is not defined by its integral kernel (7.30).
A complete development needs change of normalization lemmas for the Fourier transform, the Hermite eigenfunctions of , unitary equivalence of LinearPMaps and its effect on adjoints and resolvents, self-adjointness of maximal real multiplication operators, polar coordinates on , and graph-norm approximation by cut-offs. The normalization bridge and the multiplication-operator results are reusable across the series. Contributions of either are welcome.
A quantum-mechanical Hamiltonian is usually a sum of a kinetic energy (for a free particle, in units with , ) and a potential energy . Observables must be self-adjoint operators, not merely symmetric ones: only then does the spectral theorem apply and the time evolution exist as a unitary group. Self-adjointness of is usually a direct computation. For the sum it is not, because and are unbounded, and the sum of two self-adjoint unbounded operators need not be self-adjoint or even densely defined.
The Kato–Rellich theorem settles this when is small compared with in a precise sense. The result goes back to Rellich's perturbation theory of spectral decompositions (see the notes to Section V.4 of Kato's monograph), and Kato used it in 1951 (Trans. AMS 70, 195–211) to prove that atomic Hamiltonians with Coulomb interactions are self-adjoint. It is the standard first tool in the mathematical theory of Schrödinger operators. This mission formalizes Section 6.1 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009): the notion of relative boundedness, its characterizations, the theorem itself, and the second resolvent formula.
Let be a complex Hilbert space with inner product , conjugate-linear in the first slot. A linear operator is a linear map defined on a subspace , its domain. The sum is defined on . is symmetric if is dense and for . It is self-adjoint if it equals its adjoint , domains included, and essentially self-adjoint if its closure (the operator whose graph is the closure of the graph of ) is self-adjoint. is bounded from below by if for all .
The resolvent set is the set of for which is a bijection with bounded inverse , the resolvent.
An operator is bounded if and there are constants with
The -bound of is the infimum of the admissible . If is bounded, the product is defined on all of for .
Let be self-adjoint and symmetric with -bound less than one. Then
and if is bounded from below by and (6.1) holds with constants and , then
The printed form of (6.3) has where this statement has . The printed version is false: a two-dimensional example with , , has lowest eigenvalue of about . The corrected constant is the one in Kato's monograph (Theorem V.4.11). The lower bound is stated for every admissible pair , not for the -bound itself, which is an infimum and need not be attained.
Kato–Rellich is the entry point to self-adjointness of Schrödinger operators. With the Sobolev estimates of later chapters it gives self-adjointness of on for , which covers the hydrogen atom and, through the -body extension, every atom and molecule with Coulomb interactions. The lower bound (6.3) says the perturbed Hamiltonian is still bounded from below, which is the mathematical form of stability of the ground state. The second resolvent formula is used throughout perturbation theory: to compare spectra (Weyl's theorem on essential spectra), to study resolvent convergence, and in scattering theory.
In a formal library, relative boundedness is the shared layer on which every later statement about Schrödinger operators rests. Mathlib has unbounded operators (LinearPMap), their adjoints and closures, but no relative boundedness, no resolvent of an unbounded operator, and no perturbation theorem for self-adjointness. The theorem is textbook material and has been proved many times; what does not yet exist is a machine-checked proof for unbounded operators in this generality.
Self-adjointness of is a statement about the adjoint , whose domain is defined implicitly. The inclusion follows from symmetry, but the reverse inclusion does not come from any manipulation on . It requires knowing that certain ranges are all of , and that range information is not visible from the inequality (6.1) alone. Relating the -bound, an infimum over constants in an inequality on , to norms of the bounded operators is where the self-adjointness of enters. For the essentially self-adjoint case, the domains of three different closures have to be compared. For the lower bound, the constant depends on and in two regimes, and the printed version of the formula gets one regime wrong.
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed and not needed.LinearPMaps H →ₗ.[ℂ] H; is Mathlib's sum on the intersection of the domains; closures are LinearPMap.closure; self-adjointness is Mathlib's IsSelfAdjoint; symmetric operators include density of the domain.IsRelativelyBoundedWith A B a b contains the domain inclusion and . The -bound relativeBound A B is valued in and equals exactly when is not bounded, so "-bound less than one" cannot hold vacuously.spectrum is not used. resolvent A z is off , and statements use it only at points of or eventually along rays that lie in .opNorm) are valued in ; " is bounded" means everywhere defined with finite norm.A complete development needs basic facts about resolvents of self-adjoint operators ( and the norm estimates for ), the closed graph theorem for closable operators, and Neumann series. All of these are reusable in later missions of this series: Weyl's theorem, the free Schrödinger operator, atomic Hamiltonians. Contributions that build these as general LinearPMap lemmas are welcome.
A second-order elliptic equation in divergence form, , is usually solved in a weak sense: the Lax–Milgram theorem or the Fredholm alternative produces a function , which has only first-order weak derivatives, and the equation holds after one integration by parts against every test function. The phrase "solution of a PDE" then covers objects for which the second derivatives appearing in need not exist. Regularity theory closes this gap: under smoothness of the coefficients and the data, weak solutions have exactly as many derivatives as the equation suggests. It is used throughout the calculus of variations, spectral theory and nonlinear PDE.
The interior estimate for divergence-form operators with coefficients goes back to the difference-quotient technique of L. Nirenberg (1955) and is standard in textbooks such as Evans, Partial Differential Equations, §6.3, and Gilbarg–Trudinger, Chapter 8. This mission follows the treatment in J. K. Hunter's lecture notes, §4.11 and Appendix 4.C.
Points of are written , and is the th standard unit vector. Let be an open set. A set is compactly contained in , written , if is nonempty and open, its closure is compact, and .
A test function is an infinitely differentiable with compact support inside (the space ). A function is the weak derivative of a locally integrable (multi-index ) if for all test functions . The Sobolev space consists of the functions whose weak derivatives of order at most exist and lie in , with norm ; more generally uses . The space is the closure of in .
The coefficients are functions , , which are bounded (), symmetric () and uniformly elliptic: for some ,
Given , a function is a weak solution of if
No boundary condition is imposed on .
For the th difference quotient of is , and with pointwise length .
If moreover , then for every there is a constant , depending only on , , and the coefficients, such that every weak solution of with satisfies and
The goal theorem shows that weak solutions of divergence-form equations with coefficients are strong solutions: their second weak derivatives are square integrable on compact subsets, so the equation holds pointwise almost everywhere. The iterated version (Theorem 4.28) and its corollary turn the existence theory for weak solutions into existence of smooth solutions whenever the coefficients and data are smooth; in combination with Sobolev embedding this is how one proves that eigenfunctions of the Dirichlet Laplacian on an open set are smooth in its interior.
All of these results are classical and fully proved in the literature. To the best of the platform's records, none is formalized: Mathlib has Lebesgue spaces, Fréchet derivatives and Hilbert-space tools, but neither weak derivatives nor Sobolev spaces on open sets, and there is no elliptic regularity result in any proof assistant known to the maintainers. A complete development would therefore also deliver reusable infrastructure: weak derivatives, and its norm, difference quotients and their calculus, and cut-off functions subordinate to .
The formal computation behind the estimate — testing the equation against for a cut-off and using ellipticity — is illegitimate for a weak solution, because the test function involves second derivatives of that are not yet known to exist. Replacing derivatives by difference quotients makes every step meaningful but requires a separate theory: commuting difference quotients with weak derivatives, a discrete product rule and integration by parts, and a compactness argument in (reflexivity) that turns an -uniform bound into a weak derivative. The error terms involve difference quotients of the coefficients, which is where enters, and the final estimate has to be closed with a Cauchy inequality and a second localization to replace by .
Space is = EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; coordinates are 0-based (i : Fin n), so the book's are EuclideanSpace.single 0 1, …. Functions are real-valued on all of and only their values on the relevant open set matter. Weak derivatives (HasWeakDeriv, weakDeriv), (MemW), its norm (sobolevNorm, valued in ℝ≥0∞) and (MemW0) are defined in the mission; weakDeriv is a chosen representative and is only used under hypotheses guaranteeing existence. Exponents are p : ℝ≥0∞; conjugate exponents use ENNReal.HolderConjugate. and are ContDiffOn ℝ k and ContDiffOn ℝ ∞ on (smooth, not analytic); "" for a Sobolev function means a.e. equality on with such a function.
Conventions committed to:
∃ C : ℝ is quantified after , the coefficients, the ellipticity constant and (and ), and before and .The theorems are not trivialized by junk values: the difference quotient is only used at , the weak formulation's Bochner integrals are integrable under the stated and hypotheses, and the conclusion asserts existence of all weak derivatives of order at most two, not merely a bound on a norm that could be computed from junk representatives.
Contributions welcome: a library of weak derivatives and Sobolev spaces on open subsets of compatible with these definitions, cut-off functions for (Mathlib's ContDiffBump and exists_smooth_tsupport_subset are natural starting points), and Banach–Alaoglu for , .
Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested parties. Each party reports its private data, the algorithm computes an outcome, and payments are arranged so that no party gains by misreporting. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001). Their running example is task scheduling on unrelated machines: tasks are distributed among machines owned by different agents, each agent knows only its own processing times, and the designer wants to minimize the make-span.
Without incentives the problem is classical: minimizing make-span on unrelated machines is NP-hard and admits a polynomial 2-approximation (Lenstra, Shmoys, Tardos, 1990). With selfish agents the question changes: which approximation ratios can a truthful mechanism guarantee? This mission formalizes the paper's upper bound, the MinWork mechanism, which is the benchmark every later lower bound for truthful scheduling is compared with.
Timeline.
There are agents and tasks. Agent 's type is the vector of positive times, being the time agent needs to perform task . A type vector is . An allocation sends each task to one agent; is the set of tasks agent receives. The make-span of is
and agent 's valuation is .
A direct mechanism asks every agent to declare a type, computes an allocation from the declared vector , and hands agent a payment . Agent 's utility is , with its true type. The mechanism is truthful if declaring maximizes agent 's utility for every declaration of the others, and strongly truthful if truth-telling is the only such dominant strategy. An allocation rule is a -approximation if for every type vector and every allocation .
The MinWork mechanism allocates each task to an agent with minimal declared time for it, breaking ties arbitrarily. For each task it wins, an agent receives the second-best declared time :
The Lean development uses the same names: load, makespan, IsTruthful, IsStronglyTruthful, IsApprox, IsMinWorkAlloc, secondBest, minTime, minWorkPay.
For and every MinWork allocation rule with payments as above,
The theorem gives the first positive result for truthful scheduling: a mechanism that is truthful in the strongest sense and is within a factor of optimal, whatever the tie-breaking rule. Every lower bound in the paper (Theorems 4.6, 4.10 and 4.12) and in the later literature measures itself against this ratio. Since the 2023 resolution of the Nisan–Ronen conjecture, the ratio is known to be tight for deterministic truthful mechanisms.
The result is proved in the paper; it is not known to be formalized in any proof assistant. The platform already has Groves' theorem in an abstract form (AGT.vcg_incentive_compatible). This mission connects that abstract statement to a concrete combinatorial mechanism, and it adds the strict part of strong truthfulness for any number of tasks and agents, which the paper proves only for one task and two agents. The vocabulary (make-span over unrelated machines, direct scheduling mechanisms, strong truthfulness) is shared with the seven later missions of this series.
Truthfulness follows from Groves' theorem once MinWork is identified as a VGC mechanism. The identification requires the payment identity at every declared vector and under every tie-breaking rule, including ties at the winning time. The main difficulty is the strict part of strong truthfulness. A misreport that differs from the truth only on one task must still be shown to lose strictly for some declarations of the others. Those declarations must stay positive, and on every other task they must leave the outcome unchanged. The paper's proof covers only one task and two agents and leaves the general case as "similar". Its printed inequality also has the two utilities in the wrong order (see below), so it cannot be transcribed directly.
Fin n and tasks are Fin k. An allocation is a function Fin k → Fin n, and an agent may receive no task. Types are positive reals, and every truthfulness and approximation quantifier ranges over positive true types, positive misreports and positive declarations of the others.IsMinWorkAlloc). Every result holds for every tie-breaking rule, including rules that depend on the whole declared vector. No particular argmin is fixed.Finset.sup' / Finset.inf' over nonempty finite sets, so they are true maxima and minima with no default values.AGT.vcg_incentive_compatible.Hilbert's Nullstellensatz ("theorem of zeros") is the basic link between algebra and geometry. It was proved by David Hilbert in his second major paper on invariant theory in 1893, after his 1890 paper that proved the basis theorem, and it is a foundational result of algebraic geometry. It gives an algebraic criterion for when a system of polynomial equations over an algebraically closed field has a solution, and an algebraic criterion for when one polynomial vanishes wherever a given family does. Every dictionary between affine varieties and ideals — points and maximal ideals, algebraic sets and radical ideals, irreducible sets and prime ideals — is a consequence.
This mission follows the Wikipedia article Hilbert's Nullstellensatz (snapshot of 27 September 2026): its introduction, its section Formulations, the statement of Zariski's lemma from Proofs, and the first theorem of Generalizations (finitely generated algebras over Jacobson rings).
Let be a field and an algebraically closed field extension of (every non-constant polynomial over has a root in ). Write for the polynomial ring in variables. A point is an -tuple , and is the value of a polynomial at .
If vanishes on , then
This is the statement of the article's section Formulations, with the coefficient field and the algebraically closed field allowed to differ.
The Nullstellensatz makes the zero sets of polynomial systems accessible through ideals: solvability of a system becomes the ideal-membership question , and the geometry of algebraic sets becomes the algebra of radical ideals. Consequences include the identification of the points of with the maximal ideals of , the description of irreducible algebraic sets by prime ideals, and the reduction of the fundamental theorem of algebra to the case . The Jacobson-ring version extends the first equality of the intersection formula to every finitely generated algebra over a field.
All statements here are classical and proved. Mathlib already contains versions of several of them in its own vocabulary (Jacobson rings, Zariski's lemma, and a Nullstellensatz over an algebraically closed coefficient field). What this mission adds is a single set of statements matching the article's formulations: the version with separate fields , the explicit systems-of-equations form, the point-ideal and irreducibility correspondences over , and the intersection formula — and, for solvers, the bridges from these concrete statements to Mathlib's abstract ones.
The inclusion is immediate; the content is the reverse inclusion, which requires producing a point of from purely algebraic data. When the ideal lives over while the points live over , so a result stated only for does not apply directly: an ideal of must be related to the ideal it generates in without losing membership information. For the correspondences, the explicit ideals and the closed-set definition of irreducibility must be matched with the abstract notions (maximal spectrum, irreducible closed subsets) used in the library.
MvPolynomial (Fin n) k. When , is a -algebra and evaluation of a polynomial over at a point of goes through .Polynomial.degree, with .MvPolynomial.zeroLocus, MvPolynomial.vanishingIdeal, and IsJacobsonRing.Column generation solves linear programs with far too many variables to list: one works with a small subset of the columns, the restricted master problem (RMP), and adds columns of negative reduced cost as a pricing problem finds them (Lübbecke and Desrosiers 2005, §2.1). Many integer programs from vehicle routing, crew scheduling and crew pairing are reformulated so that the master problem is a set-partitioning problem: every row (a customer, a flight leg, a task) must be covered by exactly one selected column (a route, a pairing, a schedule). The linear relaxation of such a master is solved by column generation, and an integer solution is then sought by branch-and-price, branch-and-bound with column generation at every node.
Branching in branch-and-price is not free. Fixing a master variable to does not stop the pricing problem from regenerating the same column, and handling that complicates the pricing problem. The rule that avoids this for set partitioning goes back to Ryan and Foster (1981): branch on a pair of rows, requiring them to be covered either by the same column or by two different columns. Both requirements are constraints the pricing problem can respect directly. Lübbecke and Desrosiers call it "the most common scheme in conjunction with column generation" (§7.3, p. 1020) and state the proposition that makes it well defined as their Proposition 3.
Timeline:
Rows are indexed by and columns by a finite set . A matrix has every entry equal to or ; column covers row when . The set-partitioning system of the RMP's linear relaxation is
A vector is a basic feasible solution of this system when it satisfies all its constraints and, among the constraints active at (the equality rows, and the constraints with ), there are linearly independent ones. Equivalently, is feasible and the columns of in the support of are linearly independent. A solution is fractional when it is not a vector, .
For two rows the Ryan–Foster quantity is , written pairCover A lam r s in Lean: the total weight on the columns that cover both rows. For it is the row sum, equal to on every feasible .
For every matrix and every fractional basic feasible solution of , ,
The two rows are automatically distinct. The statement concerns every fractional basic solution, not only an optimal one, and no cost vector enters it.
For every solution of and every pair of rows ,
This is the paper's requirement that "integer solutions remain intact" (p. 1019), specialised to the two branches "" and "" of the paragraph after Proposition 3.
Proposition 3 is what makes Ryan–Foster branching a valid branching scheme in the sense of §7.3: the current fractional solution violates both branches for the chosen pair, so it is excluded from both children, while by the milestone every integer solution survives in one of them. The same pair-of-rows idea underlies branching in bin packing, graph colouring, vehicle routing and crew scheduling codes, where it is used because both branches translate into constraints on the pricing problem rather than on individual master variables.
The paper states the result and refers its proof to Ryan and Foster (1981); no machine-checked version of the proposition is known. This mission produces a formal statement tied to a standard, representation-aware definition of basic solutions (Bertsimas–Tsitsiklis Definition 2.9, already on the platform) and, once proved, a verified lemma that any formal development of branch-and-price for set partitioning can cite.
An argument that uses only feasibility and a fractional coordinate cannot work. Without basicness the claim is false: with one row and two identical columns, , the vector is feasible and fractional, yet the only pair of rows is , whose quantity is . The difficulty is to turn basicness, a linear-algebra condition, into a combinatorial statement about which rows the fractional columns cover. A set-partitioning matrix need not have full row rank, so the familiar description of basic solutions through an invertible basis matrix is not available in general.
Fin m and columns Fin n, so is identified with . is a real matrix Matrix (Fin m) (Fin n) ℝ with the hypothesis IsZeroOneMatrix A (every entry or ); is lam : Fin n → ℝ, since λ is a Lean keyword. Columns are vectors; the equivalent reading as subsets of the rows is only prose.LinearOptimization.IsBasicFeasibleSolution (LinearOptimization.stdFormSystem A (fun _ => 1)) lam, from the platform definitions BasicSolution and ActiveConstraints. This definition needs no full-row-rank assumption, which a set-partitioning matrix need not satisfy, and it is not replaced by an ad hoc support condition.¬ IsZeroOneVector lam.A complete development needs linear-algebra facts about basic solutions of standard-form systems without a rank assumption (support columns linearly independent), which are reusable beyond this mission. Contributions welcome: that characterization as a lemma, and proofs of the milestone and of the goal.