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?
The multi-armed bandit problem asks how to share effort sequentially among several independent projects, each of which evolves only while it is worked on. It models the scheduling of jobs on a single machine, the order in which to explore candidate sites, sequential clinical trials and the allocation of research effort among competing projects. Before 1972 the problem had no general solution: dynamic programming over the joint state of all projects is intractable as soon as there are more than a few of them.
J. C. Gittins and D. M. Jones (1974) announced, and Gittins (1979) set out in full, a solution of a striking form: each project can be assigned a number depending only on its own current state, its dynamic allocation index (DAI, now the Gittins index), and it is optimal to work on a project whose index is largest.
Timeline. Gittins and Jones presented the index result at the European Meeting of Statisticians in 1972 (proceedings 1974). Gittins (1979) gave the general discrete-time formulation, stated the Forwards Induction Theorem and the DAI Theorem without proof, and proved the attainment Lemma of its Section 4. Whittle (1980) gave a dynamic-programming proof through the retirement formulation, Weber (1992) the prevailing-charge interchange argument, and Tsitsiklis (1994) a short inductive proof. Gittins, Glazebrook and Weber (2011) is the standard monograph; Lattimore and Szepesvári (2020, Chapter 35) give a measure-theoretic treatment on general state spaces.
A bandit process is a Markov chain on a measurable state space with transition kernel . Applying the continuation control at process time earns the discounted reward , with , and moves the chain one step; the freezing control leaves the state unchanged and earns nothing. For a stopping time of the chain (possibly infinite) write
The dynamic allocation index of in state is the largest reward per unit of discounted time obtainable by continuing for at least one step:
A simple family of alternative bandit processes consists of bandit processes. At each stage a policy chooses exactly one of them to continue, possibly at random and as a function of the whole past; the others are frozen. A policy is optimal if it attains the supremum of the total expected discounted reward over all policies.
The Lean development uses the published objects markovChainMeasure P x (the chain law), IsPositiveStoppingTime, stoppedRatio P r α τ x (), gittinsIndex P r α x (), MarkovBanditPolicy k S, markovBanditMeasure P π x n (the law of the first stages) and markovBanditDiscountedValue P r α π x (the total expected discounted reward), with written α and written r.
For every policy and initial state vector ,
BanditAlgorithm.gittins_index_theorem, already Proved.The result. The DAI Theorem replaces a dynamic program on the product of state spaces by one-dimensional optimal stopping problems. The "only if" half says more than that the index rule is one optimal policy: it characterizes every optimal policy, so any rule that departs from the index on a set of positive probability loses reward. The Lemma identifies the stopping rule that attains the index, which is how indices are computed in practice, and Corollary 1 is the finite-horizon version on which the paper's numerical algorithm (Section 7) rests.
Formalizing it. The sufficiency half is formalized: BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári Theorem 35.9) is Proved on the platform, together with gittins_index_policy_dominates, gittins_stopping_ratio_le_index and gittins_epsilon_optimal_stopping. The attainment Lemma is Proved only for countable state spaces with bounded rewards (AllocationIndices.optimal_stopping_set, Gittins–Glazebrook–Weber Lemma 2.2), and the necessity half is on no platform item. This mission asks for the Lemma on general standard Borel state spaces with integrable rewards, the finite-horizon Corollary 1, and the full equivalence. The Forwards Induction Theorem of p. 153, which needs superprocesses and forwards induction policies, is outside its scope.
The "only if" direction is the new content, and it does not follow from the sufficiency theorem: knowing that one index policy is optimal says nothing about a policy that sometimes plays a lower-index process. The deviation must be shown to cost a strictly positive amount whenever it happens with positive probability, which requires a strict comparison that survives discounting, ties in the index and infinite stopping times. A second obstacle is measure-theoretic. On a general state space the index is a supremum over uncountably many stopping times, its measurability is not available, and the Lemma's stopping rule is a stopping time only if is measurable; the arguments of the countable case, which treat each state separately, do not transfer.
All objects are the published discounted -armed Markov bandit of Def_GittinsIndex and the stopping-time quantities of Def_AllocationIndices_Index; time is indexed from , stopping times are -valued and adapted to the coordinate filtration, and the index is the real supremum over stopping times . The explicit readings committed to are:
A trivializing formalization is ruled out: the goal is not stated for index policies on every history (which would only restate the referenced theorem), the index is the published supremum over stopping times rather than a one-step reward or a finite-horizon quantity, competitors are not restricted to Markov or deterministic policies, and the Lemma's stopping rule starts at time , so it never stops at once. A one-point state space satisfies all hypotheses together and admits a policy.
Useful infrastructure, reusable beyond this mission: measurability of the Gittins index on standard Borel spaces, a measurable selection of a maximal-index arm, and an interchange argument for -armed Markov bandits on general state spaces. Proofs of any milestone, and of either half of the goal, are welcome.
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.
Markov decision processes are the standard model of sequential decision making under uncertainty in operations research, control and artificial intelligence. Their finite-horizon, discounted and average-cost versions are all solvable in polynomial time, by dynamic programming or linear programming. Papadimitriou and Tsitsiklis (The Complexity of Markov Decision Processes, Math. Oper. Res. 12(3), 1987) asked the next question: can these problems be solved fast in parallel, in polylogarithmic time on polynomially many processors (the class NC)? Their Theorem 1 answers no, unless every polynomial-time problem parallelizes: all three versions are P-complete. The proof is a short reduction from the circuit value problem (CVP), the canonical P-complete problem (Ladner, 1975). This mission formalizes the mathematical heart of that reduction: the constructed process has optimal expected cost zero exactly when the circuit evaluates to true.
The result is the first of a series of five missions on the same paper; the others treat the deterministic special cases (which are in NC) and the partially observed case (which is PSPACE-hard).
A circuit is a finite sequence of triples with . Each is one of the operations false, true, and, or. A triple with is an input; a triple with is a gate, and a gate reads two earlier triples, . The value of an input is its constant; the value of a gate is the Boolean operation applied to the values of triples and . The value of is the value of triple .
A finite Markov decision process has a finite state set , an initial state , and at each state a nonempty finite set of decisions. Taking decision at state at time costs and moves to with probability . A policy chooses a decision for every state and time. For a horizon the expected cost of is
and the optimal expected cost is over all policies.
From a circuit the proof of Theorem 1 builds a stationary process : one state per triple plus an absorbing state . An input state has one decision, moving to , at cost if the input is false and if it is true. An or gate has two free decisions, moving to and moving to . An and gate has one decision, moving to or with probability each. All other costs are zero. The initial state is triple and the horizon is .
In the Lean development these are MDPComplexity.CircuitValue.MDP (with Policy, trajProb, expCost, optCost), Circuit (with val, value, lastIdx) and Circuit.toMDP.
for every circuit with triples (theorem1_reduction). This is the claim "the optimum expected cost is 0 or less iff the value of was true" on p. 445.
The discounted analogue, which the paper asserts in one sentence: for , the optimal expected discounted cost of is at most iff is true (discounted_reduction).
Combined with the log-space computability of from , the goal shows that the finite-horizon Markov decision problem is P-hard, hence not in NC unless P = NC. This is the reason dynamic programming for general Markov decision processes is believed to be inherently sequential, and it frames the contrast drawn in the rest of the paper: deterministic processes are in NC, and partially observed ones are PSPACE-hard. The construction is also stationary, so it shows that even the stationary finite-horizon problem is P-hard, as the paper remarks.
The theorem is proved in the paper, in one paragraph; it is not open. To our knowledge no machine-checked proof of it exists. Formalizing it produces a precise statement of what the reduction proves, a reusable finite-trajectory model of finite-horizon Markov decision processes with time-dependent policies, and a reusable encoding of Boolean circuits and their value.
The informal argument is short, but two points need care. First, the optimum ranges over all time-dependent policies, which form an infinite type; the infimum is attained only because the expected cost depends on finitely many decisions, and this must be established rather than assumed. Second, the passage from "the expected cost is zero" to "the circuit is true" turns a statement about trajectory probabilities into a statement about the recursive value of the circuit, and the and gates (where both successors are reached with positive probability) behave differently from the or gates (where only the chosen successor is reached). Reasoning only along a single path, as for a deterministic process, does not suffice at and gates.
Theorem 1 is a complexity statement: "The Markov Decision Process problem is P-complete in all three cases." Membership in P, the log-space computability of the construction, the notion of P-completeness, and the average-cost case are not part of this mission; Mathlib has no log-space reductions or class P. The mission states the correctness of the reduction, for the exact process of the proof.
Conventions committed to:
Fin k (paper index is Lean index ); via [NeZero k]. The fields of an input are unused (the paper sets them to , not a triple index). Triple need not be a gate.Option (Fin k), with none the state ; decisions are Fin 2 at or gates and Fin 1 elsewhere.A formalization that defines the optimal cost directly as "the cost of the best choice at the or gates", or optimizes only over stationary policies, would make the goal a restatement of the circuit's value; the mission's optimum is over all time-dependent policies of the general model.
Contributions welcome: proofs of the milestones and the goal; lemmas on the trajectory model (marginalization of trajProb, attainment of the infimum for policies that matter only up to time ) that are reusable for any finite-horizon process.
A Markov decision process with finitely many states and decisions, a discount factor and the objective of minimizing expected discounted cost is the basic model of sequential decision making in operations research and reinforcement learning. It is solvable in polynomial time by linear programming. Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked the finer question of whether it can be solved fast in parallel, and showed a sharp split: the general (stochastic) problem is P-complete (their Theorem 1), so it is unlikely to admit a polylogarithmic parallel algorithm, while the deterministic special case, where every transition probability is 0 or 1, is in NC (their Theorem 4).
The deterministic case is a shortest-path problem with a twist. Every policy traces a walk in a graph, and the cost of the walk counts its -th arc with weight . The paper's argument identifies the optimal discounted cost with the cost of a finite combinatorial object, a sigma, and computes it from discounted min-plus matrix products. This mission formalizes that identity.
A deterministic stationary Markov decision process consists of a finite set of states, an initial state , and for each state a finite nonempty set of decisions. Decision costs and leads with certainty to the state . Equivalently, it is a directed graph on with an arc of weight for each decision; parallel arcs and loops are allowed.
A policy chooses a decision for every state and time ; it is stationary if does not depend on . From it produces the states and the discounted cost
The optimal discounted cost is , the infimum over all policies .
A sigma is a walk along decisions whose nodes are distinct and whose last node repeats an earlier one, with : the walk from up to the first repetition of a node. It is a prefix of arcs followed by a cycle of arcs. Its discounted cost is the discounted cost of the infinite walk that follows it and repeats its cycle forever.
In the min-plus semiring (addition is , multiplication is , zero is ), let be the least cost of a decision from to ( if none), let multiply every finite entry by , and let
with the min-plus identity. The entry is the least discounted cost of a -arc walk from to .
For ,
with both minima attained. This is the claim on pp. 446–447 on which Theorem 4 rests. The algebraic expression is the corrected form of the paper's (see Formalization scope).
BertsekasDP.discounted_main_theorem (Proved), and the deterministic case is stated in this mission's model.The identity reduces an optimization over infinite objects, the time-dependent policies, to a minimum over finitely many closed-form expressions in matrix entries. Each is a product of min-plus matrices, and matrix products parallelize well; that is the source of the NC algorithm. The same reduction, with the discounting removed, underlies the minimum-mean-cycle characterization of the average-cost problem (mission II of this series), and the sigma structure reappears in the stationary finite-horizon analysis (mission IV).
On the formalization side, the result has been proved in the paper only as a short paragraph, which cites the existence of stationary optimal policies and leaves the algebra to the reader. Its printed formulas contain index slips (below). A machine-checked version fixes the exact constants. To our knowledge none of these statements has a formal proof. The existence of stationary optimal policies for finite discounted problems is formalized on the platform in Bertsekas's general stochastic setting.
The obvious argument says: an optimal policy may be taken stationary, a stationary deterministic policy produces an eventually periodic path, and an eventually periodic path is a sigma. The first step is the substantial one: the optimum is an infimum over all time-dependent policies , and a non-stationary policy can follow any walk at all, so this step is a statement about the whole dynamic program, not a combinatorial fact about a single walk. The second part of the goal adds a matching argument in the other direction: the expression ranges over arbitrary -arc walks and closed -walks, which need not be simple, so one must check that none of them beats the best sigma, and that the best sigma has and . Finally, the discount factors must be tracked exactly; the printed formulas are off by one power of in two places.
The Lean development lives in the namespace MDPComplexity.Discounted, with one definition file and five theorems. Conventions committed to:
DetMDP S has a finite state type, a nonempty finite decision type at each state (the paper says "a finite set "; nonemptiness is implicit since a policy must choose a decision), a successor map and real costs.optDisc is the infimum over all such policies. Defining it over stationary policies or over sigmas would make the goal true by definition. That shortcut is ruled out, and the stationarity step is part of the content.tsums, which are junk () for non-summable series; every statement that sums costs assumes , under which the series converge absolutely.Tropical (WithTop ℝ), so is ⊤ and the product is Mathlib's matrix product over the tropical semiring.Not formalized: membership in NC, the processor count , the parallel time, and the P-completeness of the general problem. Mathlib has no parallel complexity classes. Only the identity that makes the algorithm correct is a target.
Contributions welcome: proofs of any milestone. A bridge from DetMDP to BertsekasSSPModel (taking decisions as controls and 0/1 transition rows) would let milestone 2 be derived from the platform's proved Proposition 7.3.1. A direct proof of the deterministic case is also welcome. The lasso and walk lemmas are reusable for the other missions of the series.
Online matching describes allocation when requests must be answered as they arrive. A matching decision uses only the edges revealed so far and cannot be revised when later requests appear. In the bipartite setting studied by Karp, U. Vazirani, and V. Vazirani, the arriving vertices are girls and the possible partners are boys. Even when the full graph has a perfect matching, a fixed greedy priority can leave many girls unmatched. The paper introduced RANKING, which randomly chooses the boys' priority order once and then uses that order for every arrival.
The question is quantitative: how many pairs does RANKING guarantee in expectation against a graph and an arrival order chosen before its random ranking? The paper's target is a fraction approaching of the pairs in a perfect matching. Its printed Theorem 1 concerns an auxiliary algorithm called EARLY; the RANKING statement follows the intended chain through Lemmas 3 and 5. The original EARLY analysis has a gap for general upper-triangular matrices, so this mission states the RANKING target and the earlier, unaffected lemmas separately. This distinction matters because an assertion about EARLY would be a different formalization target.
A bipartite graph has a boy side and a girl side , each with vertices. An edge means that boy may be paired with girl . A matching is a collection of edges in which no boy or girl occurs twice. The standing hypothesis for the performance guarantee is that the graph has a perfect matching: some bijection from boys to girls selects an edge for every boy. The graph is otherwise arbitrary.
Girls arrive in a predetermined order. When girl arrives, only her incident edges are revealed. RANKING first chooses a uniformly random permutation of the boys. For each arriving girl, it selects the highest-ranked adjacent boy who is still unmatched, if one exists. Write for the final matching. The expected size is the finite average over all rankings. The guarantee must hold for every graph and every predetermined arrival order; relabeling girls lets the formal statement fix their order to .
The paper also uses a dual rows-arrive view. Boys arrive in an order and choose among eligible girls, whose priority order is fixed. This is the same greedy rule with the sides exchanged. For its triangular reduction, the columns are numbered and column has highest priority. An upper-triangular matrix with unit diagonal is a graph with every edge and with an edge only when . On such a graph, the auxiliary algorithm EARLY declines to match row if column is already covered by EARLY's own matching. For any matching , denotes the indices for which both row and column are covered.
For every , one threshold must work for every size and every graph with a perfect matching:
This is the uniform lower-bound reading of the paper's target. It does not prescribe a finite- additive constant. The mission goal is the RANKING assertion drawn from the paper's Theorem 1 and Lemmas 3 and 5. The six milestones formalize the paper's Lemmas 1–5 and the corollary to Lemma 4, in their source order. They cover the side-exchange identity, arbitrary refusal algorithms, the triangular reduction, the matching-count identity, its expected form, and the pointwise comparison with EARLY.
The guarantee gives a concrete worst-case floor for a simple randomized allocation rule: as the graph size grows, RANKING matches at least an asymptotic fraction of the pairs available in a perfect matching, in expectation. The order is selected before the random permutation, matching the paper's performance measure. The lower bound remains meaningful on sparse graphs and does not rely on a density assumption. The original paper also studies the limit on what any randomized online algorithm can guarantee; that upper-bound result is treated in a separate mission.
A formal development here would provide reusable finite definitions for online greedy matching, arbitrary state-dependent refusal, fixed-order duality, and uniform expectation over permutations. The goal is a theorem statement awaiting a machine-checked proof; compiling the draft declarations verifies their Lean syntax and types, not their truth. The local mission separates the valid early structural statements from later statements whose published EARLY argument does not justify them on general upper-triangular graphs.
The random permutation does not make the fate of different vertices independent. Matching one girl removes a boy who might be essential to a later girl, so a per-arrival probability estimate cannot simply be added across all arrivals. The dual and triangular views capture useful structure, but turning that structure into a uniform bound for every graph is the main obstacle. In particular, reasoning about EARLY as if its matched-column set had the same monotonicity as unrestricted RANKING fails on some upper-triangular matrices. A proof of the goal must establish the RANKING guarantee without treating those later EARLY statements as available facts.
Boys and girls are both Fin n; an adjacency matrix is a relation between them. A published predicate represents a perfect matching as an edge-preserving bijection. The generic greedy run processes arrival times in increasing order and interprets a smaller priority index as higher rank. It makes a new matching decision only from the current matching and the arriving vertex. RANKING's returned edges are consistently ordered as (boy, girl), even though girls arrive. The dual run has rows arriving in an arbitrary permutation and takes column as highest priority in Lean's zero-based numbering. EARLY's refusal test consults the matching constructed by EARLY itself.
All expectations are finite averages over Equiv.Perm (Fin n), scaled by . The formal claim is with a perfect matching, the displayed lower bound. Placing before preserves the worst-case meaning. The perfect-matching condition is essential: the empty graph cannot satisfy a positive linear guarantee. The triangular matrix in Lemma 3 retains every diagonal edge, so a zero matrix cannot witness the reduction. These conventions rule out vacuous versions of the goal and reduction.
The definitions of partial matching, covered vertices, greedy run, RANKING, EARLY, and uniform average are part of the mission. A complete proof may build further finite counting and permutation machinery; such lemmas can be shared beyond this paper. Contributions toward the six milestone statements, the goal, and faithful supporting results are in scope. Lemmas 6–12 and the printed EARLY Theorem 1 are outside this mission because their analysis depends on claims that fail for some matrices allowed by their surrounding assumptions.
A supplier who sells through a single newsvendor retailer faces double marginalization: the retailer bears the whole cost of leftover stock but earns only the retail margin, so under a plain wholesale-price contract he orders less than the integrated supply chain would. The literature reviewed in G. P. Cachon's chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003) shows that buy-back, revenue-sharing and related contracts correct this distortion. Section 6.5 asks what happens when the supplier sells through several retailers who compete for the same customers.
Competition can push in the opposite direction. When customers buy wherever stock is available, a retailer who stocks more also takes demand from his rivals, and he does not count that loss as a cost. This demand-stealing effect pushes the retailers towards over-ordering, which offsets double marginalization. §6.5.1 makes this precise in the proportional allocation model, in which total demand is split among the retailers in proportion to their inventories. The model goes back to the deterministic version of Wang and Gerchak (2001); related allocation models are those of Lippman and McCardle (1997) and Anupindi and Bassok (1999), and Mahajan and van Ryzin (2001) observe the same mitigation of the need for coordinating contracts.
This mission formalizes §6.5.1 of the chapter's January 2003 third draft, pp. 48–53.
There are retailers and one supplier. Total retail demand is random, with distribution function that is differentiable on with density , strictly increasing on , and satisfies . The retail price is and the supplier's unit production cost is , with . Goodwill costs, the salvage value and the retailers' handling cost are zero.
Retailer orders . Write and . Retailer receives the demand . Under a buy-back contract he pays per unit ordered and is refunded per unit left over; is the wholesale-price contract. His expected profit is
Because total sales depend only on the total stock, the integrated chain earns with , and its optimal stock solves the newsvendor equation , Eq. (20). A Nash equilibrium is a profile of orders in which each maximizes over all orders . A contract coordinates the chain when its equilibrium total order is .
Two contract prices appear on p. 52: the wholesale price that induces total stock , and the buy-back wholesale price
For , and solving (20), with : maximizes ; ; the profile in which every retailer orders is the unique Nash equilibrium; and at that equilibrium
The milestones are the section's own claims, in attack order: the newsvendor characterization (20); the inequality ; the closed form of and its strict concavity in the retailer's own order (p. 50); the first-order condition and Eq. (21); the monotonicity and limits of the left side of Eq. (22), giving a unique root for ; the unique, symmetric Nash equilibrium for every ; the increase of the equilibrium total in ; that induces , that , and that the supplier's profit under wholesale pricing has negative slope at ; the coordinating price with for ; and the ratio (p. 53). A companion item states the endpoint , at which the supplier takes all of .
The section answers two questions. First, with competing retailers a plain wholesale-price contract can coordinate the chain and still leave the supplier a positive margin, which a single retailer never allows. Second, that contract is not the supplier's best wholesale price, and it fixes a single division of profit. Buy-back contracts remove both limitations: the family coordinates for every and moves the supplier's share continuously from to all of . The ratio also measures how little a coordinating contract adds when many retailers compete (80% of the optimal profit at ).
The results are proved in the chapter, mostly by short computations, and none of them has been machine-checked. The formalization makes explicit what the page leaves implicit: that no equilibrium has a retailer ordering zero, the limits behind "from 0 to 1", and the density condition behind the strict sign on p. 52. It also produces a reusable proportional-allocation game and a Nash-equilibrium predicate for nonnegative real strategies.
The algebraic identities (the profits at the coordinating contract, the ratio , the derivative at ) are routine once has its closed form. The closed form itself requires computing the expectation with proportional shares and identifying with .
The real obstacle is the uniqueness of the equilibrium. The page argues from first-order conditions, which describe only interior best responses. A complete proof must show that each retailer's profit is strictly concave in his own order, that no retailer orders zero in equilibrium, and that the all-zero profile (where has in a denominator) is not an equilibrium. Strict concavity is the delicate step. The second derivative mixes the density with the term , and concavity has to be established on the closed half-line, including the boundary .
Retailers are indexed by Fin n with (the page's ). The comparison in also allows a single retailer, as the page does. Orders are real numbers , and best responses range over all . The demand law is a probability measure on carried by with finite mean, is its cdf, and is a field with HasDerivAt F (f y) y for . These are the chapter's standing assumptions (p. 7). The condition is needed for (20) to have a solution. The integrated optimum enters each theorem through the hypothesis , which determines it uniquely. Transfers run from the retailers to the supplier.
Added or made explicit relative to the page: in the concavity claim (at the profit is linear); for the strict sign of the supplier's marginal profit; positivity of the total order wherever appears. The page's printed slips (the first-order condition rescaled by , "", "") are corrected in the statements and kept in the milestone quotes.
Ruled out as trivializing: and are the printed formulas, not "the price at which is an equilibrium"; the supplier's profit is computed from the transfers, not as minus the retailers' profits; the equilibrium statement quantifies over all nonnegative deviations, so restricting attention to interior or symmetric profiles is not an option.
A complete development needs interval integrals of a cdf, the fundamental theorem of calculus for , and strict concavity from a strictly decreasing derivative. The proportional-allocation game and the Nash predicate are reusable for the other allocation models of §6.5. No platform item is referenced: the competing-retailer game of Cachon and Lariviere (2005), RevShareCoord.Competing.*, uses deterministic revenue functions and is a different model.
Many combinatorial optimization problems ask for the largest value of a linear objective over discrete feasible solutions. A linear program over the convex hull of those solutions has the same optimum, so one approach is to describe that hull by inequalities. For matching, for example, inequalities support efficient optimization; for other problems, the full family can be very large. A generator of violated inequalities offers a different interface: given a proposed point, it either certifies hull membership or produces one valid inequality that the point violates. Karp and Papadimitriou asked what the existence of an efficient generator implies for the underlying decision problem. Their answer is Theorem 2 of the technical report.
The report appeared as MIT/LCS/TM-154 in 1980 and later in SIAM Journal on Computing in 1982. Its first theorem addresses a small facial description whose inequality family belongs to NP. This mission concerns its second theorem, where the inequalities may be generated on demand in polynomial time. The conclusion is stronger: the decision language itself belongs to P. The report derives an NP-complete consequence as Corollary 2, conditional on the unresolved equality P = NP. The published article gives the later bibliographic record; all numbering here follows the technical report.
A combinatorial optimization problem consists of a binary input language , a nonnegative integer dimension , and a set of feasible vectors for each . The report requires polynomial-time recognition of , of correctly sized pairs , and of feasible pairs . An instance adds an integer objective . Its threshold decision language is
Write for the convex hull of the feasible vectors. A generator receives and a rational vector . It returns “O.K.” exactly when belongs to the hull. Otherwise it returns an integer vector and integer for which while for every . The family contains every triple that occurs as some output. It is a facial description because its inequalities describe the hull exactly. The generator is small if one polynomial bounds every coefficient in every output by in absolute value. Its running time is measured on the full encoded query, including every rational coordinate. These definitions are from §§2 and 4 of the report.
The goal is the report's stated implication:
It allows any c.o.p. satisfying Definition 1, including an empty feasible set or dimension zero. It does not assert P = NP; that consequence needs the additional hypothesis that is NP-complete. The goal is supported by five source claims: the output family is facial; feasibility of system (4) is equivalent to membership in ; Lemma 4 bounds the distance from a rational point to a small hyperplane; its Corollary extends the bound to a real point on a flat; and Lemma 5 controls distance to a flat after one more hyperplane is added. The system (4) target is
The distance targets use the report's parameter and the bounds and , exactly as printed on pp. 12–13.
Theorem 2 turns an efficient separation interface into an efficient test for the threshold language. Consequently, if a c.o.p.'s decision language is NP-complete, a small polynomial-time generator would imply P = NP, as the report's Corollary 2 says. This gives a complexity barrier to a whole class of proposed cutting-plane interfaces, independently of how many inequalities the complete description contains. The result concerns the worst-case running time and output coefficient size; it does not rule out useful generators without those guarantees. Karp and Papadimitriou also point out positive applications to problems already known to be in P.
The mathematical theorem was proved in the report. The mission asks for a machine-checked version of that known result, with explicit interfaces for the generator, coefficient bounds, and the underlying complexity class. The local platform catalog already contains Cook's Turing-machine definitions and a reusable binary-integer encoding; it also contains point-to-hyperplane distance results and a Gram-determinant distance result in other settings. Theorem 2 and these particular source claims are new formalization targets here. The distance and encoding interfaces can serve later missions about separation oracles and bit complexity.
Calling the generator once does not by itself decide whether the objective threshold is attainable: the point supplied to it may be outside the hull, and a single returned inequality says only that this point is excluded. Repeatedly asking at an unchanged point may return the same inequality. The report must also control very small separations, coefficient sizes, and finite precision when an iterative linear-feasibility procedure uses the oracle. Lemmas 4 and 5 quantify the geometric gaps and movement that such a procedure needs. Its Lemmas 2, 3, and 6 address the surrounding perturbation, volume, and iteration arguments; Lemma 6 explicitly relies on another analysis for the finite-precision bound. These are substantive proof obligations even though their statements are not all separate milestones in this proposal. See §4 of the report.
The report's footnote uses for the rationals. Thus , the hull, and system (4) live in . Euclidean distances are evaluated after casting coordinates into ; a hyperplane distance is the quotient , and distance to a flat uses Euclidean infimum distance. The report does not define “affinely independent hyperplanes”; this mission reads it as linear independence of their normals, which ensures a common flat. Small hyperplanes have nonzero normals, avoiding a zero denominator.
The alphabet is . Binary tuple codes contain , an explicit vector dimension, and every integer; a rational coordinate contains its reduced numerator and denominator. The generator's string function must match the mathematical oracle on every valid query and be polynomial time in the complete code length. A malformed string is outside . The source's arbitrary polynomial bound is written for one exponent fixed before all instances. For the bit-length parameter , the printed logarithms of possibly nonpositive and are read as ceiling logarithms of absolute values, with and the printed terms retained. The source's formula remains relevant to the eventual proof of Theorem 2, although no system is a separate draft item here.
Every oracle answer must separate the queried point and remain valid on all of ; these obligations prevent an arbitrary function from satisfying the goal. The c.o.p. structure retains all three polynomial-recognition conditions of Definition 1. The paper's displayed “min” in (3) is inconsistent with its threshold language and surrounding maximization formulas; uses the printed . The typed source's “” in Lemma 4 is read as the already named point .
Contributions can develop the rational-hull equivalence, the two quantitative hyperplane lemmas, the finite-precision ellipsoid procedure underlying Lemma 6, or the perturbation and volume claims. The complexity substrate is Cook's one-tape model of P and NP, and the binary integer codec is the published ProjSchedTW_Complexity_Encoding definition. The geometry lemmas are phrased so that existing Mathlib Euclidean-space results can be reused without changing the source's rational optimization domain.
Polyhedral combinatorics attacks a combinatorial optimization problem by replacing its finite set of feasible solutions with the convex hull of that set and describing the hull by linear inequalities. Once such a description is known, the problem becomes a linear program, and linear programming duality supplies optimality certificates. For matchings, matroids and network flows this programme succeeded completely (Edmonds' matching polytope is the classical example). For the traveling salesman problem, set covering and integer programming, decades of work produced large families of valid and facet-defining inequalities but never a complete list.
R. M. Karp and C. H. Papadimitriou asked whether the failure is accidental. Their answer, in the MIT technical report On linear characterizations of combinatorial optimization problems (MIT/LCS/TM-154, February 1980; journal version SIAM J. Comput. 11 (1982) 620–632), is that for NP-complete problems a usable complete description cannot exist unless NP = co-NP. This mission formalizes the first of their two complexity results, Theorem 1, together with the steps of its proof and its Corollary 1.
A combinatorial optimization problem (c.o.p.) consists of a set of inputs, a function assigning to each input a number of variables , and for each a set of nonnegative integer vectors, the feasible solutions. The three languages , and must be recognizable in polynomial time. An instance is a pair with and , and the decision problem of is
Write for the convex hull of over the rationals. A facial description of is a set of triples , with , and , such that for every and every
It is small if for some polynomial every component of every triple has absolute value at most , so that each coefficient has polynomially many bits. The statement means that the language of the triples of is in NP: membership of a listed inequality has short, checkable proofs.
Theorem 1 converts a question of polyhedral combinatorics into one of complexity theory. Corollary 1 then says that for the traveling salesman problem, Hamiltonian circuit, set covering, integer programming and every other c.o.p. with an NP-complete decision problem, no complete linear description of the hulls has both polynomially sized coefficients and polynomially verifiable membership, unless NP = co-NP. This explains why the search for complete descriptions of such polytopes has not succeeded and why research on them turned to partial descriptions and separation. The companion result of the same paper (Theorem 2, the subject of the second mission in this series) treats separation routines and P instead of facial descriptions and co-NP.
The result itself is proved, by a short argument in the paper. To our knowledge it has no machine-checked proof. Formalizing it requires connecting three things that the platform holds only separately: Cook's Turing-machine classes P, NP and co-NP (published as CookPvsNP_defs), linear programming duality over the rationals (Farkas' lemma is published, e.g. LinearOptimization.farkas_inequality_form_fintype, for real matrices), and polynomial-time arithmetic on binary-encoded rational data, such as solving a nonsingular integer linear system. The last ingredient, a polynomial-time verifier built from a polynomial-time recognizer, is reusable for every co-NP or NP membership proof on the platform.
The mathematical content of Theorem 1 is the duality chain (i)⇔(vi): the "no" answer is certified by inequalities of and a basic dual solution. Two points make the formal proof harder than the paper's page suggests.
First, the duality chain needs care at its edges. When is empty the chain (iii)⇔(vi) can fail, so the verifier must also accept a different certificate (an infeasibility certificate from at most triples), while milestone 4 carries the hypothesis . Pointedness of the hull, which follows from , is what guarantees linearly independent rows.
Second, "Algorithm B clearly runs in polynomial time" hides a complete complexity argument on Cook's one-tape machines: parsing the input, testing and with the recognizers of Definition 1, guessing the matrix within the size bound given by smallness, invoking the NP verifier of times, and solving exactly over with polynomially bounded bit sizes (Cramer's rule bounds the numerators and denominators of ). The certificate must be of length polynomial in the input, which uses the uniform polynomial in the definition of "small". The naive certificate, a single optimal vertex of the hull, does not work: it proves a "yes" answer, not a "no".
All definitions live in the namespace KarpPapadimitriou.Facial. Strings are List Bool; is a set of Fin (n z) → ℤ with nonnegative entries; is convexHull ℚ of its image in Fin (n z) → ℚ, because the paper's "R" denotes the rationals (footnote, p. 3). Tuples are coded over the four-letter alphabet of the published ProjSchedTW_Complexity_Encoding, integers in binary, vectors prefixed by their length so that codes are uniquely decodable. P, NP, co-NP and NP-completeness are the published CookPvsNP_defs; and the triple language of are sets of codes, so strings encoding no triple lie in the complement of , as in Algorithm B's step (i). The three polynomial-time conditions of Definition 1 are fields of the structure COP.
Explicit readings of the paper's loose phrases:
Printed slips: display (3) reads "min" while and the proof maximize; Algorithm B's step (v) reads "" for . Both are formalized in the corrected sense.
A trivializing formalization is ruled out: the goal quantifies over every c.o.p. and every small facial description, with complements taken over all strings, and no hypothesis restricts or beyond Definition 1 and the definitions of p. 4–5. Claim 1 (p. 9), announced without proof, is not part of the mission.
Contributions welcome: proofs of the four milestones (milestone 4 is an exercise in rational LP duality on finite systems), a reusable library of polynomial-time integer and rational arithmetic on Cook's machines, and the closure of NP under polynomial-time reductions across alphabets that Corollary 1 needs.
Online convex optimization is the standard model for learning from a stream of data: in round a learner commits to a point in a convex set , a convex loss is revealed, and the learner pays , where is a fixed regularizer. Subgradient methods for this model use one fixed geometry (usually the Euclidean one) for every coordinate and every direction, regardless of the data. Duchi, Hazan and Singer (JMLR 12 (2011) 2121–2159) introduced ADAGRAD, which adapts the geometry to the observed subgradients. The diagonal version is one of the most widely used optimizers in machine learning and the ancestor of RMSProp and Adam. This mission formalizes the paper's full-matrix version: the proximal term is built from the matrix square root of the accumulated outer products of the subgradients, so the method adapts to correlated directions, not only to individual coordinates.
The analysis extends the regret bounds of primal-dual subgradient methods and regularized dual averaging (Nesterov 2009; Xiao 2010) and of composite mirror descent to proximal functions that change over time, and combines them with trace inequalities for the matrix square root. Concurrent work by McMahan and Streeter (COLT 2010) studied closely related adaptive proximal methods.
Vectors live in with the Euclidean inner product and norm . In round the learner plays and observes a subgradient , that is, for all . The regret against a comparator is
The outer product matrix is , a symmetric positive semidefinite matrix, and is its positive semidefinite square root. With parameters and , ADAGRAD with full matrices (Figure 2 of the paper) sets
starts at , and computes by one of two updates:
The dual (semi)norm of is , where is the pseudo-inverse.
Assume closed and convex, and convex, and minimized over at . For the primal-dual update with , every satisfies
and for the composite mirror descent update with any ,
In the order the proof uses them:
The quantity can be much smaller than the factor in the regret of non-adaptive online gradient descent with a tuned step size: it is small when the subgradients concentrate in a few directions, possibly not aligned with the coordinate axes. The paper's Corollary 11 rewrites it as times the square root of , the gradient term of the best fixed full-matrix proximal function chosen in hindsight. The supporting results have their own uses. Propositions 2 and 3 are the generic regret bounds for adaptive proximal methods. Lemmas 8–10 are trace inequalities for the matrix square root that appear throughout the analysis of second-order online methods.
The results are proved in the paper. To our knowledge none of them has a machine-checked proof. Formalizing them requires the matrix functional calculus (square roots, pseudo-inverses, real powers) in a form usable for inequalities, which Mathlib has only partly: for instance, monotonicity of the square root is in Mathlib for C*-algebras, which covers complex but not real matrices. A complete development gives a verified regret bound for an adaptive full-matrix method together with these matrix inequalities.
The online-learning half (Lemma 16, Propositions 2 and 3) is a convex-analysis argument once the proximal functions are quadratic. The obstacle is the matrix half. The natural approach to Lemma 10 is induction with a scalar inequality applied eigenvalue by eigenvalue. This fails because and do not commute, so their eigenvectors differ. One needs the concavity of on positive semidefinite matrices and its gradient, at points where may be singular. That is where Lemma 8 and the pseudo-inverse enter: the inverse root does not exist, and a limit is needed. The same issue arises in Lemma 9 and in the dual norm when .
Vectors are EuclideanSpace ℝ (Fin d), so ‖·‖ is the Euclidean norm. Matrices are Matrix (Fin d) (Fin d) ℝ, acting on vectors through Matrix.toEuclideanLin. The square root is Mathlib's CFC.sqrt under the Loewner order (MatrixOrder). The pseudo-inverse is the functional calculus of with , and is written as . Mathlib's matrix inverse is used only where the matrix is invertible or the vector is zero. Rounds are 1-based and . The losses and are real-valued convex functions, and the constraint is carried by . Each update's argmin is a predicate (the next iterate lies in and minimizes the objective there), which does not assert existence or uniqueness. A run consists of the rounds of Figure 2, with the subgradient relation imposed in every round. The subgradient relation is the platform's published ShorNonsmooth.AlmostDiff.IsSubgradient.
Restrictions and conventions, each stated in the item that needs it:
A formalization in which the next iterate need not lie in , the comparator ranges outside , is itself or its entrywise square root, or is Mathlib's matrix inverse (which vanishes on singular matrices), states a different theorem and is excluded.
Proofs need the convex-analysis optimality conditions for the two updates, the Loewner-order calculus of CFC.sqrt on real matrices (Lemma 13), concavity and differentiability of , and limits in the functional calculus. The matrix lemmas (13, 14, 8, 9, 10) are reusable outside this paper. Alternative proofs, for instance of Lemma 10 through operator concavity, are welcome.
Policy gradient methods optimize a parameterized policy directly by gradient ascent on its expected discounted return. They underlie most practical reinforcement-learning systems, yet for a long time their convergence was understood only locally: the objective is not concave, and plain gradient ascent can stall on plateaus. The natural policy gradient (NPG) of Kakade (2001) preconditions the gradient by the pseudoinverse of the Fisher information matrix of the policy, so that steps are measured in the geometry of the induced action distributions rather than in parameter space. NPG is the conceptual ancestor of trust-region methods such as TRPO and PPO.
Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 2021) prove that exact NPG with softmax policies converges to the optimal value at rate , with constants that depend on neither the number of states, nor the number of actions beyond , nor any distribution mismatch coefficient. This mission formalizes that result, Theorem 5.3 of the paper, and the lemmas its proof rests on.
Timeline. Kakade (2001) introduced NPG and observed that, for softmax policies, it moves toward the greedy policy. Kakade and Langford (2002) proved the performance difference lemma. Even-Dar, Kakade and Mansour (2009) analyzed experts algorithms in changing MDPs, whose regret argument this proof adapts; Geist, Scherrer and Pietquin (2019) studied regularized policy iteration with related rates. Agarwal et al. (preprint 2019, journal 2021) gave the dimension-free bound formalized here.
A finite discounted MDP consists of finite sets (states) and (actions, nonempty), a transition kernel , rewards and a discount factor . A policy assigns to each state a distribution over actions. Its value is the expected discounted sum of rewards started from ; for a start distribution , . The state–action value is and the advantage is . The discounted state visitation distribution is
An optimal policy has for every policy and every state ; write .
The softmax policy with parameter is . The Fisher information matrix with respect to is
and the NPG update with step size is
where is the Moore–Penrose pseudoinverse and are the quantities of . Following §5.3, every state is assumed reachable from : for each some policy has . The normalizer appears in the lemmas.
For NPG (15) from with any fixed , for all ,
If moreover and , then for every .
The result. Theorem 5.3 is a global, non-asymptotic guarantee for a non-concave policy optimization problem, with no dependence on and no distribution mismatch coefficient: the same analysis does not go through for plain softmax policy gradient, whose rates in the same paper carry such coefficients or are only asymptotic. It explains why Fisher preconditioning helps, and it is the template for the paper's later analysis of NPG with function approximation (§6) and for subsequent work on linear convergence of NPG and on entropy-regularized variants.
Formalizing it. The theorem is proved on paper; no machine-checked proof is known. A formal development needs: a policy-gradient identity for softmax policies, the computation of the Moore–Penrose pseudoinverse of a singular, block-structured Fisher matrix acting on the policy gradient, the performance difference lemma in the unnormalized convention, and a telescoping regret argument with Kullback–Leibler divergences between action distributions. Each of these is reusable: the performance difference lemma and the visitation-distribution calculus serve every result of the paper and much of the reinforcement-learning literature.
The obvious approach, treating NPG as gradient ascent on a smooth objective, fails: is non-concave and its smoothness constant grows with , which would give a rate depending on the state space and on distribution mismatch. The dimension-free rate comes only after the NPG step is rewritten exactly as a multiplicative-weights update on each state's action distribution, and this rewriting is itself delicate. The Fisher matrix is always singular (each state's block annihilates the all-ones vector), the pseudoinverse returns the minimum-norm solution, which is not but differs from it by a state-dependent offset; and the identity holds at a state only if that state carries positive visitation weight, which is why reachability from is assumed. A newcomer's first idea, replacing by "any solution of " or by an ordinary inverse, does not define the algorithm.
Lean conventions (Mathlib, namespace PolicyGradTheory.NPG):
S → A → ℝ (π s a ) satisfying the published IsPolicy; transitions P s a s' ; values, -functions and state occupation probabilities are the published FoundationsML definitions PolicyValue, QFunction, OccupationDist, and optimality is IsOptimalPolicy. is the value of a policy assumed optimal, never a supremum over arbitrary functions.EuclideanSpace ℝ (S × A), so norms are Euclidean and gradient is .VectorSpaceOpt.IsPseudoinverse (minimum-norm least-squares inverse, which on Euclidean space is the Moore–Penrose pseudoinverse); Mathlib has none.The goal does not assume the soft-policy-iteration form, the improvement bound or monotonicity; those are milestones to be proved, and a statement taking any of them as a hypothesis would not be Theorem 5.3. The parameter form "" of Lemma 5.1 is not stated, since the pseudoinverse step differs from it by a state-dependent offset (as the lemma's own proof on p. 70 shows); only the policy form, which is invariant to that offset, is a target.
Contributions welcome: the softmax policy-gradient identity and score-function formula, existence and uniqueness of the minimum-norm least-squares inverse on Euclidean space, Kullback–Leibler identities for finite distributions, and the summability facts behind the visitation distribution.
Many counting problems in probability, combinatorics and statistics ask for the law of the number of occurrences of rare, weakly dependent events: long head runs in coin tossing, matching segments between two DNA sequences, isolated vertices or small subgraphs in a random graph, clusters of points in a scan statistic. Chen's 1975 adaptation of Stein's method gives an explicit error bound for approximating such a count by a Poisson law. Arratia, Goldstein and Gordon (Ann. Probab. 17 (1989) 9–25) recast it in terms of a neighbourhood of dependence for each event. In this form the error bound needs only the first two moments of the indicators whenever each event is independent of the events outside its neighbourhood. The paper's examples (head runs, DNA sequence matching, birthday-type problems) made this form standard in applied probability.
The paper has two main results. Theorem 1 bounds the distance between the law of the total count and a Poisson law; it is essentially contained in Chen (1975). Theorem 2, which the authors describe as new, is a process version. It compares the joint law of all the indicators, that is, where the events occur, with a Poisson process. Theorem 3, a corollary, compares a dependent family of events with an independent family having the same marginal probabilities. This mission formalizes Theorem 2, the finite-dimensional bound it is derived from, the steps of its proof in §6, and Theorem 3.
Let be a probability space and an index set. For let be a Bernoulli random variable, , with
For each fix a set with , the neighbourhood of dependence of . Put and
Roughly, measures the size of the neighbourhoods, the expected number of neighbours of an occurrence, and the dependence between an event and the events outside its neighbourhood. In many applications is independent of , so .
The dependent Bernoulli process is , a random element of . The Poisson process on with intensity is with the mutually independent and Poisson with mean .
Distances are measured in the paper's total variation norm,
which is twice the usual total variation distance.
The bound has no dependence on and no assumption on beyond countability (which the setting forces).
The result. Theorem 2 says that when , , are small, the set of indices at which the dependent events occur is close in law to a Poisson process with the same intensity. The bound covers every event about the locations, not just the total count. It is in the strong total variation norm and needs only moment information when . Theorem 3 turns this into a decoupling statement: a dependent family of rare events is almost indistinguishable from an independent family with the same marginals. The process bound is the form used when the positions of rare events matter, for example in the distribution of the location of the longest match in sequence comparison and in scan statistics.
Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would give a Lean statement and proof of a Chen–Stein bound with explicit constants, for countable index sets and arbitrary dependence. It would also include the coordinatewise Stein operators on and the bounds on their solutions, which are reusable for other multivariate Poisson approximations. A companion mission formalizes Theorem 1, including Lemma 1 (the bounds on the one-variable Stein solution) on which milestone 2 rests.
The total variation distance between two laws on cannot be bounded coordinate by coordinate, because the are dependent. The one-variable Stein equation controls only the law of a single integer-valued statistic. The paper passes through finite-dimensional block sums and replaces the coordinates one at a time. At each replacement the error has to be charged to the terms of indexed by the current block, so that the total over all blocks reproduces without a factor . Two further points need care. First, the bound is the only one available for differences in a coordinate other than the one being replaced; this is why the constants are larger than in Theorem 1. Second, the infinite index set requires a limiting argument from finitely many blocks to the full process.
MarkovChainCLT.tvDist (supremum over measurable sets of ). Dropping the factor would make the goal twice as strong and false in general.tsums, equal to the true sums almost surely. A partition is a surjection (Fin d), so Lean's coordinate 0 is the paper's coordinate .Needed infrastructure: product measures and independence on , Poisson laws (Mathlib's poissonMeasure), conditional expectation, and a one-variable Stein bound (Lemma 1). Contributions of proofs of any milestone, of the general step of §6, and of the one-dimensional Lemma 1 are welcome.
Counts of rare events often look Poisson even when the events are dependent. For example, a local pattern in a random graph can overlap another copy of the pattern, so the corresponding occurrence indicators are not independent. The useful question is quantitative: how far is the distribution of the total count from a Poisson distribution with the same mean? Arratia, Goldstein and Gordon give a bound in terms of three quantities that can be estimated from neighbourhoods of dependence. Their 1989 paper applies the Chen–Stein method to the count and then to the full point process. This mission concerns the count bound, Theorem 1.
The authors explain that the result is essentially contained in Chen’s earlier work, while their one-variable proof prepares the process result in Theorem 2. The bound remains useful as a precise statement of the dependence conditions under which the Poisson approximation works. The process theorem belongs to the companion mission.
Let index Bernoulli indicators , each taking values in on a probability space with law . Write , and let
For each , choose a dependence neighbourhood containing . The neighbourhoods need not be symmetric, and the theorem imposes no independence condition: dependence on indicators outside is measured directly. Define and
The remaining quantities use conditional expectation. Let , and let be the sigma algebra generated by all outside . Put
Conditioning on the count retains less information than conditioning on all far indicators, so . Let have the Poisson law with mean . The paper defines as twice the usual supremum over events: .
The goal is the complete four-clause statement of Theorem 1, including its strict final inequality:
The intermediate targets are the Stein-operator inverse identity, the bound on a telescoping term, display (11) relating the approximation error to , and the two clauses of Lemma 1. The goal keeps the coefficients and both forms of fixed, as the paper states them.
The result reduces a distributional approximation question to local sums of probabilities and conditional-dependence errors. When , and are small, the entire law of the count is close to its Poisson comparison law, and the probability of no occurrence has its own sharper bound. The latter is useful whenever a model asks whether at least one rare event occurs. The result applies without demanding exact independence outside the chosen neighbourhoods; the residual dependence appears in .
The paper proves these results. The formalization task is to give the known estimates machine-checked statements and proofs with the constants and probability conventions exposed. Mathlib supplies the Poisson measure and conditional expectation, while the mission adds the paper-specific neighbourhood sums and Stein operators. The formalized theorem can be reused for count approximations in other dependent-indicator models once those models supply bounds on the three error quantities. No machine-checked proof is claimed here: the theorem items are proposed targets with sorry bodies.
A first approximation based only on misses overlapping event pairs. Bounding pair dependence through alone also misses dependence between one indicator and the aggregate of far indicators. The authors' third term measures that remaining effect by conditional expectation. The proof must control the Stein solution uniformly while preserving its precise constants; replacing that control with a qualitative bound would not recover Theorem 1. In the countably infinite setting, the sums and conditional expectations also require careful handling of convergence and measurability. The proof of Lemma 1 is attributed in the paper to Barbour and Eagleson; it is a substantive target here rather than an assumed bound.
The Lean index type is countable. Under the paper's assumptions and , only countably many indices can exist, so this representation retains the stated probabilistic setting. Indicators are measurable natural-number-valued functions with values at most one. The parameter is a positive real equipped with the exact HasSum statement for the probabilities. The Poisson law is Mathlib's poissonMeasure at converted to a nonnegative real parameter.
The sums defining use extended nonnegative reals, so divergence becomes rather than the real tsum default zero. The random counts and use natural-number tsum; their divergent-input default can occur only on a null set under the finite-mean hypotheses and therefore does not change their laws. Measurability of these counts follows from countability and measurability of each indicator. The far-field sigma algebra is generated by the measurable indicators, and the formalization checks that it lies below the ambient sigma algebra, avoiding a default-zero conditional expectation. The paper's total variation norm is exactly 2 * MarkovChainCLT.tvDist, with the factor two retained.
The source writes a strict final inequality without discussing infinite error sums. The Lean statement conditions that single strict clause on ; otherwise both sides can be infinite and strict comparison is false. The other three clauses allow infinite bounds, as the source does. Lemma 1 fixes the Stein inverse at zero exactly as the paper chooses and uses explicit pointwise sup-norm bounds over all nonnegative integers. Display (11) allows , a strengthening of the displayed case. These choices rule out loss of the norm's factor two, disappearing divergent sums, default-zero mapped measures or conditional expectations, and an unannounced independence assumption.
Online marketplaces, ad exchanges and real-estate platforms sell items that are each described by a vector of features and are rarely seen twice. A seller who prices such items cannot learn a demand curve item by item. It must learn how features map to values, while pricing, from accept/reject feedback alone. Cohen, Lobel and Paes Leme (Management Science, 2020; SSRN 2737045) model this as feature-based dynamic pricing with adversarial features and a linear valuation. They show that a direct multi-dimensional binary search (PolytopePricing) can have regret exponential in the dimension (their Theorem 1). Their EllipsoidPricing algorithm, a pricing variant of Khachiyan's ellipsoid method (Khachiyan 1979), has worst-case regret quadratic in the dimension and logarithmic in the horizon (their Theorem 2). This mission formalizes Theorem 2 and the chain of lemmas behind it.
Fix a dimension , a radius and a horizon . Nature picks an unknown parameter with Euclidean norm . In each period a product arrives with a feature vector , , and market value . The seller sees , posts a price , and a sale occurs iff , earning . The regret (Eq. (1)) is
and the worst-case regret of a policy is its maximum over and over nature's (possibly adaptive) choice of features.
An ellipsoid with center and positive definite shape matrix is . EllipsoidPricing with parameter keeps an ellipsoid , starting from the ball . In period it computes
the minimum and maximum of over .
Write for the smallest eigenvalue of a symmetric matrix .
There is a universal constant such that for all , , , and , EllipsoidPricing run with satisfies
This is the paper's claim, with no constant fixed.
The result. Theorem 2 shows that contextual posted-price learning with adversarial features costs only polynomially many "probing" sales in the dimension. A direct cutting-plane search over the polytope of consistent parameters (PolytopePricing) cannot do this: its worst-case regret is exponential in (Theorem 1). The ellipsoid analysis via the smallest eigenvalue (Lemmas 2–4) is reused in the paper's noisy-valuation extension (ShallowPricing, §6) and in later work on contextual pricing and contextual search.
Formalizing it. No part of the paper is machine-checked. The Eq. (4) containment is already proved on the platform (Bertsimas–Tsitsiklis Theorem 8.1). The volume factor there is , weaker than the used here. The eigenvalue lemmas on rank-one perturbations (Lemmas 2–4) are new to the platform and reusable for any analysis of ellipsoid-type updates. A formal proof of the goal would also settle a gap in the printed proof, noted under the formalization scope.
The obvious argument is the textbook ellipsoid bound: volume shrinks by per exploration, so exploration must stop. This fails because the ellipsoid need not become small in every direction. The volume can go to zero while one axis stays long, and then a feature along that axis keeps triggering exploration. The paper replaces the volume argument by a lower bound on the smallest eigenvalue, which needs a sign analysis of the characteristic polynomial of a rank-one perturbation (Lemmas 2–4) together with the exploration test . The constant in Lemma 4 is chosen to make a specific inequality hold for every .
The regret bound needs, in addition, a per-round bound for exploration periods. The printed proof (p. 16) uses "the trivial bound of regret per round". That bound is not immediate when an exploration price is accepted, since the center can leave and the round's regret is then only bounded by . This is why the goal is the -form with an unspecified universal constant rather than the proof's explicit inequality.
Fin d → ℝ; is the dot product θ ⬝ᵥ x. Both norms are Euclidean, encoded as and ; Mathlib's ‖·‖ on Fin d → ℝ is the sup norm and is never used. Ellipsoids, the ball, and the update (4) are the published LinearOptimization.ellipsoid, ellipsoidBall, ellipsoidUpdateCenter and ellipsoidUpdateMatrix.Fin d → ℝ in . is as printed, not Mathlib's charpoly.