Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many limit theorems of probability in Banach spaces, among them the strong law of large numbers and the law of the iterated logarithm for vector-valued random variables, reduce to sharp estimates of the tail probability
for independent random variables with values in a Banach space . For many years these estimates were obtained with martingale methods, and they were not optimal. Chapter 13 of M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces (Publ. Math. IHÉS 81, 1995), explains how the isoperimetric inequalities of the earlier chapters, in particular control by points (Theorem 3.1.1), give such estimates with explicit constants.
Timeline. M. Ledoux observed (unpublished note on Gaussian randomization, reference [L] of the paper) that for Gaussian sums one may split into its conditional mean given plus a deviation, and that the conditional mean has a monotonicity property that replaces positivity arguments ([L], Eq. (13.1)–(13.2) of the paper). Ledoux and Talagrand used this to characterize the Banach-valued random variables satisfying the law of the iterated logarithm (1988). The resulting conviction that an isoperimetric principle was at work led to Talagrand's 1989 isoperimetric theorem (Ann. Probab. 17), superseded in the 1995 paper by Theorem 3.1.1. Ledoux–Talagrand, Probability in Banach Spaces (1991), Theorem 6.17, proves a variant of the bound formalized here that also allows truncation of the variables.
Let be a real Banach space with dual , and let be independent (not necessarily identically distributed) -valued random variables. Let be Rademacher signs: independent, independent of , with . Following the paper, write
where is expectation in the signs only. The conditional mean is . The weak variance of a point is
The decreasing rearrangement is the -th largest norm, and is the sum of the largest norms.
For sets , the -point distance of is
For let and with copies of .
With and , for all integers , and ,
The goal keeps the paper's explicit constants.
The result. Theorem 13.4 bounds the tail of a Rademacher sum in an arbitrary Banach space using three quantities only: the mean , the weak variance , and the law of the largest summands. No moment assumption on the beyond these is needed, and are free parameters to optimize. By symmetrization, such bounds are the main input for the law of large numbers and the law of the iterated logarithm in Banach spaces, for the integrability of sums, and for comparison of moments.
Formalizing it. The result is proved in the paper (and in a different form in Ledoux–Talagrand 1991). It is not formalized: Mathlib has independence, product measures and the dual of a normed space, but no Rademacher sums in Banach spaces and none of Talagrand's isoperimetric inequalities. The mission yields a machine-checked statement of the vector-valued tail bound with explicit constants, connected to the -point inequality (Theorem 3.1.1, posed in mission IV of this series) and to the concentration of for bounded (Theorem 13.2, posed in mission IX).
The obvious approach controls by its mean plus a concentration term. Bounded-difference (martingale) inequalities do not work here: the increments are , which can be unbounded and heavy-tailed, so the resulting bound depends on rather than on the much smaller weak variance . Concentration for the signs conditionally on (Theorem 13.2) gives the weak variance, but at scale , a random quantity. The difficulty is to make both the conditional mean and uniformly controlled on most of the space, at the cost of discarding only a few large summands; a single-point isoperimetric inequality does not supply this.
CompleteSpace W, MeasurableSpace W and BorelSpace W; is W →L[ℝ] ℝ with the operator norm. is a real ⨆ over the dual unit ball, which is nonempty and bounded above by .Fin N → W with = Measure.pi μ for laws μ i (independent, not identically distributed). Signs are Fin N → Bool under the platform's uniform measure Komlos.spMeasure N (referenced). The joint law is the product of the two. Coordinates are 0-based; the rearrangement index is 1-based as in the paper.∫⁻) in , so they need no integrability hypothesis, and makes the goal hold with an empty event. Probabilities are in , so or makes the corresponding term .ℕ∞-valued, and no Bochner integral of a possibly non-integrable function appears.Needed infrastructure: Rademacher sums in Banach spaces, order statistics of finitely many reals, the -point inequality on general product spaces, and Theorem 13.2 for Bernoulli variables. The rearrangement and the -point distance can be reused elsewhere. Contributions are welcome on any milestone, and on proving Proposition 13.3 from a stated form of Theorem 13.2.
A random walk in a random environment on moves one step right with probability and one step left with probability from site , where the are themselves i.i.d. random variables. In his 1975 paper, F. Solomon (Ann. Probab. 3(1):1–31, DOI 10.1214/aop/1176996444) decided recurrence and transience of this walk and computed its speed. Section 4 of the paper isolates a piece of that analysis: the conditional mean time for the walk to cross one bond, given the environment.
Fix the environment, make reflecting, and let be the mean first-passage time from to . Conditioning on the first step gives with , and satisfies a linear recursion with random coefficients (p. 28). The sum is, up to an affine change, the expected time to reach level in that environment. Recursions of the same form, with i.i.d. coefficients, are the random difference equations studied by Kesten (Acta Math. 131, 1973) and Vervaat (Adv. Appl. Probab. 11, 1979); they recur in queueing (waiting-time recursions), insurance (discounted cash flows, "perpetuities") and the analysis of stochastic algorithms.
Let be a probability space and independent, identically distributed, nonnegative real random variables. The system of difference equations (4.1) is
In the Lean development Z σ n ω is defined by this recursion (module SolomonRWRE.DiffEq.System), so it is a function of and needs no existence hypothesis. Unfolding gives the closed form (4.3), .
The mean is (nu P σ); need not be integrable, and is allowed. The products are (rho), and the block sums of the proof are
the sums of the products of consecutive 's inside . For one step of the proof the sequence is extended to a two-sided i.i.d. family (module TwoSided), with .
The goal fixes nothing beyond the paper's hypotheses: any law on , integrable or not. Both cases are almost-sure limits.
If then a.s. and converges in law to ; if the series diverges, in probability; when is defined, the two cases are and .
The result. Theorem (4.4) gives the almost-sure growth rate of the cumulative mean passage time of a random walk in a random environment: linear with slope when , superlinear otherwise. This is the averaged counterpart of the speed law of §1 of the paper (Theorem (1.16)), where the limiting speed is exactly the reciprocal of . The superlinear case is the starting point of the paper's §4 limit laws for (Lemma (4.5) to Theorem (4.9)), which are stated without proof. Lemma (4.2) concerns the single variable , and its dichotomy is a statement about perpetuities .
Formalizing it. The theorem has been proved since 1975; what this mission adds is a machine-checked proof. No result about random difference equations, random products, or this paper is on the platform. The proof needs, for a nonnegative stationary ergodic sequence with possibly infinite mean, the almost-sure convergence of averages in . That convergence is not in Mathlib in this form (Mathlib has the i.i.d. strong law for integrable variables, ProbabilityTheory.strong_law_ae), and Birkhoff's pointwise ergodic theorem is posed on the platform as an open item (Birkhoff1931.tendsto_birkhoffAverage_condExp). A completed mission therefore leaves behind a nonnegative, infinite-mean ergodic theorem for block products of i.i.d. sequences, which is reusable well beyond this paper.
The obvious argument fails at independence. is a sum of products sharing the factor , so are neither independent nor stationary, and no law of large numbers applies to them directly. The regrouping into produces sums of -dependent block products, which are stationary but not independent, so the i.i.d. strong law does not apply either. Moreover there are such groups at time , so letting and grow together needs a uniform argument: Fatou's lemma gives only the lower bound. The upper bound requires a different object, , which is stationary because it looks infinitely far into the past, and it exists only because makes the backward series converge. A second trap is the infinite-mean case: may be non-integrable, and every integrability-based ergodic or strong-law statement must be adapted to nonnegative variables with values in .
σ : ℕ → Ω → ℝ; the hypotheses (IsIIDNonneg) are on (the shifted family n ↦ σ (n + 1)): measurable, pointwise nonnegative, mutually independent (iIndepFun), and identically distributed with (IdentDistrib). is unused and unconstrained.∫⁻). A Bochner integral would return for a non-integrable , which would put and make the goal false; this trivializing reading is excluded by the definition of nu.ENNReal.ofReal, which loses nothing because . In the case , is computed in and is finite.Finset.Icc 1 n); in the upper limit uses natural-number subtraction, which gives the empty sum for .IsIIDNonnegZ on σ : ℤ → Ω → ℝ; is computed from its restriction to . This mirrors the page's "without loss of generality"; the goal keeps the one-sided family.TendstoInDistribution; "" is for every ; is the difference of the -valued expectations of its positive and negative parts, required not to be both infinite, with .Contributions welcome beyond the milestones: an ergodic theorem for nonnegative stationary sequences with values in ; the identity ; and the construction of a two-sided i.i.d. extension of a one-sided sequence, which turns milestone 5 into a statement about the goal's sequence.
A renewal process models the successive replacements of an article that fails and is replaced at once: light bulbs, machine components, the inter-arrival times of a queue. The central quantity is the renewal function , the expected number of replacements up to time . Long-run average costs of maintenance and inventory policies, the throughput of regenerative systems and the rates in renewal–reward arguments are all read off the growth of . W. L. Smith's survey Renewal Theory and Its Ramifications (J. R. Statist. Soc. B, 1958) organized the field around this function and opened with its oldest general limit result, the elementary renewal theorem, proved in full in §1.2 (pp. 245–247).
Timeline.
Let be a probability space and real random variables that are mutually independent, identically distributed, non-negative, and not almost surely zero: . Lifetimes equal to zero with positive probability are allowed.
In Lean these are IsRenewalProcess P X, S X n, N X t, H X P t, mu1 X P, zeta X t and trunc Δ X in the namespace SmithRenewal.Elementary.
with and when . No moment beyond the first is assumed, and not even the first: the infinite-mean case is part of the goal.
The result. The elementary renewal theorem is the law of large numbers for the renewal function: in the long run renewals occur at mean rate . It is the basis of the renewal–reward theorem, of long-run average cost formulas for replacement, maintenance and inventory policies, and of rate computations for regenerative queues. The sharper results of Smith's survey — Blackwell's theorem (1.2) and the key renewal theorem (1.3) — refine it and reduce to it on averaging.
Formalizing it. The theorem has been proved since 1941; what this mission adds is a machine-checked development of the continuous-time, real-valued renewal process in Lean, which Mathlib does not contain. Mathlib has the strong law of large numbers, independence and identical distribution, but no renewal counting process, no Wald identity and no renewal function. The platform holds a proved discrete Erdős–Feller–Pollard theorem for integer renewal sequences, a different statement about a different object; to the curators' knowledge the elementary renewal theorem for general non-negative lifetimes has not been formalized.
The almost-sure statement is close to the strong law, since . The obvious next step, taking expectations, fails: almost-sure convergence does not imply convergence of means, and has no evident integrable dominating function. The exact relation (1.1) involves a sum with a random number of terms stopped at , and by itself it bounds from one side only, because the residual lifetime can have infinite mean. When the relation is unavailable altogether, yet the theorem still claims a limit. Throughout, is a priori allowed to be infinite on a null set and to be infinite, so finiteness itself is part of what must be established.
X : ℕ → Ω → ℝ, with the paper's as X 0, X 1, …. IsRenewalProcess P X bundles measurability, mutual independence (iIndepFun), IdentDistrib (X i) (X 0), non-negativity at every sample point, and P {X 0 = 0} < 1. Strict positivity is not assumed.ℕ∞ of ; it is for and may be on a null set.ENat.toNat; on the null event this is , which never affects an expectation.trunc Δ X, never separate formulas.Ruled out. A goal restricted to , a renewal function defined through or the renewal equation, or a real-valued ratio with in (where and an infinite integral becomes ) would each be a different, weaker or trivially true statement; none of them is the goal.
Needed infrastructure and welcome contributions. A Wald identity for stopping indices of i.i.d. sums with values in ; the comparison of a renewal count with a negative binomial count; uniform-in- moment bounds for ; and the lim inf/lim sup squeeze in . The renewal process definitions and the Wald identity are reusable for Blackwell's theorem, the key renewal theorem and renewal–reward arguments. Alternative proofs of the goal (Feller's Tauberian route, a uniform-integrability argument) are welcome as long as they prove the stated goal.
An arbitrator choosing an outcome for several people can ask them about their preferences, but the answer to that question may affect the outcome. A person who expects to gain from a false report may give one. Roger Myerson's 1979 paper puts this incentive problem inside a bargaining model: the arbitrator may randomize over collective choices, and an allocation is considered feasible only if some mechanism makes truthful reporting an equilibrium. The paper then applies a weighted Nash bargaining criterion to the resulting set of feasible interim payoffs. The mission formalizes the existence and uniqueness result for that criterion, along with the finite Bayesian model on which it depends.
The issue matters whenever an agreement is selected using information known privately to its participants. If the arbitrator evaluates a payoff vector that can arise only when somebody has a reason to lie, that vector cannot serve as a credible bargaining alternative under the model's own behavior assumption. Myerson's feasible set keeps the behavioral constraint visible when the group compares agreements. This mission addresses the paper's Theorems 1 and 3 and the claims between them that establish the relevant sets and their reference point.
Let be a nonempty finite set of players. Player has a nonempty finite type set , and the group has a nonempty finite set of possible choices. A type profile is . The utility is player 's payoff when choice occurs and is the true profile. A nonnegative function on type profiles, summing to one, is the common prior. Write for the probability that player has type , and for the posterior probability of conditional on that type. Every is positive, so the conditional probabilities are defined.
A choice mechanism asks each player for a response and assigns a probability to each choice at each response profile . For the direct mechanisms used here, the response set of player is : a response is a claimed type. The probabilities are nonnegative and sum to one for each response profile. If a player whose true type is instead reports , while the others report truthfully, the player's conditional expected utility is . The posterior weights true profiles; the mechanism sees the profile with only coordinate replaced by ; and utility is evaluated at the true profile .
The mechanism is Bayesian incentive-compatible when for every player and pair of types. Its interim payoff vector has one coordinate for every player-type pair. The set contains the vectors attained by all direct choice mechanisms; contains those attained by Bayesian incentive-compatible direct choice mechanisms. Theorem 1 says is nonempty, convex, compact, and contained in . The nonemptiness claim includes the mechanism that selects each choice with probability , independent of all reports.
Fix a conflict outcome : the choice that occurs if bargaining fails. Its conflict payoff vector gives each player type the conditional expected utility from that fixed choice. A constant mechanism selects regardless of reports. It is incentive-compatible and generates , so . The individually rational incentive-feasible set is
For , the generalized Nash product of equation (18) is
A bargaining solution is a vector in that maximizes over that set. Myerson's Theorem 3, the goal of this mission, says that if the constant conflict mechanism is not incentive-efficient—that is, an incentive-compatible mechanism strictly improves every player-type payoff over it—then exactly one such vector exists:
The milestones follow the paper's claims: the uniform mechanism is incentive-compatible; has the four properties in Theorem 1; the conflict vector belongs to ; every Nash-product maximizer strictly improves each conflict payoff when such improvement is feasible; and every implementing mechanism is incentive-efficient. The final claim concerns a mechanism that realizes the maximizing vector. It does not assert uniqueness of that mechanism.
Theorem 1 supplies a feasible set that respects truthful reporting. Theorem 3 selects a unique interim payoff vector from that set after a conflict outcome is specified. It thereby gives a well-defined allocation criterion for the paper's finite Bayesian collective choice problems. Myerson also observes that several mechanisms may implement the same solution. The allocation, rather than a unique mechanism, is the object selected by the theorem.
The result was proved in the 1979 paper. The work here is a machine-checked statement and, for solvers, a proof of that known result and its supporting claims in Lean. The mission's statements are open proof targets; the source paper's proof is not claimed to have been formalized already. A related platform item on Nash's two-player axiomatic characterization concerns a solution function on compact convex subsets of . It is a distinct result and supplies neither this paper's Bayesian model nor Theorem 3.
The set of all real-valued functions on choices and reports is much larger than the set of mechanisms: probabilities must be nonnegative and sum to one at every report profile. Bayesian incentive compatibility adds inequalities involving the true and reported type in different positions. Theorem 1 requires these constraints to give the compact, convex set of attainable interim payoffs, rather than merely a formal collection of payoff functions.
The Nash product also has a boundary: an individually rational vector may match the conflict payoff in one coordinate, making its product zero. Theorem 3's hypothesis has to rule out a zero maximum before uniqueness of an interior maximum can be concluded. The weights matter in that uniqueness statement, and the result ranges over all player-type coordinates, not only one aggregate payoff per player. Restricting the maximization to an arbitrary small subset, fixing two players, or assuming a positive maximum would change the theorem.
Lean represents players, each type set, and choices as finite nonempty types. Type profiles are dependent functions ; interim vectors are real functions on the disjoint union , with the product topology. A mechanism is a real function subject to explicit nonnegativity and sum-to-one constraints. Both and quantify only over functions satisfying those constraints. Conditional beliefs use the common prior in equations (3)–(4), and positive marginal probabilities make every denominator meaningful without requiring positive probability for each full profile. The positivity of every is an assumption the paper makes implicitly by dividing by it in (3); it is a field of the problem structure, not a hypothesis of the theorems. The subjective reading of and that the paper permits on p. 63, the response-plan equilibria of Section 3, and the numerical example of Section 6 are outside this mission.
Strict dominance means a strict gain for every player type. The constant mechanism, conflict vector, and individually rational set are defined from the problem data. The conflict vector is defined by equation (16), while its equality with the constant mechanism's payoff is a theorem item. The product uses real powers with the paper's marginal weights and is compared only on , where each base is nonnegative. A solution is a maximizer property; it is not chosen in advance or supplied as a theorem hypothesis. These choices exclude vacuous encodings of incentive efficiency, unrestricted mechanisms, and a maximization domain that already contains only a nominated winner.
A complete proof development needs finite sums and products, continuous and convex maps on finite-dimensional real spaces, compactness of the constrained mechanism set, and facts about positive weighted real powers or logarithms on the strictly positive region. The model definitions can be reused for the paper's separate revelation-principle mission; this mission also welcomes proofs of the explicit claims about the uniform mechanism, the conflict mechanism, and product maximizers.
A product made by a chain of operations can carry stock in front of every operation, between every pair of them, and as finished goods. Each such inventory point buffers demand uncertainty, and each costs money to hold. Kenneth F. Simpson, Jr. asked which of these points should carry stock at all, and how much, in In-Process Inventories, Operations Research 6 (1958) 863–873. His answer is that the cheapest configuration is an extreme one: every inventory point is either kept full or eliminated.
The paper is the origin of what is now called the guaranteed-service model of multi-echelon inventory theory.
There are operations in series. Operation has a processing time . Behind each operation is an inventory point that promises to fill any order within a service time . The incoming service time (from raw materials) and the outgoing one (to the customer) are fixed constants; the intermediate service times are the decision variables. Inventory must protect against demand over the time , and under the paper's demand model its holding cost is proportional to the square root of that time. With constants and the total inventory cost is equation (9):
Its domain is the set of points with every variable nonnegative and every radicand nonnegative:
is a polyhedron cut out by affine inequalities. A vertex of is an extreme point: a point of that is not the midpoint of two distinct points of . An inventory with has zero average stock; one with is full.
For any constants and with ,
This is the paper's sentence "the minimum of the function occurs at one of the vertices of ", read as existence of a vertex minimizer. It fixes no constant and no particular vertex.
The p. 870 rephrasing, "for an optimal system, the service time for every nonvanishing inventory is zero", is already proved on the platform as SupplyChainTheory.gs_all_or_nothing (Snyder–Shen Theorem 6.5) and is included as a reference item. Under the dictionary stage , , , that statement is Simpson's model case .
THEOREM I turns a continuous optimization over the polyhedron into a comparison over its finitely many vertices, and in Simpson's model these are the all-or-nothing configurations. Each vertex has a physical reading as a mode of operation: which inventories are kept full and which operations are tightly coupled (THEOREM II). The property is what makes guaranteed-service models tractable by enumeration or dynamic programming in later work.
The result is proved in the paper, by an induction on faces. It has not been machine-checked. A formal development adds a checked statement of the theorem for general constants (the paper's model fixes ), an exact account of which hypotheses are needed (the positivity of the is essential, see below), and a checked vertex count for the model case. The existing platform theorem gs_all_or_nothing covers the model case in the all-or-nothing form; THEOREM I with general constants and the vertex characterization are not yet on the platform.
The domain is given by inequalities, while the conclusion is about its extreme points, which are never listed: with general constants the vertices of have no closed form, and may be lower-dimensional or have coinciding facets. Any argument therefore has to connect an inequality description of a polyhedron with its extreme-point structure, which in the paper's own text is treated informally ("faces", "edges", "an -fold repetition"). LEMMA I and LEMMA II are stronger than the existence statement: they exclude minimizers in the interior of and in the relative interior of a face, and they become false as soon as some vanishes, so they cannot follow from concavity alone. THEOREM II, though described on the page as "examine the definitions", requires an exact reindexing of the operations, processing times and cost coefficients after one variable is removed.
The sign hypothesis cannot be dropped: with , , , , , , the function on is convex and its only minimizer is the interior point .
All declarations live in SimpsonInv.Vertex. With variables a point of is S : Fin m → ℝ, and Lean index holds the paper's ; extVec S0 Sn S i returns the paper's for every , including the constant ends. The constants are sequences ℕ → ℝ, read only at indices . The space Fin m → ℝ carries the product topology, which is the Euclidean one, so interior is the paper's interior. A vertex is an element of Set.extremePoints ℝ D; a minimizer is IsMinOn f D v with .
Added hypotheses, each disclosed in its item: for (from equation (8); weakened to for concavity and dropped for existence and THEOREM II); where a minimum is asserted; at least one variable for LEMMA I and at least two for LEMMA II; and only for the vertex count, as in the paper's model. The page's "-dimensional polyhedron" is not imposed: the goal is stated for every nonempty . "On the boundary of the faces" (LEMMA II) is encoded by at least two independent active inequality normals, including when inequalities coincide.
Real.sqrt returns on negative inputs, so is never compared outside . Minimizing over all of , or replacing the vertex set by a hand-listed finite set of points, would trivialize or falsify the goal and is ruled out: the goal quantifies over Set.extremePoints ℝ D and compares only on . THEOREM II compares the original cost with the same cost function applied to new data ( operations, , ), not with a substituted copy of the original.
A complete development needs compactness and extreme-point facts for polyhedra given by inequalities and concavity facts for square roots and powers of affine maps; both are reusable well beyond this mission. Proofs of any milestone, and reusable lemmas on polyhedra given by inequalities, are welcome.
An online learner predicts a binary label for each instance before seeing that instance's correct label. Its guarantee is usually measured by its worst possible number of mistakes against a target function. Such guarantees can differ greatly across target functions: an algorithm might learn one target quickly while taking much longer on another. Littlestone and Warmuth's analysis of the Weighted Majority Algorithm asks which collections of individual mistake guarantees can coexist for one deterministic learner. In Section 7 of their 1994 paper, they isolate a condition under which these guarantees obey a strict numerical constraint. The condition concerns how the target functions vary together over the instance domain, so the result applies without a probability distribution on instances or labels.
The theorem also supports the paper's comparison between arbitrary deterministic learners and Weighted Majority. Given individual mistake bounds, its inequality is the numerical condition that makes a suitable initial weighting of the target functions possible in Theorem 7.1 and Corollary 7.1 of the same paper. The present mission centers on the inequality itself, which is independent of a particular implementation of Weighted Majority.
Let be an instance domain, possibly finite or infinite, and let be a finite family of target functions. A trial presents an instance to a learner, asks it to predict either or , and then reveals a label. A finite sequence is consistent with when each revealed label equals at that trial's instance. The learner may use the current instance and the complete history of earlier labeled trials when predicting; it does not see the current label first. No sampling or independence assumption is made.
The family is shattered by its domain when every pattern appears as the vector of function values at some instance:
This is a dual notion of shattering. The familiar VC condition asks whether a class of functions realizes every labeling of chosen instances. Here the domain realizes every joint value pattern of a chosen family of functions. The two conditions should not be interchanged.
Let be any deterministic online learner. Write for the supremum of the number of mistakes made by over every finite sequence consistent with . Since mistake counts are natural numbers, a finite supremum is an attained natural-number maximum. The theorem assumes each is finite. In the Lean representation, this is a separate finiteness condition on each target's extended-natural mistake bound.
The goal is Theorem 7.2 of Littlestone and Warmuth, pp. 244–245. For every domain, every finite family shattered by that domain, and every deterministic online learner with finite individual mistake bounds,
The inequality is strict. Replacing it by a weak inequality would lose the stated result and the threshold used in the paper's later comparison with Weighted Majority. The theorem quantifies over the learner itself; it does not select a specially behaved learning rule.
Lemma 7.1 concerns positive real numbers with integral adjacent quotients. When a positive target is no larger than their sum and is integral, some prefix sums exactly to . Lemma 7.2 concerns positive powers of two with integer exponents. If a power lies at least as high as each individual weight and at most as high as the total weight, some subset sums exactly to . Both statements and their exact source wording are recorded as the mission's milestones; they are the numbered arithmetic results used in Theorem 7.2.
The theorem limits the set of claims that one deterministic learner can make simultaneously. Small contribute large terms to the sum, so a learner cannot have arbitrarily small worst-case mistake counts for all members of a domain-shattered family. This is a worst-case statement about every finite consistent trial sequence, rather than an average-case statement about a chosen data distribution. The paper's Corollary 7.1 uses the resulting inequality to select initial weights for a Weighted Majority comparison, but that later algorithmic statement is outside this mission's goal.
Formalizing this result adds a reusable dual-shattering predicate and an exact constraint on per-target online mistake bounds to the existing online-learning definitions. The paper proves the theorem, while the mission's Lean goal and its two milestone lemmas are open proof obligations. The separate published online-learning module provides the definitions of deterministic predictors, trial histories, mistake counts, and extended-natural worst-case bounds; it does not already prove this theorem.
For a single target, an arbitrary learner may have a small finite mistake bound. The difficulty is relating those bounds across different targets without placing extra restrictions on the learner. Domain shattering gives the adversary control over the simultaneous predictions of all functions at an instance, but the labels of one trial sequence must still remain consistent with a target. A simple count of targets or of possible patterns does not directly produce the strict weighted sum, particularly when the different are unequal. The two arithmetic lemmas address exact sums of structured weights; the main theorem must also connect such weights to the learner's worst-case mistakes.
The function family is indexed by Fin n, with zero-based Lean indices corresponding to the paper's . The domain is an arbitrary type and may be infinite. Labels and predictions are Bool. ShatteredByDomain states that every Boolean pattern is realized by some domain point. The published UnderstandingML_Online definition gives OnlineAlg X Bool, finite trial histories, mistakes, and mistakeBound. The latter is valued in and ranges over all finite sequences labeled by the target. Each is converted to a natural number only after assuming its bound is finite. The powers and their finite sum are real numbers. The conclusion is the empty sum ; the shattering predicate itself then requires an instance to realize the unique empty pattern.
The two milestones use real-valued weights. Lemma 7.1 assumes because the source refers to . Lemma 7.2 represents the source's integral base-two logarithms by equations with integer , which also enforce positivity. Its maximum hypothesis is written pointwise, so an empty family is harmless: the other inequality cannot hold. A coordinate family on is verified locally to satisfy the shattering predicate, ruling out a vacuous encoding of that central assumption. Contributions proving either arithmetic milestone or the main theorem within these exact definitions are in scope.
A Nash equilibrium is a joint choice of strategies at which no player can improve their own expected payoff by changing their strategy alone. This gives a testable notion of stable behavior for a finite game, including games in which the players' aims differ. Nash's two-page 1950 note established the existence of such a point for finite games by organizing each player's best replies into a single correspondence and using a fixed-point theorem. The note identifies several properties of that correspondence and ends by comparing equilibrium payoffs in zero-sum and general games. Those claims, stated together in Nash's published note, are the subject of this mission.
The existence conclusion itself already has a proved formal statement, AGT.nash_existence, in the game vocabulary used here. The remaining claims explain what the fixed-point argument acts on: which profiles are related by countering, why countering sets are usable as values of a correspondence, and what their fixed points mean. Keeping those statements explicit makes the 1950 argument legible independently of the existence theorem's proof.
There is a finite set of players. Each player has a finite, nonempty set of pure strategies. A pure-strategy profile chooses one element of every , and is player 's payoff. A mixed strategy assigns a nonnegative real weight to each element of , with weights summing to one. The space of mixed profiles is the product of these finite probability simplices.
Players randomize independently. Thus the probability of a pure profile under is , and player 's expected payoff is
For a strategy of player , write for the payoff obtained by replacing only coordinate of . A profile counters if and, for every player , its coordinate gives that player the highest expected payoff available against the other players' coordinates of :
The countering correspondence assigns the set to each . Its graph comprises the pairs with and . A fixed point is a profile belonging to ; Nash calls it an equilibrium point.
The goal states the three properties of that Nash uses, along with the identification of its fixed points:
The milestone list follows the claims in the note: the payoff functions are polylinear and continuous; the correspondence maps mixed profiles to nonempty subsets of mixed profiles; its values are convex; its graph is closed in the sequential formulation Nash writes; and self-countering is equilibrium. A separate closed-set formulation records the graph property in the product topology.
The note also asserts a distinction about payoffs. In a two-person zero-sum game, where on every pure profile, any two equilibria have the same expected payoff for each player:
For general games, this can fail. A companion target asks for a finite two-person game with two equilibria having different expected payoffs.
The correspondence theorem records the precise conditions on which Nash's application of Kakutani's fixed-point theorem rests. Nonempty convex values and a closed graph make the fixed-point route applicable to the mixed-strategy space; the fixed-point clause says why its output is an equilibrium of the game rather than only a topological point. The zero-sum companion separates the common value of a two-person zero-sum game from the possible range of equilibrium payoffs in a general game. These consequences and the comparison appear in Nash's note.
The equilibrium existence theorem is already proved as the referenced AGT.nash_existence. What remains here is to formalize the correspondence properties and the payoff comparison as their own auditable statements, using that theorem's published game definitions. The claims are known results from 1950; their appearance as goals means proofs of these particular statements are still to be supplied in this development.
The payoff of a player depends on every player's strategy, while countering compares only one changed coordinate at a time. The relevant set of maximizers is therefore indexed by the countered profile, and all players' choices must fit into one countering profile. Establishing closedness requires passing the payoff comparisons and the probability-vector conditions through limits of profiles. The zero-sum equality concerns arbitrary pairs of equilibria, which need not use the same strategies; an argument based only on the existence of an equilibrium cannot give it. For general games, a single equilibrium says nothing about whether another equilibrium has a different payoff.
The Lean development uses a finite player type ι, finite pure-strategy types S i, real payoffs u, and the published definitions AGT.IsLottery, AGT.IsMixedProfile, AGT.expectedPayoff, and AGT.IsMixedNash. The goal and nonempty-value milestone require each S i to be nonempty. The note's probability distributions implicitly require this; the player type itself may be empty. A mixed profile is a tuple of finite real weight vectors, with no measure-theoretic integration or hidden normalization. In the two-person claim, players are 0, 1 : Fin 2.
Convergence is in the ordinary product topology of the real coordinate spaces. The sequence index is because the note also uses for the number of players. Counters u P Q requires to be a mixed profile and compares with every mixed deviation against ; this rules out arbitrary weight vectors and comparisons against the wrong opponents. Neither continuity nor the existence of a best response is assumed in the goal: those properties are targets. The definition layer and the payoff continuity and polylinearity results can be reused by other finite-game formalizations.
Monotone sequences of random elements arise wherever a quantity can only grow: cumulative work or queue contents under a monotone recursion, the iterates of a monotone operator applied to a random initial state, or the successive approximations produced by coupling constructions in which each stage dominates the previous one. When the values live in a partially ordered space rather than on the real line (vectors with the coordinatewise order, functions with the pointwise order, measures with a stochastic order), the classical fact that a bounded nondecreasing real sequence converges no longer applies directly, and one needs a statement about which modes of convergence are automatic.
Kamae, Krengel and O'Brien answer this in Section 6 of Stochastic Inequalities on Partially Ordered Spaces (Ann. Probab. 5 (1977) 899–912). Their Theorem 6 shows that, for a nondecreasing sequence in a partially ordered Polish space, three modes of convergence that are in general strictly ordered by strength (tightness of the laws, weak convergence of the laws, convergence in probability) coincide, and it identifies exactly when almost sure convergence joins them. The paper announces an application of Theorem 6 to a new pointwise ergodic theorem in a forthcoming paper of Krengel. This mission formalizes Theorem 6 and its proof steps; the source is the published Annals of Probability version, and printed page numbers equal PDF page numbers plus 898.
Let be a Polish space with metric : a complete separable metric space. It carries a closed partial ordering , meaning a partial order whose graph is a closed subset of , and its Borel -algebra. These are the paper's standing assumptions (Sec. 1, p. 899).
Let be a probability space and measurable maps (random variables) that are nondecreasing: for every . Write for the distribution of . The four modes of convergence are:
The space satisfies condition (17) if for all sequences with for every , implies . In Lean this is Regular17 E, and the modes are LawsTight, LawsConvergeWeakly, ConvergesInProbability and ConvergesAS.
For every probability space and every nondecreasing sequence of random variables in ,
and
The result. Without monotonicity, tightness gives only weakly convergent subsequences (Prokhorov), and weak convergence of laws says nothing about the random variables themselves. Theorem 6 says that order removes both gaps: tightness of the marginal laws of a monotone sequence already produces a limiting random variable, in probability. Its second part gives an intrinsic, checkable criterion on the ordered space, condition (17), for upgrading this to almost sure convergence, and the Remarks show the criterion is not automatic. Coordinatewise-ordered satisfies (17), so there all four modes coincide for monotone sequences.
Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Mathlib has tightness, Prokhorov's theorem in one direction, weak convergence of probability measures and convergence in measure, but no results relating these modes for order-monotone sequences. The mission produces a formal proof of all four implications and of the characterisation by (17), together with a formally verified example of an ordered Polish space violating (17).
The obvious argument for (i) ⇒ (iii) imitates the real line: on each the sequence is monotone and lies in a compact set "most of the time", so it should converge. Two things fail. First, the sequence need not stay in one compact set: tightness controls each separately, and a fixed may leave infinitely often; only the subsequence of visits to is relatively compact. Second, there is no supremum available in a general partial order, so the real-line argument for the existence of a limit has no analogue, and without the closedness of the order the statement is false. Turning the pointwise statement into convergence in probability then requires a uniformity argument across . For the second part, the natural attempt to pass from a subsequence converging almost surely to the whole sequence fails without (17), which is the content of the counterexample.
The space carries [MetricSpace E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [PartialOrder E] [OrderClosedTopology E]. Second countability is equivalent to separability for metric spaces, and OrderClosedTopology is exactly a closed partial ordering. The closed order cannot be dropped: (i) ⇒ (iii) fails without it. Conventions committed to:
ProbabilityMeasure, stated through integrals of bounded continuous functions (equivalent to Mathlib's topology on probability measures for measurable ).TendstoInMeasure to a measurable limit; the a.s. limit in (iv) need not be measurable.Type; "(iv) is also equivalent" is encoded as (iv) ⇔ (iii). The quantifier over all probability spaces and all nondecreasing sequences is essential: for one fixed sequence the "only if" direction is false, and fixing would make the statement about one space rather than about .A trivializing formalization is ruled out: no hypothesis forces the sequence to be constant, the modes are not defined in terms of each other, and the second part quantifies over every probability space and sequence.
Reusable infrastructure: the four modes of convergence for random elements of a metric space, and the identification of limits through closed orders. Contributions welcome: proofs of the standard implications (iv) ⇒ (iii) ⇒ (ii) ⇒ (i) in Polish spaces, the milestone proofs, and a proof that coordinatewise satisfies (17).
In a finite game, a referee can recommend one action privately to each player according to a joint distribution. The recommendations may be correlated: learning one's own recommendation can convey information about the others'. A correlated equilibrium is a distribution for which no player gains, in expectation, by replacing a particular recommendation with another action. This solution concept uses the same payoff data as a strategic-form game but allows more joint distributions than independent mixed strategies. Hart and Schmeidler's Theorem 1 establishes that at least one such distribution exists for every finite game, with no assumptions on the payoffs beyond being real-valued. Their paper uses the finite result as the starting point for existence results with infinitely many players and, later, compact strategy spaces. Hart and Schmeidler (1989)
The authors explain that the standard route passes through a mixed Nash equilibrium: independent equilibrium strategies induce a correlated distribution. The finite theorem here is the same existence conclusion expressed directly through recommendation inequalities, which are linear in the joint distribution. That distinction matters for the later sections of the paper, where the authors examine games with infinitely many players, including an example with a countably additive correlated equilibrium but no Nash equilibrium. Hart and Schmeidler (1989), pp. 18, 21–22
Let be a finite player set. Each player has a finite, nonempty set of pure strategies, and a pure profile is a tuple in . The real number is player 's payoff at . For a player , write for all coordinates except and for the profile obtained by replacing the th coordinate with . A probability vector on is a function with for every and . These are exactly the paper's finite-game and probability-vector conventions. Hart and Schmeidler (1989), pp. 18–19
Suppose the referee draws with probability and privately tells player only . For every recommended action and alternative action , the incentive inequality is
When the recommendation has zero probability, this inequality holds automatically. Thus no conditional probability needs to be defined in that case. A probability vector satisfying every such inequality is a correlated equilibrium. The inequalities include , whose left-hand side is zero. Hart and Schmeidler (1989), p. 19, condition (1)
The mission's goal is the paper's Theorem 1, with its definition of correlated equilibrium kept explicit:
Here denotes the set of probability vectors on the finite set . The quantified payoffs are arbitrary real functions; the result specifies neither a unique equilibrium nor a particular equilibrium distribution. The milestone list records the paper's auxiliary-game correspondence, its finite minimax criterion, the nonnegative-matrix lemma, equation (2), and the final product-strategy identity. The lemma is linked to the already proved platform theorem CalibratedCE.Forecast.flow_conservation_solvable, which states the equivalent balance equations for a nonnegative matrix indexed by a nonempty finite set. Hart and Schmeidler (1989), pp. 19–20
The result guarantees feasibility of the complete system of recommendation inequalities for every finite payoff table. It is stronger as a foundation than checking an equilibrium in one game: later arguments can invoke the result after restricting a larger game to finite strategy sets. Hart and Schmeidler do exactly that in their infinite-game existence theorems. The finite theorem is already known mathematically; the task here is to give its particular statement and proof structure reusable, machine-checked declarations. Hart and Schmeidler (1989), pp. 20, 22, 24
The platform already has the general finite-game lottery vocabulary in agt_games and a proved mixed Nash-existence theorem, AGT.nash_existence. It also has AGT.IsCorrelatedEquilibrium in swap-function cost notation, AGT.swap_regret_correlated_equilibrium for approximate equilibria, and Aumann 1987's finite-probability-space model. Those results provide related notions and consequences. With and costs , the swap-function form of AGT.IsCorrelatedEquilibrium is equivalent to condition (1), since a switching rule can be optimized separately for each recommendation; the mission nevertheless states condition (1) as printed. The finite Minimax Theorem invoked on p. 19 is proved on the platform as AGT.zero_sum_minimax (a saddle-point statement for matrices indexed by Fin (m+1) and Fin (n+1), in another Mathlib environment), so the minimax milestone is the consequence the paper draws from it rather than the theorem itself. This mission fixes Hart and Schmeidler's payoff-maximizing condition (1) directly, with its recommendation-specific inequalities and auxiliary-game steps. The linked flow-conservation theorem was formalized in the Foster–Vohra series; its balance equations have the same content as the lemma on p. 19 after expanding the coefficients of an arbitrary vector . Hart and Schmeidler (1989), p. 19
The inequalities must hold simultaneously for every player and every recommended-action/deviation pair. Choosing a distribution that makes one inequality hold does not ensure the others: the same weights occur in several constraints. An arbitrary product distribution can fail even in a two-player coordination game. Passing through an existing mixed Nash equilibrium proves existence, but gives no formal account of the paper's own finite minimax and nonnegative-matrix claims. The proof obligations here include the exact correspondence between the conditional recommendation constraints and an auxiliary two-person game, plus the algebra of a product of playerwise probability vectors. Hart and Schmeidler (1989), pp. 18–20
Players are a finite Lean type ; is a finite, nonempty type, and . The profile space is the dependent product . The expression is Function.update s i t, and summing over with the th coordinate fixed to is represented by summing over profiles satisfying . Probability vectors use the published AGT.IsLottery: nonnegative real weights whose finite sum is one. No measure-theoretic integral or conditional probability appears in this finite mission. The auxiliary minimizing player's pure strategies form one set of triples , with one probability vector over all triples. Hart and Schmeidler (1989), p. 19
Nonemptiness of each is required: an empty strategy set would leave no probability vector on . The player set itself may be empty; then has one profile and the incentive conditions have no instances. The generic minimax milestone separately assumes that both of its pure-strategy sets are nonempty, so solvers must handle the playerless goal directly. Equality decisions are computational instances for finite enumeration, not restrictions on mathematical games. The correlated-equilibrium definition includes normalization and all incentive inequalities; it is not defined to hold automatically. The goal is the existence of a probability vector satisfying condition (1) itself, not a restatement through AGT.nash_existence that would make it a corollary of Nash's theorem. A sorry-free local check exhibits a correlated point mass in a two-player coordination game and another point mass that violates an incentive inequality. Contributions to the finite minimax criterion, its connection to the published balance theorem, and the sum rearrangement in the product-strategy milestone are all useful beyond this one goal.
A birth-and-death process describes a population in which each individual independently gives birth and dies at given rates. Kendall's 1948 paper (doi:10.1214/aoms/1177730285) solved the process with arbitrary time-dependent rates and, in its §4, introduced a second random variable alongside the population size: the cumulative population , the number of individuals that have ever been alive up to time . Kendall gives two readings. If is the number of current cases of a disease, is the total number of cases recorded so far, and for an epidemic that is almost certain to die out, measures its overall severity. If is the viable count of a bacterial population, is the total count, in which living and dead organisms are not distinguished.
The question of this mission is the exact distribution of for the simplest transient process, with constant rates. Kendall answers it in §5 by solving a first-order partial differential equation for the joint generating function of . The resulting law involves central binomial coefficients, the same numbers that count the total progeny of a critical binary branching process.
Let and be constants. In the simple birth-and-death process with these rates, a population of size moves to at rate and to at rate . It starts from one ancestor, . The cumulative population starts at and shares all the positive jumps of , so it never decreases. The process is transient (dies out with probability one) when .
Write for the joint law of and
for its generating function (30). Kendall shows that satisfies
and solves it with the roots of the quadratic (49), :
Setting forgets , so generates the law of . Finally
The Lean names are disc, alpha, beta, psi, x, Q and SolvesPDE, in the namespace KendallBD.Cumul.
For :
The result. The law (52) gives the full distribution of the total size of a transient linear birth-and-death population, not only its moments: the probability that the ancestor dies childless, the tail behaviour, and the dichotomy between the subcritical case (finite mean , geometric-type tail with ratio ) and the critical case (heavy tail, infinite mean). In the epidemic reading this is the distribution of the final size of a minor outbreak; it is also the total-progeny law of the embedded binary Galton–Watson tree (Harris 1963).
Formalizing it. The result is classical and proved, but it is not formalized anywhere known to this mission. A formal proof would combine three separate pieces: the explicit solution of a first-order PDE by characteristics, checked as a classical solution on the region where a probability generating function lives; a limit that selects one root of a quadratic; and the binomial series of together with its boundary value at . The companions make the moments (48), which §4 derives by a separate route, a consequence of the law.
Checking that (50) satisfies (31) is calculus once the derivatives exist. The obstacles are elsewhere. First, the roots must be ordered as , which fails at when (the roots are then and ): every statement about , , has to be made for , and the law is identified from the power series on that interval. Second, the normalization is a statement at the boundary of the series for ; at this is , the edge of the disc of convergence, where convergence of the series is not automatic and where the value uses . For the same series sums to , so the hypothesis is essential. Third, the asymptotic in the balanced case needs the asymptotics of central binomial coefficients.
All objects are real functions; the process and the joint law are not constructed, exactly as in the paper. "The law of " is read, as on p. 11, as the coefficients of the generating function , and is tied to the process through the equation (31) and the boundary condition (32). The committed conventions are:
Real.sqrt the nonnegative root;SolvesPDE: both partial derivatives exist as HasDerivAt facts and satisfy the equation, never an equation between deriv values;A goal that only asserted the power series identity would be a different and easier theorem with no birth-and-death content; the goal therefore ties to of (50) and to the equation (31)–(32).
A complete development needs the binomial series for with real coefficients (Mathlib has Nat.centralBinom and general binomial series, and the platform has the generating function of the central binomial coefficients as a proof tool), the boundary behaviour of a power series with nonnegative coefficients, and Stirling-type asymptotics of . These are reusable well beyond this mission. Contributions proving any milestone or companion, or the series lemma on its own, are welcome.
Every pure integer program can be relaxed, by dropping the nonnegativity of the basic variables of an optimal linear-programming basis, to a problem over a finite Abelian group: find nonnegative integers , one for each nonzero group element, with . R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969) 451–558) studies the convex hulls of the solutions of these group equations, the corner polyhedra, and the master polyhedron that contains all of them as faces. These polyhedra are the source of the group-theoretic approach to cutting planes: their faces are valid inequalities for every integer program with the same group, and their vertices are the candidate optimal solutions of the group relaxation.
The paper's first section shows that every vertex of such a polyhedron is an irreducible solution, and remarks (p. 460) that the converse fails in general: a typical group has many irreducible solutions that are not vertices. Section 3F identifies a family of groups where the two notions coincide, which is what makes the vertices of these polyhedra countable in closed form.
Let be a finite Abelian group written additively, with zero , and . For the group equation is
The master polyhedron is the convex hull in of its nonnegative integer solutions (for the solution is excluded). A vertex is an extreme point of .
A nonnegative integer vector is irreducible if any two integer vectors with and are equal. A finite set of group elements is independent if with integers forces for each .
The groups of §3F are those in which every nonzero element has order 2, the groups , or every nonzero element has order 3, the groups .
If every nonzero element of has order , with or , and , then for every nonnegative integer solution of the group equation
and the support of such a vertex is an independent set.
THEOREM 23 turns a polyhedral question into a combinatorial one for the elementary Abelian 2- and 3-groups: the vertices of are read off from independent subsets of the group and residues below . Gomory uses this on pp. 506–507 to count all vertices of all exactly and to derive their asymptotic number. It also marks the boundary of the general picture: groups with elements of other orders have irreducible solutions that are not vertices.
The result has been proved since 1969; no machine-checked proof exists. The mission produces a Lean statement and, once solved, a verified proof of the theorem together with the general fact that vertices of the master polyhedron are irreducible, a reusable layer for the other group-polyhedron results of the same paper. Two sentences of the printed proof (p. 506) are false as written (see Formalization scope); formalization records their corrected forms.
The direction "vertex irreducible" holds in every group and is a midpoint argument. The difficulty is the converse: showing that an irreducible solution cannot be written as a proper convex combination of other solutions, which are infinitely many and unbounded. The natural route, exhibiting a linear objective that uniquely minimizes, does not work with the objective printed on the page: solutions with the same support as but larger entries are tied with it. The argument must control those solutions through the arithmetic of residues modulo , and this is where the exponent 2 or 3 is used; the analogous residue statement fails for .
{g : G // g ≠ 0}; integer solutions are -valued and cast to ; vertices are Set.extremePoints ℝ of the convex hull of the cast solutions.convexHull, extremePoints_convexHull_subset), and finite sums in Abelian groups. Contributions welcome: any of the milestones, and a general lemma that a unique minimizer of a nonnegative linear function over the integer solutions is a vertex.A loss network is a model of a circuit-switched network: telephone networks, and more generally any system in which a request seizes several resources at once and is lost if any of them is unavailable. Exact loss probabilities in such networks are given by a product-form distribution over a state space whose size grows exponentially with the number of routes, so practitioners compute an approximation instead: the Erlang fixed point, also called the reduced-load approximation. It pretends that links block independently, computes the traffic offered to each link after thinning by the other links, and applies Erlang's single-link formula link by link. Reduced-load approximations of this kind recur throughout §§3–4 of Kelly 1991, where they appear as limits of networks with fixed and with alternative routing.
An approximation defined by a fixed point equation raises an immediate question: does the equation have exactly one solution? Under fixed routing it does, and Kelly's Theorem 3.7 (Ann. Appl. Probab. 1991, p. 338, citing Kelly 1986, reference [33] of the paper) proves it by identifying the fixed point with the optimum of a strictly convex program, the revised dual problem. The convex characterization is specific to fixed routing; the paper notes (p. 337) that for networks with dynamic routing and control nonuniquely determined behaviour can occur.
There are links, link having circuits, and a finite set of routes . A call on route uses circuits of link , and calls on route arrive as a Poisson stream of rate .
Erlang's formula (1.1) gives the blocking probability of a single link with circuits offered Poisson traffic of intensity :
The Erlang fixed point equations (3.1)–(3.2) for the vector of link blocking probabilities are
The utilization function is defined by the implicit relation (3.4),
the mean number of busy circuits on a single link whose blocking probability is .
The revised dual problem (3.5) is
and its stationarity conditions (3.6) are
The revised dual differs from the dual problem (2.3) of §2, whose optimum gives the limiting blocking probabilities of a large network, only in its last term: becomes .
The revised dual problem (3.5) has an optimum , every optimum equals , and
The goal states the characterization, not only the existence and uniqueness of the fixed point: the solution is for the optimum of (3.5).
The theorem turns a nonlinear system of equations into a smooth strictly convex minimization over the nonnegative orthant. Uniqueness of the fixed point follows at once, and the program gives a computational handle: any convex-minimization method computes the Erlang fixed point, without relying on the convergence of repeated substitution. The comparison with the dual problem (2.3) also explains the approximation: (3.6) relaxes the conditions (2.7), which force a link's carried traffic to equal its capacity before it can block, into a smooth relation in which blocking grows with carried traffic as Erlang's formula prescribes (Remark 3.8).
On Prove2Me, existence and uniqueness of the fixed point alone is already the Proved theorem KellyStochasticNetworks.erlang_fixed_point_unique (Kelly–Yudovina, Stochastic Networks, Theorem 3.20), referenced by this mission. Also referenced: KellyStochasticNetworks.erlang_strictMono (Proved: and are strictly increasing for ) and KellyStochasticNetworks.erlang_mean_busy_circuits (Proved: the mean number of busy circuits is , the reading of as a utilization). What this mission adds is the revised dual problem itself, the utilization function , and the identification of the fixed point with the optimum of (3.5); none of these is formalized on the platform.
The function is defined only implicitly, through the inverse of , so every property of the objective of (3.5) passes through properties of Erlang's formula: monotonicity, continuity, and the limit as . Differentiating needs continuity of , which must be derived from the inverse.
The paper's sentence "strictly convex: it thus has a unique minimum" covers only uniqueness. Existence of a minimizer on the unbounded set is a separate fact, a growth estimate for the integral terms, and it is part of milestone 4. The first term of (3.5) is not strictly convex when has rank less than , so strict convexity must come from the separable integral terms. Finally, optimality over yields only one-sided conditions at coordinates with ; that (3.6) is an equality there uses .
Lean namespace KellyLossNetworks.RevisedDual. Links are Fin J, routes Fin R, the incidence matrix is A : Fin J → Fin R → ℕ, rates ν : Fin R → ℝ, capacities C : Fin J → ℕ, following the published Kelly–Yudovina definitions. Every statement assumes and ; the paper uses both without stating them, and a link with makes (3.4) meaningless, since .
Erlang's formula is the published KellyStochasticNetworks.erlang and the fixed point equations (3.1)–(3.2) are the published KellyStochasticNetworks.ErlangFixedPoint, whose factor is Lean's total inverse; milestone 6 shows that no solution in reaches . Solutions are sought in , as on p. 338.
is defined by choice: for a with , and if none exists. For , the is unique, and that (3.4) holds is milestone 1, a theorem, not an axiom built into the definition. Values at or are placeholders that no statement uses. The integral in (3.5) is the interval integral . An optimum of (3.5) is a whose objective value is at most that of every .
A trivializing formalization is ruled out: replacing by any closed form other than the one fixed by (3.4) (for instance , the fluid utilization of Remark 3.8) would change the problem and reduce (3.5) to the dual (2.3); and the goal asserts the identification rather than restating the existence and uniqueness that is already Proved.
A complete development needs: inverse-function arguments for a strictly increasing continuous map of , derivatives of interval integrals with continuous integrands, strict convexity of separable sums, and first-order optimality conditions for convex functions on the nonnegative orthant. The facts about Erlang's formula and about are reusable in any reduced-load analysis. Proofs of individual milestones are welcome independently.
Nonlinear conjugate gradient methods minimize a smooth function of variables using only function values, gradients and a few vectors of storage. They are the method of choice when is so large that quasi-Newton matrices cannot be stored, and they remain a standard component of large-scale optimization software. Their convergence theory is delicate: the classical results assume exact line searches, while practical codes accept any steplength satisfying inexpensive inexact conditions.
Gilbert and Nocedal (INRIA RR-1268, 1990; journal version SIAM J. Optim. 2 (1992)) organized the global convergence theory of these methods around a single device and proved two families of results. This mission covers the first: every conjugate gradient method whose parameter is bounded in absolute value by the Fletcher–Reeves value converges under the strong Wolfe line search.
Timeline. Fletcher and Reeves (1964) and Polak and Ribière (1969) introduced the two best-known choices of . Zoutendijk (1970) and Wolfe (1969, 1971) established the summability condition now called Zoutendijk's condition. Al-Baali (1985) proved that the Fletcher–Reeves method with the strong Wolfe line search and generates descent directions and satisfies . Touati-Ahmed and Storey (1990) treated nonnegative hybrids. Gilbert and Nocedal (1990) extended Al-Baali's theorem to every with , which admits negative values and yields a convergent modification of the Polak–Ribière method.
Let be a finite-dimensional real inner product space and continuously differentiable, with gradient for that inner product. Starting from , the method generates
where , is a scalar and a steplength found by a one-dimensional search. The Fletcher–Reeves and Polak–Ribière scalars are
Assumptions 2.1: the level set is bounded, and on an open neighbourhood of the gradient is Lipschitz: .
A steplength satisfies the Wolfe conditions with if
and the strong Wolfe conditions if the second inequality is replaced by . The angle between and is given by , and the Zoutendijk condition is .
Under Assumptions 2.1, for any method of the above form with
and steplengths satisfying the strong Wolfe conditions with ,
The sequence is arbitrary within the bound; the statement contains no constants.
Theorem 2.1 (ii) (the same conclusion for an ideal line search that does no worse than the first stationary point along ) and the convergence of the hybrid method (3.7), .
Theorem 3.2 shows that descent and global convergence of Fletcher–Reeves-type methods do not depend on the exact formula for , only on the bound . Its main consequence is the hybrid method (3.7), which keeps the Polak–Ribière choice whenever it lies in , and so retains the practical efficiency of Polak–Ribière while inheriting the convergence guarantee of Fletcher–Reeves. Lemma 3.1 also shows that, under these conditions, descent need not be enforced by the line search.
The results are proved in the paper. To our knowledge none of them, nor Zoutendijk's theorem for general iterations, has a machine-checked proof in Lean; Mathlib has no theory of line search methods. A formalization would provide a reusable Zoutendijk theorem for any descent method with Wolfe steps, and a verified convergence statement for the conjugate gradient methods used in practice.
The obvious route to convergence of a descent method is to show bounded away from zero and apply Zoutendijk's condition. For conjugate gradient methods this fails: accumulates previous directions and can tend to zero. The argument must instead control the growth of , which requires bounding through the line search, and this in turn requires knowing that every is a descent direction with comparable to . The threshold is exactly what keeps the geometric series in these bounds below ; the result fails without it.
All items live in the namespace NonlinCG.FRBound. The space is a finite-dimensional real inner product space E (the paper uses "the scalar product used to compute the gradient"), and gradient f is the gradient for that product. Conventions committed to:
ℕ → E, used from index 1; index 0 is never constrained.The goal does not assume Zoutendijk's condition or descent: both are consequences (Theorem 2.1 and Lemma 3.1) and assuming either would remove part of the theorem's content. The hypotheses are jointly satisfiable (for on , , , , , ), so the goal is not vacuous.
Needed infrastructure: line-search conditions, the descent lemma for functions with Lipschitz gradient on a set, and summability arguments for . Zoutendijk's theorem is reusable for any descent method. Proofs of any item, and alternative arguments, are welcome.
A linear program often has two objectives that pull in different directions, for example cost and risk, or two policy goals whose relative weight is a matter of judgment. Gass and Saaty (NRLQ 1955) put the question in its simplest form: let every cost coefficient be an affine function of one real parameter , and find, for every value of , an optimal solution. Their paper turned this into a procedure that runs the simplex method once and then walks along the -axis, changing one basis column at a time. This parametric objective function method became a standard chapter of linear programming texts and is the prototype of parametric and sensitivity analysis in optimization software.
Timeline.
For each real the problem is
Write , an real matrix with columns , and . A basis is a list of linearly independent columns ; its basic solution has off the basis and , and it is a basic feasible solution when also . Every column has coordinates in the basis, . For a cost vector the simplex method uses ; for the cost the number is affine in :
The basis is optimal at when for all (inequalities (3)). The critical values of the basis are
The paper assumes throughout that the problem is nondegenerate: no basic feasible solution has more than zero components.
Case A is the situation where the current basis is optimal for some , so that (3) is consistent. If is finite, attained at an index with , and some , the method brings into the basis and removes the column , , chosen by the simplex ratio test; . Call the new basis and its basic feasible solution .
This contains both sentences of the paper's THEOREM: the new basis yields a minimum for at least one (namely ), and the left end of its interval of optimality equals . The statement uses "least element" and so does not presuppose that the set is an interval.
The THEOREM is what makes the parametric procedure correct. The optimality intervals of successive bases meet end to end: the basis entered at takes over exactly where the old one stops, with no gap and no overlap. Together with the stopping rule this gives the paper's summary: starting from one optimal basis, the procedure produces a finite list of bases and characteristic values covering every for which the problem has a minimum, and that set is a closed interval. The same structure underlies the piecewise linear, concave optimal value as a function of , the parametric right-hand-side method by duality, and the shadow-vertex simplex method.
The result is classical and its proof is short, but as printed it contains a sign slip: display (8) on p. 41 states the inequality in the wrong direction, so the contradiction the authors claim does not follow from what they wrote. The formal development states the corrected argument. To our knowledge none of these parametric statements has a machine-checked proof; the fixed-cost facts they rest on (the reduced-cost optimality criterion, Bertsimas–Tsitsiklis Theorem 3.1, and the feasibility of the pivoted basis, Theorem 3.2) are already proved on the platform in Shuze Chen's LinearOptimization library and are reused here as reference items.
The natural first idea is to observe that satisfies (3') and conclude. This proves only that the new basis is optimal at . The statement that nothing below works is a statement about optimality, not about the inequalities (3'): one must know that failure of (3') at means that is not optimal at . That converse of the optimality test is false for a degenerate basic solution, which can be optimal while some is positive. The nondegeneracy assumption is therefore essential, and it must be transported to the new basic solution. The other ingredient is the pivot update of when one column leaves and another enters, which the paper uses through (7) without writing it down.
The problem data are A : Matrix (Fin m) (Fin n) ℝ, b : Fin m → ℝ and cost vectors d d' : Fin n → ℝ; the parameter is the Lean variable t (λ is a Lean keyword). Indices are 0-based. Feasible set, optimality, bases, reduced costs, basic directions, the coordinates (pivotColumn) and basic feasible solutions (IsSimplexState) are the published LinearOptimization definitions. The commitments and readings of the paper's phrases are:
IsLpOptimal), never a comparison of values.WithTop ℝ and WithBot ℝ; no real infimum of a possibly empty set is used.The goal is not satisfied by a degenerate reading: its set is defined by optimality, not by the inequalities (3'), and its hypotheses hold on an explicit instance, so the statement is neither the definition of the critical value restated nor vacuous.
Not formalized: Case B (the search for a first with a minimum), Summary (1)–(2) on the whole procedure, the no-repetition remark, the computing experience (§3) and the worked example (§4). Contributions welcome include the pivot-update formula for reduced costs, which is reusable for any simplex-based argument, and the closedness of the set of cost vectors with a finite optimum.
A Markov decision problem with the average reward criterion asks for a policy that maximises the long-run reward per period of a controlled finite Markov chain. It is the standard model for repeated operational decisions with no natural horizon: inventory replenishment, machine maintenance, queue admission and routing. For finitely many states and actions, Howard (1960) and Blackwell (1962) showed that a pure stationary average optimal policy exists, and policy iteration finds one.
Linear programming formulations are older for the discounted problem (d'Epenoux, 1960) and for chains with a single recurrent class (Manne, 1960). Without a structural assumption, a stationary policy can split the state space into several recurrent classes, the multichain case, and the gain becomes a vector rather than a number. Denardo and Fox (1968) gave a linear programming approach for this case. Hordijk and Kallenberg (1979) showed that a single pair of dual linear programs suffices: an optimal policy can be read off an extreme optimal solution of the dual program. Kallenberg's tract (1983, Chapter 4) is the systematic account of this theory, and this mission formalizes its §4.2–4.4.
Let be a finite set of states. Each state has a nonempty finite set of actions, a reward for each action, and transition probabilities with . A policy chooses, at each epoch , a probability distribution on that may depend on the whole history. A stationary policy uses fixed weights at every epoch. A pure stationary policy always plays . Write , , and , in the pure case.
The average reward of from state is
and is the same expression with . The AMD-value-vector is , where ranges over all policies, and is average optimal if . A policy is Blackwell optimal if it maximises the discounted reward for all discount factors in some interval .
For a stochastic matrix , the stationary matrix is the Cesàro limit of , and the deviation matrix is . For a pure policy, and .
A vector is AMD-superharmonic if some satisfies and for all , . For weights with , the primal program (4.2.10) minimises over such pairs. Its dual is
Write .
If is an optimal solution of (4.2.11) and an extreme point of its feasible set, then a decision rule with
exists, and every such is average optimal.
The goal is stated for every finite model, with no assumption on the chain structure, and for every rule-conforming .
Theorem 4.2.4 reduces the multichain average reward problem to one linear program. Combined with Theorems 4.3.3 and 4.3.4, every pure stationary average optimal policy arises from some extreme optimal solution, so enumerating extreme optimal solutions enumerates all of them (Remark 4.2.5). The same program is the starting point for the constrained average reward problems of §4.7, where a policy must also satisfy linear constraints on its state–action frequencies. Theorem 4.4.1 is the evaluation step of multichain policy iteration.
The results are proved in the tract and, earlier, in Hordijk and Kallenberg (1979). None of them is formalized in a proof assistant. The platform has machine-checked average reward results only for unichain models, where the gain is a scalar. This mission adds the multichain theory, with general history-dependent randomized policies as competitors, and also yields reusable statements about stationary and deviation matrices of finite chains.
Under a unichain assumption, the dual variables form a stationary distribution and the -variables are unnecessary, so the obvious argument reads a policy off alone. In the multichain case the -part of an optimal solution can vanish on whole sets of states, and on those states the policy must be read off . The argument then has to show that these states are transient under the selected policy, which is where extremality is essential. For a non-extreme optimal solution the book passes instead to the randomized policy (4.3.1), which needs the separate argument of Theorem 4.3.3. A second obstacle is that optimality is against all history-dependent randomized policies, so the comparison of with must pass through the superharmonic characterisation (Theorem 4.2.2), whose proof uses the existence of a Blackwell optimal policy.
The model is the published MarkovDecisionProcesses.StationaryMDP: finite state and action types, a nonempty Finset of admissible actions per state, and stochastic rows. General policies are the published AvgHRPolicy (decision rules depending on the epoch and the full history). The criteria are the published gainInf, gainSup and optGainInf; all values are real. Average optimality is the book's lim inf notion, for every . It is not Puterman's stronger IsAverageOptimal. The stationary and deviation matrices are the published Cesàro limitMatrix and deviationMatrix. Their existence and invertibility (Theorem 2.4.1) are never assumed as hypotheses. LP variables are indexed by admissible state–action pairs, so Set.extremePoints is the book's notion of extreme feasible solution. Recurrence is the classical finite-chain notion: every state accessible from leads back to . The ergodic set of a recurrent state is the set of states accessible from it.
A formalization that assumes a unichain or ergodic model trivializes the mission (it reduces Theorem 4.2.4 to known unichain results). No statement here makes such an assumption, and the weights are strictly positive and sum to one, as in (4.2.10).
The proofs need finite Markov chain theory: the Cesàro limit, , , transience versus , and positivity of the stationary distribution on ergodic sets. They also need LP duality with complementary slackness and the existence of a Blackwell optimal pure policy. The last result is posed separately on the platform (Blackwell 1962, Theorem 5). LP duality is available as proved platform theorems (LinearOptimization.*), whose sign conventions must be matched. Contributions on the Markov chain layer are reusable across the whole series.
A Markov decision chain with finitely many states and actions is the basic model of sequential decision making under uncertainty in operations research. Inventory control, maintenance, queueing control and many other problems reduce to it. Under the average reward criterion the decision maker optimizes the long-run reward per period. For the discounted criterion one linear program yields an optimal pure stationary policy (d'Epenoux 1960). For the average criterion, De Ghellinck (1960) and Manne (1960, DOI 10.1287/mnsc.6.3.259) gave linear programs for the unichain case, where every stationary policy has a single recurrent class. In a multichain model the optimal average reward may differ from state to state, and the unichain construction no longer applies.
Hordijk and Kallenberg (Management Science 25(4):352–362, 1979, DOI 10.1287/mnsc.25.4.352) proved that in the general multichain case an average optimal policy can be found by solving only one linear program. This mission formalizes that result, Theorem 7 of the paper, together with the chain of results its proof rests on.
Timeline, following the paper's introduction:
The state space is a finite nonempty set . In state a finite nonempty set of actions is available; choosing earns the reward and moves the system to state with probability (, ). A policy chooses actions at times , possibly at random and using the whole history. For a policy and an initial state ,
is the average expected reward, and is the optimal one. A policy is average optimal if for every . A decision rule picks in every state; is the pure stationary policy that always applies . Its transition matrix is and its reward vector . The α-discounted value enters through Theorems 1, 3, 4 and 5.
Fix weights with . The dual program has a variable pair for every state and every :
for all . Its linear programming dual, the primal program, minimizes over superharmonic pairs : and for all , . For a dual solution put .
Let be an optimal solution of the dual program that is an extreme point of its feasible set, which is what the simplex method returns. Let be any decision rule with
Then is average optimal: for every , the comparison running over all policies.
In the order the proof uses them:
Theorem 7 turns the multichain average-reward problem into one linear program and one pass over its solution. No unichain or communicating assumption is required, and neither the second linear program nor the search step of the earlier Denardo–Fox–Derman procedure is needed. The rule is local: any action with a positive -variable, otherwise any action with a positive -variable, gives an optimal policy. The paper's later results (Theorem 8, the correspondence between optimal dual solutions and optimal randomized stationary policies, and Theorem 10, on extreme points) build on the same program. Companion missions of this series formalize them.
The results are proved in the paper; no machine-checked proof of any of them is known. The formalization adds a machine-checked link between linear programming duality (complementary slackness, extreme points of polyhedra) and the limit theory of finite Markov chains (Cesàro limit matrices, transient states), over the history-dependent policy class of the published average-reward model.
The obvious argument reads off any optimal dual solution and uses complementary slackness to obtain and . The second equation holds only on , and outside nothing controls the reward of . The argument closes only when is transient under , so that the stationary distribution of ignores those states. Transience is not a consequence of optimality. It uses extremality: an ergodic set inside would make the corresponding -columns of the constraint matrix linearly dependent. For a general optimal solution the paper proves optimality only of a randomized stationary policy built from (its Theorem 8(b), a companion mission), not of a pure selection. The extremality hypothesis is therefore part of the statement.
Upstream of the linear program, Theorem 6 depends on Derman's theorem and Blackwell's expansion of the discounted value near . Both compare against all history-dependent policies and need the full limit theory of and .
The model is the published MarkovDecisionProcesses.StationaryMDP (finite nonempty S, finite A, nonempty admissible sets, stochastic transitions) with history-dependent randomized policies AvgHRPolicy. is gainInf (the lim inf of the average of the first expected rewards) and is optGainInf, a real supremum that is finite because rewards are bounded. and are the published limitMatrix and deviationMatrix; the identities of Theorem 2 are the published Blackwell Lemma 1(a), (d). Conventions:
IsAverageOptimal in the published file.totalReward. "α near enough to 1" means some such that the property holds on .Pair M), so the feasible set lies in (Pair M → ℝ) × (Pair M → ℝ) and its extreme points are those of the paper's polyhedron.Set.extremePoints). A goal without extremality is a different and unproved statement, and any version that quantifies over some instead of every obeying the rule is weaker than the paper's. Both are ruled out.IsRecurrent. Maxima over and are stated as an upper bound plus attainment, so that is part of Theorem 5.A complete development needs Cesàro limits of stochastic matrices, the deviation matrix, Abelian limits of discounted values, linear programming duality with complementary slackness, and the characterization of extreme points of by linear independence of the active columns. The last two are reusable well beyond this mission, as is the identification of gainInf of a stationary policy with . Contributions to any of them, including proofs of individual milestones, are welcome.
A chance constraint limits the probability of violating a requirement rather than requiring that requirement to hold for every realization of uncertain data. Charnes and Cooper developed deterministic optimization problems for several ways of judging decisions under such constraints. Their P model gives a satisficing objective: increase the probability of reaching a specified aspiration level while meeting prescribed reliability levels for the resource constraints. The paper's concrete decision rule makes the decision vector depend linearly on the random right-hand side, and its P-model section moves from a fractional deterministic program to a convex one. The result explains how a risk-adjusted ratio can be optimized without retaining a fractional objective. The source is Charnes and Cooper, 1963, pp. 30–33, especially equations (35) and (38)–(39b).
The related linear-fractional change of variables was already being used for linear programs Charnes and Cooper, 1962; the present section applies it to constraints built from second moments rather than linear equations. That distinction matters because the normalized feasible set contains a boundary at zero scale, and because second-moment inequalities require their own convexity claim. The paper cites fractional programming results for its local-to-global assertion about (38); the mission focuses on its explicit transformed program (39). Charnes and Cooper, 1963, p. 32.
Let be positive integers and a probability space. A fixed real matrix has rows . Random vectors and give the right-hand side and objective coefficients. The paper restricts decisions to the linear decision rule , where the real matrix is chosen before is realized. Write and . A number is the given aspiration value. For each row , its reliability level is strictly between and , and is the corresponding standard-normal quantile. These are the objects of equations (5), (19b), (21), and (27) in Charnes and Cooper, 1963.
The residual has raw second moment and negative mean . The aspiration error has raw second moment . These definitions come from equations (30) and (34). The expected linear objective appearing in the deterministic programs is ; the model records the paper's assumption that the components of and are uncorrelated. Charnes and Cooper, 1963, pp. 26, 28, 30.
Program (38) chooses and maximizes . Its inequalities bound the mean objective below by , bound below by the root-mean-square aspiration error, and bound each nonnegative between the row's risk term and . The denominator satisfies . Program (39) introduces a nonnegative scale and barred variables. It fixes and maximizes the linear objective . The barred moments are calculated from and by equation (39b), rather than declared to be scaled copies of the unbarred moments. Charnes and Cooper, 1963, pp. 32–33.
Let contain every point satisfying all of (39), including . The paper's convex-programming claim becomes
The source states the claim after displaying the barred moments, in the paragraph following (39b). Charnes and Cooper, 1963, p. 33.
Let be the feasible set of (38). Provided is nonempty, the mission goal states that the normalized substitution sends each point of to a point of with the same objective, and that
The suprema may be infinite. The equality concerns the complete program (39), including . Positive-scale points have an inverse substitution; zero-scale points are retained in the comparison. This is the precise optimal-value reading of the paper's statement that (38) can be replaced by one convex program. Charnes and Cooper, 1963, pp. 32–33.
The result places the P model alongside the paper's E and V models as an optimization problem with convex feasible constraints and a nonfractional objective. A solver of (39) can compare aspiration and resource reliability within the same matrix decision rule. Equality of suprema says the transformed model has the same best attainable value even when the best value is only approached, and even when points at occur in the transformed feasible set. The forward and inverse substitution statements identify how positive-scale solutions correspond. Charnes and Cooper, 1963, pp. 30–33.
The paper result is a published mathematical claim. The present formalization states its definitions and assertions in Lean; its theorem proofs are still open. The standard Gaussian CDF and its inverse are available as a separately published Prove2Me definition, while the model-specific second moments and feasible sets must be formalized for this mission. The previously published Derman linear-fractional lemma concerns a polyhedral linear program and does not assert this P-model result. Completing the mission would add reusable formal machinery for expected-square constraints, a normalized perspective program, and equality of optimal values at a scale boundary.
The pointwise substitution only reaches points of (39) with , while (39) explicitly permits . Therefore a bijection of feasible points at positive scale alone does not establish equality of the displayed suprema. The proof also has to reconcile the squared form of the row constraints with convexity: is a raw second moment and is the square of its mean, so their difference is the variance term relevant to the risk bound. Taking the fourth inequality as a generic difference of quadratics would obscure that claim. The paper prints a conflicting square and sign in (38), which must be resolved against its earlier (29) and later (39). Charnes and Cooper, 1963, pp. 28, 32–33.
Lean uses finite index types Fin m and Fin n, real matrices and scalars, a probability measure , and Bochner integrals for the moments. Square integrability is stated for every component of and and every product ; this keeps the expected squares meaningful. The paper assumes and are uncorrelated, so the same componentwise equalities are recorded. It also assumes that each row residual has a Gaussian law under a decision matrix; the Lean theorem retains this standing assumption even though the substitution from (38) to (39) is algebraic. The quantile is imported from the published Cohen2019.Robust.PhiInvReal, with excluding its junk endpoint values. The theorem concerns (38) onward; it does not assert the paper's analogous reduction from the original probability model (35), because the text does not establish a distributional theorem for its random objective. Charnes and Cooper, 1963, pp. 26–27, 31–33.
The source phrase “replace ... by one convex programming problem” is made explicit as convexity of the (39) feasible set, feasibility and value preservation of the forward scaling, and equality of extended-real suprema. The normalization , strict , and weak are separate conditions. The slice is included, and the main theorem assumes nonempty. The barred functions are genuine expectations of the homogenized expressions of (39b). The square-and-sign discrepancy in printed (38) is resolved in favor of the form printed in (29) and (39), consistent with the nearby statement that the row constraints are the same as before. These choices exclude a vacuous denominator, an artificially smaller transformed set, and a trivially defined scaling identity. Reusable contributions include moment lemmas, convexity results for expected-square constraints, and supremum comparison for normalized programs.
Value iteration computes the optimal value function of a Markov decision process by applying the dynamic programming backup to every state until the values stop changing. When the state space is too large for a lookup table, practitioners replace the table by a function approximator: after each backup, the new values are computed only at a sample of states and an approximator (a neural net, a spline, a nearest-neighbour rule) is fitted to them. This approximate value iteration is the basis of much of reinforcement learning, and in the early 1990s it was known to work well in some experiments and to diverge in others, with no theory separating the two. Boyan and Moore (NIPS 7, 1995) exhibited divergence with linear regression and neural nets, and Tsitsiklis and Van Roy (1996) later studied the same question for feature-based architectures.
Gordon's technical report (CMU-CS-95-103, 1995; a shorter, differently numbered version appeared at ICML 1995) isolated a property of the approximator that guarantees convergence: the approximator must not exaggerate differences between target value functions in max norm. It identified a broad class with this property, the averagers (k-nearest-neighbour, kernel averaging, linear and bilinear interpolation on a mesh), and proved that in a discounted problem approximate value iteration through an averager always converges, with an explicit error bound. This mission formalizes that discounted theory: the report's §2–§3 and its error bound of §6.1.
A finite Markov decision process has states , a finite nonempty set of actions at each state , an expected one-step cost for action at state , and transition probabilities with . It is discounted with factor . A value function is a vector , measured in the max norm .
The parallel value backup operator updates every state at once:
Its fixed point is the optimal value function, the minimal expected discounted cost from each state.
A function approximator is studied through its mapping : the function sending a vector of target values to the vector of fitted values. Two operators and are compatible if the iterates converge from every initial guess .
An averager is given by constants and nonnegative weights with for every ; its mapping is
The weights are fixed in advance and do not depend on the targets .
Let be any fixed point of and . Then there is such that from every initial guess , and
The goal has two parts: convergence from every start to a common limit , and the error bound on that limit.
A further item, not a milestone, is the display after the proof of Theorem 6.2 (p. 13), the bound on the fitted output: .
Theorem 6.2 gives a guarantee that depends only on how well the approximator can represent , not on how the iteration is started: if some fixed point of the averager lies within of , approximate value iteration finds a function within of . Theorems 3.1 and 3.2 explain why: an averager is a max-norm nonexpansion, and composing a nonexpansion with a -contraction leaves a -contraction. Together they separate the approximators that are safe to use with value iteration from those that are not (linear regression is not a nonexpansion: the report's Figure 2 shows it can expand max-norm distances).
All results of this mission are proved in the report; none is open. The contraction of the discounted Bellman operator and the identification of its fixed point with the optimal value function are proved on Prove2Me (BertsekasDP.discounted_main_theorem, used here as a reference item). No machine-checked proof of Gordon's averager results or of the bound is known to exist; this mission produces one, on top of the published finite MDP model.
Each step is short on paper; the difficulty is in the bookkeeping that a formal proof cannot skip. The nonexpansion of an averager rests on nonnegative weights summing to at most one, which must be extracted from the row constraint in the max norm on . The goal's convergence clause asks for one limit shared by all initial guesses, which needs completeness of and the contraction-mapping theorem applied to , not to . The error bound compares three different fixed points ( of , of , of ) in a chain of triangle inequalities. The order of composition matters throughout: the compatibility results iterate (fit after the backup), while the goal iterates (back up after the fit), and the two may not be interchanged.
BertsekasSSPModel (Fin n states, a finite action type, nonempty admissible action sets , costs g, transition probabilities p), and is its BertsekasDiscountedBellmanOp M γ. That model allows substochastic rows; every statement adds the hypothesis for admissible , which makes it the report's MDP. Action sets may depend on the state, a harmless generalization of the report's single action set. The initial-state distribution never enters a statement and is omitted.Fin n → ℝ is Mathlib's sup norm, i.e. the max norm.BertsekasDP.discounted_main_theorem, identifies it with the optimal value function.LipschitzWith.comp, ContractingWith) and are not posed.Proofs of any item are welcome, as are reusable lemmas on max-norm nonexpansions of row-stochastic linear maps, which also serve the nondiscounted companion mission (Stable Function Approximation in Dynamic Programming II).
In the cutting stock problem, stock rolls of length are cut into pieces of lengths to fill orders. Part I of Gilmore and Gomory's work (Opns. Res. 9 (1961)) solved its linear programming relaxation by the simplex method with column generation: the columns (cutting patterns) are too many to list, so each simplex iteration finds an improving column by solving a knapsack problem. Part II (Opns. Res. 11 (1963)) extends the method in several directions. One of them, customer tolerances, lets the amount produced of each length lie in a range instead of matching a fixed demand. Total roll usage then stops being a good measure of quality, because overproducing within the tolerance is free. The natural objective becomes the fraction of waste: total waste divided by total material cut. This objective is a ratio of two linear functions, not a linear one.
The paper's answer, on p. 882, is that the ordinary simplex method still works for such an objective. It moves from vertex to vertex, at each vertex asks whether some edge improves the objective, and stops when none does. Ratio objectives of this kind, called linear-fractional programs, were studied in the same years by Isbell and Marlow (1956), Martos (1960–61, in Hungarian; in English in 1964), Charnes and Cooper (1962) and Dinkelbach (1962; see also 1967). Gilmore and Gomory say that their method is closest to Martos's. They derive the edge test for the ratio and show that, for cutting stock, choosing the entering column is again a knapsack problem.
Let be a real matrix, and . The linear-fractional program is
In the cutting stock instance (p. 881), column is either a cutting pattern with or a slack column . The right-hand side is . The numerator coefficient of a pattern is its waste (eq. (4)), and on patterns and on slacks, so is waste per roll cut. The paper drops the upper bounds on the slacks from the discussion (p. 882), and so does this mission.
A basis is a set of column indices whose columns of are linearly independent. A basic feasible solution with basis is a feasible point with for every . For a nonbasic , the edge direction of is the vector with , and for the other nonbasic . This is "the edge that would be traced out if were increased, but all other nonbasic variables kept zero" (p. 883). The quantity the simplex test inspects is the rate of change along the edge,
Assume for every feasible . Let be a basic feasible solution with basis , and suppose for every and every edge direction of . Then
The result. The edge criterion turns a nonconvex problem into one the simplex method solves. A ratio of linear functions is neither convex nor concave, so a point where no feasible direction improves the objective locally is not obviously a global minimum. The criterion says that, on a polyhedron where the denominator keeps its sign, this local test at a vertex certifies global optimality, exactly as for a linear objective. It underlies the convergence of Martos's method and of every simplex-type algorithm for linear-fractional programming. Together with milestone 4, it is what makes column generation with a knapsack pricing step applicable to the waste-fraction objective of cutting stock.
Formalizing it. The result is classical and proved; no machine-checked version is known to exist. The published platform items closest to it are Derman's Charnes–Cooper transformation of a linear-fractional program into a linear program and Matoušek's reduced-cost optimality criterion for a linear objective. Neither states an edge criterion for a ratio. A formal proof here also settles the paper's own imprecisions (see below), and yields reusable lemmas about ratios of affine functions along lines.
The obvious argument does not reach the goal. Along any single segment the objective is monotone (milestone 1), so a nonnegative derivative at in the direction of the segment would settle it. But the test at inspects only the edge directions, while a feasible point lies in the direction , which is in general not an edge. Monotonicity along each edge says nothing directly about other directions, and is neither convex nor concave, so local optimality along a few lines does not by itself transfer to the whole polyhedron. The step that has to be supplied is the passage from the edges to all feasible directions at a basic solution. It fails without the basis: at a feasible point that is not basic, or with linearly dependent columns, the edge directions need not reach every feasible point. At a degenerate vertex some edge directions leave the feasible set at once, and a test restricted to the feasible edges does not certify optimality.
The feasible set and the objective are the published definitions DermanSeqDecisions.LinProg.IsFeasible11 (, ) and DermanSeqDecisions.LinProg.fracObj (). The basis is the published MatousekLP.BFS.IsBasis. Indices are 0-based. A mission definition adds the basic feasible solution and the relational edge direction. The edge direction is given by its defining equations, not through a basis inverse, and is not required to be feasible.
Committed conventions and disclosed choices:
deriv of at : the actual rate of change, not a formula assumed to equal it.The following would trivialize the goal and are excluded: an edge hypothesis over all directions instead of the edge directions, which turns the goal into quasi-convexity along segments; an edge hypothesis stated as the global inequality; a positivity hypothesis on the denominator over all of ; and dropping the basis, under which the goal is false.
The development needs elementary real calculus (derivatives of quotients, monotonicity from the sign of the derivative) and the linear algebra of a basis (existence, uniqueness and spanning of the edge directions). The lemmas about ratios of affine functions along lines and about edge directions of a basis are reusable for any simplex-type method. Contributions of proofs of the milestones, and of auxiliary lemmas on edge directions, are welcome.
Chordal graphs (graphs in which every long cycle has a shortcut edge) appear wherever a sparse symmetric structure has to be eliminated without creating new interactions: Gaussian elimination on sparse symmetric matrices (Rose 1970), acyclic database schemes, junction trees for probabilistic graphical models, and phylogenetic and scheduling problems. In all of these applications the useful object is not the graph itself but a tree representation of it: a tree on which every vertex of the graph is a connected piece, and adjacency is overlap.
The theorem of this mission says that such tree representations exist exactly for chordal graphs. It extends the theory of interval graphs (intersection graphs of intervals on a line, i.e. of subpaths of a path), whose characterization was asked by Hajós (1957) and given by Lekkerkerker–Boland (1962), Gilmore–Hoffman (1964) and Fulkerson–Gross (1965), from paths to arbitrary trees.
Timeline. Dirac (1961) proved that every chordal graph has a simplicial vertex, a vertex whose neighbourhood is a complete subgraph. Rose (1970) used this to recognize chordal graphs efficiently, and Gavril (1972) showed that a chordal graph has at most as many maximal cliques as vertices. Renz (1970) studied intersection graphs of arcs in trees. Gavril (1974), together with Buneman (1974) and Walter (1972/1978) independently, proved that the intersection graphs of subtrees of trees are exactly the chordal graphs, and gave an algorithm that builds such a representation.
All graphs are finite and simple: a graph has a finite vertex set and a symmetric irreflexive adjacency relation. A completely connected set is a set of pairwise adjacent vertices, and a clique is a maximal completely connected set. The set of cliques of is , and is the set of cliques containing the vertex . For a vertex , is the set of its neighbours; is simplicial if is completely connected.
is chordal if every simple circuit with vertices has a chord: an edge of joining two vertices of the circuit that are not consecutive on it.
A tree is a connected graph without simple circuits. A subtree of is a nonempty set of tree vertices that induces a connected subgraph of . A family of subtrees of represents if, for all distinct ,
is a subtree graph if it has such a representation on some tree, and a proper subtree graph if it has one in which no subtree is contained in another.
for every finite simple graph . The paper calls this "the main theorem of this paper".
and, cited on p. 49, for a nonempty finite chordal graph.
The result. The theorem turns a forbidden-structure condition (no chordless cycle of length at least four) into a constructive geometric one (a tree model), and Theorem 2 makes the tree canonical: its vertices are the maximal cliques. Clique trees are the data structure behind junction-tree inference, multifrontal sparse Cholesky factorization, and dynamic programming over tree decompositions; the treewidth of a graph is defined through chordal supergraphs and their clique trees. The proper-subtree result of §3 shows a contrast with interval graphs, where proper interval graphs form a strictly smaller class.
Formalizing it. The theorem is classical and fully proved in the literature, but Mathlib has no notion of chordal graph, no Helly property for subtrees, no clique trees and no simplicial-vertex theorem. This mission produces those definitions together with the characterization, the Helly property for finite families of subtrees, the Dirac–Rose theorem under the cycle–chord definition, and closure of chordality under induced subgraphs. As far as is known, none of these results has a machine-checked proof in Lean under the cycle–chord definition.
The "only if" direction is short on paper but rests on tree facts that are not packaged in Mathlib: a connected vertex set of a tree contains the unique path between any two of its vertices, and three pairwise paths of a tree meet. The "if" direction must produce a tree on the set of maximal cliques, and the maximal cliques of a graph are not stable under passing to induced subgraphs: a clique of a subgraph need not be a clique of , and two cliques of may restrict to the same set. Relating to for a smaller graph is the step where informal arguments are routinely loose, and it is where a formal proof spends most of its effort. The Dirac–Rose theorem is cited rather than proved in the paper and needs a separate development.
A tempting shortcut is to define chordality as the existence of a perfect elimination ordering. This builds the Dirac–Rose theorem into the definition and changes the theorem being proved; it is excluded here.
G : SimpleGraph V with [Fintype V] in the goal, Theorem 2, the clique-tree claim, Dirac–Rose and the clique count. Milestones whose claims hold for infinite graphs (Lemma 1 for finite , the three-point remark, the clique-disjointness claim, subtree ⇒ chordal, induced chordality, the simplicial clique, subtree ⇒ proper subtree) are stated without finiteness, which makes them stronger. may be empty in the goal and in Theorem 2; Dirac–Rose and the clique count assume nonempty, which they need.c of length at least 4 there are vertices x, y on c with G.Adj x y and s(x, y) not an edge of c.T : SimpleGraph β with T.IsTree (not necessarily finite), and a subtree is a vertex set s with (T.induce s).Connected; subdividing the topological tree at all end-points shows the class of subtree graphs is the same. The tree type lives in the same universe as V.V; adjacency is compared only for distinct vertices. A clique is Maximal G.IsClique s; is the subtype of such sets.Commuters choose not only a route but also a departure time, trading travel delay against the penalty of arriving early or late. Static traffic assignment, in the tradition of Wardrop's user-equilibrium principle, ignores the time dimension; dynamic traffic assignment adds it, and its central modelling question is what "equilibrium" means when flows, delays and costs all vary over a time horizon. Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41(1), 1993) proposed the simultaneous route-departure (SRD) equilibrium of a path-based dynamic model and showed that it is equivalent to an infinite-dimensional variational inequality. That equivalence is the starting point of a large literature on dynamic user equilibrium: existence theory, solution algorithms and differential-variational formulations all take the variational inequality as their definition of the problem.
Timeline, as far as this mission is concerned:
A traffic network has a finite set of paths. Each path connects exactly one origin–destination (OD) pair ; denotes the paths of pair . Travellers depart during the horizon , , which carries Lebesgue measure ; "" means "for -almost every ".
A vector of departure-time densities assigns to each path a square-integrable, almost everywhere nonnegative function on : is the rate at which travellers depart at time on path . The set of such vectors is . Each OD pair has a fixed travel demand , and the feasible set is
A cost operator gives the effective delay of departing at time on path when the densities are : travel time plus a penalty for early or late arrival (13). Because densities are defined only up to null sets, the relevant lowest achievable cost on a path is an essential infimum,
and the lowest achievable cost for pair is .
Definition 3. For and a nonnegative vector , the pair is an SRD equilibrium if for every OD pair and every :
No positive-measure set of travellers can lower its cost by switching route or departure time.
For with nonnegative, square-integrable costs :
and conversely, if solves (39), then with is an SRD equilibrium. The formal goal states the two directions as two conjuncts; the second names the equilibrium cost vector explicitly, which is stronger than an equivalence with an existential .
The result. Theorem 2 converts an equilibrium defined by almost-everywhere complementarity conditions into a single variational inequality over a convex subset of a Hilbert space. This is what makes dynamic user equilibrium accessible to the general theory of variational inequalities: existence via monotonicity or compactness arguments, and projection-type algorithms in function space or after time discretization. The sufficiency half also identifies the equilibrium cost levels: they are the essential infima , so the multiplier need not be found separately.
Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof requires essential infima, the shifting of mass between paths on sets of prescribed measure (the paper cites Halmos, Proposition 41.2, for the nonatomicity of Lebesgue measure), and careful integrability bookkeeping. The development is a self-contained template for "complementarity conditions a.e. ⇔ variational inequality in " arguments, which recur in continuous-time equilibrium models.
Necessity is routine once integrability is in place, though the paper's text asserts the per-path identity , which is false; only the sum over vanishes, and that suffices. Sufficiency is the substantive half. The obvious approach, testing (39) against a perturbation that moves flow from an expensive to a cheap route, has to be carried out with sets rather than points: the costs are only defined almost everywhere, the minimal cost is an essential infimum that need not be attained at any time, and the perturbation must keep the demand constraints exact. This forces the choice of sets of exactly equal positive measure inside the positive-measure sets and , a nonatomicity argument that a pointwise proof would miss.
Densities are plain functions with a square-integrability condition with respect to Lebesgue measure restricted to , not equivalence classes; every pointwise condition is -almost everywhere, and values outside are unconstrained. Paths and OD pairs are finite types, with a map sending each path to its OD pair. The essential infimum is the literal formula (12), a real supremum; it is not the pointwise infimum, which changes when is altered on a null set and makes sufficiency false. is a real infimum over ; for a pair with no paths it is an unused default value.
The cost operator C is abstract, with the paper's measurability assumption strengthened to square-integrability so that every integral in (39) is a genuine Lebesgue integral. The network dynamics (3)–(11) that produce C in the paper are not formalized. Nonnegativity (the codomain of (13)) and square-integrability are assumed only at , which makes the formal statements stronger than the paper's. Without integrability, Lean's integral of a non-integrable function is , so (39) could hold vacuously; the added hypothesis excludes that trivialization. The goal quantifies over every cost operator satisfying these hypotheses and never fixes one. In the milestones, the reduction from to (p. 188) is taken as the hypothesis .
A complete development needs: properties of the real essential infimum (12) on a finite measure space; Lemma 2 (continuity of measure from below); the existence of measurable subsets of prescribed measure in Lebesgue measure (nonatomicity, available in Mathlib in some form); and integral bookkeeping for products of functions on a finite measure. The essential-infimum and mass-shift lemmas are reusable for other continuous-time equilibrium models. Proofs of any milestone, and cleaner restatements of the essential-infimum API, are welcome.
The Chinese postman problem, posed by Meigu Guan (Kwan Mei-Ko) in 1962, asks for a shortest closed walk in a graph that traverses every edge at least once: the route of a postman who must cover every street and return to the post office. It is the basic model of arc routing (street sweeping, snow ploughing, meter reading, inspection of networks), and it is one of the first combinatorial optimization problems shown to be solvable in polynomial time by matching methods.
Edmonds and Johnson, Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), reduce the postman problem to a parity problem: choose nonnegative integers , the number of extra traversals of each edge, so that every node becomes even, at minimum total length. Their §3 gives a complete linear description of this parity problem. The description is the first instance of what is now called the -join polyhedron (with the set of odd-degree nodes), a standard object of polyhedral combinatorics and a frequent example of total dual integrality.
Timeline:
A graph has a finite set of nodes and a finite set of edges; each edge meets two different nodes, and several edges may meet the same pair of nodes. The degree of a node is the number of edges meeting it, , where if meets and otherwise. Set when the degree of is odd (an odd node) and otherwise.
An edge meets a set when exactly one of its two ends lies in . A set is an odd set when it contains an odd number of odd nodes, and any number of even nodes.
The parity points are the vectors with
the conditions (3.1), (3.2), (3.6) of the paper. Adding copies of each edge to makes every degree even, and an Euler tour of the enlarged graph is a postman tour of . The postman polyhedron is
the conditions (3.2) and (3.5). For lengths the objective is . The dual linear program has a variable for each odd set, constraints and , and objective .
Both inclusions are claimed. The equality is between subsets of , so it also asserts that the convex hull of is closed.
In the paper's order of argument:
There are two companion statements. The first (pp. 93–94) says that in with , integrality of already forces . The second (p. 91) is the polyhedron theorem in the variables : the convex hull of the integer solutions of (3.1)–(3.3) is the set of solutions of (3.2), (3.2′), (3.3), (3.5).
The theorem turns the parity problem, an integer program, into a linear program over an explicitly described polyhedron. Optimal postman tours therefore come with dual certificates: a packing of odd cuts whose total value matches the tour's extra length. The same description underlies the theory of -joins and -cuts (Schrijver 2003, Chapter 29).
No machine-checked proof of the -join polyhedron theorem exists, on Prove2Me or, to our knowledge, in Mathlib. This mission states it in the multigraph setting of the paper. Milestones 1–4 and 6 are elementary and can serve as warm-ups. Milestone 5, total dual integrality of the odd-cut system, is the substantive step. The paper obtains it from a blossom algorithm; the milestone is stated as an existence result, so any proof of it closes it.
The inclusion is a parity count. The reverse inclusion is the theorem. Two first ideas fail. Total unimodularity does not apply, because the odd-cut constraint matrix is not totally unimodular and has many constraints whose tightness interacts. Reading the result off the matching polyhedron theorem needs the auxiliary loops and an elimination step, and the 1965 matching polyhedron describes perfect matchings of a simple graph, not this parity system on a multigraph. Some argument for integrality of the minimum for every is needed, and the paper's is an algorithm with a dual certificate. A further point is that and are unbounded: equality of hulls is not just agreement of minima over bounded objectives, and the case of objectives with a negative coefficient has to be handled separately (milestone 6).
A graph is the local ChinesePostman.Polyhedron.Graph V E: a map ends : E → Sym2 V with a proof that no edge is a loop, over finite types V and E. Mathlib's SimpleGraph is not used, because the paper allows parallel edges. Degrees, odd nodes and are computed from the graph; the set of odd nodes is never a free parameter. " meets " means exactly one end in . Odd sets range over all subsets with an odd number of odd nodes, with no nonemptiness or properness condition. Parity points are real images of integer vectors E → ℤ, so integrality is part of . Dual variables are functions Finset V → ℝ whose values matter only on odd sets: the sign condition and every sum are restricted to the odd sets. Lengths are arbitrary reals except where the page assumes (milestones 5 and 7).
Trivializing readings are ruled out: (3.5) taken over nonempty proper sets only, "meets" read as "has at least one end in", the odd nodes taken as an arbitrary set , or allowed to contain non-integral points would each give a different, and in some cases false or trivial, statement.
Every definition the statements need is in one file, ChinesePostman.Polyhedron.Setting. A complete development needs finite-dimensional convexity (Mathlib's convexHull) and linear programming duality or an integrality argument. A Lean proof of total dual integrality for odd-cut systems would be reusable for matching and -join problems beyond this paper. Proofs of any milestone, and alternative proofs of milestone 5, are welcome.
The vehicle routing problem with time windows (VRPTW) asks for minimum-cost routes from a central depot that serve every customer exactly once, respecting vehicle capacity and a time interval in which each customer's service must begin. It models school bus routing, parcel and retail distribution, and dial-a-ride services. Desrochers, Desrosiers and Solomon (Oper. Res. 40 (1992) 342–354) gave an optimization algorithm for the VRPTW that solved benchmark instances with up to 100 customers to optimality, a size far beyond earlier exact methods. Their method, which solves the linear relaxation of a set partitioning model by column generation with routes priced out by a resource-constrained shortest path dynamic program, is the template that later exact vehicle routing algorithms ("branch-and-price") follow.
The mathematical core of the method is a certificate: once the pricing subproblem reports that no route has negative marginal cost (reduced cost), the current linear programming solution is optimal over all routes the subproblem can generate, its value bounds every VRPTW solution from below, and an integral solution covering each customer exactly once is VRPTW-optimal. This mission formalizes that certificate and the lemmas of the paper it rests on.
The nodes are a depot and customers . An arc set carries, for each arc , a cost and a duration ; each node has a demand and a time window ; vehicles have capacity .
A path uses arcs of and passes through the depot only at its ends. It is resource-feasible when there are service start times with (waiting is allowed) and , and its load is at most . Its cost is , and is the number of visits of to customer . The paper uses three solution spaces:
A VRPTW solution is a set of feasible routes covering each customer exactly once; its cost is the sum of the route costs.
The set covering type model (Sec. 4) over a column set is
with and integer. Its LP relaxation replaces by and drops integrality. For dual values , , of the three rows, the marginal cost of a column and of an arc are
Let be a finite set of third-model paths, an optimal solution of the LP relaxation restricted to , and an optimal solution of its dual. If every third-model path has nonnegative marginal cost, , then
and, when arc costs are nonnegative, for every VRPTW solution ; if moreover is integral and covers each customer exactly once, its support is an optimal VRPTW solution.
The certificate is the correctness statement of column generation for vehicle routing: it says when the algorithm may stop, what the value it stops with means, and when the branch-and-bound tree can be skipped. The same argument, with a different subproblem, underlies branch-and-price for crew scheduling, cutting stock and many other set partitioning formulations. Milestone 2 is the observation that turns pricing into a shortest path problem on the original network, and milestone 7 is the preprocessing used before every dynamic program over time windows.
The paper's results are classical and their proofs are short in prose. None of them, nor any VRPTW column generation statement, has a machine-checked proof on the platform; the closest existing items concern split deliveries (Desaulniers 2010) or general finite LP duality. The mission produces a reusable formal model of resource-constrained paths, the set covering LP and its restricted dual, on which later branch-and-price papers can build.
The goal combines three ingredients that do not fit together automatically. First, LP duality for the restricted problem: the hypothesis gives an optimal dual, but optimality over all columns needs equality of the restricted primal and dual values, which is strong duality for a finite LP with equality rows and sign-constrained auxiliary variables. Second, the column set of the full LP is infinite in general: a nonelementary path can repeat customers, so the comparison must go through the finitely many columns a given feasible point uses. Third, the pricing hypothesis is about arc sums along node sequences while the LP is about column costs and visit counts; matching them needs the depot to appear exactly at the two ends of a path.
The tempting shortcut of quantifying the pricing hypothesis over the current columns only gives dual feasibility for the restricted LP, which says nothing about columns not yet generated. The lower bound also fails for arbitrary real costs, because row (4) with excludes negative-cost solutions from the LP while the VRPTW still contains them.
Nodes are Fin (n+1) with the depot 0. A path is the list of its customers; its node sequence is 0 :: p ++ [0], so a path visits at least one customer and meets the depot only at its ends. The arc set is an arbitrary relation; costs, durations, demands and windows are arbitrary reals, and every sign or triangle condition a statement needs appears in its own hypotheses. The committed readings:
Finsupp); VRPTW solutions are Finsets of routes;The goal is not to be trivialized: the pricing hypothesis ranges over all third-model paths, not the current columns; equality of primal and dual values is not assumed; the full column set is not ; and "covered exactly once" is not presupposed to mean elementary columns, which must be derived from integrality.
Contributions welcome: proofs of the milestones, a reusable finite LP strong duality interface for Finsupp-indexed columns, and lemmas about arc sums over node sequences.
Fitting a probability distribution to prescribed margins or moments is a basic task in statistics and information theory. Starting from a reference distribution, one can enforce one constraint at a time by choosing the closest distribution in I-divergence, then cycle through the constraints. In a contingency table this procedure is iterative proportional fitting. A single projection onto the intersection is the desired answer, but each step of the iteration sees only one constraint set. Csiszár's 1975 paper proves that cyclic I-projections converge to the joint I-projection when the underlying set is finite and the constraint sets are linear. This mission formalizes that result together with the geometric statements needed to identify its limit.
Let be a measurable space. A probability distribution (PD) is a probability measure on it. For PDs and , the I-divergence is the Kullback–Leibler divergence: integrate the logarithm of the density of relative to against , with value when is not absolutely continuous with respect to or the integral diverges. It takes values in and vanishes exactly when . The logarithmic conventions are and (Csiszár 1975, (1.1)–(1.3)).
Given a PD and a set of PDs that contains at least one with finite , an I-projection of onto minimizes over and itself has finite divergence. The variation distance is the distance between the densities of two PDs relative to a common dominating measure. A set of PDs is linear here when every real affine combination of two members that is still a PD also belongs to the set. This includes distributions satisfying fixed linear moment constraints (Csiszár 1975, pp. 147 and 150–151).
For the goal, is finite. Choose linear sets , and write . Beginning with , let be the I-projection of onto when and . The common feasible set is assumed nonempty and contains a PD absolutely continuous with respect to . These assumptions ensure that the intended finite-divergence projection problem is present (Csiszár 1975, Theorem 3.2).
The goal is the convergence statement of Theorem 3.2:
The goal also asserts existence of the cyclic sequence. On finite , convergence of every point mass is equivalent to convergence in variation distance. The target fixes no rate. Its milestones include existence on variation-closed convex sets (Theorem 2.1), the identity (2.6) and the tangent-hyperplane Lemma 2.1, the Pythagorean characterization and transitivity of I-projections (Theorems 2.2–2.3), the density form under general linear constraints (Theorem 3.1) and the finite-moment exponential-density characterization (Corollary 3.1(A)), and the finite-space identity used in Theorem 3.2's proof. The two displayed identities in that proof are also targets:
They specify the divergence relationships that the eventual convergence theorem must preserve (Csiszár 1975, (3.14)–(3.15)).
The theorem justifies enforcing finitely many linear distribution constraints one at a time while still obtaining the same I-projection as a simultaneous minimization. It gives a precise limit for the iterative proportional fitting procedure discussed by Csiszár, including cases in which the initial distribution has zero probabilities; strict positivity of is not required (Csiszár 1975, p. 155). The accompanying identities make the relation between a partial iterate and the final solution explicit. The result was proved in 1975. The work here is to provide machine-checked proofs of that known result and its supporting geometry, while keeping the source's extended-value and boundary conventions visible.
Successive projections minimize divergence over different sets. Minimization for one set by itself does not identify the minimizer over their intersection, and ordinary metric projection facts do not directly apply because I-divergence is asymmetric and can be infinite. The paper's statements need to handle zero densities and feasible distributions at infinite divergence without turning extended-real expressions into default values. On the finite space, convergence of a subsequence is available, but the formal claim must still identify every possible limit as the joint I-projection. These are the mathematical and representation difficulties faced by a complete proof (Csiszár 1975, §§2–3).
Lean uses Measure X and Mathlib's InformationTheory.klDiv : ℝ≥0∞ for . A projection is a finite-divergence minimizer over the stated feasible set; no real-valued infimum or implicit arbitrary witness replaces it. Variation distance uses the densities relative to , which dominates both PDs and gives the value of (1.6). Variation closure is expressed by sequential convergence in this distance. The integral is represented in extended reals using positive and negative logarithmic parts and ENNReal.log; the theorem hypotheses keep the indeterminate case out. Density equations are -almost everywhere, and a claim that has an -density explicitly includes .
For moment constraints, every integral is accompanied by integrability. Real affine combinations are tested through their values on measurable sets; the candidate combination must be a PD. The goal assumes a finite carrier with measurable singleton sets and . Lean indexes the sets by Fin k from zero, so Qs (n+1) is projected onto the set at n % k; this is the paper's rule (3.13) shifted by one. The goal asserts existence of a recursive sequence before speaking about every such sequence, and the required feasible witness has . These choices rule out an empty cyclic schedule, junk integrals, and a vacuous convergence assertion. Reusable contributions include the variation-distance and I-projection interfaces, their Pythagorean geometry, and the finite-moment density characterization; the mission's main closure remains Theorem 3.2.
Delivering goods from one depot to many customers with a fleet of trucks is the vehicle routing problem. Dantzig and Ramser formulated it in 1959 as the "truck dispatching problem" (Management Sci. 6 (1959), doi:10.1287/mnsc.6.1.80). Five years later Clarke and Wright proposed the savings procedure (Oper. Res. 12 (1964), 568–581, doi:10.1287/opre.12.4.568): start with one truck per customer and repeatedly join two routes where joining saves the most distance, as long as the trucks can still carry the loads. On the twelve-customer example of Dantzig and Ramser it reached 290 units against their 294.
The savings procedure became the standard construction heuristic for vehicle routing. It appears in every textbook treatment of the problem, is the initial solution of many metaheuristics, and is the benchmark against which later construction methods are compared. The paper states the procedure and its bookkeeping (the half matrix, the vector , Table II) but proves nothing about it. That every run of the procedure ends, and ends in a feasible allocation, is left to the reader.
A depot serves customers . The distance between every two points is given, and customer requires a load . Trucks come in capacity classes: trucks of capacity are available, with , and the trucks of the smallest capacity are unlimited, (p. 569).
A run is the ordered list of customers served by one truck, which drives . Its load is . A state of the procedure is a list of runs; its mileage is the total length of its runs. A list of runs is an allocation if every customer lies on exactly one run, and it is feasible if each run can be given a truck of capacity at least its load without using more trucks of any class than are available.
The saving of the cell is . The half matrix records if and are adjacent on a run, and counts how many ends of runs lie at . Table II counts, for each capacity level , the runs with load above and the trucks with capacity above .
The procedure starts with the runs , so for every customer. A cell is admissible if (I) and ; (II) and are on different runs; (III) after replacing those two runs by one run of load , no column of Table II has more runs than trucks. A step links an admissible cell of maximum saving, ties broken arbitrarily, by joining the two runs end to end at and . The procedure stops when no cell is admissible.
Assume symmetric distances, , , and that the initial one-truck-per-customer allocation passes the Table II test. Then every run of the procedure is finite whatever the tie-breaks; at every reachable state from which a link is possible a step exists; and every final state is a feasible allocation satisfying relation (A), for every customer, with
relation (A) at every reachable state, the permanence of links between customers, and
which together give feasibility of every reachable state. Two further milestones: when and the distances are a metric, the optimum equals the traveling salesman optimum (p. 569); and on the data of Table I every run of the procedure ends with total distance 290.
The goal is the specification the paper's procedure meets: it always terminates, never gets stuck, and outputs routes the fleet can actually drive, with the mileage the half-matrix bookkeeping predicts. The equivalence of the Table II test with truck feasibility is the reason the procedure can check capacities by counting columns instead of solving an assignment problem; it is a nested-class instance of Hall's marriage condition and is reusable for any routing or bin-assignment problem with ordered vehicle classes.
None of these statements is formalized anywhere, and the paper does not prove them. The paper makes no claim of optimality ("near-optimal", p. 568, is not quantified), and the mission does not either. A formal model of the procedure as a nondeterministic transition system is a base on which later results about savings heuristics (worst-case ratios, parallel and sequential variants) can be stated.
The obvious argument for termination, "each link removes a run", needs the invariant that every reachable state is a partition of the customers into runs; the procedure manipulates ordered lists and reverses runs, so the invariant must be carried through every step. Feasibility is not preserved by an arbitrary link but only by one that passes condition (III), and turning the column test into an actual assignment of runs to trucks is a matching argument that fails without both and the ordering of the capacities. Because ties are broken arbitrarily, every statement must hold for all runs of a nondeterministic procedure, not for one canonical execution. The worked example requires following every tie-break.
Points are Fin (M+1) with depot 0, and a run's length is SupplyChainTheory.routeCost from the referenced module SupplyChainTheory_vrp. Capacity class i : Fin (n+1) is the paper's ; availabilities are in ℕ∞; loads and capacities are real. A state is a list of runs, each an ordered list of customers; the matrix and the vector are computed from the state. The procedure is a step relation, and every invariant is stated for reachable states. Termination is Acc of the step relation at the initial state.
Choices committed to:
A correctness claim only about final states, without termination and progress, would hold for a procedure with no moves; a step relation with a fixed tie-break would prove less than the paper; invariants for arbitrary states are false; and a mileage identity for an arbitrary partition says nothing about the procedure's output. None of these is the target.
Not formalized: the informal , the shadow-cost reading of p. 571, the decomposition savings (2)–(5) of the general scheme, the load-splitting reduction of pp. 572–573, the Dantzig–Ramser methods, and the empirical comparisons and appendices.
Contributions welcome: proofs of the milestones, in particular the Table II equivalence, which needs a Hall-type argument for nested classes, and a decision procedure for the worked example.