Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A decision maker choosing a random outcome (a portfolio return, a policy's cost savings, a schedule's throughput) often has a reference outcome , the result of a benchmark policy, and wants the new outcome to be preferable to it for every risk-averse decision maker, not just on average. Expected-utility theory (von Neumann and Morgenstern) makes this precise: is preferred to by every decision maker with a concave nondecreasing utility function exactly when dominates in the second order, . Requiring as a constraint in an optimization problem avoids having to elicit any particular utility function, which is rarely possible in practice and impossible when several decision makers must agree.
Dentcheva and Ruszczyński (preprint 2002, published in SIAM J. Optim. 14(2), 2003) introduced optimization problems with stochastic dominance constraints and developed their optimality and duality theory. The central finding is that the Lagrange multiplier of a second-order dominance constraint is itself a concave nondecreasing utility function: the optimal solution maximizes the objective plus an expected utility, for a utility function implied by the problem. This interpretation underlies the later literature on dominance-constrained portfolio optimization, risk-averse stochastic programming, and the dual (quantile) theory of stochastic orders.
Let be a probability space and the space of integrable random variables with its norm topology. For the distribution function is and the second-order shortfall function is
Changing the order of integration gives (2.6), where . The relation means for all , and .
The problem data are a reference outcome , a convex closed set , a functional that is concave and continuous on , and an interval . The paper studies the relaxation in which dominance is enforced on :
The uniform dominance condition (Definition 4.1) asks for some with .
The multiplier class consists of the functions that are concave and nondecreasing, vanish on , and are affine on : for , with a constant . The Lagrangian is
Assume the uniform dominance condition. If is an optimal solution of (3.1)–(3.3), there is with
Conversely, if for some a maximizer of satisfies (3.2) and (4.3), then is optimal for (3.1)–(3.3).
The milestones follow the paper's proof. They are: finiteness of for ; the identity (2.6), already proved on the platform; Proposition 2.3 (convexity and closedness of , and its recession cone); the concavity of the constraint operator with respect to the cone of nonnegative functions; the existence of a nonnegative measure multiplier on satisfying (4.5)–(4.6); the facts that the function (), () of a nonnegative measure lies in and that every is for exactly one ; the key identity
and the weak-duality step: (3.2) implies for every .
With , the dual problem has a solution, its value equals the primal optimal value, and its solutions are exactly the satisfying (4.2)–(4.3).
Theorem 4.2 turns an infinite family of constraints, one for each , into a single scalar trade-off: at the optimum, the decision maker behaves as an expected-utility maximizer for an implicit utility , and the dominance constraint is active exactly in the sense . Theorem 5.1 makes the space of dual variables, which is the starting point of dual decomposition and cutting-plane methods for dominance-constrained problems and of their extensions to several constraints and to higher orders (Sections 6–7 of the paper, not part of this mission).
All results are proved in the paper. Apart from the identity (2.6), which is proved on the platform, none of them is formalized as far as the platform records show. A machine-checked development would provide, on top of the paper, a rigorous treatment of the measure–utility correspondence that the paper obtains from a textbook theorem "after an obvious adaptation", and a careful account of the multiplier class itself (see the scope section on the constant ). The definitions of and of the identity (2.6) are shared with the platform's missions on Dual Stochastic Dominance and Related Mean-Risk Models (Ogryczak and Ruszczyński, 2002).
The necessity half needs a Lagrange multiplier for a constraint taking values in the infinite-dimensional space ; finite-dimensional convex duality does not apply, and the multiplier first appears as a nonnegative measure on , an element of the dual of . A Slater-type point is required: without the uniform dominance condition the multiplier may not exist. This is why the dominance relation, which the paper first poses on all of , is relaxed to a bounded interval : for a reference outcome with a smallest value , , so no can dominate strictly near .
The second obstacle is the translation of that measure into a utility function. The identity (4.9) requires an interchange of integrals over and an integration by parts against the distribution function of an arbitrary integrable , followed by a limit in which the integrability of controls the linear growth of at . The converse direction needs every to be represented by a unique measure, through the left derivative of a concave function.
Outcomes are elements of Mathlib's space Ω →₁[P] ℝ over a probability measure P, coerced to functions inside integrals; no statement is pointwise in . is the published definition DualSSD.Shared.secondPerformance, a Bochner integral of over . The problem data form a structure whose fields include every standing assumption of the paper: convex and closed, concave and continuous on . The constraint (3.2) is stated in its printed expectation form, while Definition 4.1 and the proof objects use , as printed; their equality is (2.6).
Committed conventions:
A trivializing formalization is ruled out: a junk-valued expectation (a Bochner integral of a non-integrable function, which Lean sets to ) cannot occur for , and its integrability is a milestone. Dropping the concavity of or the convexity of would make the necessity half false, so these assumptions are fields of the problem data.
Infrastructure a complete development needs: convex duality for cone constraints in (or a direct separation argument in ), the Riesz representation of nonnegative functionals on , Fubini and integration by parts for Stieltjes measures, and the measure of a left-continuous monotone function. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The extensions to several dominance constraints and to higher-order dominance are not included.
In online convex optimization a decision maker picks points in a convex set , and after each choice pays for a convex cost function chosen in advance by an adversary. Performance is measured by regret: the total cost paid minus the cost of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that projected gradient descent has regret when the whole function , or at least its gradient at , is revealed after each round.
In many applications only the number is observed: a seller sets a price and sees revenue, a router picks a path and sees its delay, an advertiser places a bid and sees the cost. This is the bandit setting. Flaxman, Kalai and McMahan (arXiv:cs/0408007, SODA 2005) gave the first simple algorithm for bandit convex optimization against an oblivious adversary with general bounded convex costs: a randomized gradient descent that estimates the gradient from a single function value, with expected regret . The same one-point gradient estimate is the starting point of later work on bandit convex optimization and on zeroth-order (derivative-free) stochastic optimization; see, e.g., Bubeck and Cesa-Bianchi's survey (arXiv:1204.5721, Ch. 6) and Hazan's textbook (arXiv:1909.05207, Ch. 6).
Timeline. Zinkevich (2003): regret with full gradient feedback. Kleinberg (NIPS 2004), independently: bandit regret for Lipschitz costs by a different reduction. Flaxman, Kalai, McMahan (2004/2005): for bounded convex costs and for Lipschitz costs, with one function value per round. Later work (Bubeck, Lee, Eldan 2017 and others) reached with more complex algorithms.
Let and be the closed unit ball and the unit sphere, . The feasible set is closed and convex with
The costs are fixed before play (an oblivious adversary); each is convex on with for , where . For , is the nearest point of to .
The bandit gradient descent algorithm (Figure 1 of the paper) keeps an iterate with . At period it draws a unit vector uniformly from , independently of the past, plays
observes only , and updates
The smoothed cost is with uniform on . The expected regret after rounds is
For every , with , and ,
The paper prints the constant . Its own last step bounds the regret by with , , , and with the stated and this equals . The goal states the bound the proof establishes.
The tuning identity (p. 9): at , , for .
Theorem 2 (p. 9). If each is -Lipschitz on , then with , , , and large enough that ,
The theorem shows that bandit feedback costs only a polynomial factor in regret for arbitrary bounded convex costs, with an algorithm that is gradient descent plus one random perturbation per round. Lemma 1 is the general tool behind it: an unbiased estimate of the gradient of a smoothed function from one function value. It is reused across zeroth-order optimization, bandit learning and stochastic approximation. Lemma 2 is a self-contained regret bound for projected gradient descent with noisy gradients, the shape in which Zinkevich's analysis is most often applied.
The results are proved in the paper and are standard. To the platform's knowledge none of them has a machine-checked proof. Related statements from Bubeck and Cesa-Bianchi's survey, for differentiable Lipschitz losses, are open on the platform, and two earlier formalizations of the textbook versions were disproved because of missing regularity or independence hypotheses. Formalizing this mission produces a checked one-point gradient identity for continuous (not differentiable) functions on the sphere, a measure-theoretic regret bound for stochastic projected gradient descent, and the corrected constant of Theorem 1.
The bandit algorithm itself is simple; the difficulty sits in Lemma 1 and in the measure theory around it. The paper derives Lemma 1 from Stokes' theorem, , and the ratio of the volume to the surface area of a ball. Mathlib has neither this divergence identity on balls in nor the explicit link between its spherical measure and the surface integral needed here. The identity must hold for functions that are merely continuous near the ball, since convex costs need not be differentiable.
The obvious first idea, differentiating under the integral sign in , fails because is not differentiable. The second obvious idea, applying Lemma 1 to as given, fails at the boundary of , where is unconstrained. Lemma 2's conditional expectation requires that the direction be independent of the iterate , and the integrability and measurability of the played points come from continuity of convex functions in the interior of .
Points are EuclideanSpace ℝ (Fin d) with , and rounds are numbered . The costs are functions on , and no statement assumes anything about them outside : no global convexity, continuity, differentiability or Lipschitz bound. The standing model is part of the goal's hypotheses: is convex with , the costs are convex on with values in there, and . Additions and conventions:
uniformSphere d). Uniform marginals alone are not enough.IsBGDRun) required for every outcome. Projection uses the published predicate IsNearestPoint, and regret the published pseudoRegret, whose minimum is an infimum over the subtype; it is attained in every use here.A formalization that assumed integrability of the costs along the run, assumed differentiable or globally Lipschitz costs, dropped the independence of the directions, or stated through Mathlib's gradient (which is off differentiability) would trivialize or change the result. All of these are ruled out.
Needed infrastructure: the divergence identity for the ball average (Lemma 1), conditional expectation given for vector-valued variables, continuity of convex functions on the interior of a convex set, and nearest-point projection onto closed convex sets. The first two are reusable well beyond this mission. Contributions toward Lemma 1 in particular are welcome.
An optimization model often needs a probability distribution for an uncertain cost or demand, while a practitioner has only a finite sample from that distribution. Replacing the distribution by the empirical one can hide uncertainty in its estimated mean and covariance. Delage and Ye use a finite-sample confidence region for these two moments to justify a distributional ambiguity set in data-driven stochastic programming Delage and Ye, 2010. The present mission concerns the confidence region itself: it asks how far the population moments can be from the sample estimates when the normalized random vector has bounded support.
The source for every theorem index and page number here is the authors' draft dated 20 February 2008, not an independently checked pagination of the published article. Its §4 starts from independent observations and Assumption 4, then obtains a sample-mean bound, a covariance bound around the known mean, and finally the joint bound for estimates computed entirely from the sample.
Let have distribution , mean , and covariance . Assume is positive definite. For independent observations , the empirical mean and empirical covariance in this section are
The divisor is , including for the covariance; the paper's earlier discussion of an unbiased estimator with divisor does not govern §4. When the true mean is known, write . Matrix order means is positive semidefinite. The squared Mahalanobis distance of a vector is .
Assumption 4 bounds the normalized observations: for some , with probability one. Equivalently, lies almost surely in a Euclidean ball of radius ; it has mean zero and covariance . The sample law is , the product measure of identical copies. These choices make the probability in each target an assertion about genuinely independent observations.
For , set
Theorem 2 is the goal. Write and , and assume . The target is the simultaneous event
with probability at least . The last denominator is a correction: printed (12c) says , while the authors' union-bound display on draft p. 13 says . The printed version fails, for example, for symmetric observations, whose sample covariance is and for which its claimed lower bound would require an implausibly large sample-mean square. The proof's displayed bound gives the stated draft pp. 13–14.
Lemma 2 bounds the normalized sample mean. Corollary 1 turns it into the Mahalanobis bound for . Lemma 3 gives a two-sided matrix bound for ; Corollary 2 transfers that bound to . A separate theorem item states the centring identity . The final milestone is the rank-one matrix inequality used in Theorem 2's proof. Their statements follow the draft's §4.1–4.2.
The joint region places both true moments inside explicit data-dependent matrix inequalities at a chosen confidence level. That is the statistical input for the paper's later moment-based distributional uncertainty sets. The result is known in the source; this mission asks for machine-checked proofs of its corrected statement and its supporting concentration and matrix results. The Lean items are currently open theorem statements, so a successful draft compilation does not constitute formal verification of the inequalities.
Related platform results include a proved two-sided constant-bound McDiarmid inequality (UnderstandingML.mcdiarmid_inequality_pi) and an open per-coordinate upper-tail version (StabGen.Uniform.mcdiarmid_inequality). Neither is identical to the cited Theorem 1 of this draft, so the milestone list starts with the paper's Lemma 2 and does not restate Theorem 1.
The known-mean covariance estimate is a sum of outer products of normalized observations. Controlling its largest and smallest eigenvalues together requires concentration of a matrix-valued statistic, rather than a separate scalar bound for each entry. Once the true mean is replaced by , the covariance changes by a rank-one matrix; the mean bound must control that correction in Loewner order. A direct replacement of by therefore does not preserve both sides of Corollary 2 automatically.
Vectors are Fin m → ℝ, and matrices are real Fin m × Fin m matrices. The Euclidean squared length is a dot product; Lean's generic norm on functions is a supremum norm and is not used for it. The Loewner order is (B - A).PosSemidef. The distribution has a probability measure and coordinatewise finite moments, so its real-valued mean and covariance integrals are well defined. The true covariance is positive definite, reflecting the section's nonsingularity assumption. Samples have the product law . The chapter's normalized case records zero mean, identity covariance, and the almost-sure ball bound.
Every statistical result assumes ; the logarithms and confidence levels are then in their intended domain. Positive rules out division by zero in empirical averages. Lemma 3 carries the paper's explicit sample-size threshold, and the goal reads “ large enough” as , which keeps the upper covariance denominator positive. The expression under the other square root is nonnegative in every satisfiable positive-dimensional normalized setting, because . It is not an added assumption. The probability conclusions use , which is what the paper's proofs show despite the phrase “greater than.”
The goal assumes the source's distributional and support conditions, not the probability conclusions of its supporting corollaries. This prevents a vacuous route that merely postulates the desired confidence event. A complete proof will need reusable product-measure concentration facts, moment and matrix algebra, and a positive-definite quadratic-form bridge. Contributions to those components and to each milestone are in scope. Corollary 3's data-derived radius is excluded because the draft's conditioning argument does not establish its claimed confidence level. Corollary 4 as a probability statement, Theorem 3, and Corollary 5 depend on it; Remark 2 concerns a separate Gaussian eigenvalue density.
A controlled Markov process (CMP), or Markov decision process, models a system that moves randomly between states while a controller chooses actions that influence both the cost incurred and the next state. When the planning horizon is long and no discounting is natural (queueing control, inventory, communication networks, maintenance), the criterion of interest is the long-run average cost. Average-cost problems are harder than discounted ones: the dynamic programming operator is no longer a contraction, and an optimal policy need not exist without structure.
The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organizes the theory by state space. For Borel state spaces and bounded costs, §6.1 follows Dynkin and Yushkevich and works with canonical triplets: a pair of bounded functions and a policy that make the policy optimal for every finite horizon with a fixed terminal cost. Theorem 6.3 is the statement that explains why this notion is the right one: a canonical triplet solves the average-cost problem.
Timeline. The notion of a canonical policy was introduced by Yushkevich (1973) and developed in Dynkin and Yushkevich's Controlled Markov Processes (1979, Chap. 7), which contains the substance of Theorem 6.3 (i)–(iii). Mandl (1974) introduced the discrepancy function that bears his name. The almost-sure statements (v)–(vi) are due to Georgin (1978). Coupled optimality equations for the multichain case go back to Howard (1960).
The model is a five-tuple . The state space and the action space are Borel spaces. For each state , is a nonempty compact set of admissible actions, and is measurable. is a transition kernel and a measurable one-stage cost, nonnegative on .
A policy chooses the action at time at random from a kernel that may depend on the whole history and charges only . The class of all such policies is . Each policy and initial state determine a law of the state–action process , with expectation .
For a horizon and a terminal cost ,
The average cost is and the optimal average cost is . The span of a bounded function is .
With the bounded measurable functions, a triplet with and is canonical if
A policy is strong average optimal if
Let be a canonical triplet and let be bounded on . Then for each :
The proof's milestones are: ; the decomposition ; part (i) on its own; and .
If is constant and is Mandl's discrepancy function, then for every and ,
and the running average converges to almost surely if and only if almost surely. Moreover is sample path average cost optimal. The intermediate milestones are on , the almost-sure limit under every policy, and almost surely under .
The result. Theorem 6.3 reduces the average-cost problem on a general Borel space to finding a canonical triplet. Once one is found, is the optimal average cost from every initial state, possibly state-dependent as in multichain models, and the canonical policy is optimal in a strong sense: its worst-case long-run performance is no worse than the best-case long-run performance of any competitor, at every finite horizon up to the additive constant . With constant , optimality also holds path by path. The rest of §6 of the survey looks for conditions on and that produce a canonical triplet, and those results rely on this theorem.
Formalizing it. The result is classical and proved; it has no machine-checked proof that we know of. Formalization requires measure-theoretic infrastructure for history-dependent policies on Borel spaces (Ionescu-Tulcea path measures, finite-horizon costs, infima over all admissible policies) together with a strong law for bounded martingale differences for parts (v)–(vi). Both are reusable for any average-cost result on general state spaces.
Parts (i)–(iii) are short on paper; the work is in making every quantity genuine. The infimum ranges over a class of kernels, and turning (6.4) into a usable inequality needs the family bounded below. The decomposition of needs integrability, which comes from the almost-sure confinement of the trajectory to , a consequence of admissibility under the path measure. Parts (v)–(vi) need the conditional expectation identity from the Markov structure of the path measure, and a martingale strong law. The tempting shortcut of restricting to stationary or Markov policies is not available: and every competitor are arbitrary history-dependent randomized policies.
Kernel.trajMeasure. is a Bochner integral and a real infimum; every theorem assumes bounded on , which makes both genuine.EReal, so no limit superior or inferior is a junk value. Part (iii) is the two equalities and .Contributions welcome: a.s. confinement of trajectories to , integrability lemmas for , the Markov property of trajMeasure in the form above, and a strong law for bounded martingale differences.
A retailer that sells products in several categories, channels or stores has to decide which products to offer in each. Customers substitute: a product left out of the assortment sends some of its demand to other products, and some of it away. The nested logit model (McFadden 1974, 1981) is the standard choice model for this situation. It groups products into nests, so that substitution within a nest differs from substitution across nests. Assortment optimization under this model asks which products to offer in each nest so as to maximize expected revenue.
Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) split the problem into four cases: dissimilarity parameters at most one or unrestricted, and nests that are fully or only partially captured. The problem is polynomially solvable in the first case and NP-hard in the other three. Every approximation guarantee in the paper for the hard cases (Theorems 7, 10, 11, 12) comes from one general framework, set up in §2: a linear program equivalent to the assortment problem, and Theorem 1, which turns a feasibility certificate for that linear program into a performance guarantee. This mission formalizes that framework.
There are nests and products in each nest. Product of nest has revenue and preference weight , and the products in each nest are ordered so that . Nest has a no-purchase weight and a dissimilarity parameter . The weight of choosing no nest at all is . If the assortment is offered in nest , write
A customer picks nest with probability , and then a product of that nest by the multinomial logit model. The expected revenue is
and problem (2) is .
The linear program (3) in the variables minimizes subject to
Given candidate collections of assortments for each nest, the linear program (4) is (3) with the second family of constraints imposed only for in the collection of nest .
Let be an optimal solution of (4), and let solve , problem (5), in every nest. If is feasible for (3) for some , then, with ,
The theorem fixes no candidate collection and no value of . Each later section of the paper instantiates it with its own collection and its own factor, so a formal proof applies to all of them.
Theorem 1 is the common step behind the paper's four approximation guarantees: the factor or of Theorem 7, the factor 2 of Theorem 10, the factor of Theorem 11, and the of Theorem 12. Each of these reduces to checking that a scaled optimum of a small linear program is feasible for (3). With Theorem 1 formalized, those guarantees reduce to inequalities about candidate collections, which are the subject of the sister missions of this series. The upper bound (16) and Proposition 13 give the instance-specific bound that the paper uses to assess its assortments numerically.
The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The formal work adds two things: the statements below are made exact at the degenerate inputs the prose passes over (an empty assortment, ), and a formal proof certifies the framework once for every later instantiation.
The equivalence of (2) and (3) rests on decomposing a maximum over joint assortments into a sum of per-nest maxima, and on reading the fractional objective as a linear constraint. Both steps need care where a denominator can vanish. The binding argument for (4) is a perturbation argument: lowering must keep every constraint satisfiable, which needs a continuity and monotonicity property of the right-hand side in . The obvious one-line reading of Theorem 1, " and ", is correct only once both of these facts are established with their hypotheses. In particular, it is false when (see below). Proposition 13 requires that the supremum over the box be finite, which comes from the boundedness of on .
Nests are a finite type ι and products are Fin n, indexed . An assortment is a finite set of products per nest, and a candidate collection is a set of such finite sets. Powers are real powers, and Lean's gives . is for an arbitrary optimal assortment ; no supremum over assortments is taken. "Optimal solution of (4)" means feasible with minimal , and " solves (5)" means belongs to the collection of nest and maximizes the objective of (5) over it at .
Standing assumptions and pins. These are and ordered revenues, together with , and . The paper allows zero-weight padding products and , but its own conventions fail there. Theorem 1 and the binding milestone add . The page allows , but then Theorem 1 is false: take one nest with , , and candidates . Then and meet every hypothesis with , yet . The equivalence of (2) and (3) and the bound from (16) keep , as the page does, and assume at least one nest and one product: with neither and , every is feasible for (3).
A formalization that assumes the binding equality, the identity , or the inequality in the goal would trivialize it. Those facts appear only as milestones. Likewise, reading "optimal solution of (4)" as mere feasibility would make the goal false rather than easier.
The development needs only finite sums, real powers and elementary order reasoning. Proposition 13 also needs the boundedness of a continuous function on a box and the convexity of a pointwise supremum of affine functions. Welcome contributions include proofs of the milestones, the goal from them, and reusable lemmas on the per-nest decomposition of maxima, which the sister missions of this series use as well.
Many control problems in queueing, inventory and communication systems run indefinitely, and the quantity of interest is the long-run cost per unit time rather than a discounted total. The average cost criterion is harder to analyse than the discounted one: the discounted dynamic programming operator is a contraction, while the average cost problem has no contraction, and on an infinite state space its behaviour depends on the recurrence structure of the controlled chain. The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organises the theory around the average cost optimality equation (ACOE) and the conditions under which it has a solution.
Timeline (as recorded in the survey's §3 and §5). Derman studied the ACOE and characterized optimal stationary policies by its solutions (Derman, On sequential decisions and Markov chains, Management Sci. 1962; Denumerable state Markovian decision processes — average cost criterion, Ann. Math. Statist. 1966). Taylor introduced a vanishing discount argument for a replacement problem (Ann. Math. Statist. 1965). Ross extended it to general countable models, showing that uniformly bounded differential discounted value functions yield a bounded solution of the ACOE (Ann. Math. Statist. 1968, two papers; Introduction to Stochastic Dynamic Programming, 1983). Sennott replaced the uniform bound by one-sided bounds and obtained the average cost optimality inequality (Oper. Res. 1989). The survey presents Ross's result as Theorem 5.2, following the 1983 book; this mission formalizes it.
A controlled Markov process on the countable state space consists of a metric space of actions; for each state a nonempty compact set of admissible actions; a cost ; and transition probabilities . For fixed , the maps and are continuous on .
An admissible policy chooses, at each time , a probability distribution on that may depend on the whole past . The class of all of them is , and is the class of stationary deterministic policies, maps with . Each initial state and policy define a law of the trajectory, with expectation . For a discount factor ,
and , . The differential discounted value function is . A pair , , , solves the ACOE if
In the Lean development these objects are CMP, Policy, StationaryPolicy, pathMeasure, discCost, avgCost, discValue (), optAvg (), hRel () and ACOE.
Assume for all and , and that there is with for all such and . Then there are , a bounded and a sequence , , with
The goal does not assert that is the optimal average cost; that follows from Theorem 5.1 and Remark 5.1(a), which are milestones.
Theorem 5.2 is the template of the vanishing discount method. Under its hypothesis the average cost problem has a bounded solution of the ACOE, so (through Theorem 5.1) the optimal average cost is a constant independent of the initial state, it is attained by a stationary deterministic policy, and it is the Abelian limit of the scaled discounted values. Recurrence conditions on the controlled chain, such as uniformly bounded mean return times to a fixed state (Theorem 5.3 of the survey), are verified by checking the hypothesis of Theorem 5.2; the later results of §5 refine its conclusion under weaker hypotheses.
The theorem itself is classical. What this mission adds is a machine-checked statement and, eventually, proof, on a model with history-dependent randomized policies, compact action sets and unbounded costs, together with the supporting verification theorem (Theorem 5.1) and the discounted optimality equation. To our knowledge none of these results has been formalized in Lean; Mathlib has the Ionescu-Tulcea construction of the path measure but no controlled Markov processes.
The obvious argument fixes a sequence , extracts a pointwise convergent subsequence of the bounded functions and of the bounded numbers , and passes to the limit in (5.6). Two steps resist this. First, the limit of a minimum over is not in general the minimum of the limits: the convergence of must be shown to be uniform on the compact set , which requires more than pointwise continuity of each . Second, the subsequential limit could depend on the subsequence, so part (iii), a limit along all , needs an independent identification of , here as the optimal average cost through Theorem 5.1, which in turn needs the comparison with arbitrary history-dependent policies. The discounted optimality equation behind (5.6) also has to be established for unbounded costs, where is not the unique fixed point of .
The state space is ℕ; state 0 is the reference state of . Policies are history-dependent randomized stochastic kernels with the admissibility constraint , and , are infima over all of them. Costs are lower Lebesgue integrals with values in , built from Mathlib's Kernel.trajMeasure. The following choices make implicit hypotheses explicit:
ℕ these are the lower semicontinuous functions bounded below), with convergent series.A formalization in which is an infimum over stationary policies only, in which the ACOE is an inequality or holds for one fixed action, or in which is computed from values through a junk conversion, would trivialize the goal; all three are excluded by the definitions above.
A complete development needs the Ionescu-Tulcea path measure for history-dependent policies, the discounted optimality equation for nonnegative unbounded costs, Scheffé-type uniform convergence on compact action sets, and the martingale identity behind Theorem 5.1. The model file is reusable by the other missions of this series and by any countable-state average cost result; proofs of the milestones are welcome independently of the goal.
In a stochastic multi-armed bandit a player repeatedly chooses one of distributions ("arms") and observes a reward drawn from it; the goal is to collect as much reward as possible, which amounts to pulling suboptimal arms as rarely as possible. Lai and Robbins (1985) showed that any reasonable strategy must pull a suboptimal arm at least times up to horizon , where is a Kullback–Leibler divergence between arm and the best arm, and Burnetas and Katehakis (1996) extended the bound to general models. Strategies matching this rate are called asymptotically optimal.
The popular UCB algorithms of Auer, Cesa-Bianchi and Fischer (2002) use Hoeffding-type confidence bounds and are not asymptotically optimal outside special cases. Cappé, Garivier, Maillard, Munos and Stoltz (Ann. Statist. 41(3), 2013; arXiv:1210.1136) analyse kl-UCB, which replaces the Hoeffding radius by a Kullback–Leibler confidence region, and prove a finite-horizon bound whose leading term is exactly the Lai–Robbins constant. This mission formalizes that result for one-parameter exponential families (Theorem 1), the main-text steps of its proof skeleton, and its two corollaries for bounded rewards.
Timeline: Lai and Robbins (1985) lower bound and asymptotically optimal index policies; Agrawal (1995) sample-mean based index policies; Auer, Cesa-Bianchi and Fischer (2002) finite-time analysis of UCB1; Garivier and Cappé (2011) kl-UCB for bounded rewards; Cappé et al. (2013) the unified analysis formalized here.
A canonical exponential family is given by a dominating measure on and a function , with densities . The parameter set is the natural parameter space , assumed to be an open interval (the family is regular), and is twice differentiable. The mean of is , an increasing function, so is determined by its mean in the open interval . The divergence (11) is
extended by continuity to the closure , possibly with the value .
There are arms with laws and means ; . At each round the player picks an arm based on the past and receives a reward drawn from . is the number of pulls of arm in rounds , and the mean of the rewards obtained from arm so far.
kl-UCB (Algorithm 2) with a nondecreasing exploration function pulls each arm once and then, for , pulls an arm maximizing the index
With for and , for every suboptimal arm and every horizon ,
where and is the derivative in the first argument.
Corollary 1 (p. 17, kl-UCB with the Bernoulli divergence for arbitrary rewards in ) and Corollary 2 (p. 18, UCB with radius ), stated as separate theorems.
Theorem 1 shows that kl-UCB is asymptotically optimal in every regular one-parameter exponential family (Bernoulli, Poisson, Gaussian with known variance, exponential, Gamma with known shape), and it does so with an explicit bound valid at every horizon, not only in the limit. Corollary 2 improves the constants of the classical UCB1 analysis, and Corollary 1 shows that the Bernoulli kl-UCB index is uniformly better than UCB for all bounded rewards.
The result is proved in the paper; its proofs are in the supplemental article (DOI 10.1214/13-AOS1119SUPP, Appendix A), not in the main text. No machine-checked version exists. The platform has a formal analysis of a Bernoulli KL-UCB variant with another exploration function (Lattimore–Szepesvári's Theorem 10.6), which is a different statement. The formalization adds the general exponential-family index, the random-sample-size deviation bound (13) and the full finite-time constant.
The obvious argument bounds by a union bound over the possible values of , which costs a factor and destroys the logarithmic rate. The deviation bound (13) has to control an empirical mean whose number of summands is chosen by the algorithm itself, losing only a factor over the fixed-sample Chernoff bound; this is the step that needs the strategy to be non-anticipating. The second-order terms depend on the curvature of between and , measured by and , and the explicit constants must be tracked through every step. The empirical mean can be an endpoint of (Bernoulli rewards at small sample sizes), where is only defined as a limit.
The rewards are a stack (the -st reward of arm ), mutually independent and i.i.d. per arm, the representation of §2.2; this is the platform's RegretBandits.Stochastic.IsStochasticBandit, and the law of is pinned to . Arms are Fin K. The exponential family is the platform's OptimalBAI.OptProportions.ExpFamily (with , i.e. strict convexity, which the page derives); the natural-parameter-space condition is a separate hypothesis. A run of kl-UCB is a pathwise predicate: rounds pull every arm once and later rounds pull an argmax of the index, ties broken by any rule. The arm choices are measurable and non-anticipating (a measurable function of the arms and rewards already observed). The index (12) is a real supremum over a set containing the empirical mean, so it is never a junk value, and the divergence at an empirical mean on the boundary of is computed in . Statement (13) is made for : at its printed right-hand side is .
A trivializing formalization is ruled out: the run predicate forces both initialization and argmax, the index sets are nonempty and bounded, the reward stack is independent under the probability measure, and the Bernoulli divergence is never evaluated at or .
A complete development needs exponential-family calculus (convex conjugate of , continuity of up to the boundary), Chernoff bounds for exponential families, a peeling/maximal inequality for random sample sizes, and the counting arguments of §3.1. The deviation bound and the counting arguments are reusable for every index policy on the platform.
Sparse graphs with small nontrivial eigenvalues, expanders, are basic objects in combinatorics and theoretical computer science. They are used in error-correcting codes, derandomization, sorting networks, and the analysis of random walks. The Alon–Boppana bound says that a -regular graph on vertices has a nontrivial eigenvalue of absolute value at least (Alon 1986; Nilli 1991). Graphs that reach are Ramanujan graphs.
The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (1988) and Margulis exist only for degrees with prime, and only for very sparse sequences of vertex counts. Constructions with for every degree came from Mohanty, O'Donnell and Paredes (STOC 2020, arXiv:1909.06988), but their graphs also do not have every number of vertices. Alon (arXiv:2003.11673, Combinatorica 41, 2021) asked for near-Ramanujan graphs of every degree and every large size. Theorem 1.3 of that paper answers this up to : for every , every and every large with even there is an explicit -graph with .
A -graph is a -regular simple graph on vertices in which every nontrivial eigenvalue of the adjacency matrix has absolute value at most . The trivial eigenvalue is , with the constant eigenvector . Equivalently, every eigenvalue of with an eigenvector , , satisfies .
Distances are graph distances, and they are between components. The -neighbourhood of a vertex is . The -neighbourhood of an edge is , and is the set of vertices at distance exactly from . A set contains no cycle if the subgraph induced on it is a forest. A ball contains at most one cycle if its induced subgraph has at most as many edges as vertices.
The construction starts from a -regular graph on a vertex set and a set . Write for the set of neighbours of , and let be a perfect matching on . Then is the subgraph induced on , is the graph of matching edges , and .
Let , , . Suppose is an -graph in which the -neighbourhood of every vertex contains at most one cycle, and . Then for every with even and ,
The hypotheses on are what Theorem 3.3 (Mohanty–O'Donnell–Paredes) supplies, and that theorem is not formalized.
Theorem 1.3 shows that the size restrictions of algebraic Ramanujan constructions cost nothing spectrally: up to an arbitrarily small , the Alon–Boppana bound is attained by explicit graphs on every admissible vertex count. The deletion method is local. It turns any near-Ramanujan graph whose short cycles are sparse into graphs of all nearby sizes, so it applies to future constructions as well. Lemma 3.2 is a self-contained delocalization statement in the tradition of Kahale 1995: eigenvectors of eigenvalues at least in absolute value cannot concentrate near tree-like edges.
The result is proved on paper. To our knowledge none of it is formalized; Mathlib has adjacency matrices, extended graph distance and acyclicity, but no theory of expanders. A complete development would give machine-checked versions of a delocalization lemma, of the greedy selection of far-apart vertices away from short cycles, and of the variational eigenvalue bound for induced subgraphs. It would also check two points the paper passes over. The proof of Theorem 1.3 treats only positive eigenvalues . And its claim that the -neighbourhood of a matching edge is cycle-free fails when two deleted vertices are at distance exactly . This mission states the corrected forms (see Formalization scope).
The spectral bound for does not follow from interlacing alone. Deleting vertices is harmless, since by (9) the quadratic form of is controlled by . But the added matching contributes up to to , which can be as large as for an eigenvector concentrated on . The obvious estimate therefore gives only . Closing the gap requires showing that an eigenvector of a large eigenvalue spreads its mass over the layers around each matching edge (Lemma 3.2). That in turn needs those neighbourhoods to be trees in and pairwise disjoint, which is where Lemma 3.1's choice of is used. The combinatorial part, tracking distances and cycles in when mixes edges of with matching edges, is the main formalization burden.
SimpleGraphs with real adjacency matrices adjMatrix ℝ. The (n, d, λ) predicate requires IsRegularOfDegree d, symmetry, row sums , and for every eigenpair with , . Distances use the extended SimpleGraph.edist, never dist (which is across components). Cycle conditions are on induced subgraphs, and "at most one cycle" on a ball is . Deleted vertices are a Finset U; the new graph lives on the subtype {v // v ∉ U}. The matching is a fixed-point-free involution of .In most control problems the controller does not see the state of the system. It sees noisy observations, remembers its past controls, and must act on that record. Inventory systems with delayed or inaccurate counts, maintenance of machines whose wear is only inspected, target tracking, and medical treatment planned from test results all have this form. The standard device for such problems is to replace the hidden state by a summary of the record, most often the conditional distribution of the state given the observations, and to solve a dynamic program whose state is that summary.
For finite or countable spaces this reduction goes back to Åström (1965) and Striebel (1965), who introduced the conditional distribution of the state as a "sufficient statistic" for control. Chapter 10 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996) carries it out for Borel state, control and observation spaces, with universally measurable policies and costs that are only lower semianalytic. In that generality the measurability of the reduced model is the whole difficulty, and the chapter isolates exactly what a summary must satisfy for the reduction to be exact.
The imperfect state information model (ISI) of Definition 10.3 has a nonempty Borel state space , control space and observation space ; a discount factor ; a lower semianalytic cost ; a Borel state transition kernel ; Borel observation kernels and ; and a horizon . The initial state has distribution , , and then , . The controller knows the information vector and must choose , where the constraint set is analytic.
A policy consists of universally measurable stochastic kernels that respect the constraints (Definition 10.4). Together with it determines probability measures on the histories , the cost
and the optimal cost (Definition 10.5). Assumption asks that the expected discounted negative part of the cost be finite for every policy and initial distribution; asks the same of the positive part.
A statistic is a sequence of Borel maps into nonempty Borel spaces. It is sufficient for control (Definition 10.6) if (a) the constraints can be read off from it, with analytic; (b) the conditional law of given is a Borel kernel , for every and every policy; and (c) the conditional expectation of given is a lower semianalytic function . The perfect state information model (PSI) of Definition 10.7 has states , constraints , costs and transitions ; its cost and optimal cost at are and . The initial distribution of is
A Markov (PSI) policy acts in (ISI) through .
Under or ,
and a Markov (PSI) policy that is optimal, -optimal or weakly --optimal for (PSI) is respectively optimal, optimal at , or -optimal at for (ISI); under an -optimal (PSI) policy is -optimal for (ISI). Here is weakly --optimal if when and otherwise, and -optimal if (Definition 10.8).
Proposition 10.3 says that an imperfect-information problem loses nothing by being solved in the reduced model: the optimal cost is the -average of the reduced optimal cost, and good reduced policies are good original policies. Combined with Proposition 10.6, every (ISI) model has such a reduction, so the finite-horizon dynamic programming theory of Chapter 8 (existence of -optimal policies, the dynamic programming algorithm) transfers to partially observed problems on Borel spaces. Proposition 10.4 turns this into a structural statement about the original problem: nearly optimal controllers need to retain only the statistic.
These results are proved in the book. None of them is formalized: the platform's related results (Bäuerle–Rieder's partially observable models with observation densities, and the linear-quadratic-Gaussian separation theorem) work in different models and do not cover universally measurable policies, analytic constraints, or lower semianalytic costs. A machine-checked version makes the conditional-expectation bookkeeping of the reduction explicit, and the definitions of this mission (universal measurability, lower semianalytic functions, the book's extended integral, history measures built from universally measurable kernels) are reusable by every other chapter of the book.
The obvious argument says: replace the state by the statistic, observe that costs and transitions depend only on the statistic, and conclude. In the Borel setting each step is a measurability claim that the naive argument does not supply. The conditions of Definition 10.6 are almost-everywhere statements about conditional distributions under every pair , while the reduced model needs genuine kernels; the policies are only universally measurable, so integrals and compositions must be taken with respect to completions; the costs take the values , so interchanging sums and integrals requires the finiteness assumptions and ; and the inequality requires producing, from an arbitrary history-dependent (ISI) policy, a Markov (PSI) policy with the same cost, which the naive argument does not do.
EReal with the book's convention written out explicitly (badd, bsum, extIntegral); Mathlib's EReal subtraction () is never used where both terms can be infinite.ProbabilityMeasure C that are measurable for the completion of every probability measure. History measures are characterized by their values on rectangles. Families indexed by the stage are indexed by all of ; only stages are constrained.Contributions are welcome on any milestone. Basic facts that a full development needs, such as composition of universally measurable maps (Proposition 7.44), measurability of integrals against universally measurable kernels (Proposition 7.46), and existence of the history measures (Proposition 7.45), can be posed and proved as supporting lemmas; they are reusable across the book.
A graph is perfect if every induced subgraph has chromatic number equal to its clique number. Berge conjectured in 1961 that a graph is perfect exactly when it contains no odd hole and no odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved this strong perfect graph theorem in 2006 (Ann. of Math. 164 (2006), 51–229). Perfect graphs matter beyond graph theory: for them the stable set polytope is described by clique inequalities, so maximum weight stable set and colouring problems become polynomially solvable linear programs (Grötschel, Lovász and Schrijver).
The proof reduces the theorem to a decomposition statement (1.3 of the paper): every Berge graph is basic or admits one of a few decompositions. That statement is in turn proved in twelve steps, listed as 1.8.1–1.8.12. Each step excludes one kind of configuration from a Berge graph without the decompositions. This mission is step 1.8.5, restated as 13.4: it deals with Berge graphs that contain a long odd prism but no appearance of . It is the only step of the proof that needs proper 2-joins in the complement and proper homogeneous pairs.
All graphs are finite and simple; is the complement of . A path is an induced subgraph which is a path, and its length is its number of edges. An antipath is a path of . A hole is an induced cycle of length at least , and an antihole is the complement of a hole of . is Berge if every hole and antihole of has even length.
A prism consists of two disjoint triangles , and three paths from to , such that the only edges between different paths are the triangle edges. It is long if some has length , even if all three lengths are even, and odd otherwise.
A subdivision of a graph replaces every edge of by a track, these tracks being disjoint except at their ends. appears in if is isomorphic to an induced subgraph of for some bipartite subdivision of , where is the line graph.
The decompositions in the conclusion (pp. 53–54):
The intermediate objects come from Sections 11–13 of the paper:
Let be Berge with no appearance of in or in , and suppose contains a long odd prism as an induced subgraph. Then
In the order of the paper's argument:
13.4 removes long prisms from the analysis. Combined with 10.6 (the even prism), it shows that a recalcitrant graph contains no long prism in or , which places it in the class (p. 154). The later steps (double diamonds, odd wheels, pseudowheels, wheels) all assume this. The step-connected strip and staircase method developed here is also the paper's model for growing a maximal structure and then classifying how the rest of the graph attaches to it.
The theorem has been proved since 2006; no machine-checked proof of it or of any of its steps is known. The proof of 13.4 also cites these results of the same paper, which are posed in other missions of this series:
The difficulty is the volume of case analysis behind every statement. The paper does not prove the exact analogue of the even-prism result 10.6. It warns (p. 127) that it does not know whether that analogue holds, and adds the two extra outcomes instead. The obvious first idea is to take a long odd prism and analyse attachments to it as in Section 10. The paper does not get the result that way (p. 127): it replaces two of the three paths by a maximal step-connected strip. Controlling how every remaining vertex or connected set attaches to such a strip is what the breaker results do. Maximality is also delicate. "Strongly maximal" refers to staircases of the complement, so and must be handled in one framework.
Graphs are SimpleGraph V on a Fintype vertex type with decidable equality. is Gᶜ.
G.induce X, so is connected. Anticonnectedness is the same notion in Gᶜ.Every hypothesis of the paper is kept. "No appearance of " is in and in for the goal, and in for the milestones. The goal also keeps "Berge", "no even prism" and "no 1-/2-breaker" where the page has them. 12.1's "exactly one" is an exclusive disjunction. 11.4 is a non-existence statement.
A formalization with non-induced paths, with the complement dropped from "one of ", or with a strip, staircase or breaker predicate that no graph satisfies would make the targets empty or false. The definitions here are checked against a concrete graph: the 8-vertex prism with path lengths is a long odd prism, and it carries a staircase. Contributions are welcome: proofs of the milestones, and reusable material on induced paths, holes and line graphs of subdivisions.
A linear program is solved with data that, in practice, is rarely known exactly: coefficients come from measurements, estimates or forecasts. Robust optimization asks for a solution that remains feasible for every realization of the data in a prescribed uncertainty set, and among those the one with the best guaranteed objective value. Ben-Tal and Nemirovski introduced this framework for linear programming in Robust solutions of uncertain linear programs (Oper. Res. Lett. 25, 1999), following their treatment of robust convex optimization (Math. Oper. Res. 23, 1998) and Soyster's earlier work on inexact linear programming (Oper. Res. 21, 1973). The robust counterpart has since become the starting point of a large literature on uncertainty sets, budgets of uncertainty and adjustable policies.
A natural first objection is that the robust counterpart might be needlessly conservative: by demanding feasibility for all realizations simultaneously, it could be infeasible, or have a worse value, even when every individual realization is perfectly well behaved. This mission formalizes the paper's answer (§2.2): under two structural hypotheses, the robust counterpart is no worse than the worst realization.
Fix and write a linear program in the homogeneous form (6)
where is a real matrix and is componentwise. Every linear program can be put in this form. The matrix is uncertain: it is only known to lie in an uncertainty set of matrices. Each gives an instance with feasible set and optimal value ; the family of instances is . The robust counterpart (7) is
and its optimal value is . Since does not change when is replaced by its closed convex hull, the paper assumes throughout that is convex and closed.
Let be the set of all realizations of the -th row, the projection of onto the data of the -th constraint. The uncertainty is constraint-wise if : the rows vary independently. The Boundedness Assumption asks for a convex compact set that contains the feasible set of every instance.
If the uncertainty is constraint-wise and the Boundedness Assumption holds, then
The milestones follow the paper's proof: the row-wise description (8) of robust feasibility; the inclusion of in every instance's feasible set; the reduction of the semi-infinite system (8) on to a finite subsystem; the statement that the finite system (10) then has no solution at all; the Farkas certificate (11); the construction of one infeasible instance from it; and part (i) alone, which part (ii) uses for an augmented program.
The §2.2 example (every instance has optimal value 1, the robust counterpart is infeasible), and the two invariance remarks: is unchanged under passing to the closed convex hull of (§2.1) or to the product of its projections (§2.2).
Proposition 2.1 says that, for constraint-wise uncertainty, robustness costs nothing beyond what the worst realization already costs: the robust counterpart is feasible exactly when every instance is, and its optimal value equals the worst instance value. The §2.2 example shows the hypothesis cannot be dropped: there, correlated uncertainty in two rows makes every instance solvable with value 1 while the robust counterpart is infeasible. Together with the invariance of under passing to the product of projections, this explains why row-wise (constraint-wise) uncertainty sets are the standard modelling choice in robust linear optimization.
The result is proved in the paper; no machine-checked version is known to exist. Formalizing it produces a reusable development of semi-infinite linear systems: the compactness reduction to finite subsystems, a homogeneous Farkas alternative, and the row-averaging argument that uses convexity and the product structure of .
The robust counterpart has a continuum of constraints, one for each , so Farkas' Lemma cannot be applied to it directly. The step that requires care is passing from infeasibility of this semi-infinite system to infeasibility of a single instance. Compactness yields only finitely many instances whose joint system has no solution in ; those instances are in general all feasible individually, and the infeasible instance has to be manufactured from their rows. Without constraint-wise uncertainty the manufactured matrix need not lie in , which is exactly what the §2.2 example exploits. Part (ii) needs the optimal values of the instances to be attained on compact feasible sets, which is where the Boundedness Assumption enters again.
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and is 0 ≤ A *ᵥ x in the componentwise order. The -th row of is A i and is a ⬝ᵥ x. The projections are the images of under , not free sets, and constraint-wise uncertainty is the inclusion (the reverse inclusion always holds). The Boundedness Assumption keeps both convexity and compactness of , as on the page.
Optimal values are infima: is the greatest lower bound (IsGLB) of over , and (9) states that is the least upper bound (IsLUB) of the set of real optimal values of the instances. No real sInf/sSup is used, so no junk value can make the statement true.
The goal carries the paper's standing assumption that is convex and closed, and one disclosed addition: is nonempty. The paper takes this for granted; without it part (i) fails for and the supremum in (9) ranges over the empty set. The goal does not assume that the robust counterpart or any instance attains its optimum, and it does not mention finite subsystems, multipliers or the averaged matrix; those appear only in the milestones. A formalization in which the uncertainty sets are arbitrary sets with , or in which optimal values are taken as sInf without boundedness, would not be faithful and is ruled out.
A complete development needs: compactness arguments for families of closed half-spaces, a Farkas alternative for homogeneous systems with one normalizing equation, and elementary convexity of linear images. These pieces are general and reusable beyond robust optimization. Proofs of the milestones, alternative arguments (for instance via LP duality for part (ii)) and proofs of the companion statements are welcome.
Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets equipped with a rank function, or equivalently a family of independent sets, obeying a few postulates abstracted from the linear dependence of the columns of a matrix. The obvious first question about such an abstraction is whether it is genuinely more general than its model, that is, whether there are matroids that do not arise from any matrix. Section 16 of the paper answers it with a seven-element example, now called the Fano matroid , and proves that no real matrix corresponds to it.
The question has had a long life. Representability of matroids over a given field is a central theme of matroid theory: Tutte (1958) characterized the matroids representable over the field with two elements by a single excluded minor, the four-point line , and the regular matroids by three excluded minors, , and its dual; and Seymour's decomposition of regular matroids (1980) rests on the same objects. Whitney's §16 is the starting point of this line: the first proof that the abstract postulates admit matroids outside linear algebra over .
Timeline:
Let be an matrix with columns . For a set of columns, let be the rank of the submatrix formed by those columns. Regarding the columns as abstract elements gives a matroid on with rank function : the matroid of . A matroid corresponds to if it is the matroid of , with elements matched to columns.
A circuit of a matroid is a minimal dependent set. For a circuit of the matroid of , there are numbers with for every row , and exactly for ; the set of such vectors is written when only the support condition is meant. Stacking one such row per circuit gives the circuit matrix of , determined up to nonzero factors on its rows.
A fundamental set of circuits of a matroid with nullity ( the number of elements) is a family of circuits with such that the elements can be ordered with and for ; it is strict if for every .
The matroid of §16 has elements ; its bases (maximal independent sets) are all three-element sets except
The number of rows is arbitrary; the existence clause makes the non-existence statement non-vacuous.
The result. The theorem separates the abstract notion of matroid from linear dependence over : some matroids are not real-representable. It also exhibits that representability depends on the field, because the same matroid is the matroid of a matrix over the integers mod 2 (milestone 8). Everything later written about representability over particular fields, excluded-minor characterizations, and the gap between abstract and linear matroids starts from this distinction. Theorem 32 is of independent interest: it translates statements about circuits of a represented matroid into the vanishing of minors of a normalised circuit matrix.
Formalizing it. The result is classical and its proof is short on paper, but it is not formalized in Mathlib, which has matroids (Matroid, circuits, ranks) but no column matroid of a matrix with a rank-of-submatrix characterization, no circuit matrix, and no Fano matroid. The mission produces those objects and the bridge lemmas (Theorem 29, Lemmas 10–11, Theorem 32) that connect matroid circuits with linear algebra of the circuit matrix. No machine-checked proof of the non-representability of the Fano matroid over in Lean is known to the curators.
The obvious attempt is a direct search: suppose a real matrix has as its matroid and derive a contradiction from the seven dependent triples. This does not work as stated. Each rank condition is a determinantal (nonlinear) condition on the entries, the number of rows is unbounded, and a representation is determined only up to row operations and column scalings, so there is no finite case check and no single linear computation that settles the question. The contradiction has to come from an argument that is invariant under these symmetries, and the milestones (circuit vectors determined up to scaling, fundamental sets spanning, circuits detected by minors) are what such an argument needs to be stated in. The field also matters: the argument must use that in , since over a field of characteristic 2 the statement is false (milestone 8).
Matroids whose ground set is the whole (finite) type. The Fano matroid lives on Fin 7, Whitney's element being k - 1; the seven triples are written out literally. Matrices are Matrix (Fin m) ι K; "the matroid of " means: ground set everything, and the rank M.eRk N of every finite set of columns equals Matrix.rank of the column submatrix.Fin t with , and determinants are of square submatrices in the paper's row and column order.Reusable beyond this mission: the matroid of a matrix over a field, the circuit matrix, fundamental sets of circuits, and the Fano matroid. Contributions welcome: proofs of the milestones, and a proof of the goal by any route, including one that does not go through Theorem 32.
Whitney's 1935 paper introduced matroids as an abstraction of linear dependence among the columns of a matrix. Most of the paper works over the real numbers; its appendix asks which matroids arise from matrices of integers mod 2, that is, matrices with entries 0 and 1 in which rank and dependence are computed over the two-element field. These are today's binary matroids. They include the cycle matroids of graphs (Whitney closes the paper by noting that graphs correspond to mod-2 matrices with exactly two ones in each column) and they are the setting of several later structure theorems: Tutte's excluded-minor characterization of binary matroids (Tutte 1958), Seymour's decomposition of regular matroids (Seymour 1980) and Seymour's theory of binary clutters and max-flow min-cut (Seymour 1977), which underlies parts of combinatorial optimization.
Whitney's answer is an intrinsic postulate, (C*), on the circuits of the matroid, stated without reference to any matrix, and a constructive representation theorem (Theorem 37): a matroid satisfying (C*) is the matroid of a mod-2 matrix, and the matrix is unique once the columns of one base are fixed.
A matroid on elements is given by its independent sets; its circuits are its minimal dependent sets, its rank is the size of a base, and its nullity is . Here is a Mathlib Matroid (Fin n) whose ground set is all of Fin n.
Subsets of the elements are added mod 2: a sum of finitely many sets is the set of elements lying in an odd number of them (for two sets, the symmetric difference). A cycle is a sum mod 2 of circuits; the empty sum is the null cycle . A set is a true sum of sets that have no common elements and whose union it is. Postulate (C*) requires that each cycle be a true sum of circuits.
With , a family is a strict fundamental set of circuits with respect to if , each is a circuit, and contains but no other .
For a matrix over the integers mod 2 with columns , columns are independent (mod 2) if no non-null subset of them sums to the zero column. The matroid corresponding to has the column indices as elements and these independent sets.
Let satisfy (C*), with elements and base . For every matrix mod 2 (any number of rows) whose columns are independent mod 2,
Milestone 7 and the goal together characterize binary matroids as the matroids satisfying (C*).
The result. Theorem 37 and the p. 532 claim give an intrinsic, matrix-free description of the matroids representable over the two-element field, and Theorem 36 parametrizes all of them by arbitrary subsets of a base. Uniqueness in Theorem 37 says that a binary representation is determined by the columns of one base; in modern terms, binary matroids are uniquely representable over GF(2) up to row operations. Every later theory of binary matroids, including graphic and cographic matroids, Tutte's excluded-minor theorem and Seymour's decomposition, starts from this equivalence.
Formalizing it. The results are proved in the paper and in textbooks (e.g. Oxley, Matroid Theory, Ch. 9) but, at the Mathlib revision used here, there is no notion of a matroid represented by a matrix over a field, and no binary-matroid theory. On Prove2Me, the existing binary objects (SeymourMFMC.Binary.*) are binary clutters defined through blockers, not matroids represented by mod-2 matrices. This mission produces the representation predicate for mod-2 matrices, the cycle space of a matroid, and the equivalence between (C*) and binary representability.
Writing down candidate columns is not the hard part; showing that the matroid of the completed matrix is itself, and not merely a matroid sharing some of its circuits, is. Whitney's example at the end of §9 exhibits two different matroids with a common strict fundamental set, so agreement on fundamental circuits does not by itself identify a matroid; any argument must use (C*) on both the given matroid and the matroid of the matrix. A naive comparison of independent sets column by column does not close this gap. Uniqueness likewise depends on the independence mod 2 of the prescribed columns: without it, different completions can give the same matroid.
Matroid (Fin (r + q)) with ground set Set.univ; Whitney's is k - 1, his is the range of Fin.castAdd q, and is Fin.natAdd r (i - 1). Writing removes natural-number subtraction; is not a free parameter, since is required to be a base.sumMod2); cycles are sums over finite sets of circuits; true sums are unions over finite pairwise-disjoint sets of circuits; (C*) is SatisfiesCStar on the circuit family {C | M.IsCircuit C}. These definitions take the circuit family as a parameter, so that the (C₂) milestone is posed for an arbitrary family of sets, as Whitney poses it.Matrix (Fin m) (Fin n) (ZMod 2) with any ; independence mod 2 of columns is LinearIndepOn (ZMod 2) of the columns (the rows of the transpose). IsMatroidOf M A compares all independent sets, not only bases.Contributions welcome: the general fact that the matroid of a vector family over a field exists (a reusable Matroid.ofFun-style construction over any field), the cycle-space lemmas, and proofs of the milestones in any order.
A single-server queue in which customers arrive according to a renewal process and are served in exponentially distributed times is the system GI/M/1. Observed just before successive arrivals, its queue length is a Markov chain on , the imbedded chain introduced by D. G. Kendall (Kendall 1953, Ann. Math. Statist. 24, pp. 338–354). Whether this chain settles into a statistical equilibrium, keeps returning to the empty state without one, or drifts off to infinity is the first question asked about the queue, and every later quantity (stationary queue lengths, waiting-time distributions) presupposes the answer.
F. G. Foster's 1953 paper (Foster 1953) answers it for GI/M/1 and for M/G/1 by a different route from Kendall's direct analysis: it first proves general criteria, stated in terms of solutions of linear equations and inequalities in the transition matrix, for a countable Markov chain to be ergodic, recurrent or transient, and then checks them on the two queueing matrices. The criteria are of independent use; one of them (Theorem 2 of the paper) is now known as Foster's criterion, the starting point of the drift (Lyapunov-function) method for stability of Markov chains and queueing networks.
Timeline. Kendall (1951, J. Roy. Statist. Soc. B 13) studied queue-length processes directly, including a recurrence argument for M/G/1 that Foster's §3 reproduces; Kendall (1953) introduced the imbedded-chain method and, for GI/M/1, proved by it that is sufficient for ergodicity (Foster 1953, p. 359); Foster (1953) proved the full classification, ergodic iff and recurrent iff , by the general criteria. This mission treats the GI/M/1 half; a companion mission treats M/G/1.
A transition matrix on the states is an array of nonnegative reals whose rows sum to . For a state , is the probability that the chain started at returns to at some later step. The chain is recurrent if for every , transient if for every , and ergodic (recurrent-nonnull, positive recurrent) if moreover every mean recurrence time is finite. Foster's general theorems concern an irreducible chain (every state reachable from every state), assumed aperiodic for simplicity.
The GI/M/1 chain is described by a sequence of positive numbers with : is the probability that exactly services are completed between two arrivals. With the tails ,
that is , for , and for . In Lean this matrix is gim1Matrix a. The traffic parameter is defined through its inverse,
the mean number of service completions per interarrival interval (rhoInv a, and rho a ).
Together: ergodic for , recurrent-null for , transient for . The statement carries no constants and leaves the sequence free apart from positivity and normalization.
Milestones 2–4 are stated for a general irreducible aperiodic chain.
The classification tells exactly when the GI/M/1 queue is stable: the stationary distribution of the imbedded chain, which is geometric, exists precisely in the ergodic case , and for the queue grows without bound. Theorems 1 and 4 are general tools, reusable for any countable chain: Theorem 1 characterizes ergodicity by summable invariant vectors, Theorem 4 characterizes transience by bounded harmonic functions off one state. Theorem 7 is the extinction criterion of branching processes and recurs throughout applied probability.
All of these results are proved in the literature (Foster 1953; Feller's textbook for Theorem 7 and a version of Theorem 4). As far as a search of the platform shows, none of them has a machine-checked proof; the platform holds related special cases for the G/M/1 queue with a specific interarrival law (QueueingFundamentals.GM1.unique_root_unit_interval, open), but not the general lemma or the classification. A formalization would provide the general criteria as reusable library results and the first verified stability classification of a non-Markovian queue's imbedded chain.
The matrix is explicit, but none of the three properties is a finite computation: ergodicity and recurrence are statements about return times over all horizons, so each direction must go through an existence or nonexistence statement about infinite systems of equations. For the converse directions the obvious argument fails: exhibiting a candidate solution such as shows nothing until it is known that ergodicity forces every such solution to be summable, and showing that no bounded nonconstant solution of (7) exists when requires control of all solutions, not of one. The general criteria themselves rest on limit theorems for and on interchanging infinite sums, and the infinite-mean case has to be carried along everywhere.
QueueingFundamentals_Foundations_MarkovChain: TransitionMatrix (entries p, nonnegativity, rows summing to via HasSum), returnProb, meanRecurrenceTime, Irreducible, Aperiodic, PositiveRecurrent. "Ergodic" is PositiveRecurrent. IsRecurrent and IsTransient are defined state by state from returnProb; their complementarity for irreducible chains is a theorem, not a definition.TransitionMatrix whose entries equal gim1Matrix a; such a matrix exists for every admissible (rows sum to ), so the statement is not vacuous.ℝ≥0∞), with : an infinite mean gives , and that chain is ergodic.HasSum or Summable), so that a divergent series cannot satisfy an equation or inequality vacuously. In Theorem 1's sufficiency half the may be of either sign. In Theorem 7 the distribution is renamed to avoid a clash with .Many problems in imaging, signal processing and statistics are convex minimizations of the form
where is smooth, and are nonsmooth but have computable proximity operators, and is a bounded linear operator, for example a discrete gradient in total-variation denoising. Primal–dual splitting methods solve such problems using only , the proximity operators of and , and applications of and , without ever inverting or computing the proximity operator of .
Condat's 2013 paper (JOTA 158(2):460–479; final author's version HAL hal-00609728v5) introduced Algorithms 3.1 and 3.2, which handle all three kinds of terms at once, allow relaxation and summable errors, and contain earlier methods as special cases. Together with the closely related work of Vũ (Adv. Comput. Math. 2013), it is the standard reference for the "Condat–Vũ" algorithm.
Timeline. Chambolle and Pock (2011) proved convergence of their primal–dual algorithm, without a smooth term and without relaxation, under (J. Math. Imaging Vis. 40). He and Yuan (2012) interpreted it as a proximal point algorithm in a modified metric (SIAM J. Imaging Sci. 5). Condat (2013) added the smooth term , relaxation and errors (Theorem 3.1), and, for , proved weak convergence for relaxation parameters up to (Theorem 3.2), the result of this mission.
Let and be real Hilbert spaces and a bounded linear operator with adjoint and operator norm . Write for the proper, lower semicontinuous, convex functions . For , the conjugate is , the proximity operator is , and the subdifferential is .
Fix , and . The primal–dual inclusion (6) asks for with
then minimizes and solves the dual problem. The paper assumes this inclusion has a solution.
Given , relaxation parameters and error terms , , Algorithm 3.1 iterates, from any ,
Algorithm 3.2 exchanges the roles: it computes from first, then using .
Suppose and , , and
Then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, there is a solution of (6) with and weakly.
Remark 3.2 (the goal with affine, , instead of ) and Theorem 5.2 (the version with composite terms and condition ).
The result. Theorem 3.2 covers the Chambolle–Pock algorithm with relaxation and summable errors, in arbitrary real Hilbert spaces. Over-relaxation often speeds the method up in practice, and the error terms justify inexact proximity operators. Theorem 5.2 extends it to any finite number of composite terms by full splitting. The convergence statement makes no reference to a Lipschitz constant, so it applies whenever the problem has no smooth part.
Formalizing it. The result is proved on paper; no machine-checked version of Theorem 3.2, of the Krasnosel'skii–Mann lemma with errors, or of the proximal point algorithm under the condition is known to exist. A formal proof would supply reusable pieces of monotone-operator theory in Hilbert spaces: weak convergence of Fejér-type iterations, the change of metric induced by a positive operator, and maximal monotonicity of sums with a skew operator.
The algorithm is not a fixed-point iteration of a nonexpansive map in the original inner product: the coupling between the primal and dual steps breaks nonexpansiveness. The difficulty is to find a metric in which it becomes one, to show this metric is equivalent to the original one (which is where , strictly, is needed), and to transfer maximal monotonicity, zeros and summability of the errors to the new metric. Weak convergence in infinite dimension also requires an Opial-type argument rather than compactness. Mathlib provides inner product spaces, the operator norm and adjoints, but neither maximal monotone operators nor resolvents nor Krasnosel'skii–Mann iteration theory.
The spaces are real Hilbert spaces (InnerProductSpace ℝ and CompleteSpace). Functions valued in are EReal-valued, with the published IsProperClosedConvex. The conjugate is an EReal supremum, so can take the value . Proximity operators enter as maps with the published IsProx property; the subdifferential is the published IsSubgradient. The product with the inner product is WithLp 2 (X × Y). Weak convergence is for all . "" means partial sums tend to , and "" means summability of a nonnegative series.
Standing assumptions are hypotheses: , and (6) has a solution. With the smoothness assumption on is automatic. The paper's assumption that (1) has a minimizer follows from the solvability of (6) and is not stated. The goal is a conjunction over the two algorithms, and the limit is chosen after the run.
The condition is strict, , and relaxation is open, . A goal quantifying over no run, assuming the limit exists, or fixing before the initial point would be a different and weaker statement. Proofs of the milestones, of Theorem 5.2 via the product-space identities (49)–(52), and general results on monotone operators are welcome.
Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract rank function that behaves like the rank of a set of vectors. Part II of the paper opens with the decomposition of a matroid into components. The question it answers is basic to every later use of matroids: when does a matroid split into independent pieces, and how can the pieces be recognized?
For the matroid of a graph (elements = edges, rank = number of vertices minus number of connected pieces spanned) the components are the 2-connected blocks of the graph, and Whitney's theorem recovers the classical fact that two edges lie in a common block exactly when they lie on a common cycle. Whitney had studied separability of graphs in Non-separable and planar graphs (1932), and footnote 11 of the 1935 paper points out that the theorem identifies König's "Glieder" of a graph with components. Matroid connectivity built on this notion runs through later structure theory: Tutte's higher connectivity, Seymour's decomposition of regular matroids, and the matroid minors project all start from the separation of a matroid into components.
A matroid on a finite ground set is given here by Mathlib's Matroid structure, with rank function for (Mathlib's M.eRk X) and circuits, the minimal dependent sets (M.IsCircuit). Whitney treats every subset as a matroid in its own right, a submatroid, with the rank function of restricted to subsets of . For sets he writes for the union, for the number of elements of , and
for the nullity of .
Rank is subadditive: . A submatroid is separable if it can be divided into two disjoint groups , each containing at least one element, with
and non-separable otherwise. Every single element is non-separable. A component of is a maximal non-separable part of : a nonempty non-separable set contained in no strictly larger non-separable subset of .
For two distinct elements of ,
Components are defined by the rank function, circuits by dependence; the goal asserts that the two descriptions agree.
The result. Theorem 19 makes the component decomposition computable from circuits alone and shows that "lying on a common circuit" is an equivalence relation on distinct elements, a fact that is not evident from the circuit axioms. Theorem 18 adds that the decomposition is the unique one with additive rank. Together they are the starting point of matroid connectivity: the direct-sum decomposition of a matroid, the reduction of many matroid problems (representability, duality of components, Whitney's own Theorems 24–26 on duals of components) to the connected case, and the higher-connectivity theory that followed.
Formalizing it. The results are classical and proved in the paper; nothing here is open. To our knowledge Mathlib at the pinned revision has no notion of matroid connectivity or components, so this mission produces the first machine-checked development of Whitney's §10: the rank-based definition of separability, the disjoint decomposition into components, the circuit characterization, and the ear-type construction of non-separable matroids (Theorem 17). These are reusable for any later formalization of matroid connectivity, including Whitney's results on duals of components.
The two directions of Theorem 19 rest on different machinery. That two elements on a common circuit lie in one component follows from the rank theory (Theorems 13 and 16). The converse is the substantial direction: a component is defined by the failure of rank additivity, which only says that every division of the component is crossed by some circuit (Lemma 9). It does not directly give one circuit through two prescribed elements. Combining circuits that cross different divisions into a single circuit through both and requires the circuit elimination property together with a minimality argument over subsets of the component; the naive attempt of chaining overlapping circuits from to gives a connected chain of circuits, not one circuit.
Matroid α with [M.Finite]; Whitney's matroids are finite. A submatroid is a subset M.E with the rank M.eRk restricted to its subsets; results that Whitney states for "a matroid " are stated for subsets of an ambient finite matroid, which is the same statement applied to the submatroid .ℕ∞-valued M.eRk, finite on a finite matroid, so (10.1) is an equation of natural numbers. Nullity is computed in as the number of elements minus the rank.IsSeparable M X requires two nonempty, disjoint groups with union and additive rank; without nonemptiness every set would be separable. IsNonSeparable M X adds M.E. IsComponent M K requires nonempty, non-separable, and maximal; nonemptiness excludes the empty set, which is vacuously non-separable.Matroid.IsCircuit.M.eRk and circuit elimination (both in Mathlib), the relation between circuits of M ↾ X and circuits of M inside (Matroid.restrict_isCircuit_iff), and finiteness arguments for maximal non-separable sets. Proofs of the milestones, alternative proofs of the goal, and lemmas relating components to Mathlib's direct sums of matroids are all welcome.Many problems in imaging, signal processing and statistics take the form
where and are convex functions whose proximity operators can be computed cheaply, is a linear operator such as a finite-difference gradient, and is smooth. Total-variation denoising, the lasso with a structured penalty, and constrained least squares are of this type. Because is generally not proximable even when is, practical methods split the problem so that each step uses only , , and , without inverting any operator.
L. Condat (J. Optim. Theory Appl. 158 (2013)) introduced a relaxed, inexact primal–dual iteration of this kind; B. C. Vũ (Adv. Comput. Math. 38 (2013)) studied the same structure for monotone inclusions. With the iteration is exactly the method of Chambolle and Pock (J. Math. Imaging Vis. 40 (2011)). They proved convergence in finite dimension assuming , and no errors. He and Yuan (SIAM J. Imaging Sci. 5 (2012)) extended this to a constant relaxation under the same other hypotheses (Condat, §3.1.1). Condat's paper proves three convergence theorems. This mission is the third: in finite dimension and with , the iterates converge under the step-size condition , equality included. Equality matters in practice: one can set and tune a single parameter, as in the Douglas–Rachford method.
Let and be real Hilbert spaces and a bounded linear operator with adjoint and operator norm . Write for the proper, lower semicontinuous, convex functions , and let , . The Fenchel conjugate is , the proximity operator is , and the subdifferential is .
The primal–dual inclusion (6) asks for with
A solution gives a minimiser of the primal problem and a solution of its dual.
Algorithm 3.1 chooses , , relaxation parameters , error terms and an initial estimate , then iterates
Algorithm 3.2 swaps the roles of the primal and dual variables: the dual step comes first, and the primal step uses . Section 5 extends both to (Algorithms 5.1 and 5.2), with the inclusion (48) in place of (6).
Let , be finite-dimensional, , , and assume (6) has a solution. If
then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, converges to a solution of (6).
With the operator (20) and the error-free step of Algorithm 3.1:
Remark 3.2 (Theorem 3.3 with affine, i.e. in (2)) and Theorem 5.3 (the analogue for composite terms, with (i) replaced by ) are included as draft theorems.
Theorem 3.3 is the convergence guarantee behind the common practice of running the Chambolle–Pock iteration and its relaxed variants at the critical step size . It covers relaxation parameters up to and summable errors in both proximity operators. It applies directly to the discrete models of imaging and statistics, which are finite-dimensional. Theorem 5.3 extends it to any finite number of composite terms in parallel.
None of the statements of this paper is formalized on the platform. Machine-checked convergence proofs for primal–dual splitting are not available in Mathlib. The mission would produce the first ones, together with two standalone tools of general use: the inexact Krasnosel'skii–Mann theorem (Lemma 4.1), and Polyak's recursive-inequality lemma (Lemma 4.6), which is a standard tool for stochastic and inexact iterations.
The usual proof treats the iteration as a proximal-point or forward–backward step in the space with the inner product . That argument needs strictly positive, which is exactly what fails when : then has a nontrivial kernel, is only a seminorm, and weak convergence in the -geometry says nothing about the components of in . The proof replaces the iteration by its "shadow" on , uses that factors through , and recovers the full iterates through continuity of and a recursive inequality. The last step requires strong convergence of the shadow sequence, which is where finite dimension enters. Infinite-dimensional versions require different arguments and are not claimed here.
Spaces are real inner product spaces with CompleteSpace; the goal and Theorem 5.3 add FiniteDimensional. Functions in take values in EReal and satisfy the published predicate IsProperClosedConvex (never , finite somewhere, lower semicontinuous, convex epigraph). The conjugate is an EReal supremum. Proximity operators are maps , satisfying the published minimisation predicate IsProx for and ; such maps exist and are unique for functions. The subdifferential is the published IsSubgradient. Runs of the algorithms are predicates on pairs of sequences with arbitrary initial point, and the limit is chosen after the run. "" for a series is divergence of its partial sums, "" is summability of a nonnegative series, and convergence in the goal is norm convergence.
The standing assumptions of pp. 3–4 are hypotheses: , and (6) has a solution. The paper's other standing assumption, that problem (1) has a minimiser, follows from the second and is omitted. In the milestones, the operators and are plain maps on . The projector is not built: "" is stated as "", which is equivalent because is self-adjoint. Each milestone drops finite dimension, so it is stated at least as strongly as on the page.
The strict inequality would make the goal a corollary of the weaker Theorem 3.2 with an extra finite-dimensional upgrade. The goal keeps . Weak convergence in place of norm convergence, an chosen after , or a solution of (6) fixed before the run would each weaken the theorem, and all are excluded.
Useful infrastructure includes: firm nonexpansiveness of for EReal-valued functions; -ness of the conjugate and Moreau's identity; maximal monotonicity of plus a skew operator; and the inexact Krasnosel'skii–Mann theorem. All of it can be reused for Theorems 3.1 and 3.2 of the same paper, and for Douglas–Rachford and three-operator splitting. Proofs of individual milestones are welcome independently of the goal.
A graph is perfect if every induced subgraph has chromatic number equal to its clique number. Perfect graphs are the graphs for which colouring and clique problems behave as linear programs do: the stable-set polytope of a perfect graph is described by its clique inequalities, so maximum weight stable sets and minimum colourings can be computed in polynomial time (Grötschel, Lovász & Schrijver 1988). In 1961 Berge conjectured that a graph is perfect exactly when it has no odd hole and no odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved this, the strong perfect graph theorem, in Ann. of Math. 164 (2006).
The proof is a decomposition theorem: every Berge graph is basic or admits one of a few decompositions. The paper reaches it through twelve steps, 1.8.1–1.8.12 (p. 59), each handling graphs that contain a certain configuration. This mission poses step 1.8.3, Theorem 9.6. It handles Berge graphs that contain the line graph of a bipartite subdivision of , all such line graphs being degenerate.
All graphs are finite and simple. denotes the complement of . A hole is an induced cycle of length at least , an antihole is a hole of , and is Berge if all its holes and antiholes have even length. A path is always an induced path, and an antipath is a path of . The length of either is its number of edges.
Line graphs and appearances. The line graph has vertex set , two edges adjacent when they share an end. is a subdivision of if it arises from by replacing every edge by a track (a path, not necessarily induced), these tracks disjoint except for their ends. appears in if, for some bipartite subdivision of , is isomorphic to an induced subgraph of ; is then an appearance of . For the appearance is degenerate if some 4-cycle of contains the four vertices of degree three. A -enlargement is a 3-connected graph with a proper subgraph isomorphic to a subdivision of . An appearance is overshadowed if some branch of of odd length , with ends , has a vertex of nonadjacent to at most one edge at and at most one edge at .
Knots and striations. A knot is formed by two paths with ends and two antipaths with ends . They are pairwise disjoint and of length , is anticomplete to , is complete to , and the ends are joined in a prescribed twisted pattern (pp. 107–108). A degenerate appearance of is a knot. A strip is a family of paths ("rungs") from to through ; an antistrip is a strip of . A striation is made of strips and antistrips. All rungs and antirungs are odd, the strips are pairwise anticomplete, the antistrips pairwise complete, and every strip is parallel or co-parallel to every antistrip, with enough "twists" between them (p. 112). A striation is maximal if no striation has a strictly larger vertex set. The paper defines when a set of vertices is local for a knot or striation and when it resolves one.
Outcomes. A double split graph has its vertices partitioned into () and (). Each is an edge and each a nonedge, distinct pairs are anticomplete and distinct pairs complete to each other, and every and are joined by exactly two disjoint edges. A skew partition of has disconnected and disconnected. It is balanced if no odd path joins nonadjacent vertices of through and no odd antipath joins adjacent vertices of through . A proper 2-join is a partition of whose only cross edges are complete joins – and –, with the side conditions of p. 53.
Let be Berge, with every appearance of in and in degenerate and no induced subgraph of isomorphic to . Then
9.3–9.5 assume that no -enlargement appears in or and that no appearance of in or is overshadowed. An optional, non-milestone item poses 9.7 (p. 118): a Berge graph with an appearance of is a line graph or the complement of one, a double split graph, or admits a proper 2-join (in or ) or a balanced skew partition.
9.6 is the step of the proof that produces double split graphs, one of the five basic classes. In the main argument it follows step 1.8.1 (5.1, nondegenerate appearances of ) and is combined with it in 9.7. Through 9.7 it gives the first half of 13.5: every recalcitrant graph belongs to the class and so contains no appearance of in or .
The theorem has been proved since 2006. We know of no machine-checked proof of the strong perfect graph theorem or of any of its steps. Mathlib has line graphs and graph embeddings but no subdivisions, appearances or decompositions of Berge graphs. This mission produces a faithful Lean statement of step 1.8.3 and of the four lemmas its proof rests on, together with Lean definitions of knots, strips and striations.
The obvious approach would take a degenerate appearance of and study how each remaining vertex attaches to it, as §§5–6 do for nondegenerate appearances. This does not close. A degenerate appearance can be read as a line graph or as its complement, so the analysis of a vertex in and in has to be run at once. Single vertices can also be absorbed into larger structures that the line-graph analysis does not see. The proof grows the appearance to a maximal striation and classifies attachments to it, and the hard steps are 9.4 and 9.5. Their proofs need 9.3 in every case, and they use maximality to refute configurations that would let the striation grow.
Graphs are SimpleGraph V on a Fintype with decidable equality. Every object is defined as on the page, in the namespace StrongPerfectGraph.DoubleSplit.
SimpleGraph.lineGraph; "isomorphic to an induced subgraph" is an induced embedding ↪g. Subdivisions and enlargements range over graphs on Fin k.Fin m, Fin n.Dropping the bars of the complement would make the theorem false or vacuous. So would reading "path" as a non-induced path, or encoding a decomposition so that it always exists. The statements use the complement explicitly, induced paths throughout, and the full definitions of p. 53–54.
The proof of 9.6 also uses results of the same paper that are posed in other missions of this series. These are 2.1, 2.2, 4.1 and 4.2, posed in mission II (skew partitions), and 5.3, 5.8, 6.1 and 7.5, posed in mission III (line graphs). They are not posed again here. The bridge 9.2 between knots and line graphs, whose proof the paper omits as obvious, is not posed either. Proofs of 9.1, of 9.3, and reusable lemmas about knots and striations are welcome.
Finite-horizon stochastic control on general state and control spaces — inventory levels, queue lengths, positions, beliefs — cannot be written down without measure theory, and the measure theory turns out to be the hard part. The dynamic programming (DP) recursion "start from zero and minimise one stage at a time" is easy to state, but on uncountable spaces the minimisation in each step produces functions that need not be Borel-measurable, and the infimum over policies has to be taken over a class large enough to contain near-minimisers. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978; Athena reprint 1996) resolved this by working with universally measurable policies and lower semianalytic costs. Chapter 8 is the finite-horizon core of that theory, and the infinite-horizon results of Chapter 9 and the imperfect-information reduction of Chapter 10 are built on it.
Timeline. Blackwell (1965) treated discounted problems on Borel spaces with bounded costs and Borel policies, where ε-optimal Borel policies may fail to exist. Strauch (1966) studied positive and negative models. Blackwell, Freedman and Orkin (1974) introduced analytic sets and analytically measurable policies into DP. Bertsekas and Shreve (1978, Chapters 7–8) gave the universally measurable finite-horizon theory formalized here, including the unbounded-cost assumptions (F⁺)/(F⁻).
A finite horizon stochastic optimal control model is a nine-tuple . The state space , control space and disturbance space are nonempty Borel spaces (topological spaces homeomorphic to Borel subsets of complete separable metric spaces). The constraint is nonempty and is analytic in . Disturbances are drawn from a Borel stochastic kernel , the system moves by with Borel, the discount factor is a positive real, the one-stage cost is lower semianalytic ( is analytic for every real ), and is the horizon. The state transition kernel is .
A set is universally measurable if it is measurable for the completion of the Borel σ-algebra under every probability measure. A policy chooses from a universally measurable stochastic kernel concentrated on ; it is Markov if depends on only, and nonrandomized if every is a point mass. denotes all policies and the Markov ones. A policy and an initial distribution determine a probability measure on state–control paths, and the -stage cost and optimal cost are
Assumption (F⁺) requires , and (F⁻) requires , for every policy, initial state and stage, where is the marginal of on the -th pair. The DP operators are
under (F⁺) or (F⁻), where . The goal leaves the horizon, the discount factor and the sign of unrestricted beyond (F⁺)/(F⁻), and it compares an infimum over all history-dependent randomized policies with a pointwise recursion.
In attack order: Lemma 8.1 (the cost of a Markov policy equals ), Proposition 8.1 and Corollary 8.1.1 (Markov policies suffice), Lemma 8.2 (an ε-optimal universally measurable kernel for one application of ), Lemma 8.3 (under (F⁺), ), Lemma 8.4 (monotone and bounded convergence for ). Two consequences of the goal complete the chapter's existence theory: Corollary 8.2.1 ( is lower semianalytic) and Proposition 8.3 (ε-optimal nonrandomized Markov policies under (F⁺); nonrandomized semi-Markov and randomized Markov ones under (F⁻)).
Proposition 8.2 says the DP algorithm computes the true optimal cost of the Borel model, with no restriction to Markov or nonrandomized policies and with costs that may be unbounded in either direction. Corollary 8.2.1 identifies the regularity of the value function — lower semianalytic, possibly not Borel (Example 1 of Chapter 8) — and Proposition 8.3 turns the recursion into near-optimal policies. These results are the base case for the infinite-horizon theory of Chapter 9 (positive, negative and discounted models are analysed as limits of finite-horizon problems) and for the sufficient-statistic reduction of Chapter 10.
All results here are proved in the book. None is formalized: the platform has finite-state, finite-action DP theorems and Borel models with Borel-measurable policies, but no universally measurable policies, no lower semianalytic costs and no Ionescu-Tulcea construction for universally measurable kernels. The mission poses the finite-horizon Borel theory, with reusable infrastructure: the universal σ-algebra, universally measurable kernels, iterated path integrals representing integration against the induced path measure, and the operator calculus on extended-real functions with the convention .
The obvious argument fails at measurability. On countable spaces, Proposition 8.2 follows from the Part I argument: induct on , choose near-minimising controls state by state, assemble them into a policy. On Borel spaces, a pointwise choice of near-minimisers is not a policy unless it is measurable, and is generally not Borel even when and are; Borel policies are too few for -optimal ones to exist. The book's way out needs the selection theorem for lower semianalytic functions (Proposition 7.50), integration of universally measurable functions against universally measurable kernels (Propositions 7.45–7.46), and care with infinite values: without (F⁺) or (F⁻), the integral of the stage sum and the sum of the stage integrals can disagree, and Lemma 8.1 fails.
Lean conventions:
[TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [IsBorelSpace X] [Nonempty X]. IsBorelSpace is the book's Definition 7.7.EReal. Addition inside costs and integrands uses the book's convention (badd), not Mathlib's, which gives . Integrals are with (extInt).universalSigma). Kernels are universally measurable in the sense of Lemma 7.28(b).pathInt).A trivializing formalization is excluded by construction. is the infimum over all policies in , not over Markov or nonrandomized ones. is the integral of the stage sum against the path measure, never the operator composition of Lemma 8.1, so the goal does not collapse to the Part I result.
A complete development needs:
This infrastructure is reusable for the infinite-horizon Borel models (Chapter 9), for the imperfect-information reduction (Chapter 10), and for papers that cite this book. Contributions of these supporting lemmas as separate theorems are welcome.
In 1935 Hassler Whitney asked which properties of linear dependence among the columns of a matrix can be stated without reference to the matrix at all. His answer, On the Abstract Properties of Linear Dependence (American Journal of Mathematics 57, 1935), introduced the matroid: a finite set together with a rank function obeying three short postulates. The notion now underlies combinatorial optimization (the greedy algorithm is optimal exactly on matroids, and matroid intersection and partition generalize bipartite matching and arborescence packing), graph theory (graphic and cographic matroids), coding theory and the study of linear representations over finite fields.
A defining feature of the subject is that the same structure can be axiomatized in several apparently unrelated ways: by rank, by independent sets, by bases, by circuits. Each axiom system is convenient for different arguments, and passing between them, a so-called cryptomorphism, is routine in practice. Whitney's paper is where these equivalences first appear. Part I, §§2–4 and §6 (pp. 510–514), derives the basic properties of rank from the rank postulates, deduces from them the postulates for independent sets, and shows that the two systems are equivalent. This mission formalizes that first equivalence.
Let be a finite set of elements . Following Whitney, write for , for the union and for the intersection of subsets; is the number of elements of .
A rank system is a function on the subsets of satisfying
The nullity of is , and is independent when . The increment of (3.1) is , written when .
An independence system is a predicate "independent" on the subsets of satisfying
From an independence system one recovers a rank by letting be the number of elements in a largest independent subset of . In the Lean development these objects are IsRankSystem, nullity, Delta, indepOfRank, IsIndepSystem and rankOfIndep, all in the namespace WhitneyMatroid.RankIndep.
Both translations and both round trips are part of the goal: Whitney's conclusion is not only that each system implies the other but that "the definitions of the rank and the independence or dependence of any subset of agree under the two systems".
The equivalence makes the rank function and the family of independent sets two descriptions of one object. Every later result of Whitney's paper, and of matroid theory generally, moves between them without comment: the circuit postulates of §5 and §8, the base postulates of §7 and the duality of §§11–13 are all phrased through rank or independence as convenient. Theorem 3 is the submodularity of rank, the property that connects matroids to submodular function minimization and polymatroids; here it is derived from the purely local postulates (R₁)–(R₃), which constrain the rank only under the addition of one or two elements.
On the formal side, Mathlib defines Matroid through independent sets (with constructors from other axiom systems) and proves submodularity of its rank; the platform has submodularity for Mathlib matroids (FamousTheorems.matroid_rank_submodular_7a). Neither starts from Whitney's local rank postulates. What this mission adds is a machine-checked derivation of the global properties of rank from (R₁)–(R₃) and of Whitney's original equivalence, stated for his own postulates, so that the later missions of this series, which work from the same postulates, rest on a verified foundation. The result itself has been settled since 1935; the open work is the formal proof.
The postulates (R₂) and (R₃) are local: they speak about adding at most two elements to a set. Monotonicity and the bound follow by adding elements one at a time, but the submodular inequality relates arbitrary sets, and nothing in (R₃) mentions more than two new elements. The gap between the local and the global statement is the substance of Lemmas 3, 4 and Theorem 3, and the deduction of (I₂) depends on it.
In the converse direction the rank is defined as a maximum over independent subsets, while (I₂) only augments a set from an independent set with exactly one element more; (R₃) for the derived rank is a statement about three sets that are not given in that form. The round trips are where the two halves meet, and each depends on the global properties of the first half rather than on the postulates alone.
Elements form a type α with [Fintype α] [DecidableEq α]; subsets are Finset α, and the matroid is the whole type. Ranks, nullities and increments take values in ℤ, so differences never truncate; Whitney allows any number, but (R₁) and (R₂) force nonnegative integers. Postulate (I₂) is stated in Whitney's form with N'.card = N.card + 1, not the general augmentation for . Postulates (R₂), (R₃) keep their hypotheses . Lemmas 3, 4 and Theorem 3 are stated for arbitrary subsets ; Lemma 1's monotonicity for arbitrary , the form in which the paper uses it. rankOfIndep is the supremum of cardinalities over the independent members of the powerset.
The paper takes for granted that the empty set is independent in system (I). Without that hypothesis, the predicate declaring nothing independent satisfies (I₁) and (I₂) vacuously, the supremum defining the rank returns , and the round trip fails; the goal therefore assumes independent in part 2 and proves it in part 1. A formalization in terms of Mathlib's Matroid would make the goal a restatement of library facts, since Mathlib's matroids are independence systems by construction; the goal is deliberately about the postulates as predicates on functions and on families of sets.
A complete development needs only finite set combinatorics (Finset.card, induction on finite sets, Finset.sup). The derived lemmas (monotonicity, submodularity, (I₂)) are reusable for any later work from Whitney's rank postulates, including the circuit-postulate equivalence of the companion mission. A bridge from rank systems to Mathlib's Matroid (via IndepMatroid.ofFinset) would be a welcome addition but is not part of the goal. Proofs of the milestones in any order are welcome; Theorem 3 and the §4 deduction are the natural first targets.
Mathlib.Data.Matroid (matroids via independent sets; IndepMatroid.ofFinset). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matroid/Basic.htmlAbstract dynamic programming, in the form developed by Denardo (1967) and Bertsekas (1977), studies sequential decision problems through a single monotone mapping : the cost of using control at state when the future is valued by the function . Chapters 2–5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), analyze this model when policies are arbitrary selectors and is defined on all extended-real functions on .
That generality breaks down as soon as the state and control spaces are uncountable. A stochastic control problem on Borel spaces needs measurable policies, so that the expected cost is an integral rather than an outer integral, and the functions on which acts must be measurable for the same reason. Chapter 6 of the book introduces a generalized abstract model in which the policies are drawn from a prescribed class and is only defined on a prescribed class of functions. The examples on p. 94 are the models of Part II: universally measurable policies with lower semianalytic costs (Chapters 8–9), analytically measurable policies (Section 11.2), and the semicontinuous models of Definitions 8.7–8.8. Chapter 6 is the bridge that lets the abstract results of Part I be invoked for these models.
The data are a state space , a control space , nonempty constraint sets , and three restricted classes: sets of functions , where is the set of all functions , and a set of selectors with . The mapping is monotone: in implies . For and ,
A policy is a sequence with every ; their set is . Given with , the -stage and infinite-horizon costs are
and the optimal costs are and . For a stationary policy write .
Five standing conditions tie the classes together: A.1 (every control is the value of some ), A.2 ( is closed under and under adding constants), A.3 ( is closed under every , , and under adding constants), A.4 (-minimizing selectors for , , exist in ), and A.5 ( and are closed under pointwise limits). Assumption asks for a closed subset of the space of bounded real functions with the sup norm , containing and invariant under on and under on , such that every exists and is real, each is -Lipschitz on , and every -fold composition is a -contraction on for some .
Under A.1–A.5 and : is the unique fixed point of in , with and ; each , , is the unique fixed point of in ;
a stationary is optimal iff ; and for every some stationary policy in satisfies .
In attack order:
The other results of Sections 6.2–6.3 are posed in the mission as separate theorems:
Proposition 6.4 is the statement that makes value iteration, Bellman's equation and stationary -optimal policies available for discounted problems whose admissible policies are restricted, for instance to measurable ones. Without it, each measurable model would need its own fixed-point argument. The finite-horizon Propositions 6.1–6.3 play the same role for the dynamic programming algorithm , and their hypotheses (, exact selection) are exactly what Chapters 7–8 verify for universally measurable policies.
The book states Propositions 6.4 and 6.5 without proof (p. 97), referring to the proofs of Chapter 4; Propositions 6.1–6.3 are justified by "nearly verbatim repetition" of Chapter 3. A formalization therefore supplies proofs that are only indicated in print, and checks that A.1–A.5 really suffice for each step of the Chapter 3–4 arguments. None of these results has a machine-checked proof that we know of; the companion missions of this series formalize the unrestricted special case (, ) of Chapters 3 and 4.
The Chapter 4 proof of Proposition 4.2 applies the contraction mapping theorem to on . Here the obvious transcription fails at two points. First, maps into itself but only maps into itself, so the fixed-point theorem must be applied on two different sets, and these are closed only because of A.5. Second, every argument that picks a near-minimizing selector at each state must produce a selector in : pointwise choices are no longer allowed, and A.1, A.4 and the exact selection assumption are the only sources of admissible selectors. Proofs of Chapter 3–4 that build a policy state by state cannot be copied.
Functions on are S → EReal. is a total Lean function, but monotonicity is assumed only on and every statement evaluates only at functions of . is limUnder; Assumption makes the limit exist. is Mathlib's ; a bound between extended-real functions means both are real everywhere and , which is how the book's convention reads a norm of a difference. No statement adds values of opposite infinite sign, so Mathlib's EReal addition agrees with the book's wherever it is used. and are infima over only, the -optimality notions keep the book's two-case form at , and is a positive integer.
The chapter collapses to Chapters 3–4 if or is built in; here , and are arbitrary and constrained only by A.1–A.5, and is never defined as a fixed point.
A complete development needs the -step contraction mapping theorem on a closed subset of , monotonicity lemmas for and , and the restricted-class versions of Propositions 3.1–3.4 and 4.1–4.4. These are reusable for the Borel models of Chapters 8–9. Proofs of any milestone, and sorry-free lemmas about the Assumption contraction, are welcome.
A perfect graph is a finite simple graph in which every induced subgraph has chromatic number equal to its largest clique size. This equality gives a structural reason that a clique lower bound on the number of colours is attainable for every induced part of the graph. Berge proposed a forbidden-subgraph description of perfect graphs: a graph should be perfect exactly when it has neither an odd hole nor an odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved that statement in The strong perfect graph theorem, Annals of Mathematics 164 (2006), Theorem 1.2. Their proof separates possible configurations in a Berge graph and shows that each either belongs to a controlled class or admits a decomposition.
This mission isolates the even-prism step, Theorem 10.6 of that paper. A prism is one of the configurations that can appear in a Berge graph even though odd holes and antiholes do not. The step matters because its conclusion leaves only a specific nine-vertex graph or one of two decompositions that the larger proof handles elsewhere. It is the result identified as step 1.8.4 in the authors’ outline (paper, pp. 59 and 124).
All graphs here are finite and simple. A path means an induced path; a single vertex is allowed as a path of length zero. A hole is an induced cycle with at least four vertices, and an antihole is a hole in the complementary graph. A graph is Berge if every hole of and of its complement has even length.
A prism has two disjoint triangles, and , joined by three pairwise vertex-disjoint induced paths from to . Between distinct paths, the only edges are those in and those in . The prism is even when all three have even length. “ contains an even prism” means that such paths exist as an induced configuration in ; may have other vertices. “ is an even prism” means the paths cover every vertex of (paper, pp. 93 and 119).
An appearance of is an induced copy in of the line graph of a bipartite subdivision of the four-vertex complete graph. It is nondegenerate if no four-cycle of contains all four branch vertices. Only appearances in are excluded in this mission; appearances in are allowed by the hypotheses (paper, pp. 72, 74–75).
A proper 2-join partitions the vertices into two sides with specified, nonempty attachment sets. The cross edges are exactly the two complete attachment pairs; every component of either side meets both of its attachment sets. If a side is itself a path between singleton attachment sets, that path has odd length at least three. A balanced skew partition divides the vertices into and so that is disconnected, is disconnected in the complement, and two path parity conditions hold: no odd path crosses between nonadjacent vertices of , and no odd antipath crosses between adjacent vertices of (paper, pp. 53–54).
The numbered milestones are Theorems 7.2–7.4 and 10.5. They assert common parity of the three prism paths, common neighbours of an anticonnected set at both end triangles, preservation of two neighbours under replacement of one even prism path, and the balanced skew partition forced by a major vertex. A vertex is major when it is adjacent to at least two vertices of each end triangle. These milestones match the paper’s statements on pp. 93 and 123 (paper).
For a Berge graph with no nondegenerate appearance of in ,
The first case describes the entire graph, not just an induced nine-vertex subgraph. The statement fixes all outcomes exactly as in Theorem 10.6, p. 124.
Theorem 10.6 removes even prisms from the unresolved part of the strong perfect graph theorem’s structural argument. If the graph is larger than the exceptional prism and has no nondegenerate appearance, the theorem supplies a proper 2-join or a balanced skew partition. Subsequent results can work with those decompositions instead of treating arbitrary attachments to a prism (paper, §10 and the outline at 1.8.4).
The mathematical result is proved in the 2006 paper. The work here is to give its graph objects and statements machine-checkable meanings, then formalize the known proof. This proposal contains open Lean theorem statements and sorry-free definitions; the proof obligations remain for solvers. The definitions of induced paths, holes, subdivisions, and decomposition predicates can also support other steps of this paper. The Roussel–Rubio lemma and the balanced-skew-partition results of §§2–4 are proved in the same paper and posed in mission II of this series. The prism-attachment result 10.4 is posed in mission VI, where it is used most directly.
An outside connected set can attach to several parts of a prism without containing a single major vertex. Its attachments need not be local to one path or one triangle, so checking vertices one at a time does not decide which decomposition exists. The paper’s §10 distinguishes several attachment patterns; the evenness of the paths and the exclusion of a nondegenerate appearance restrict them, but do not themselves give a 2-join or skew partition by a one-line parity argument. The larger proof must also account for attachments throughout the graph while preserving the full definitions of both decomposition outcomes (paper, pp. 119–127).
Lean represents a graph as SimpleGraph V with a finite vertex type. The prism is three lists of vertices, each an induced path; the lists are disjoint, and the cross-edge condition admits exactly the two end triangles. Reversing a list changes its orientation but not the underlying graph configuration. A hole uses a cyclic list with the closing edge; Berge checks holes in both and . Connectivity is reachability in an induced graph, so the empty vertex set is connected as the paper says. A subdivision uses six tracks on a finite carrier, with all its vertices and edges accounted for; the appearance uses an induced graph embedding of its line graph. The exception checks that the prism covers the whole graph and that .
These encodings require genuinely induced paths and the paper’s nondegenerate appearance condition. Dropping either would change the theorem. The proper 2-join includes component reachability and the odd-path special case; the balanced skew partition includes both path parity clauses. The nine-vertex graph formed by two triangles and three two-edge paths has a separate sorry-free Lean witness, so the exceptional outcome is nonvacuous. Useful contributions include the numbered prism lemmas, attachment analysis for 10.6, and reusable results about finite induced paths and graph subdivisions.
Linear programming, with , is the basic model of operations research, and the complexity of solving it is a central question of algorithm theory. Interior-point methods follow the central path: primal–dual pairs with and for every , as the path parameter decreases to . A classical short-step method needs iterations, each solving a linear system with the matrix , for a total of roughly operations or more.
Cohen, Lee and Song (J. ACM 68(1), 2021; arXiv:1810.07896) showed that linear programs can be solved in time (for the current values of the matrix multiplication exponent and its dual ), matching the cost of multiplying two matrices. The analysis has two halves: a data structure that maintains the projection matrix lazily, and the stochastic central path method, which replaces each Newton step by a sparse random step and proves that the iterates still stay close to the central path. This mission formalizes the second half.
Timeline: Karmarkar's projective method (1984) gave the first polynomial interior-point method; Renegar (1988) gave the path-following bound; Vaidya (1989) reduced the per-iteration cost with low-rank updates; Lee and Sidford (2014–2015) reduced the iteration count to ; Cohen, Lee and Song (STOC 2019, J. ACM 2021) reached ; van den Brand (2020) derandomized the result.
Vectors are in and products, quotients and roots of vectors are coordinatewise. For and vectors , means for all ; for a scalar is defined likewise. The number of variables is and has full row rank .
The potential is , evaluated at with ; it is small exactly when every is close to .
StochasticStep (Algorithm 1) takes positive , a direction , a sampling parameter and the output of a data structure with . It rescales to , (), draws a sparse vector with independent coordinates, with probability and otherwise, and computes the step through the projection . The draw is repeated until and are at most ; the output is .
Main (Algorithm 2) sets , , , , starts at , and in each iteration sets , takes the direction
runs StochasticStep, and falls back to a deterministic ClassicalStep whenever .
For every iteration , almost surely Assumption 4.1 holds for the input of iteration (in particular and ), almost surely the resampling loop of iteration succeeds with positive probability, and
The paper writes ; its proof gives the constant .
Lemma A.1 (variance of a product), Lemma 4.12 (properties of ), Lemma 4.2 (explicit step), Lemma 4.3 and Claim 4.7 (moments and success probability of the sampled step), Lemma 4.8 (moments of ), and Lemma 4.13:
Lemma 4.14 is what makes the randomized method usable: the iterates stay in the -neighbourhood of the central path along the whole run, and the expensive fallback is rare enough that its expected cost, , is negligible. The paper's cost bound (Lemma 4.16) and its main theorem rest on it. The same potential-based "stochastic central path" analysis was reused in later solvers, for instance for empirical risk minimization (Lee, Song and Zhang, COLT 2019).
The result is proved in the paper; no machine-checked version exists. A formalization pins down the probabilistic model that the paper leaves implicit (independence of the sampled coordinates, the law of the resampling loop, a data structure and fallback that see only the past) and checks the constants, several of which are tight against printed slack (Remark 4.4).
The running-time claims of the paper (Theorem 2.1's expected time , Lemma 4.16, Section 5) are not part of this mission: they live in an arithmetic cost model that Lean does not have. The accuracy guarantee of Theorem 2.1 (Lemma A.6, ClassicalStep from [57]) is also outside the mission.
The obvious argument would bound each quantity under the product law of the sparse direction. But StochasticStep resamples, so the step actually taken is distributed according to that law conditioned on a success event, and expectations and variances shift. A second difficulty is that is controlled only in expectation, while Assumption 4.1 must hold surely at every iteration; this is reconciled by the deterministic ClassicalStep fallback, which caps at , and by an induction over iterations of under the trajectory law. Claim 4.7 needs a Bernstein inequality, which Mathlib does not yet provide.
Coordinates are Fin n, vectors Fin n → ℝ, a Matrix (Fin d) (Fin n) ℝ with A.rank = d, and the natural logarithm. is written out as ; is stated coordinatewise. The sampled direction has law Measure.pi of two-point laws; the step taken by StochasticStep has that law conditioned (ProbabilityTheory.cond) on the success event, and every , of Lemmas 4.3, 4.8 and 4.13 is under this conditioned law. mp.Query is replaced by its value ; the data structure and ClassicalStep are arbitrary measurable functions , of the history with the only properties the paper uses. The trajectory is Mathlib's Ionescu-Tulcea measure, with kernels equal to the step law of Main. is the number of variables of the program the loop runs on.
Deviations from the page, all recorded in the items: Assumption 4.1 is used with instead of the printed , because Main sets to exactly that value; is instantiated as , the constant of the paper's proof; the conclusions of Lemma 4.14 are stated for every iteration index rather than while ; at the second term of is . No hypothesis is imposed.
A trivializing formalization is ruled out: every statement that integrates against the conditioned law also concludes that this law is a probability measure (so it cannot be the zero measure), the goal concludes that each resampling loop succeeds with positive probability, the oracles , cannot see the coins of the current iteration, and the goal is about the whole iterated process from the initial point, not one step from an arbitrary law.
Contributions welcome: a Bernstein inequality for bounded independent sums, conditional-law lemmas for cond of Measure.pi, and Markov-kernel measurability for the step law; these are reusable beyond this mission.
The neutral theory of molecular evolution holds that much of the genetic variation observed at the molecular level is caused by selectively neutral mutations rather than by selection. To test it against data one needs the distribution of allele frequencies that a neutral model predicts, and in practice that distribution has to be compared with a sample from the population, never with the whole population. Ewens (Ewens 1972) derived the equilibrium distribution of allele counts under the infinite alleles model, now called the Ewens sampling formula; it underlies classical tests of neutrality and appears throughout combinatorics and probability as the law of the cycle type of an Ewens-distributed random permutation and of the Chinese restaurant process.
Chapter 7 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) obtains the infinite alleles model as a limit of the reversible migration processes of Chapters 2 and 6, and uses reversibility to answer questions about allele ages and fixation. The mission formalizes the finite, combinatorial results of that chapter.
Timeline. Kimura and Crow (1964) introduced the infinite alleles model. Ewens (1972) found its equilibrium sampling distribution (7.6). Kingman (1978, J. London Math. Soc.) characterized the consistency of random partitions under sampling, the property Theorem 7.1 asserts for the Ewens family. Kelly (1979, Chapter 7) derived (7.6) as a limit of reversible migration processes, and the consistency and the allele-age results from the reversibility of a labelled population process.
A population consists of individuals, each carrying an allelic type. Its description is , where is the number of allelic types carried by exactly individuals, so that
For a real parameter , the Ewens distribution on descriptions is
where is the binomial coefficient for real . In the infinite alleles model, individuals die at rate , each death is followed by the birth of an offspring of a uniformly chosen survivor, and the offspring is a mutant of an entirely new type with probability ; then (7.6) is the equilibrium distribution with (7.5).
A random sample of size without replacement is a uniformly random -element subset of the labelled individuals, each of the subsets being equally likely; the sample has a description in the same sense.
The number of individuals carrying one given allele performs a random walk on with intensities
An allele is quasi-fixed when it is the only allele present ().
If and the population description is distributed as , then a random sample of size drawn without replacement has description with probability , the same being used for both sizes:
The results. Consistency under sampling is what makes the Ewens formula usable as a statistical model: the predicted distribution for an observed sample does not depend on the unknown population size, only on . Kelly deduces from it the sufficiency of the number of alleles in a sample for and the heterozygosity (Exercises 7.1.5, 7.1.8). The formula (7.9) gives the equilibrium frequency of the oldest allele, and Theorem 7.9 gives the quasi-fixation probability from which the mean time between quasi-fixations follows (Corollary 7.10).
Formalizing them. All four results are classical and proved; none has a machine-checked proof on the platform or in Mathlib as of this writing. The mission produces a reusable formal Ewens distribution over integer partitions, a definition of sampling without replacement by counting labelled subsets, and an absorption probability for an explicit birth–death walk. Proofs independent of Kelly's process argument are welcome.
The book's proof of Theorem 7.1 is a process argument: in a population whose size fluctuates between and , a drop in size acts as a random deletion, and the truncated equilibrium (7.7) restricted to each size gives and . Turning that into a statement about finite sets requires the equilibrium of a truncated reversible process, which is not available here, so a formal proof must either build that process or find a direct combinatorial route. A direct route has to relate, for each description of the sample, the number of -subsets of a labelled population with a given description to products of binomial coefficients, and sum the result against (7.6); the bookkeeping over partitions is where the work lies. Theorem 7.9 needs a solution of the first-step equations of a non-symmetric walk and the identification of that solution with a hitting probability defined as a limit.
Nat.Partition n, with the multiplicity of the part ; the product in (7.6) runs over . The real binomial coefficient is the published definition AppliedComb.GenFun.binomReal.Fin M with allelic types Fin M → ℕ; the description of a labelled set is computed from the labelling. The sampling probability is times the number of -subsets whose restricted labelling has the given description. It is not defined by a formula on descriptions, and a definition that removed individuals one at a time in proportion to class sizes (the book's proof route) is ruled out as a definition because it presupposes the reduction the proof must supply.Contributions of general partition and sampling lemmas (counting subsets with a given description, the generating function identity ) are reusable beyond this mission.
A graph is perfect if every induced subgraph has chromatic number equal to its clique number, and Berge if no induced subgraph is an odd cycle of length at least five (an odd hole) or the complement of one (an odd antihole). Berge conjectured in 1961 that the two classes coincide. Chudnovsky, Robertson, Seymour and Thomas proved this, the strong perfect graph theorem, in Ann. of Math. 164 (2006), 51–229. Perfect graphs matter beyond graph theory. A graph is perfect exactly when its stable-set polytope is defined by clique inequalities (Chvátal; Lovász), so the theorem characterizes the graphs on which the stable-set and colouring integer programs are solved by their linear relaxations.
The proof is a structure theorem. Every Berge graph is basic (bipartite, the complement of a bipartite graph, the line graph of a bipartite graph or its complement, or a double split graph), or it admits a proper 2-join, a proper homogeneous pair or a balanced skew partition. The proof splits into twelve steps (1.8.1–1.8.12, p. 59), each about Berge graphs that contain a particular configuration. This mission is the first step, statement 5.1 of the paper. It covers Berge graphs that contain a large line graph, and it takes up Sections 5–8 (pp. 72–107).
All graphs are finite and simple. For a graph , is its complement. A path is an induced path, and its length is its number of edges. A track is a path in the conventional, not necessarily induced, sense. A set is connected if is connected, and anticonnected if is connected.
The line graph of a graph has vertex set , and two edges are adjacent when they share an end. is a line graph if for some graph . A subdivision of a graph replaces each edge of by a track from to , the tracks being disjoint except for their ends. A branch-vertex is a vertex of degree at least . A branch is a maximal track whose internal vertices are not branch-vertices. is 3-connected if it has more than three vertices and no set of at most two vertices disconnects it.
For a bipartite subdivision of , is degenerate if some 4-cycle of passes through its four vertices of degree three. A graph appears in if is isomorphic to an induced subgraph of for some bipartite subdivision of .
Two decompositions occur in the conclusion. A skew partition is a partition of with not connected and not anticonnected. It is balanced if no odd path joins two nonadjacent vertices of through , and no odd antipath joins two adjacent vertices of through . A proper 2-join is a partition of with nonempty disjoint such that:
The development needs further objects, each defined on its page: saturating edge sets and major vertices (pp. 77, 81), overshadowed appearances (p. 85), -enlargements (p. 75), and -strip systems with their rungs (p. 98).
Let be Berge and let be a bipartite subdivision of such that is nondegenerate and is an induced subgraph of . Then
The proposal also contains 5.2 (p. 73, step 1.8.2: Berge graphs containing ) and 5.3 (p. 74) as theorems without milestones.
5.1 is the line-graph step of the decomposition theorem. It turns "contains a substantial line graph" into "is a line graph or decomposes". The later steps of the proof start from the complementary case, where no such appearance exists (degenerate appearances in §9, prisms in §§10–13). The strip-system technique of §8 can be reused: it assembles all alternative rungs of a line-graph appearance and analyses how the rest of the graph attaches to it.
The strong perfect graph theorem is proved, but to our knowledge no proof assistant has a machine-checked proof of it. This mission formalizes one of its twelve structural steps. Several results of the same paper that the proof of 5.4 uses are posed in other missions of this series and are not posed here:
The statements 5.5, 5.6, 5.8, 8.3, 8.4 and 8.5 are also used in the proof. They are open to solvers as further lemmas.
Knowing that contains some appearance of is not enough to make a line graph or to decompose it. Vertices outside the appearance can attach to it in many ways. Each such pattern has to be shown to be impossible in a Berge graph, or to yield a larger appearance of a bigger graph , or to yield a decomposition. The first idea, analysing one outside vertex at a time, fails for two reasons. Connected sets of "minor" vertices can attach non-locally even when each vertex alone attaches locally (5.8). And anticonnected sets of "major" vertices are what produce the skew partitions (6.1). The small cases make things harder: , and degenerate subdivisions of are basic in several ways at once, so the theorem fails for them without the nondegeneracy hypothesis.
Graphs are SimpleGraph V on a Fintype. is Gᶜ. is Mathlib's H.lineGraph on H.edgeSet. " is an induced subgraph of " is an induced embedding H.lineGraph ↪g G, and "" says that this embedding is surjective. Paths and holes are vertex lists with the induced-adjacency condition. Tracks are vertex lists with consecutive vertices adjacent; their adjacency is not induced. Subdivisions carry an injection of and one track per edge of . These tracks are internally disjoint, avoid internally, and cover every vertex and every edge of . "3-connected" includes the paper's convention of more than three vertices. "", "" mean isomorphism. Existentially quantified graphs ( in an appearance, the enlargement , the graph of which is a line graph) live on Fin n.
The standing assumptions are those of each statement: is Berge and is 3-connected. In 7.1 the two edges are taken distinct, as the conclusion requires. "Up to symmetry" in 6.1 becomes an existential choice of the labelling of the 4-cycle and of the order of .
The formalization would be trivial if paths were allowed to be non-induced, if the complement bars in 5.4 and 6.1 were dropped, or if a "subdivision" could share internal track vertices or carry extra vertices or edges. The definitions rule out all three. A sorry-free check shows that is a subdivision of itself and is not bipartite.
Reusable infrastructure: tracks, branches, subdivisions, 3-connectivity, appearances and strip systems. Contributions are welcome on the graph-theoretic lemmas 5.3 and 7.1, which do not need Berge graphs, and on the Berge-specific milestones in the order listed.