Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many decision problems have set-valued outcomes rather than single numbers. Typical cases are a portfolio whose risk is a set of capital vectors, a vector optimization problem whose image is upper-bounded by an ordering cone, or a robust model whose value is the set of all achievable outcomes. Set optimization minimizes such a map . The first difficulty is how to compare two sets. In the complete lattice approach of Heyde and Löhne (2011) and of the survey by Hamel, Heyde, Löhne, Rudloff and Schrage (2015), the values are taken in a complete lattice of sets, so that infima exist. A solution is then a set of arguments that attains the infimum and consists of minimal points.
Crespi, Hamel, Rocca and Schrage (arXiv:1812.03300v1, published in Mathematics of Operations Research, 2021) generate both the set relation and the lattice from an arbitrary family of monotone scalar functions on a preordered set. The construction needs no linear structure on the image space. It covers vector orders, scalarizations by linear functionals and orders given by indicator functions. On top of it they define approximate solutions with tolerance , and prove a Weierstrass-type existence theorem: compactness of approximate minimizer sets yields exact solutions, and the approximate sets converge to the exact ones in the Hausdorff sense.
Let be a preordered set and . Let be a family of monotone functions , so that implies .
For a map on a non-empty set , the problem is
and for . For and , let if and , with .
In §4, is a separated (Hausdorff) topological linear space over .
Let and , and suppose is compact for all . Then is non-empty and compact, and for every neighbourhood of and all sufficiently small
If, additionally, every is lower semicontinuous, then is non-empty and a -solution of (P).
The theorem is the existence result of the paper's framework. It turns a compactness condition on approximate minimizer sets into an exact solution in the sense of Definition 3.7: a set of arguments that attains the lattice infimum and consists of minimizers. The Hausdorff convergence statement is a well-posedness result: approximate minimizers computed with a tolerance lie close to exact -minimizers when is small. The framework applies to vector optimization with a cone order, to set-valued risk measures and to orders given by indicator functions, all as instances of the same .
The results are proved in the paper. None of them is formalized on the platform or in Mathlib, which has neither set relations nor lattice-valued solution concepts. This mission produces machine-checked statements of the lattice of Ψ-closed sets, inf-stability, approximate solution concepts with their conventions, and the existence theorem. Later set optimization missions can build on these definitions.
The individual arguments are short. The work lies in the extended-real bookkeeping and in using the lattice structure correctly:
EReal, and the empty infimum is . carries [Preorder Z], and is a Set (Z → EReal) with every member monotone. A map into is f : X → Set Z together with the hypothesis that every value is Ψ-closed. The lattice structure is therefore Proposition 2.3, not a built-in instance.The development needs extended-real infima, lower semicontinuity into EReal, and Cantor's intersection theorem for nested compact sets in Hausdorff spaces, all available in Mathlib. The definitions of inf-extension, Ψ-hull, set relation and approximate solutions are reusable beyond this paper. Proofs of any milestone, and of alternative routes to the goal, are welcome.
Hiring decisions often rest on a recommendation from someone who knows the candidate: a thesis adviser, a former supervisor, a colleague. Referrals are a common channel of labor market matching, and their value depends on whether the recommender can be trusted. An adviser who cares about his candidate has a reason to overstate the candidate's quality, and the main check on this is the adviser's reputation: a recommendation that turns out badly costs the adviser future credibility.
Câmara, Jia and Raffiee (2023) study this trade-off in a one-period recommendation game in which reputation enters as a state variable, and ask a question about matching between advisers and firms: which firms are more likely to hire the candidates of strong-reputation advisers? Their answer is that it depends on the shape of the firm's outside market, not only on its average quality. This mission formalizes that result, together with the equilibrium characterization it rests on.
A focal candidate has skill , , high with probability ; the average skill is . An adviser with reputation privately observes and a personal bias , distributed on with a continuous CDF of full support. He sends a message (recommend or not). A firm privately observes the value of an outside candidate, distributed on with a continuously differentiable CDF , density and full support, and hires either the focal candidate (payoff equal to the candidate's skill) or the outside one (payoff ).
If the adviser recommends a high-skilled candidate who is hired, his reputation rises to ; if he recommends a low-skilled candidate who is hired, it falls to , with ; otherwise it stays at . He receives the reputation payoff of his final reputation, plus if his candidate is hired. The payoff loss from an unsuccessful hire is
and the paper's standing Assumption (A1) is : an adviser with a higher reputation has more to lose. The solution concept is perfect Bayesian equilibrium with two tie-breaks: an indifferent firm hires the focal candidate, and an indifferent adviser does not recommend a low-skilled candidate.
In equilibrium a low-skilled adviser lies (recommends) exactly when his bias exceeds a threshold , and the firm's belief after a recommendation is
The largest possible benefit from lying is . A market is top-heavy if is strictly increasing, and bottom-heavy if is strictly decreasing.
Let be the ex-ante probability that the firm hires the focal candidate in an equilibrium at reputation . For all and all equilibria at and :
and both inequalities are strict when and . Part (iii) of the proposition, assortative matching, is (i)–(ii) restated.
The result separates two notions of a firm's "strength" that are often conflated: the average quality of its outside options and the shape of their distribution. Two firms with the same average outside candidate can respond in opposite ways to an adviser's reputation. Firms with access to many strong outside candidates (top-heavy) favor candidates of high-reputation advisers; firms whose outside options are concentrated at the bottom favor candidates of low-reputation advisers. The paper uses this to explain assortative matching between strong advisers and strong firms without assuming it, and connects it to the persuasion literature, where the convexity of the sender's payoff in the receiver's posterior determines how much information the sender wants to reveal (Kamenica and Gentzkow 2011).
All results here are proved in the paper, in Appendix A. None of them has a machine-checked proof. A formal development makes precise several points the prose leaves implicit: what "increasing" means where the adviser's behavior stops responding to reputation, that the comparison holds for every equilibrium and not only for a constructed profile, and which regularity of the shape definitions need.
The obvious argument treats the threshold as a known function of and differentiates. Two steps break this. First, is defined implicitly by a fixed-point condition that couples the adviser's incentive with the firm's Bayesian belief, which itself depends on ; existence and uniqueness of the equilibrium, and the threshold form of every equilibrium (not merely of one candidate profile), have to be established before any comparative static makes sense. Second, the hiring probability is not monotone in for every : a higher threshold makes a recommendation more persuasive but rarer, and the two effects cancel exactly for linear . The sign is decided only by the curvature of , which enters through its density, so the definition of top- and bottom-heavy markets has to be related to convexity of the CDF on the support. A further subtlety is that the hiring probability is constant for reputations at which the adviser never lies, so the monotonicity is strict only from reputations with .
All quantities are real numbers. The laws of the bias and of the outside option are probability measures , on with mass one on , no atoms and strictly increasing CDFs on ; and are their CDFs, is on (not on all of , which would force and rule out top-heavy markets), and is the derivative of on . The functions , , are differentiable on , and (A1) is stated as there.
Strategies are pure and Boolean-valued: for the adviser and for the firm, as in the paper's footnotes 15–16. They are required to be measurable, which the paper leaves implicit; message and hiring probabilities are measures of the corresponding sets. Best responses are imposed for every bias in and every outside value in , so uniqueness in Proposition 1 is on those supports. Beliefs lie in and follow Bayes' rule after every message sent with positive probability. The adviser's expected utilities are eqs. (6)–(8), with in (7); the sentence leading into (7) misprints it as .
"Increasing in " in Propositions 2 and 3 is formalized as weakly monotone on together with strict monotonicity from every with ; strict monotonicity on all of is false. The goal quantifies over arbitrary equilibrium profiles at both reputations: a statement about the threshold or about a profile the theorem itself constructs would reduce the goal to milestones 1, 5 and 8 and is ruled out. The standing assumptions are satisfiable together with a top-heavy market (for instance on with uniform bias).
The development needs only Mathlib's measure theory (CDFs from measures), one-variable calculus (monotonicity from the sign of a derivative, convexity from a monotone derivative) and slope inequalities for convex functions. The general facts in milestones 7 and 8 are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative decompositions of Proposition 1.
Not formalized here: the second sentence of Proposition 2 (the firm's ex-ante payoff increases in ), Proposition 4 (the low-reputation trap), Propositions 5 and 6, and the extensions of §5.
Many combinatorial optimization problems are linear programs over a polytope with exponentially many facets, and one way to solve them by a polynomial-size linear program is to write the polytope as the projection of a higher-dimensional polytope with few facets. The minimum number of facets needed is the extension complexity of the polytope. It is now understood for most textbook polytopes: flows, matchings (Rothvoß 2017), arborescences, travelling-salesman tours and stable sets (Fiorini et al. 2015). Matroids are a notable exception.
For a matroid , the independence polytope is the convex hull of the characteristic vectors of the independent sets. Rothvoß showed by a counting argument that many matroids have independence polytopes of exponential extension complexity (Math. Program. 2013), so a polynomial bound can only hold for special classes. Regular matroids, those representable over every field, are the natural class: they contain the graphic and cographic matroids, and Seymour's decomposition theorem describes all of them.
Timeline:
A matroid has a finite ground set and a family of independent sets; . For , is its characteristic vector, and
An extended formulation of a set of size is a system , with exactly inequalities such that if and only if some satisfies the system. The extension complexity is the least such . The paper defines as the minimum number of facets of a polytope projecting onto , and on p. 1 it gives the extended-formulation form as an equivalent definition.
A matroid is regular if it is represented over by a totally unimodular matrix : a set is independent exactly when the corresponding columns of are linearly independent. It is binary if it is represented over . It is graphic if it is the cycle matroid of a multigraph (independent sets are forests) and cographic if its dual is graphic. A cycle is a disjoint union of circuits. For binary , the sum has ground set , and its cycles are the sets , with a cycle of , that lie in that ground set. This sum is a 1-, 2- or 3-sum when the two ground sets share zero, one or three elements, under the side conditions of p. 3. In the 3-sum case the shared set is a triangle, a 3-element circuit of both parts. A matroid is 3-connected if it is neither a 1-sum nor a 2-sum.
The constant is not fixed; the exponent is the paper's. Section 8 of the paper sketches an improvement to without proof, so the goal keeps the proved exponent.
The result. Theorem 1 shows that linear optimization over the independent sets of any regular matroid is a linear program of size polynomial in , written down without any algorithm. Regular matroids are the largest classical matroid class for which such a bound was in question, and the bound separates them from general binary matroids. The proof also gives an extended formulation for the circuit dominant of a regular matroid, a separate result that this mission does not include.
Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs a Lean theory of matroid sums (1-, 2- and 3-sums defined through cycle spaces), decompositions of regular matroids along trees, and extended formulations, with explicit bounds on how the size of an extended formulation behaves under products, intersections with hyperplanes and convex hulls of unions. Seymour's decomposition theorem enters only through Theorem 6, which can be taken as a black box while the polyhedral part is formalized.
The obvious induction fails at 3-sums. For 1- and 2-sums, the extension complexities of the parts add (Lemma 3), and an induction gives a polynomial bound. For a 3-sum, the best known symmetric formulation for has size with (p. 4). A constant larger than 1 compounded over a decomposition tree of logarithmic depth only gives a quasi-polynomial bound, and over an unbalanced tree an exponential one. So the parts of a 3-sum have to be treated differently, and the decomposition tree has to be rebalanced into a star whose leaves have at most about half the elements.
The cographic centre is a second obstacle: the formulation of the centre's part is known only when every triangle shared with a leaf is the set of edges at a degree-3 node of the underlying graph, and getting there requires the decomposition tree of Proposition 27.
Matroid α over one ambient type ; the parts of a sum share elements of (the triangle elements) that are not in . Statements that construct decompositions (Theorem 6, Proposition 27, Lemma 4) take infinite, so that fresh elements exist; otherwise "not a 2-sum" could hold for want of room.IsEFOfSize and extensionComplexity (size = number of inequalities, equations free). Every upper bound is the existence of an extended formulation of the stated size, and bounds in terms of the parts quantify over extended formulations of the parts. This rules out the trivializing reading with an infimum that is on sets with no extended formulation.A seller of a good with network externalities (a social app, a telecom plan, a game console) gains from knowing how strongly each consumer's demand depends on the consumption of others. Candogan, Bimpikis and Ozdaglar (Operations Research, 2012) showed that, on a known network, the optimal price vector of a monopolist and the resulting revenue have closed forms built from the matrix . In practice the network is estimated from data and is never known exactly. A seller who commits to prices on the basis of a forecast then faces revenue that moves with the true network .
Baron, Hu and Malekian (SSRN 3561270, 2020; published as a Technical Note in Operations Research, 2022, doi:10.1287/opre.2022.2302) ask how large that movement can be in the worst case, when the forecast error is bounded in spectral norm. Their Theorem 1 gives an exact answer depending on the network only through its largest eigenvalue. This mission formalizes that theorem, read in the SSRN version of 2020-03-25.
There are agents on a network with , and, as for any network without self-loops, . A parameter scales the peer effect, collects the agents' primary values, and is the seller's marginal cost.
The game has two stages. In the first, the seller chooses a price vector . In the second, each agent chooses a quantity , with utility
A consumption equilibrium is a profile in which each maximizes over . The seller's revenue is , and the optimal revenue is its supremum over all prices and their equilibria. Assumption 1 asks for every ; Assumption 2 asks .
The forecast error is measured by the uncertainty set
with the spectral norm. The seller fixes the price that is optimal for the forecast ; consumers then play the equilibrium on the realized , producing revenue . The revenue volatility is the supremum of the relative change over and . Finally, is the largest absolute value of an eigenvalue of .
Under Assumptions 1 and 2, for every with , every admits an interior consumption equilibrium at the seller's ex-ante price, and
The theorem turns a robustness question about an equilibrium of a game into a single spectral quantity. A seller can read off the worst-case relative revenue change from , and , and compare networks by their largest eigenvalue: denser, more central networks are more exposed to estimation error. The paper uses it to compare chains and complete networks (Proposition 3) and as the deterministic benchmark for its stochastic analysis (Theorem 2).
The result is proved on paper; no machine-checked proof exists. A formalization adds three pieces that are absent from the platform: the network pricing game stated as an equilibrium (not as a closed-form demand), the optimality of the price over all of , and the Neumann series for real matrices under .
The obvious argument substitutes Proposition 2's closed form and bounds a difference of resolvents. Two steps resist this. First, the realized network need not satisfy Assumption 1, so the existence, uniqueness and positivity of the equilibrium on must come from the spectral bound alone. Second, the bound is a supremum of a generalized Rayleigh quotient over , which must be related to the spectral norm of through a constrained-optimization argument. Tightness needs the top eigenvector, which is only non-negative in general, so the supremum is generally not attained in the open set .
The game-theoretic layer is not a formality: Proposition 2 asserts optimality over every price vector, including those at which some agents consume nothing.
Agents are Fin n; vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The norm is Mathlib's scoped spectral norm (Matrix.Norms.L2Operator). is the supremum of over the real spectrum (used only for symmetric matrices), and is computed from the complex spectrum. Condition (1) is written , equivalent to the printed form when , and avoiding Lean's convention .
Conventions added to the page, each disclosed in the items:
The optimal revenue and the revenue on are defined from the game (suprema over prices and equilibria), never by Proposition 2's closed form; a formalization that substitutes the closed form would make Propositions 1–2 vacuous and reduce the goal to a matrix inequality, and is ruled out.
A complete development needs: potential games with concave potentials on , linear complementarity for diagonally dominant matrices, the Neumann series and Perron–Frobenius for non-negative matrices, the spectral theorem for real symmetric matrices, and a Lagrange multiplier rule for a quadratic constraint. The Neumann series criterion and the norm–radius equality for symmetric matrices are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative decompositions of Part 3.
Classical sample-size calculations for a clinical trial fix a significance level and a power and solve for the number of patients. They do not ask what the trial is for. A value-based design asks instead: given what it costs to recruit patients and what a better adoption decision is worth to the patients treated after the trial, how long should the trial run and how fast should it recruit? Health technology assessment bodies such as NICE already decide adoption on cost-effectiveness grounds, and Bayesian decision-theoretic trial design goes back to the value-of-information literature of the 1990s and 2000s (Claxton & Posnett 1996; Chick, Forster & Pertile 2017).
Alban, Chick and Forster (Management Science 2023) make the two decisions explicit, recruitment duration and recruitment rate , and let the regulatory context decide the population that benefits after the trial. Their asymptotic result, Proposition 5, says that the optimal number of patient pairs grows as the square root of that population, and that the optimal expected net gain per post-trial patient converges to a value that does not depend on the switching costs.
A new technology N is compared with a standard S. A fraction of patients is on N before the trial. Patients are randomised in pairs; recruiting at rate for a time yields pairs. The incremental net monetary benefit of N over S has prior , each pair gives an observation , and . After pairs the posterior mean has predictive law with .
After the trial the decision maker adopts N, adopts S, or keeps the current mix, paying fixed switching costs . Without discounting, the expected net gain of a design with is
where is the cost per patient, the setup cost of recruitment capacity, and switches on rewards to trial patients. Without a trial, . The post-adoption population is either a fixed pool, , or set by a fixed horizon, , with incidence and observation delay . The paper also treats discounting at rate ; the asymptotic results take .
Problem (5) maximises over , where Table EC.1 takes and . With and , the paper distinguishes four cases: I (, fixed pool), II (, fixed horizon), III (, fixed pool), IV (, fixed horizon).
Write , for the standard normal density, for the standard normal linear loss, and
Assume and . For every selection of optimal designs, with :
with (Case I) or (Case IV). In Case II the denominator is , and in Case III (corrected, see below) it is . The goal also asserts that optimal designs exist once the population is large.
The closed form (8) of through ; existence of an optimal design (Proposition 1); the reductions to one decision variable (Propositions 2–4); and the four case lemmas EC.1–EC.4 of Appendix C.4, which together give Proposition 5. Lemma EC.4 adds the finer statement that in Case IV both and grow like .
The result turns an optimisation without a closed-form solution into a rule of thumb: for a large population, the optimal trial enrols about patients. The authors show in their ProFHER application that the approximation is accurate at realistic sizes. It also explains two qualitative facts, that fixed-pool and fixed-horizon contexts reach the same value per patient, and that switching costs become irrelevant at scale.
The paper proves these results with asymptotic arguments that are sketched in places ("by rearranging and some additional asymptotic approximations"). A formal proof makes every limit exchange explicit. The formalization also corrects a misprint: the Case III constant in Proposition 5 and the constant in (EC.4) are printed without the setup-cost term , and the proof's own optimality condition shows that it belongs there. None of these results has been machine-checked before; the platform has the normal linear loss and nothing on clinical-trial design.
The objective is not concave in , has a jump where the trial stops running, and its optimiser has no closed form. The square-root law concerns an arbitrary optimiser as the population grows. So it is not enough to differentiate an asymptotic approximation of and solve the first-order condition. One must show that every optimiser escapes every bounded set, that the exact first-order condition holds there, and that the error terms of and of the indifference points and vanish at the right rates. In Case IV two decision variables diverge at different rates, and the fixed horizon couples the trial length to the post-trial population.
All quantities are real. A design is a pair . The post-adoption term of is a Bochner integral against gaussianReal µ0 σZ², and is the published InventoryControl.normalLoss. is defined by the expectation (7) and (9), never by the closed form (8), which is a milestone. Optimality is IsOptOn f S x: and on .
Decision sets follow §3.6.1: in Cases I and II, with ; in Case III, with ; in Case IV, both are free. Under a fixed horizon, is added, because beyond it , outside the model (§2.4.1 requires ). The finite box statements use , , and a fixed pool has , as in Table EC.1. Other added hypotheses: the standing sign conditions of §2 and Table EC.1 (; ; ; ), (used in the proof of Proposition 1), and .
Limits are asserted for every selection of optimisers. A separate conjunct asserts that optimisers exist for large populations, so the statement cannot be satisfied vacuously by an empty set of optimisers. It is not about a stationary point of an approximation, and is never replaced by a formula.
Two printed slips are corrected and labelled. In Proposition 5, Case III has constant , and (EC.4) has the factor in its denominator. Both follow from the cost of pairs at fixed , which is ; at the corrected constant matches a numerical optimum to four digits, the printed one does not. The branch of Lemma EC.4, Proposition 6 (discounting) and the comparative statics of §3.5 are not formalized.
A complete development needs Gaussian expectations of piecewise-linear functions, semicontinuity arguments on a box with a jump, and asymptotic analysis of argmax sets. The Gaussian-loss identities are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the case lemmas.
The monotone complementarity problem (MCP) asks, for a continuous monotone map on the positive orthant, for a pair with , , and for every . It contains linear programming, convex quadratic programming, the monotone linear complementarity problem and the Karush–Kuhn–Tucker conditions of smooth convex programs. Interior-point methods solve it in polynomially many Newton-type steps when a strictly positive, well-centered starting point is known, but in general no such point is known, and the problem may be infeasible or feasible without any positive feasible point.
Andersen and Ye (Mathematical Programming 84, 1999) extended the homogeneous self-dual embedding of linear programming to the nonlinear MCP: one embeds the problem into a homogeneous problem that always has a trivial interior starting point, solves it by a path-following method, and reads off either a solution or a certificate of infeasibility. Section 8.4 of Ye, Interior Point Algorithms: Theory and Analysis (Wiley 1997, doi:10.1002/9781118032701) presents this construction, the convexity property of the residual set it rests on, and the analysis of one step of the algorithm. This mission formalizes that section.
Vectors are compared componentwise; is the all-ones vector, , , the Euclidean norm and the open orthant. A map is monotone if for all ; denotes its Jacobian.
The residual set is , and for the slice .
The homogeneous map on , with points written , is
The homogeneous model (HMCP) asks for with minimizing .
A map on is scaled Lipschitz with a monotone increasing if
The algorithm works in with and . At an iterate let and . The direction solves
and for a step size the new iterate is and .
Assume is scaled Lipschitz with , and let
If and , then and
The goal remains true when is only assumed differentiable on and scaled Lipschitz; this variant is posed beside the goal (see Formalization scope).
Theorem 8.29 is the one-step invariant behind the iteration bound of the homogeneous algorithm: combined with Lemma 8.28 it shows that the infeasibility residual and the complementarity gap shrink by the same factor per step while the iterates stay in a fixed neighborhood of the central path. Together with Theorem 8.25 (v)–(vi), which identifies solutions and infeasibility certificates of the MCP from maximal complementary solutions of the homogeneous model, this yields an algorithm that needs no feasible starting point and detects infeasibility. The convexity of (Theorem 8.23) is the structural fact that makes the homotopy path of the homogeneous model well defined.
These results are proved in the book (with Theorem 8.19, which Theorem 8.23 uses, left as an exercise). None of them is formalized on the platform: the existing Andersen–Ye material covers only the linear complementarity case, as a set-valued operator, and no statement about scaled Lipschitz maps or the nonlinear homogeneous map exists. A completed development gives a machine-checked analysis of an interior-point step for a nonlinear problem, with every constant explicit.
The algebra of Lemmas 8.27 and 8.28 depends on the identities and , which require differentiating a map defined through ; working with as a Fréchet derivative rather than a hand-written block matrix is part of the work. In Theorem 8.29 the nonlinearity enters only through the scaled Lipschitz bound, which applies only when , so the step must first be shown to stay well inside the orthant before the neighborhood estimate can be closed; the norms involved (, , and the scaled norms , ) must be chained in the right order. Theorem 8.23 is of a different kind: its proof passes through the homeomorphism of Theorem 8.19, whose proof the book leaves as an exercise, and a compactness argument along a homotopy.
Two points in the printed text need care. The block matrix (8.24) displayed for has a spurious transpose in its lower-left block; with the printed matrix Lemma 8.24 would fail for nonsymmetric , and the statements here use the true Jacobian. The printed proof of Theorem 8.25 (iii) (the scaled Lipschitz constant of from that of ) establishes the bound with , not the stated , and only for ; that part is not in this mission, and Theorem 8.29 assumes the scaled Lipschitz property of directly, as the book does.
Vectors are Fin N → ℝ, a point of is z : Fin (n+1) → ℝ with Fin.init z and z (Fin.last n) , and every Jacobian is Mathlib's fderiv. The standing assumptions of §8.4 are explicit hypotheses of every theorem: continuous and monotone on the open orthant , and differentiable there wherever or appears (the section assumes this silently). In the scaled Lipschitz condition, "monotone increasing" is read as nondecreasing on and ranges over . The direction is any solution of (8.42)–(8.43). The new dual iterate is defined by the first line of (8.47); its closed form is a conclusion. The book writes no in the statements of this mission: , , and are the book's explicit constants. is a total function in Lean (division by returns ), but every statement evaluates it and its derivative only at .
A trivializing formalization is excluded: the scaled Lipschitz hypothesis is not vacuous (it holds, for instance, for with any admissible ), the direction is not assumed to have any property beyond (8.42)–(8.43), and the monotonicity of and the identities (8.41) are proved milestones, not hypotheses of the goal.
Beyond the paper. One variant is posed: central_step_strong (strengthened) drops the continuity and monotonicity of from Theorem 8.29, because the scaled Lipschitz condition already forces , the only use the proof makes of monotonicity.
The development needs Fréchet derivatives of compositions with , finite-dimensional norm inequalities, and, for Theorem 8.23, invariance of domain or a direct proof of Theorem 8.19. The definitions (monotone maps on the orthant, the scaled Lipschitz condition, the homogeneous map) are reusable for the remaining parts of Theorems 8.25 and 8.26. Contributions of a proof of Theorem 8.19, and of the faithful Theorem 8.25 (iii), are welcome.
Primal-dual interior-point methods for linear programming come with two kinds of guarantee. The worst-case one is a bound of iterations to reduce the duality gap below . The asymptotic one says what happens to the duality gap near the end of the run, where practical codes spend their final iterations. For the predictor-corrector method of Mizuno, Todd and Ye (1993), Ye, Güler, Tapia and Zhang (1993) showed that the same algorithm that achieves the best known worst-case bound also drives the duality gap to zero quadratically. The proof needs neither nondegeneracy nor convergence of the iterates. Chapter 7 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley 1997, DOI 10.1002/9781118032701) gives a self-contained account. This mission formalizes its LP core.
Timeline, as attributed in the chapter's notes (§7.5): Zhang, Tapia and Dennis first obtained superlinear convergence of a primal-dual method assuming the iterates converge, and quadratic convergence assuming nondegeneracy. Quadratic convergence for general LP, with neither assumption, was first established by Ye, Güler, Tapia and Zhang, and independently by Mehrotra and by Tsuchiya. The monotone LCP version (§7.3) is due to Ye and Anstreicher, who also showed that the predictor step cannot converge superlinearly when no strictly complementary solution exists (Proposition 7.13). Monteiro and Wright extended that negative result to Newton-like methods in general.
Fix a real matrix of rank , and . Consider the standard-form pair
An interior point is a triple with , , , . Write , , for the all-ones vector and . The neighbourhood of the central path is
The strict complementarity partition collects the indices on which some optimal is positive () and those on which some optimal slack is positive (). The predictor direction at is the solution of
It is the case of the direction defined by , , . The scaling is , and denotes the Euclidean norm of the subvector of indexed by . Algorithm 4.5 (predictor-corrector, ) starts in . At each iteration it takes the largest step along that keeps the iterate in , then a full step along back towards the central path.
The order of convergence of a sequence (Definition 1.1) is the supremum of the with . Quadratic convergence (Definition 1.2) means .
For every there is a constant , depending only on and , such that at every with the predictor direction satisfies
The goal fixes no value of : it asserts only that one constant serves every point, which is the content the later results use.
Theorem 7.5, together with Lemma 7.3, says the whole predictor direction is . Through the step-size bound of Lemma 4.17 this gives and hence : quadratic convergence of the duality gap (Theorem 7.6). The same least-squares structure yields the LCP version (Theorem 7.12) and the variants of §7.4. Bounds of this kind on the directions near the optimal face also underlie finite termination and basis identification schemes.
On the formal side, no machine-checked development of interior-point asymptotics is known to the authors of this mission. Mathlib has the linear algebra (ranges, block matrices, least squares through orthogonal projection) but no linear-programming duality theory beyond what other missions supply. A formal proof would supply the Goldman–Tucker partition, the uniform bounds (7.6) and a Hoffman-type bound for least-squares solutions in reusable form.
Everything rests on a constant being uniform. For a single interior point, any bound holds with some depending on the point, so the content is entirely in choosing before the point. The natural first attempt bounds the direction through and on all indices, and this fails: on the entries grow like , and on they shrink like . Only the split along the optimal partition, with the least-squares characterization of the "large" components and the uniform bounds (7.6), balances the two. Relation (7.6) itself requires the partition to be strict (Goldman–Tucker) and an a priori bound on the iterates. For Theorem 7.6 the algorithm's step-size rule has to be carried as defined: a largest step over an interval of neighbourhood memberships.
Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. All norms are Euclidean. and are defined as unions of supports of optimal solutions; that they partition the indices is a consequence solvers must prove, not an assumption. The standing assumption appears as a hypothesis.
Instantiations of the book's (p. 213: "may depend on and/or the original problem data, but … independent of the iteration "):
A constant chosen after the point would make the goal trivially true; the statements quantify first to rule this out. Algorithm 4.5 is run for every (no termination test), and its step is the greatest admissible , not a supremum. The order of convergence and all limits superior take values in EReal, so infinite values are not collapsed to junk reals. Lemma 7.4's second problem is stated as corrected (the printed objective is ill-typed and the sign of is inconsistent with (7.4)); see the findings.
Beyond the paper. One strengthened variant: Theorem 7.5 on for every and without the rank condition. The book's proof uses the neighbourhood only through , and the rank of enters nowhere.
Needed infrastructure: LP duality and strict complementarity (Goldman–Tucker), a Hoffman-type bound for minimum-norm solutions, and weighted least squares. The definitions of the neighbourhood, the direction and Algorithm 4.5 are shared with the chapter 4 analysis and are reusable for other interior-point results. Contributions proving any milestone independently are welcome.
Worst-case analysis of interior-point methods gives iteration bounds of order or , while practical codes finish in a number of iterations that barely grows with the problem size. Chapter 6 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley 1997, doi:10.1002/9781118032701) addresses the gap probabilistically. Its rigorous half (§6.2) takes the simplest nontrivial problem, the homogeneous linear feasibility problem with a random Gaussian matrix, and shows that it is solved in iterations with high probability, then extends this to random linear programs through the homogeneous self-dual model.
That analysis rests on a geometric fact about random cones: the probability that random vectors lie in a common open half-space through the origin. The answer is Wendel's formula (J. G. Wendel, A problem in geometric probability, Math. Scand. 11 (1962), 109–111); Ye restates it as Corollaries 6.11–6.12 and draws from it Theorem 6.13: with probability one a random homogeneous system is strictly feasible on exactly one side of its theorem of the alternative. Strict feasibility is what makes the condition number of the problem finite, which is what an interior-point termination procedure needs.
Let be a real matrix with columns ; vector inequalities are componentwise and is the all-ones vector. The homogeneous system (6.5) is
and its alternative (6.11) is the system , in . An interior feasible point of (6.5) is an with and ; of (6.11), a with .
In the standard Gaussian model (§6.2.2) the entries of are independent random variables. With the book defines
and is the same sum with replaced by .
A partition chooses columns for the matrix and leaves the other in . System (6.12) asks for with
For the one-step analysis of §6.1, is an orthogonal matrix with first column , and is uniformly distributed on the unit sphere of .
The Lean development lives in the namespace YeIPA.Random: the module YeIPA.Random.Setting defines IsFeasible65, IsInterior65, IsFeasible611, IsInterior611, IsFeasible612, gaussianMatrix, pnd and uniformSphere.
For , and standard Gaussian ,
Theorem 6.13 is the input to the chapter's main results: Theorem 6.15 (a feasible point of a random system satisfies the scaling condition (6.9) with high probability) and the iteration bounds of Theorems 6.16 and 6.23 for random feasibility and random LP problems. It turns a deterministic theorem of the alternative, which allows degenerate configurations, into a statement that such configurations have probability zero. Corollaries 6.11–6.12 are Wendel's formula in the form used for linear programming, and also give the exact probability that a random homogeneous system is feasible, a quantity that recurs in the analysis of random linear programs and of perceptron capacity. Lemma 6.5 is the concentration estimate behind the one-step analysis of predictor steps in §6.1.
None of these results is formalized on Prove2Me or, as far as a search shows, in Mathlib. Wendel's formula has no machine-checked proof that this mission could reference; the platform's PoissonDirichlet.Wendel.* items concern an unrelated identity. A complete development adds Gaussian random matrices, conic theorems of the alternative and an exact geometric probability to the platform.
The book cites Wendel's formula ("It is shown that …") and leaves its proof as Exercise 6.3, so Corollaries 6.11–6.12 must be proved from scratch. The natural first idea, conditioning on the column space or on a single column and integrating, does not close: the count of half-spaces is combinatorial, not an integral that evaluates in closed form. The probability-one statements need general position of Gaussian columns, which is the property that rules out the degenerate cases of the theorem of the alternative. Corollary 6.12 is not a consequence of Corollary 6.11 alone: the gap between "feasible" and "strictly feasible" is an event that must be shown to be null, and the book's own argument passes through the dual system and the identity for , which is itself part of what must be proved. Lemma 6.5 is a uniform statement over all orthogonal completions of , with an explicit threshold rather than an unspecified constant.
Vectors are functions on Fin n (indices ), matrices are Matrix (Fin m) (Fin n) ℝ, and the Gaussian model is the product measure Measure.pi of gaussianReal 0 1 over the entries, a sample being read as Matrix.of A. Probabilities are values of this measure in , compared with through ENNReal.ofReal. "With probability one" in Theorem 6.13 is an almost-everywhere statement for that explicit measure; the failure set is null. The section's standing assumption that has full row rank (p. 187) is carried as in the probabilistic statements, under which a Gaussian has rank almost surely, and as in Lemma 6.14. Every probabilistic statement assumes ; for both systems are empty and is undefined. In Lemma 6.14 a partition is an injection from into the columns; the variable is the last coordinate of a vector on Fin (m+1). In Lemma 6.5 the sequence is indexed by , the matrices are arbitrary with , deletes the first column, the uniform law is Lebesgue surface measure on the sphere normalized to mass one, is natural, and is written coordinatewise. No result of this chapter uses an bound in the stated items, so there are no constants to instantiate; Lemma 6.5's threshold is the book's own.
A trivializing formalization is ruled out: the probabilities are those of the explicit product Gaussian measure (not an arbitrary measure, nor "for almost every " against an unspecified measure), interior points are required to be strictly positive in every coordinate, and Theorem 6.13 asserts both the emptiness of one system and an interior point of the other.
Beyond the paper. One variant is posed. YeIPA.Random.lemma_6_14_corrected (corrected, finding F1) adds to Lemma 6.14: as printed the lemma fails for , where is empty and solves (6.12) for every , e.g. . The faithful Lemma 6.14 stays the milestone.
Infrastructure that a complete development needs and that is reusable beyond this mission: general position of Gaussian matrices (every minor nonzero almost surely), Gordan's theorem of the alternative for , Wendel's formula, and tail bounds for coordinates of a uniform point on the sphere. Proofs of any milestone, and of these supporting facts as separate lemmas, are welcome.
Karmarkar's 1984 algorithm solved linear programs in polynomial time by reducing a logarithmic potential function by a constant at every step (doi:10.1007/BF02579150). Its successors replaced Karmarkar's projective transformations with a primal-dual potential that measures the duality gap and the distance from the central path together. Tanabe, and Todd and Ye (1990, doi:10.1287/moor.15.3.508), introduced this potential. Ye (1991) and Kojima, Mizuno and Yoshise (1991) showed that one fixed reduction per step, for the parameter , gives the best known iteration bound . The potential-reduction method needs no step that stays close to the central path. It became one of the standard interior-point methods, and its analysis was later carried over to semidefinite and conic programming.
Chapter 4 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley, 1997, doi:10.1002/9781118032701) proves this one-step estimate for two algorithms. The first is the primal-dual potential-reduction algorithm (§4.3), which alternates a primal projected-gradient step with an update of the dual lower bound. The second is the symmetric primal-dual algorithm (§4.4), which moves along the Newton direction toward a point of the central path. This mission formalizes both estimates and the lemmas they rest on.
Let be a real matrix of rank , with , , . The standard-form pair is
and both are assumed to have interior feasible points. Vector inequalities are componentwise, is the all-ones vector, , , is the Euclidean norm and . The interior consists of the triples with , , , . For , the primal-dual potential and the primal potential with lower bound are
The potential-reduction step (§4.3, ). At with , let
The dual update is with , and .
The symmetric step (§4.4). With and , the direction solves , , . The step size is for a constant .
There is a constant such that for every such LP and every , with , and ,
Theorem 4.9 says that the potential can be lowered by a fixed amount no matter where the iterate is. Either the primal step makes progress, or the dual update produces a feasible, nearly central dual point with a smaller gap. Since , a constant decrease per step yields the bound of Corollary 4.10 without any neighborhood of the central path. Lemmas 4.11 and 4.12 give the same conclusion for the symmetric algorithm, with decrease . These are the per-step facts behind practical potential-reduction codes and their conic extensions.
The platform has no statement of these results. LinearOptimization.interior_point_potential_reduction (proved) turns a constant decrease of a different potential into an iteration count. The Mizuno–Todd–Ye bounds on the second-order term of the Newton step, which are Ye's Lemmas 4.14, 4.15 and 4.19, are already formalized as AdaptiveStepIPM.PredCorr.lemma_1a, AdaptiveStepIPM.WideNbhd.lemma_1b, lemma_1c and lemma_2c. They belong to the path-following part of the chapter and are not repeated here. Formalizing Theorem 4.9 checks the case split and its numerical constants, and produces a reusable layer: the weighted projection , the dual estimates , , and the potential identities.
The case split is driven by , which is defined through a projection, but Lemma 4.8 reasons about it through the identity (4.11). The book states that identity without proof. It needs the normal equations for , , and so the invertibility of . The primal case needs and before any logarithm is evaluated. It also needs the first-order term to equal exactly, which uses that is an orthogonal projection. The dual case combines Lemma 3.1, applied to , with the arithmetic–geometric mean inequality and the bound . The constant must be checked for every : with and the two decreases are about and , so the margin over is small. Lemma 4.11's proof is omitted in the book. Unlike its Chapter 3 analogue it needs no normalization , but the exact cancellation of its first-order term has to be verified. Lemma 4.12 is left as an exercise.
Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; indices are -based. The Euclidean norm is written out as norm2. The rank of , the existence of interior points (p. 63) and (Chapter 4 preamble, p. 109) are bundled as StandingAssumptions A b c and are a hypothesis of every theorem, together with . The vector is defined by its projection formula, not by (4.11), so (4.11) is something to prove. Matrix inverses are Mathlib's ⁻¹, which is on singular matrices and never reached under the rank assumption.
Explicit constants: Theorem 4.9 does not fix the step length , and the proof chooses (with in the case split). The goal is stated for the step (4.10) with . Its is quantified before , , , , and the iterate, so one number serves every instance. A formalization in which depends on the instance, or in which the step is any point that happens to lower the potential, would be trivial; both are ruled out by stating the theorem for the book's step (4.10) and dual update (4.12)–(4.13) with a uniform . No result in this mission uses .
Beyond the paper. One variant is posed: a strengthened Theorem 4.9 for every with the same (finding F1). The proof uses only through and , and both hold for .
Not in scope: the iteration-count statements (Theorems 4.4, 4.7, 4.13, 4.20, Corollary 4.10), which the book gives with ; Karmarkar's algorithm and the path-following analysis of §§4.1–4.2 (Proposition 4.2, Lemmas 4.5–4.6), which need the max-potential of the dual level set; and the predictor-corrector Lemmas 4.16–4.17 and Theorem 4.18, which are statements about an algorithm's sequence.
Interior-point methods for linear programming do not move along the boundary of the feasible region; they follow a curve of points that stay "central". The basic notion of centrality is the analytic center of a polytope, the interior point that maximizes the product of the slacks of its defining inequalities (Sonnevend, 1986, doi:10.1007/BFb0043914). Every path-following and potential-reduction algorithm repeatedly computes an approximate analytic center, so it matters how "approximately centered" is measured and what one Newton step does to that measure.
Chapter 3 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley, 1997, doi:10.1002/9781118032701) answers both questions for a polytope given by linear inequalities. It introduces three measures of proximity to the analytic center (dual, primal and primal-dual), proves that they are equivalent, and shows that the corresponding Newton steps square them. The same estimates reappear, with minor changes, in the complexity analysis of Karmarkar's algorithm and of the primal-dual potential-reduction methods of the later chapters. This mission formalizes those statements.
Let be a real matrix and . Vector inequalities are componentwise, is the all-ones vector, , , and is the Euclidean norm. The chapter works under standing assumptions: has rank , , and the polytope
is bounded with nonempty interior. An interior point of has . The homogeneous primal set is ; its interior points have , .
Three potential functions are used:
The analytic center is the interior point of maximizing , and the primal potential minimizer is the interior point of with minimizing .
The three proximity measures are
The dual Newton step is ; the primal Newton step is ; the primal-dual Newton directions solve , , , and are taken with step size for a constant .
For an interior point of , an interior point of , the analytic center and the primal minimizer :
Theorem 3.2 is what makes an "approximate analytic center" a well-defined notion: whichever of the three measures an algorithm controls, the other two and the potential gaps follow. Parts 3 and 4 convert a small residual into a bound on the logarithmic-volume gap and on the relative distance to the true center. These are the quantities used to start the Newton procedures of Theorem 3.3 and Corollary 3.8, and to bound the number of central-section and potential-reduction steps elsewhere in the book. Lemma 3.12 and Theorem 3.13 are the per-step estimate of the primal-dual potential-reduction method, the template for the linear-programming algorithms of Chapter 4.
None of these statements is formalized on Prove2Me. The platform has self-concordant Newton analysis (ConvexOptimization.newton_quadratic_phase_contraction) and proximity measures for self-scaled cones (SelfScaledIPM.FuncProx.*, open), but neither works with Ye's measures or steps. The results are classical and proved in the book. Formalizing them yields a reusable linear-algebraic layer (projections , scaled least squares, the primal-dual Newton system) for any later interior-point mission. It also checks hypotheses the book leaves implicit: Lemma 3.12 is false without the normalization that §3.4.2 states only once.
Most of the chapter's arguments are short on paper but depend on facts that are only described in words. In (i), and are the optimal values of weighted least-squares problems, and the domination needs that variational characterization, which goes through the invertibility of and (rank ). Part 4 is not a one-step estimate: it is obtained by running the Newton procedures of Theorem 3.3 and Corollary 3.8 indefinitely, summing a geometric series of quadratically shrinking corrections, and identifying the limit with the analytic center. That identification requires uniqueness of the center (strict concavity on a bounded polytope) and the correspondence between and through . Part 3 needs that correspondence as well. The positivity of the damped iterates in Lemma 3.12, which the book asserts "can be verified", has to be established before any logarithm is evaluated. Theorem 3.13 requires constants independent of , which rules out every argument that loses a dimension factor.
Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; indices are -based. The Euclidean norm is written out as norm2, since Mathlib's norm on Fin n → ℝ is the sup norm. Matrix inverses are Mathlib's ⁻¹, which is on singular matrices. The rank hypothesis makes every inverted matrix positive definite at the points where the theorems use it, so the junk value is never reached. The standing assumptions (rank , , bounded with nonempty interior) are bundled as StandingAssumptions A c and are a hypothesis of every theorem. The normalization of §3.4.2 is a hypothesis of Lemma 3.12 and Theorem 3.13. The analytic center and the primal minimizer are defined by their extremal properties, not by the optimality system , so the goal cannot be obtained by unfolding a definition. The theorems are stated for the steps exactly as the book defines them, never for an arbitrary "good" step.
Explicit constants: no result in this mission uses . Theorem 3.13's constants are existential in the book ("we can choose … for a positive constant "). They are stated as quantified before , , and , which is what the proof establishes. A formalization in which or depends on the instance would be trivial and is ruled out by this quantifier order.
Beyond the paper. One variant is posed: a sharpness probe of Lemma 3.12 with the normalization removed (findings F1, F3). With , , , , the step only rescales , so the potential is unchanged while the claimed bound is about . A disproof is the expected outcome.
Not in scope: Theorem 3.11 (the primal-dual Newton step), whose positivity claim fails as printed (finding F2); the iteration-count theorems 3.4, 3.7, 3.9, stated with ; the central-section Lemmas 3.5–3.6; and Theorem 3.10 (affine scaling). Contributions welcome: the least-squares characterization of , as reusable lemmas, and the uniqueness of the analytic center.
Primal-dual interior-point methods for linear programming generate strictly positive iterates that approach the solution set but never reach it: the duality measure tends to zero, yet no iterate is ever an exact solution. Many applications need more than an approximate point — an exact optimal basis, a vertex, or the optimal partition of the variables into those that are positive and those that vanish at optimality. Chapter 7 of Stephen J. Wright's Primal-Dual Interior-Point Methods (SIAM 1997) studies the end game of these methods: how fast decreases once the iterates are close to the solution set, and how to jump from an interior iterate to an exact solution.
The finite termination procedure formalized here is due to Ye (Math. Programming 1992): guess the optimal partition from the current iterate and project onto the face of the feasible set it determines. The superlinear analysis of the affine-scaling step goes back to Ye, Güler, Tapia and Zhang (Math. Programming 1993); its key uniform bound on weighted least-squares solutions was proved independently by Stewart (Linear Algebra Appl. 1989) and Todd (Oper. Res. 1990). The bound on solutions of linear systems used throughout is Hoffman's (J. Res. Nat. Bur. Standards 1952).
Fix , , , with no assumption on the rank of . The primal problem is subject to , ; the dual is subject to , . Let and be their sets of optimal solutions and . The optimal partition is
A strictly complementary solution is with for and for . The quantity
measures how far the solution set reaches into each coordinate, and .
The strictly feasible set consists of triples with , , , . The duality measure is . The wide neighborhood is for , and the 2-norm neighborhood is , where is the vector of products and is Euclidean.
The affine-scaling direction at is any solution of
The partition estimate at is , , and the projection problem of Ye's procedure is
For there is a threshold such that every with
satisfies (i) and , and (ii) the projection problem has a solution, and every solution is a strictly complementary solution. The threshold is existential, as printed; the goal does not fix its value.
Theorem 7.12 turns any path-following method into a finite algorithm: once falls below , one linear least-squares problem, costing about one interior-point iteration, returns an exact strictly complementary solution, and with it the optimal partition. For integer data the threshold is bounded below by , which is how interior-point methods are made to terminate exactly within their polynomial iteration bounds (Chapter 3 of the book). Theorem 7.4 and Lemma 7.6 give the competing route — the affine-scaling step is , so predictor steps approach full length and the predictor-corrector method converges two-step quadratically.
None of these results is formalized on the platform. Hoffman's error bound exists there for a single consistent system with a constant chosen after the right-hand side; Lemma A.3 and its variant need one constant for all right-hand sides. The optimal partition, , the uniform weighted least-squares bound and the projection step are reusable for any formal treatment of interior-point methods, degenerate linear programs or error bounds.
Near a degenerate solution set the linear systems defining the affine-scaling step become arbitrarily ill-conditioned: the diagonal scaling has entries tending to and to , and the coefficient matrix has no nonsingular limit unless the solution is unique. Any bound that passes through the conditioning of that matrix degrades as ; the constants of Theorem 7.4 and Lemma 7.2 must be independent of the scaling. For Theorem 7.12 the difficulty is uniformity in the other direction: the threshold must be one number for the whole neighborhood, which needs a bound on the distance from an iterate to a face of the feasible set that does not depend on the iterate.
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, points are triples (x, lam, s); the Euclidean norm is defined explicitly (Mathlib's default on Fin n → ℝ is the sup norm). Directions and the projection problem are defined by their equations and optimality, never by closed-form formulas. uses real suprema, which agree with the book's whenever ; every theorem is vacuous otherwise. No rank assumption on is made except in Lemma A.4, where the page states it. is not a hypothesis: membership in a neighborhood implies it.
Explicit constants: the book writes "there is a constant" in Lemmas 5.13 and 7.1; their proofs give (5.32) and (7.6), which are used. The constants , , , , have no closed form in the book (they come from Lemma 2.5, Hoffman's lemma and Lemma 7.2) and stay existential, but each is quantified before the point, the right-hand side or the scaling it must work for; a constant chosen after the point would make Theorem 7.4 trivial. A trivializing form of the goal — a threshold allowed to be , or a conclusion about some minimizer chosen by the solver — is ruled out by requiring , existence of a minimizer, and strict complementarity of every minimizer ( is not unique). In Lemma 7.6 the largest step is a hypothesis (IsGreatest), and the statement also asserts that the whole interval is admissible.
Beyond the paper: one variant is posed. lemma_A_3_strong (strengthened, finding F1) is Lemma A.3 for every consistent system , instead of ; this is Hoffman's 1952 theorem. Finding F2 records that the printed proof of Theorem 7.4 covers only full-row-rank ; the statement is kept as printed.
Needed infrastructure: LP optimal solution sets and the optimal partition, matrix inverses and ranks, finite sums. A uniform Hoffman bound and the Stewart–Todd bound are reusable well beyond this mission; contributions of either are welcome.
Interior-point methods for linear programming are usually analysed under the assumption that the primal-dual pair has a strictly feasible point, or at least a solution. A solver used in practice cannot assume this: it must either return a solution or report that the primal or the dual problem is infeasible. The homogeneous self-dual approach embeds the linear program into one larger problem that always has a solution and reads the answer off that solution. Ye, Todd and Mizuno introduced the HSD form (Ye, Todd, Mizuno 1994); Xu, Hung and Ye simplified it (Xu, Hung, Ye 1996). The approach is used in production interior-point codes. This mission formalizes Chapter 9 of Wright's textbook (Wright 1997), together with the parts of Appendix A on which its proofs rest.
Let , , . No assumption is made on the rank of . Vector inequalities are componentwise. The primal-dual pair is
The primal solution set consists of the feasible that attain the minimum of . The dual solution set consists of the feasible that attain the maximum of . The primal-dual solution set is .
The simplified HSD form introduces scalars and asks for with
Here is free. This is a mixed monotone linear complementarity problem (mLCP) with a skew-symmetric matrix. It always has the zero solution. A solution is strictly complementary if and .
More generally, a self-dual linear program (9.1) has the form subject to , , , where and are skew-symmetric. Its mLCP (9.2) asks for with , , and . A solution is strictly complementary if .
The HSD form of Ye, Todd and Mizuno starts from an initial point with , . It sets , and , and adds a free variable . The result is the mLCP (9.8):
The right-hand side quantifies over all strictly complementary solutions. It is not vacuous, because such solutions always exist.
In attack order:
Theorems 9.2 and 9.3 make the simplified HSD form a complete decision procedure for linear programming. Any strictly complementary solution of (9.5) has one of two forms. Either , and then solves the original pair. Or , and then the solution certifies that the primal or the dual problem is infeasible. Path-following methods converge to strictly complementary points. An algorithm applied to a problem that always has a solution therefore settles the original problem, without any feasibility assumption. Theorems 9.4–9.6 transfer this to the HSD form, which also admits the strictly feasible starting point (p. 184) and so can be solved by a feasible interior-point method.
On the formalization side, nothing about the simplified HSD form is on the platform yet. The Ye–Todd–Mizuno form appears in other missions as open statements about a single strictly self-complementary solution, under a hypothesis of the form . Theorems 9.5 and 9.6 here instead quantify over all strictly complementary solutions and use the hypothesis , so they are separate statements. Appendix A's Theorem A.1 is the classical KKT theorem for linear constraints, and Theorem 9.1 is a structural fact about skew-symmetric complementarity problems. Both can be reused beyond this chapter.
The "if" direction of Theorem 9.2 is short once strictly complementary solutions of (9.5) are known to exist. That existence is Theorem 9.1, which is the substance of the chapter. Monotone LCPs in general need not have strictly complementary solutions. A solver has to show that the self-dual structure rules out the failure seen for general monotone LCPs, for a problem in a nonstandard form with free variables and equality rows.
The "only if" direction needs more than one well-chosen solution. It needs the fact that all strictly complementary solutions of (9.5) have the same support. The book asserts this without proof (finding F3 in FINDINGS.yaml), so a solver must supply it. Theorem 9.5 also requires a strictly complementary solution of (9.8) with whenever . Here the normalisation row of (9.8) has to be satisfied, which the simplified form does not ask for.
Vectors are Fin n → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ; and may be zero. The definitions file WrightPDIPM.SelfDual.Setup writes out the systems (9.2), (9.5) and (9.8) row by row, exactly as printed, together with their solution and strict-complementarity predicates. and are defined by optimality against every feasible point, with no infimum, so they are empty when the optimum is not attained. The gradient in Appendix A is the vector of Fréchet partial derivatives, and every statement that uses it assumes differentiability. The Euclidean norm is defined explicitly.
Several standing hypotheses of the book are made explicit:
The page writes for in Theorem 9.6. This is a misprint, and the formal statement uses . No statement in this selection carries an constant.
Theorem 9.2 must not be formalized with "strictly complementary" weakened to "solution", since the zero solution would then falsify the right-hand side. Its right-hand side must not be read as an existence claim either. The statement keeps the book's universal quantifier over strictly complementary solutions.
Beyond the paper. Two variants are posed beside the faithful statements. theorem_9_3_strong (strengthened, finding F1) is Theorem 9.3 for every solution of (9.5) with , since the book's proof never uses strict complementarity. theorem_9_6_strong (strengthened, finding F2) is the same strengthening of Theorem 9.6, via Theorem 9.4.
A complete development needs:
The KKT and Goldman–Tucker statements, and the mLCP definitions, are reusable for the LCP material of Chapter 8. Contributions of any milestone are welcome. Theorems 9.7–9.8, about Algorithm IPF diverging on infeasible problems, are not included.
Primal-dual interior-point methods solve a linear program by following the central path from a point with strictly positive primal variables and dual slacks . The classical analysis assumes that the starting point is feasible: it already satisfies the equality constraints and . In practice such a point is rarely available, and the production codes of the early 1990s (OB1, and later the solvers built on Mehrotra's method) instead start from an arbitrary positive point and let the Newton steps reduce the constraint violation together with the duality gap. These infeasible-interior-point methods worked well long before they were understood. Global convergence was first proved by Kojima, Megiddo and Mizuno (Math. Programming 61, 1993), and polynomial complexity of a long-step variant by Zhang (SIAM J. Optim. 4, 1994).
Chapter 6 of Stephen J. Wright's Primal-Dual Interior-Point Methods (SIAM 1997) gives a self-contained account of this theory for one representative long-step method, Algorithm IPF. This mission formalizes the statements of that chapter.
Let (no rank assumption), , , and consider the primal s.t. , and the dual s.t. , . The solution set consists of the triples with , , and for all . For a triple the residuals are and , and the duality measure is . Norms are Euclidean unless marked.
Fix a starting point with , with residuals and duality measure . For and , the neighborhood is
Algorithm IPF has parameters and . At iterate it picks and solves the linear system
where , and . It takes the largest such that the point lies in and there is at most . That point is the next iterate. The analysis uses and the scaling .
A positive sequence converges Q-linearly if for some and all large . It converges R-linearly if it is dominated by a Q-linearly convergent sequence.
If and the start is infeasible, , then along Algorithm IPF
The statement fixes no rate. It asserts only the shape of the convergence, so it survives any improvement of the constants.
Theorem 6.1 is the reason infeasible starts are safe. A practitioner may start from any positive point. If the problem has a solution, the method then removes the infeasibility and the duality gap at a linear rate, without a Phase I. Lemma 6.7 is the core estimate: one uniform lower bound on the step length gives both rates, and its -explicit form (6.38) gives the complexity of Theorem 6.2. Theorems 6.8 and 6.9 show that the iterates identify the optimal partition . This is the basis of the finite-termination procedures of the next chapter.
These results are proved in the literature and in the book. They have not been machine-checked: the Prove2Me corpus contains a formalized convergence theorem for Vanderbei's path-following method under a boundedness hypothesis, but no infeasible-interior-point theory with the neighborhood . The mission would produce the first checked proof of global linear convergence for an infeasible primal-dual method. The definitions it introduces (the algorithm as a predicate on sequences, Q-/R-linear convergence) can be reused for the self-dual and termination chapters.
The obvious argument for a feasible method bounds the second-order term by a multiple of through the orthogonality . With infeasible iterates this orthogonality fails, and the cross terms involve the iterates themselves, which are not bounded a priori. The step from "the residuals shrink" to "the step length stays bounded below" therefore needs a bound on in terms of . That bound has to come from a solution of the linear program. The hypothesis is essential. The page prints Theorem 6.1 without it, but on the infeasible program , , the neighborhood condition keeps bounded away from zero. A solver should also note that the explicit displayed in the proof of Lemma 6.7 drops a factor against the bound (6.47) derived just before it, and can equal . Only the existential statement survives as printed. The bound (6.38) is left to the reader in the book (Exercise 4).
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ. Euclidean norms and the 1-norm are defined explicitly, because Mathlib's default norm on Fin n → ℝ is the sup norm. "Generated by Algorithm IPF" is a predicate on the sequences , , and the directions. The direction is given by its linear equations, not by a closed form, and "the largest " is an IsGreatest hypothesis on the admissible set rather than a constructed maximum. The neighborhood is anchored at the run's own start. Every statement carries the hypotheses the chapter states once and then omits: ; (p. 111); where the proof starts from a solution (pp. 127, 185); and, for Lemma 6.7, a start inside (pp. 109, 120). Constants , , , are positive and quantified before the iteration index. in (6.38) is quantified after the algorithm's parameters and before the dimension and the instance. That is how "independent of " is rendered.
Explicit constants. Lemma 6.6's "a constant independent of " is stated with the value its proof sets, . The book gives no explicit for (6.38), and none is invented. Theorem 6.2 () is not posed, because an explicit iteration count would rest on that unproved exercise.
A trivializing formalization is ruled out. The Q-linear predicate requires and , not only a ratio bound, and R-linear convergence is domination by such a sequence. is explicit, since division by zero would make (6.49) vacuous. No hypothesis beyond the book's is added to make a run easier to exhibit, and the greatest step length is required to exist exactly as the algorithm prescribes.
Beyond the paper. One sharpness probe accompanies the goal: Theorem 6.1 with removed, expected to be false by the counterexample above; a disproof is the sought outcome.
Infrastructure that would help: the identity , orthogonality of and when and , the Goldman–Tucker theorem (strictly complementary solutions exist; Wright, Theorem 2.4), and Hoffman's bound for Theorem 6.9. Contributions of reusable lemmas on Q-/R-linear sequences are welcome.
Primal-dual interior-point methods are the standard polynomial-time algorithms for linear programming and the basis of most commercial LP solvers. Among them, path-following methods are the ones with the cleanest complexity theory: they keep every iterate inside a neighborhood of the central path and shrink the duality measure by a fixed factor per step. Chapter 5 of Stephen J. Wright's Primal-Dual Interior-Point Methods (SIAM 1997) presents three such methods — a short-step method, the Mizuno–Todd–Ye predictor-corrector method, and a long-step method — and analyzes each from a small set of one-step estimates.
The short-step method and its iteration bound go back to Kojima, Mizuno and Yoshise (1989) and Monteiro and Adler (1989); the predictor-corrector method with two nested 2-norm neighborhoods is due to Mizuno, Todd and Ye (Math. Oper. Res. 1993); the long-step method in the wide neighborhood with its bound is in the same line of work. Wright's chapter gives a single, uniform treatment of the three, with explicit constants.
Fix , , , with no assumption on the rank of . The primal problem is subject to , , and the dual is subject to , . A primal-dual point is a triple . The strictly feasible set consists of the triples with , , and (componentwise).
For vectors write , and , so is the vector of pairwise products . The duality measure is . The 2-norm neighborhood of the central path is
and the one-sided -norm neighborhood is , .
Given a centering parameter , a search direction is any solution of the step equations
Along it, and . The vector of products is the second-order term that the linearization ignores.
Let satisfy
If and solves the step equations with this , then
This is a one-step statement with no algorithm loop. It is the invariant of the short-step method (, ).
Theorem 5.6 is the step that turns the linear decrease of (Lemma 5.1) into a convergence proof: once the full step is known to stay in , the duality measure falls by the factor at every iteration, and the generic complexity theorem of Chapter 3 gives the iteration bound, the standard bound for primal-dual interior-point methods. Lemmas 5.7 and 5.8 give the same bound for the adaptive predictor-corrector method, and Lemma 5.10 with Theorem 5.11 the bound for the long-step method, which is the variant closest to practical codes.
On the platform, the Mizuno–Todd–Ye predictor-corrector analysis has been formalized in a different parametrization (pairs with an existential dual multiplier, and a different step bound); the results of this chapter in Wright's triple form, the general Lemma 5.3, the short-step invariant and the long-step reduction are not yet formalized. A machine-checked version yields reusable infrastructure: the step equations, the two neighborhoods and the pairwise-product bounds are used by every later chapter of the book (infeasible methods, superlinear convergence, finite termination).
The step equations are linear, but neighborhood membership is not: the products are quadratic in , and the quadratic coefficient is not controlled by the equations individually — only the sum vanishes. A bound on in terms of alone, uniformly over the neighborhood, is the crux; a naive bound through the norms of and separately involves the conditioning of and is not uniform. The second subtlety is strict positivity: the proximity inequality at every does not by itself rule out a coordinate of or changing sign, and the conclusion of Theorem 5.6 requires , for the whole segment.
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, points are triples (x, lam, s). The norm is the explicit Euclidean norm (Mathlib's default norm on Fin n → ℝ is the sup norm). and are subsets of , so membership includes both equality constraints and strict positivity. The direction is defined by its linear equations, never by a closed-form solution, so no rank assumption and no nonsingularity are presupposed. Where the page leaves the ranges implicit, the standing ones are hypotheses: for , for , for the step equations. In Lemmas 5.1 and 5.5, ranges over all reals, as the page places no restriction on it.
Explicit constants: the book's "there is a constant independent of " in Theorem 5.11 is replaced by the its proof derives (p. 100); every other constant is printed in the statements. In (5.19), the case is read as ; real division by zero, which would make and Lemma 5.7 trivial on the interval , is excluded by an explicit case split. "The largest " in Algorithms PC and LPF is a hypothesis (IsGreatest) on the chosen step, never a construction. A trivializing formalization — one that states only the proximity inequality without strict feasibility — is ruled out by the definition of .
Beyond the paper: one variant is posed beside the faithful goal. theorem_5_6_strong (strengthened, finding F1) is Theorem 5.6 for every real : condition (5.15) already forces when , and the bound is not used by the argument.
Needed infrastructure: finite sums and the Euclidean norm on Fin n → ℝ, Matrix.mulVec and dot products, real powers. Proofs of Lemma 5.3 and of the positivity argument along the segment are reusable well beyond this mission; contributions of either are welcome.
Interior-point methods solve linear programs by moving through the interior of the feasible region instead of along its edges. Two families dominate the theory: path-following methods, which keep the iterates near a central path, and potential-reduction methods, which instead measure progress by a single merit function and only ask that it fall by a fixed amount at every iteration. The second family grew out of Karmarkar's projective algorithm (Karmarkar 1984). The primal-dual potential used here was introduced by Tanabe and by Todd and Ye (Todd–Ye 1990), and the primal-dual step analysed in this mission is that of Kojima, Mizuno and Yoshise (Kojima–Mizuno–Yoshise 1991). It attains the iteration bound, the best known for any interior-point method.
The mission follows Chapter 4 of S. J. Wright, Primal-Dual Interior-Point Methods (SIAM 1997), the standard graduate text on the subject. Its argument is self-contained and fully quantitative: a fixed decrease of per step, and an explicit iteration count.
Let , and , with no rank assumption on . The primal problem is subject to , , and the dual is subject to , . The strictly feasible set is
inequalities being componentwise. The duality measure is . Write , and .
For a parameter , the Tanabe–Todd–Ye potential is
evaluated where . Algorithm PR iterates as follows. At it computes the search direction , the solution of
It then sets and takes a step length that minimizes over .
The analysis compares along the direction with a quadratic. For define
and the quadratic estimate . Let , and with . Here is the Euclidean norm and the max-norm.
For , , , the direction above, and :
and every minimizer of the potential along the direction satisfies
The goal fixes and the constant because the book does. Its proof in fact gives .
Theorem 4.6 is the per-iteration guarantee of the method. Combined with Theorem 4.4 it yields Corollary 4.7. At this is an bound on the number of iterations needed to reduce the duality measure below . The same template underlies potential-reduction methods for linear complementarity and semidefinite programming: a fixed decrease of a potential, plus the inequality linking the potential to .
Formalizing the chapter yields a machine-checked complexity proof of a primal-dual interior-point method for linear programming, with every constant explicit. It also yields reusable pieces: the logarithmic estimates of Lemma 4.1, the bound of by the potential, and the generic counting argument of Theorem 4.4. The results are classical and proved on paper. No formal version of this chapter exists on the platform. The related published items cover a different potential-reduction method (Mizuno–Todd–Ye, in a wide neighbourhood) and a different counting bound (Bertsimas–Tsitsiklis).
The proof of Lemma 4.5 is the centre of the argument. It needs a lower bound on uniform over all strictly feasible points, including badly centred ones. A naive bound through loses the factor that cancels against .
The hypothesis is essential, and Theorem 4.6 does not print it. It is stated for Lemma 4.5 and Corollary 4.7. For the conclusion fails: at , the potential can fall by at most about .
The step from the quadratic estimate to the potential has its own subtleties. The open interval need not contain a minimizer, and can equal (at , ). The second conclusion of the goal is therefore stated for every minimizer, and a proof must not assume .
Vectors are Fin n → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ. All definitions are in Definitions.Def_WrightPDIPM_Potential_Setting. These are Fo, mu, Phi, alphaMax, IsFeasibleDirection, IsPRDirection, g1, g2, q, vvec, vmin, rvec, alphaBar and IsPRStep. The search direction is defined by its linear equations, never by a closed-form inverse. The arg min of the line search is a hypothesis (IsMinOn on the open interval), never constructed.
is the formula itself, and every statement evaluates it only at positive vectors. Standing hypotheses of the chapter are explicit binders: , , for Lemma 4.3(i), and for Theorem 4.6. Indices are integer ceilings compared with in .
The book's O(·) in (4.32) is decoration: the explicit is what is stated. Theorem 4.6 has no O(·); its constants are and .
A trivializing formalization is ruled out. The direction is the solution of the PR system, not an arbitrary feasible direction (for which the claim is false). The coefficients are computed from it, not free reals (for which it would be empty). never takes Lean's junk value , since whenever .
Beyond the paper. Two variants are posed next to the faithful items.
lemma_4_5_strong (strengthened, finding F2) proves (4.28) for . Lemma 4.5 prints a strict inequality, but its proof covers the endpoint, which Theorem 4.6 and Corollary 4.7 use.theorem_4_6_probe (sharpness, finding F1) is Theorem 4.6 under only . It is expected to be false, since a centred point with , falls by at most , and a disproof is welcome.Contributions welcome: proofs of any milestone, a proof of the goal, and a disproof of the probe.
Estimating a probability density, a conditional probability or a conditional density from data can be written as solving a linear operator equation whose right-hand side is a distribution function. The true is unknown; only its empirical estimate is available, built from observations. The Glivenko–Cantelli theorem and the Kolmogorov–Smirnov law (Vapnik 2000, §7.3) guarantee that is close to in the uniform metric. However, the operator (for densities, integration) has an unbounded inverse. A small change in the right-hand side can produce an arbitrarily large change in the solution, so solving directly gives nonsense. Hadamard called such problems ill-posed.
Regularization handles this. Tikhonov (1963) proposed replacing the equation by the minimization of a penalized residual. Tikhonov and Arsenin (1977) proved that the regularized solutions converge to the true solution when the data error and the regularization parameter go to zero together in a controlled way. Vapnik and Stefanyuk (1978) extended this to random right-hand sides, the case of statistical estimation, and Stefanyuk (1986) to the case where the operator is estimated as well. Chapter 7 of The Nature of Statistical Learning Theory collects these results, without proofs, as the foundation of its SVM approach to density and conditional-probability estimation. This mission formalizes them.
Let and be metric spaces and a continuous one-to-one operator. The operator equation (7.12) is . Its solution exists and is unique, but need not be continuous.
A regularization functional is a map that is lower semicontinuous and whose sublevel sets are compact for every . Its domain is . In Lean this is NatureSLT.IllPosed.IsRegularizer.
Tikhonov's functional (Method T) for a parameter and a right-hand side is
which is NatureSLT.IllPosed.tikhonovFunctional. A regularized solution is any minimizer of over .
In the deterministic problem, for every an approximation with is given, and minimizes with and . In the stochastic problem, are random elements of converging to in probability, and minimizes with and . When the operator is also estimated by random continuous operators , their distance to is measured by (7.48),
which is NatureSLT.IllPosed.operatorDistance.
Let the exact solution lie in the domain of , and suppose satisfies (7.17):
Then every family of minimizers of satisfies in as . This is the weakest statement in the chapter: it fixes no rate and assumes only metric structure.
The constants are the book's: the of (7.17), the of (7.21), the factor and the threshold of Theorem 7.4, and the , of (7.49).
Theorem 7.1 is what makes regularization a method rather than a heuristic: it names the admissible parameter choices, no faster than , under which the regularized solution recovers the true one. Theorems 7.3 and 7.4 turn it into probability statements. Combined with any rate of convergence of the empirical distribution function, they give consistency of density estimation by Method T, which is the Corollary on p. 239. Theorem 7.5 does the same when the operator itself is estimated from data, as in conditional probability estimation (§7.9). Chapter 7's SVM estimators of densities and conditional probabilities rest on these statements.
The results are classical and proved in the literature cited. None of them is machine-checked. The platform has Tikhonov-regularized dynamics (TikhonovHDD) and finite-dimensional ridge identities (RobustLS.Tikhonov), but not the convergence theory of Tikhonov's method for operator equations. A formalization supplies a reusable notion of regularization functional on a metric space, the Tikhonov functional over , and the operator distance (7.48), for later work on inverse problems and nonparametric estimation.
The obvious approach, inverting and passing to the limit, fails because is not continuous: alone does not force . The deterministic theorems need control of the regularized solutions that the residual does not give, and in Theorem 7.2 that control must be obtained without compact sublevel sets, since the balls of an infinite-dimensional Hilbert space are not compact. In the stochastic theorems the difficulty is uniformity: a deterministic convergence statement for each outcome does not give the explicit comparison of probabilities that (7.21) and (7.49) assert. In (7.49) the bound must hold for every parameter below a threshold that depends only on , , .
Two warnings from reading the chapter apply. Theorem 7.4 as printed is false: with exact data () both probabilities vanish for all large , and the strict inequality fails (finding F1). Also, the three "uniqueness" properties of listed on p. 235 are mutually inconsistent at , which is why they are not assumed (finding F3).
All statements live in NatureSLT.IllPosed. takes values in ℝ≥0∞. The book's "positive" is nonnegativity and its domain is . "Semicontinuous" is lower semicontinuity. The exact solution is assumed to lie in the domain of (the book assumes this tacitly); otherwise every point could minimize . Every theorem is stated for every family of minimizers, given as a hypothesis, never for a chosen sequence, and does not assert that minimizers exist. Statements of the form "there exists a sequence that converges" are a trivializing formalization and are ruled out. The limit in (7.17) is read as a limsup in , and is taken along . Hilbert spaces are real. Linearity of (Theorems 7.2 and 7.4) makes a real normed space. In the stochastic theorems the probability space is arbitrary, and the random elements , (and in 7.5 the random distance ) are Borel measurable by hypothesis, so no event gets probability zero by convention. In (7.48) a point with contributes if and otherwise. In Theorem 7.5, is quantified before the random data, so it is uniform over all of them.
Beyond the paper. One variant item is posed: [Corrected] Theorem 7.4, the same statement with in place of . Its evidence is the exact-data counterexample above, which has been checked in Lean. The faithful Theorem 7.4 stays a milestone.
Not included: the Glivenko–Cantelli theorem in the book's in-probability form (the platform's GlivenkoCantelli.glivenko_cantelli is the almost-sure form), the Kolmogorov–Smirnov limit laws (7.10)–(7.11), and Theorem 7.6, whose notion of consistency is not pinned down on the page. Contributions welcome: compactness arguments in metric spaces, weak compactness and the Radon–Riesz property in Hilbert spaces, and measurability lemmas for minimizers.
A support vector machine never computes its feature map. It only evaluates a kernel , the inner product of the feature vectors of and . When the features are the first terms of an expansion, or infinitely many terms damped by regularizing weights, the learning algorithm is practical only if that inner product has a closed form. Chapter 6 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1), §6.3–6.5, gives such closed forms for the kernels generating orthogonal-polynomial, spline and Fourier expansions. It also states Theorem 6.1, which lifts any one-dimensional kernel to dimensions. The book prints these identities without proof and cites classical sources (Mikhlin 1964; Gradshtein and Ryzhik 1980). Several of them, as printed, are off by a constant factor, which a formal check settles.
Kernels in this mission are real functions of two real variables (or of two vectors of ) of the form , a finite or convergent sum over basis functions with weights .
For and real with , the series converges and
The only numbered theorem of the section, Theorem 6.1, is close to an unfolding of the definitions. The goal is therefore the deepest identity of the section that is correct as printed.
Milestones 2, 4 and 6 are stated exactly as printed and are believed false (see Formalization scope). A disproof of each is a complete answer.
The result itself. Each closed form replaces an infinite or high-dimensional inner product by a constant number of elementary operations. That is what makes the regularized Fourier, Hermite and spline kernels usable in an SVM. Theorem 6.1 is the mechanism by which every multidimensional kernel of Chapter 6 is obtained from a one-dimensional one. The constants matter in practice. A wrong prefactor rescales the kernel matrix, and so the effective regularization of the SVM solution.
Formalizing it. The identities themselves are classical (Christoffel 1858, Darboux 1878, Mehler 1866, and the Fourier series of on ). As far as a search of the platform shows, none is stated on Prove2Me in these forms. SpikedWishart.Separated.eq_299 (Open) is one Christoffel–Darboux instance for a specific Hermite family. AronszajnRK.Product.direct_product_kernel concerns reproducing-kernel Hilbert spaces, not finite or summable feature sums. The mission produces machine-checked versions of the book's catalogue, together with a formal verdict on the three displays that are off by a constant.
The goal and (6.32) are infinite-series identities with no ready-made counterpart in the library, and the goal holds only on . Outside that range the left side is -periodic and the right side is not, so no argument that ignores the range can succeed. The Christoffel–Darboux formula needs a theory of orthogonal polynomials for a general measure, which Mathlib does not yet provide. (6.24) involves the iterated derivatives of and a doubly infinite parameter family. The spline identity requires evaluating a piecewise-polynomial integral exactly. Theorem 6.1 for infinite bases requires summability over a product index set . The three false displays (2, 4, 6) hide their error in a constant factor. Two of them still reduce to an identity a solver may expect to hold.
Everything is over . Series are stated with HasSum, or as Summable together with an equation for tsum. A divergent series therefore never reads as . Sums over are written over with in place of . The Christoffel–Darboux polynomials are indexed as in the book ( is the constant), they are orthonormal up to , and the measure has all moments finite. The Hermite is the physicists' family, defined through iteratedDeriv. It is not Mathlib's probabilists' Polynomial.hermite. The normalization constants of (6.24) are existentially quantified, since the book does not give them. The range of in (6.24) and (6.26) is : the book's without the singular point . The Dirichlet display is stated where . The goal adds , which the page leaves unstated. Spline points lie in with . In Theorem 6.1, the multidimensional kernel is the sum over multi-indices of products of basis functions, a statement to be proved and not the product of kernels by definition. A formalization that defined the -dimensional kernel as would make the theorem trivial, and is ruled out.
Beyond the paper. Three corrected variants sit beside the faithful statements. Each changes one clause only. dirichlet_kernel_corrected (finding F1) uses the denominator , since at and the printed display reads . hermite_kernel_corrected (F2) takes without the Gaussian factor. At the printed (6.24) forces for all , and the corrected form is Mehler's formula. hermite_kernel_multidim_corrected (F3) uses the prefactor , since at , , the printed (6.26) reads . One further observation is recorded without a variant: (6.33) also holds for , because both sides are even in .
Reusable beyond this mission are the two definitions (the physicists' Hermite functions and the truncated power) and any proof of the summable form of Theorem 6.1. Proofs, disproofs of the three false milestones, and general lemmas on Fourier series of and are all welcome.
Primal-dual interior-point methods are the standard polynomial-time algorithms for linear programming and the basis of most commercial LP solvers. They do not move along the boundary of the feasible polyhedron, as the simplex method does. Instead they follow a curve through its interior, the central path, toward the solution set. Every convergence and complexity result about these methods assumes that this curve exists. Stephen J. Wright's monograph Primal-Dual Interior-Point Methods (SIAM, 1997, doi:10.1137/1.9781611971453) proves existence in its Chapter 2 from the standard LP background: existence of solutions, boundedness of solution sets, the Goldman–Tucker partition, and a primal-dual logarithmic barrier.
This mission is the first in a series that formalizes the book chapter by chapter. Later missions (potential reduction, path following, infeasible methods, finite termination, the homogeneous self-dual form) take the objects defined here as given.
Let , and . Nothing is assumed about the rank of . The primal and dual linear programs in standard form are
with all vector inequalities componentwise. The primal-dual feasible set consists of the triples with , and . The strictly feasible set is the same set with . The solution sets are , the minimizers of (2.1); , the maximizers of (2.2); and . The index sets and collect the coordinates for which some has , and some has , respectively.
For , the central path conditions (2.25) ask for with
The reduced strictly feasible set is the set of pairs such that for some . The primal-dual log barrier on it is
In Lean all of these objects live in the single definition module WrightPDIPM.CentralPath.LP, under the names F, Fo, OmegaP, OmegaD, Omega, indexB, indexN, Hcirc, ftau and CentralPathConditions.
If and , then two things hold. First, has exactly one local minimizer relative to :
Second, the central path conditions (2.25) have a solution .
The result itself. Theorem 2.8 shows that the central path exists as soon as the problem has a strictly feasible primal-dual point. Every path-following and potential-reduction method in the book either tracks this curve or measures its iterates against neighbourhoods of it, so the theorem is the foundation the book's convergence and complexity results stand on. Theorem 2.4 provides the strictly complementary partition , which the local and superlinear convergence analysis and the finite-termination results use. Theorems 2.1 and 2.3 are the duality and boundedness facts beneath both.
Formalizing it. These are classical results with complete textbook proofs. The work left is machine-checking them in the book's own form: standard-form LP, no rank assumption, the primal-dual barrier rather than the primal barrier, and minimality relative to . Related statements are already on the platform: Farkas's lemma and LP strong duality in Bertsimas–Tsitsiklis form, a central-path theorem in Matoušek–Gärtner form under the assumption with the primal barrier, and Goldman–Tucker for the inequality-form LP. None of them is any of the statements above, but their proofs may be reusable.
The natural first step is to minimize by compactness. This does not work directly, because is neither closed nor bounded and is not coercive on all of . The quadratic term is indefinite in general, and only its restriction to the affine set of feasible pairs is linear. To obtain a minimizer one must show that the level sets of inside are compact. This needs a boundedness statement (Lemma 2.5) that uses a strictly feasible point in an essential way, together with lower bounds that keep away from . A second difficulty is that has empty interior in whenever . Passing from the minimizer to the conditions (2.25) is therefore a constrained first-order argument with multipliers, and it must work without having full row rank, so the multiplier is not unique. For Goldman–Tucker, the obstacle is the step from "every index is positive at some optimum" to a single optimum that is positive on every index of and of at once.
Vectors are Fin n → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ. Inequalities are componentwise. Indices are 0-based in Lean and is Set.univ. Primal-dual points are triples (x, λ, s). "Bounded" means Bornology.IsBounded. and are defined as sets of optimal points (feasible, and at least as good as every feasible point), so no infimum or supremum is taken and an unattained optimum gives the empty set. No rank assumption on is made anywhere. No result in this chapter has an or an unspecified constant, so no constants are instantiated.
"Local minimizer in " means IsLocalMinOn (ftau τ) (Hcirc A b c), that is, minimality among nearby points of . Local minimality in all of would make the claim false. Uniqueness is asserted for the minimizer only, never for . uses Real.log and is only ever evaluated on , where every .
The hypothesis is part of the goal and cannot be weakened. If , then and the first conclusion becomes false. A formalization that drops it, or one that replaces "unique local minimizer on " with "a global minimizer exists", is not this theorem.
The book prints Theorem 2.4 without a hypothesis. The faithful item carries the section's standing case , which by Theorem 2.1 gives .
Beyond the paper. One sharpness probe, theorem_2_4_probe, states Theorem 2.4 exactly as printed, with no hypothesis. It is expected to be false. For , , , the primal is infeasible and the dual objective is unbounded, so . A disproof is the sought outcome.
Infrastructure that is reusable beyond this mission includes the standard-form LP objects, the solution sets and the / partition, all of which later chapters use; KKT conditions for linearly constrained convex minimization; and strict convexity of . Contributions of general lemmas toward any of these are welcome.
A separating hyperplane in is a classifier of VC dimension , so a bound on its generalization error that goes through the VC dimension degrades with the dimension of the space. Support vector machines construct hyperplanes in feature spaces of enormous dimension and still generalize. Chapter 5 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) explains this by a different capacity measure. When a hyperplane is required to separate the data with a margin , and the data lie in a ball of radius , the VC dimension is bounded by roughly , independently of .
Timeline. The optimal (maximal margin) hyperplane goes back to Vapnik and Chervonenkis (1965, 1974). Its use with kernels, in place of an explicit feature space, is due to Boser, Guyon and Vapnik (COLT 1992), and the soft-margin support vector machine to Cortes and Vapnik (Machine Learning 20 (1995)). The margin bound appears as Theorem 5.1 of the book, which prints no proofs (Preface, p. xi). In Burges's tutorial (Data Min. Knowl. Disc. 2 (1998)) the bound for "gap tolerant classifiers" carries a ceiling, .
Vectors live in with the Euclidean inner product . A -margin separating hyperplane is a hyperplane with and . It classifies as if and as if ; vectors in the strip get no label (§5.4.2, p. 132). Vectors are shattered by these hyperplanes if each of the labelings is realized by one hyperplane that classifies every with label . The VC dimension on a set is the largest for which some are shattered, or . In Lean these are MarginClassifies, MarginShatters and marginVCDim in NatureSLT.Margin.
For training data with , a hyperplane is in canonical form if for all (5.8). The optimal hyperplane satisfies (5.8) and minimizes over and (5.9). Its support vectors are the with equality in (5.8). The dual functional is (5.17). In Lean: IsCanonicalSeparating, IsOptimalHyperplane, supportVectors and dualW.
If every lies in a sphere (closed ball) of radius and , then
with the integer part. As printed this is false (see Beyond the paper), and a disproof of the goal is a legitimate outcome of the mission.
Theorem 5.1 is the reason the book gives for the generalization of the optimal hyperplane in high-dimensional feature spaces (§5.6.1). With the bound (3.24) it drives the Corollary on p. 133 and the choice of in structural risk minimization. Milestones 1–4 are the convex-optimization facts on which the construction of the support vector machine rests: margin maximization as a quadratic program, its Kühn–Tucker characterization and the dual problem. Milestone 5 is the condition under which a kernel can replace the feature-space inner product.
On the platform, UnderstandingML.hard_svm_max_margin (the analogue of milestone 1 with the convention ) and UnderstandingML.support_vectors (the bias-free Hard-SVM) are proved. UnderstandingML.kernel_iff_posSemidef characterizes kernels by positive semidefinite Gram matrices, and HighDimStat.Rkhs.thm12_20_mercer_v2 (open) is the eigen-expansion of a continuous kernel on a compact space. There is no margin-dependent VC dimension bound; the BartlettNN.Margin.* results bound fat-shattering dimensions of real-valued classes. The mission adds the book's bias-carrying statements, the first formal Δ-margin VC bound, and machine-checked settlements of the misprinted statements.
The dimension part of the bound, , is the classical VC dimension of affine half-spaces; the content is the radius part. A solver has to control how far apart the two classes of an arbitrary dichotomy of points in a ball can be pushed by a unit-normal hyperplane with a free bias. The bias does not cancel for unbalanced dichotomies, and this is exactly where the printed integer part and the correct bound part ways. The Kühn–Tucker milestone requires optimality conditions for a convex quadratic program with linear inequality constraints. The Mercer milestone requires the spectral theory of Hilbert–Schmidt integral operators on of a set of positive Lebesgue measure. Neither is packaged in Mathlib in this form.
Vectors are EuclideanSpace ℝ (Fin n); training data are indexed by Fin ℓ; labels are real numbers with as a hypothesis, and both classes present, the setting of §5.5. In the shattering definition, labels are booleans. "Sphere of radius " is a closed ball about an arbitrary center; and are hypotheses. The VC dimension takes values in , so an unbounded family is , never a junk value. Shattering requires every point to be classified with its margin: a definition that let points fall into the strip would make the bound trivial, and is ruled out. Optimality is a predicate on a given pair ; no item asserts that an optimum exists. The typo "" of §5.4.2 is read as . The Mercer items take () measurable of positive Lebesgue measure, with orthonormal in and the expansion converging in .
Not drafted: the Corollary on p. 133 and Theorem 5.2 (p. 139). Both are probabilistic, and their hypotheses (what the VC dimension of a set of partial classifiers means inside (3.24), the training-set size in the leave-one-out argument) are not pinned down on the page.
Beyond the paper. Two [Corrected] variants are posed beside the faithful items. (1) Theorem 5.1 with the ceiling : the vertices of an equilateral triangle inscribed in the unit circle of are shattered with , while , a counterexample to the printed bound that has been checked in Lean. (2) Mercer's theorem with in the condition and the coefficients: a kernel over the incomplete system on has positive coefficients, yet for .
Contributions welcome: a convex-quadratic-programming KKT library for finitely many linear constraints; integral operators with kernels and their spectral expansion; disproofs of the faithful Theorem 5.1 and Theorem 5.3.
Empirical risk minimization (ERM) chooses, from a fixed set of functions, the one with the smallest average loss on the training sample. Its risk is controlled by bounds whose confidence term grows with the VC dimension of the set and shrinks with the sample size . When the ratio is small, a fixed set is either too poor to approximate the target or too rich to be estimated reliably. The structural risk minimization (SRM) principle of Vapnik and Chervonenkis (1974) resolves this by nesting sets of growing capacity and choosing, as a function of the sample size, the element in which to minimize the empirical risk. It is the conceptual ancestor of model selection by complexity penalties, of support vector machines' margin control, and of the minimum description length principle.
Chapter 4 of Vapnik's The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) states the asymptotic rate of SRM (Theorem 4.1) together with the two finite-sample risk bounds it rests on, (4.1) and (4.2), and the finite-class bound (4.25) from which the book derives its minimum description length bound. The book prints no proofs; the standard ones are in Vapnik, Statistical Learning Theory (Wiley 1998), and Vapnik–Chervonenkis, Theory of Pattern Recognition (1974).
Let be a probability measure on a set and , , a set of nonnegative measurable functions indexed by an arbitrary set . The risk is and the empirical risk on an i.i.d. sample is .
The VC dimension of a set of real functions is the largest number of points shattered by the indicators , , , where for and otherwise (§3.6). In Lean: NatureSLT.SRM.vcDimReal Q A B : ℕ∞.
A structure is a sequence of nested nonempty subsets , (4.3). It is admissible if each has finite VC dimension and either (i) on , or (ii) for some (4.4). Write in case (i) and in case (ii). The union is assumed dense in for the metric .
A law (4.5) chooses an element, and minimizes over . The rate of approximation is (4.8).
Following footnote 3 (p. 97), random variables converge to with asymptotic rate if, for some constant , in probability. In Lean: NatureSLT.SRM.ConvergesWithRate.
If the law satisfies
then converges in probability to with asymptotic rate
This is NatureSLT.SRM.theorem_4_1, stated as printed. Finding F1 shows that as printed it is false: a law that keeps returning to a small element satisfies (4.7) while the risks oscillate. Finding F4 shows that the footnote-3 notion of rate can fail even when . A disproof of the goal is therefore a legitimate outcome.
Every constant is the book's: the and of , the and the under the root in (4.1), in (4.2), and the under the root in (4.25).
Theorem 4.1 is the book's asymptotic statement that SRM is consistent and adapts to the target. The rate is the sum of an approximation term and an estimation term, so a priori knowledge of the approximation rate yields the best law , as in the Example (4.9) on p. 98, where gives the rate . The bounds (4.1) and (4.2) are the finite-sample inequalities SRM minimizes in practice, for bounded and for heavy-but-not-too-heavy-tailed losses. (4.25) is the starting point of the book's comparison of SRM with the minimum description length principle (Theorem 4.3).
The platform holds related but different statements: UnderstandingML.srm_bound and UnderstandingML.srm_nonuniform_rate (SRM as nonuniform learning over a countable union with weights), UnderstandingML.mdl_bound (a prefix-free description-length bound with other constants), and FoundationsML.ModelSelection.srm_learning_guarantee_v2 (Open, Mohri et al.'s form). None states the asymptotic rate of Theorem 4.1 or the relative-deviation bounds (4.1), (4.2), (4.25) in the book's form. As far as is known, none of the four statements of this mission has a machine-checked proof.
The goal combines three things that each fail in a naive treatment. First, the uniform bound must be applied to a different class at every sample size, so its constants must be uniform in the element. Second, the approximation term tends to only if , which (4.7) does not imply; a proof that assumes it proves a different theorem. Third, the footnote-3 rate is a statement about the limit of a normalized error, not a bound on it, so an bound alone does not establish it.
For (4.1) and (4.2), the step from a VC dimension to a bound with these exact constants goes through the relative-deviation inequality with the annealed entropy at and the bound on the growth function in terms of . For (4.25) the obstacle is the relative (not additive) form: Hoeffding's inequality gives the wrong shape and does not suffice.
Samples are functions under the product measure (Measure.pi). is a type, the structure is Λs : ℕ → Set Λ (monotone, every element nonempty, indexed from ), and , are given sequences tied to the structure by the two admissibility cases. The empirical minimizer is a given map from samples to , and its existence is not claimed. Measurability is explicit throughout. Each is measurable and integrable, and the risk of the minimizer is a measurable function of the sample. In (4.1) and (4.2), the event "the bound holds for all " is assumed measurable. The ratio in (4.4) and (3.19) is multiplied out, with assumed integrable. Infima are over nonempty sets bounded below by , so no junk value of ⨅ enters. In (4.1) and (4.2) the range is assumed: the page leaves it implicit, and outside it the printed can be negative and the printed bound false (finding F5). The trivializing formalization the series warns about, a non-measurable event read as probability or an infimum over an empty element read as , is ruled out by those hypotheses.
Beyond the paper. One variant is posed: NatureSLT.SRM.theorem_4_1_corrected ([Corrected], finding F1). It adds and reads the rate as for some constant . It is not a milestone. The planner also notes (F3) that the printed derivation of (4.27) from (4.25)–(4.26) has a gap. Those statements are not part of this mission.
Reusable infrastructure: the VC dimension of a real class, the product-measure sample space, and the footnote-3 notion of rate. Contributions welcome: proofs or disproofs of each item, and a published definition of vcDimReal that the other missions of this series could reference.
Statistical learning theory asks when minimizing the error on a finite sample also controls the error on unseen data. For a set of classifiers, the answer given by Vapnik and Chervonenkis is governed by a single combinatorial quantity: how many different ways the set can label points. Bounds on the generalization error of empirical risk minimization are stated in terms of the logarithm of this number, the growth function, and they are informative only if the growth function grows sublinearly in .
The theorem at the centre of this mission says that there is no middle ground: the growth function is either exactly for every , or, from some point on, it is bounded by a logarithmic function . The integer is the VC dimension. This dichotomy is what turns the abstract bounds of Chapter 3 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) into constructive ones (Eq. (3.24) of the book).
Timeline. Vapnik and Chervonenkis announced the connection between the growth function and the shattering number in 1968 and proved it in 1971 (Theory Probab. Appl. 16 (1971)), in the form for all or . Sauer (J. Combin. Theory A 13 (1972)) and Shelah (Pacific J. Math. 41 (1972)) independently proved the sharp polynomial bound . The logarithmic form used in the book follows from that sum together with the estimate . The book states its results without proofs (Preface, p. xi).
Let be a nonempty set and a nonempty set of parameters, and let , , be a set of indicator functions on : each takes only the values and . For a sample (repetitions allowed), let
be the number of different binary vectors obtained as ranges over (Section 2.3.2, p. 42). The growth function is
(Section 2.7, p. 55), with the natural logarithm. Since , always .
Points are shattered if for every some has for all . The VC dimension is the maximum number of shattered points, or if arbitrarily many points are shattered (Section 3.6, p. 80). For a set of real functions , the VC dimension is that of the indicators , (Eq. (3.22)), where the step function is for and for .
In the Lean development these are numSeparations, growthFunction, Shatters, vcDim, stepFunction and vcDimReal in the namespace NatureSLT.GrowthFunction.
Either
or there is an integer with and such that
The range is the one the book gives in both of its restatements of the theorem: the display after the Definition on p. 79 and Eq. (3.23) on p. 83.
The dichotomy is what makes the VC dimension a usable complexity measure. Combined with the bounds of Section 3.3, it gives distribution-free generalization bounds whose confidence term depends on and only (Eq. (3.24)). It also explains why finiteness of the VC dimension is a sufficient condition for consistency of empirical risk minimization for every probability measure (p. 80): the growth function, divided by , tends to zero exactly when it is not linear. Examples 1 and 2 show that the VC dimension is not the number of parameters: linear functions have as many as their parameters, while a one-parameter family of sines has infinitely many.
The theorem is classical and has been proved many times. Related statements are already machine-checked on the platform in other forms: Sauer's lemma for concept classes (ComputationalLearning.sauer_lemma, FoundationsML.RademacherVC.sauer_lemma, HighDimProb.Chaining.sauer_shelah), the bound (ComputationalLearning.phi_polynomial_bound), the 1971 dichotomy with the bound for sets of events (VapnikChervonenkis.GrowthFunction.theorem1_growth_dichotomy), and the VC dimension of open halfspaces with labels (UnderstandingML.vcDim_halfspaces). What is not on the platform is the book's statement: the logarithmic bound for the growth function of an indexed set of -valued functions, with characterized through the growth function itself, and the book's examples with the closed half-space convention . This mission produces that statement and connects it to the shattering definition.
The obvious argument proves only half. That and pin down the largest shattered set is elementary; the content lies in the bound for : a class that shatters no points must realize only polynomially many labelings of every points, with the explicit constant of the logarithmic form, and nothing in the definition of the growth function gives this directly. A tempting shortcut is to read the bound as valid for every , as the theorem's display does in isolation: this is false whenever , since exceeds . The range is essential. For the examples, the upper bound in Example 1 is a Radon-type statement about points in , and Example 2 requires controlling the sign of simultaneously for all with one parameter.
Indicator functions are boolean-valued, true standing for , and written Q α z for the book's ; samples are maps Fin ℓ → Z, so indices run from . is the cardinality of the finite set of realized vectors in Fin ℓ → Bool; the supremum over samples is a supremum of natural numbers bounded by , and is Real.log of its cast. The VC dimension is valued in ℕ∞. and are assumed nonempty in every theorem, so the supremum is over a nonempty set of samples and is at least ; the junk value never enters. At the book's expression is undefined; the formal statements evaluate it as , the limit as , and the correct bound in that case, where . The step function has . Points of are EuclideanSpace ℝ (Fin n); in Example 1(ii) the bounds of the real-function definition are , .
A trivializing formalization is ruled out: the goal is the disjunction of a linear growth function and the explicit bound with fixed by and , not an existence statement over an arbitrary and not a bound in which an empty parameter set makes the growth function vanish.
Beyond the paper. One variant is posed beside the faithful goal: a sharpness probe (growth_function_dichotomy_probe) claiming the logarithmic bound for every , i.e. without . Its evidence: for and all subsets, and . A disproof is the sought outcome.
A complete development needs: finite cardinality arguments for sets of binary vectors, the Sauer–Shelah lemma for an indexed family (Mathlib has Finset.card_shatterer_le_sum_vcDim for finite set families), the estimate , Radon's theorem or an affine-independence argument for Example 1, and elementary trigonometry for Example 2. The bridge between indexed families of indicator functions and set families is reusable by every later mission of this series. Contributions of any milestone, of bridge lemmas to the existing Sauer-type theorems, and of a disproof of the probe are welcome.
Every guarantee that a learning machine trained by empirical risk minimization will perform well on unseen data rests on one kind of statement: a bound on the probability that, simultaneously over a whole set of functions, observed frequencies stray far from the probabilities they estimate. Vapnik and Chervonenkis proved the first such bounds for sets of events in 1968 and 1971 (Vapnik–Chervonenkis 1971), with the growth function as the capacity measure and the constant . Vapnik's later monographs (Estimation of Dependences Based on Empirical Data, 1979; Statistical Learning Theory, 1998) refined the constants, replaced the growth function by the distribution-dependent annealed entropy, introduced the relative-deviation bound that underlies fast rates for small risks, and extended everything to bounded real-valued loss functions. Chapter 3 of The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) collects the resulting "basic inequalities of the theory of bounds" in their final form, stated without proof, and derives from them the confidence bounds used throughout the book (structural risk minimization in Chapter 4, support vector machines in Chapter 5).
This mission formalizes those inequalities exactly as the book prints them.
Let be a probability space and let , , be a set of functions on indexed by an arbitrary parameter set (parameters need not be vectors). An i.i.d. sample is drawn from , i.e. from the product measure . For each the risk and the empirical risk are
When every is an indicator function (values in ), is the probability of the event and its frequency. The number of different binary vectors , , is , the number of separations of the sample by the set. Two capacity measures are built from it:
The annealed entropy depends on ; the growth function does not and dominates it.
For a set of real functions with , the book passes to the set of indicators , , , where for and otherwise; and are the annealed entropy and growth function of this indicator set.
For indicator functions and every ,
The constants are the book's: the factor , the exponent , and the entropy evaluated at . No sample-size restriction is imposed beyond .
The result itself. Theorem 3.1 and its relatives turn a capacity estimate into a confidence interval for the risk of every function in the set at once, including the one chosen by empirical risk minimization. They are the bridge between the combinatorics of Chapter 3 (the growth function is either or at most for VC dimension ) and every algorithmic guarantee in the rest of the book: structural risk minimization, the VC bound for margin hyperplanes, the support vector machine. The relative-deviation form (Theorem 3.2) is what makes bounds of order rather than possible when the empirical risk is near zero.
Formalizing it. The book prints no proofs. The classical argument is published (Vapnik–Chervonenkis 1971; Vapnik 1998, Chapter 4), but with other constants: the 1971 theorem has and needs , and the 1998 version has in place of . On Prove2Me the 1971 form is proved as VapnikChervonenkis.Inequality.theorem2_uniform_deviation_bound, together with its symmetrization and permutation lemmas, and finite-class uniform convergence with is proved as UnderstandingML.finite_class_uniform_convergence. Neither states the book's constants, the annealed entropy, the relative deviation or the real-function extension, so the statements here are new. Settling whether the book's constants hold as printed, for every , is part of the work.
The obvious route to Theorem 3.1 replaces the supremum over the possibly uncountable set by a finite one through a ghost sample of size and a count of separations on the doubled sample. Every step costs constants: the symmetrization inequality loses a factor and requires to be large, and the conditional deviation bound for sampling without replacement brings its own exponent. Reproducing the textbook argument therefore tends to yield the 1971 or 1998 constants, not the printed with no sample-size condition; reaching or refuting the printed form is the crux. The relative-deviation bound needs a separate normalization argument, and the real-function bounds require relating deviations of to deviations of its level-set indicators uniformly in the level .
The finite-class item (3.26) with (3.25) is expected to be false as printed: a single fair coin with and violates it (finding F1).
The sample is z : Fin ℓ → Z under Measure.pi (fun _ => F) with [IsProbabilityMeasure F]; is an arbitrary type and . Indicator functions carry the hypothesis that every value is or ; real functions carry with . and are written inline as the integral and the normalized sum. The event "the supremum exceeds " is written "some has deviation exceeding ", which is the same event for a strict inequality; a bare ⨆ α over an unbounded family would read Lean's junk value and make the bound trivially true, and is not used. Probabilities are compared in with ENNReal.ofReal of the real bound, and "with probability at least " is ENNReal.ofReal (1 - η) ≤ F^ℓ(event) with . In Theorem 3.2 and (3.4) the supremum runs over the with , which excludes the zero denominator.
The book assumes the events it measures to be measurable; this is made explicit: each is measurable, (or the counting function of the indicator set) is measurable on wherever an expectation of it appears, and the deviation events are measurable at every level. These hypotheses are needed so that a non-measurable count cannot turn into and make the bound vacuous or stronger than the book's. The finite-class items need no event-measurability hypothesis.
The definitions are numSeparations (, via Set.ncard of the set of vectors), annealedEntropy, growthFunction (a real supremum, bounded by for -valued families) and levelIndicators (indexed by , with ). They are reusable by any development of VC theory in this form.
Beyond the paper. One corrected variant is posed: eq_3_26_finite_corrected, the finite-class two-sided bound with in place of in (3.25). The evidence (finding F1) is that with and , , , the half-width is about while with probability . With the statement is the standard two-sided finite-class bound.
Welcome contributions: proofs or disproofs of the goal and milestones with the printed constants; proofs of the corrected variant; a disproof of the faithful (3.26) with (3.25).
A Jackson network of exponential single-server queues has a stationary distribution of product form: the numbers of customers at the nodes are independent in steady state, each geometric (Jackson, 1957; Jackson, 1963). The same property holds for a large family of networks (Kelly, Reversibility and Stochastic Networks, 1979), and it is what makes performance formulas for such networks explicit. A network can also be read as a quasi-birth-and-death process (QBD): take the number of customers at one node as the level and the vector of queue lengths at the other nodes as the phase. The phase set is then infinite, , and product form becomes the statement that level and phase are independent in steady state. Ramaswami and Taylor (Stochastic Models 12, 1996, pp. 121–142 and 143–164) characterized when a QBD has this independence property and used the characterization to find new product-form networks. Chapter 15 of Latouche and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM, 1999), gives a simplified version of these results, and this mission formalizes it.
Fix a countable set of phases, finite or infinite, and four real matrices indexed by . A continuous-time QBD is the Markov process on the states , with level and phase , whose infinitesimal generator is block-tridiagonal:
and are nonnegative, and have nonnegative off-diagonal and strictly negative diagonal entries, and the rows of sum to zero. The level is the set . The process stays in a state for an exponential time of rate and then jumps to with probability ; this jump chain together with the mean sojourns describes it. It is assumed irreducible and regular (finitely many transitions in every bounded time interval). It is positive recurrent if it returns to every state with probability one and the expected return time is finite. A stationary probability vector , partitioned by levels, satisfies , and .
Two matrices indexed by phases are defined by what they mean for the process:
The level is independent of the phase in steady state if for some probability vector on and some probability density on the levels. A vector is positive if for every phase.
The process is positive recurrent with level and phase independent in steady state if and only if there are a positive vector with and a scalar with
then for all . The criterion uses only the blocks of , not .
The goal says that independence of level and phase forces the level to be geometric, and it reduces the question to a linear system in for a fixed . That system involves only the generator's blocks, so it can be checked for models whose rate matrix has no closed form. Together with Theorem 15.2.1 it gives a QBD proof of the product form of open Jackson networks, and the same approach led Ramaswami and Taylor to product-form networks beyond Jackson's. The level-dependent version (§15.3) is described in the book but not proved there.
Formalizing the chapter adds the continuous-time layer of the matrix-analytic series: a generator on a countable state space, regularity, and positive recurrence defined by return times, with expected sojourn times as sums over trajectories of the jump chain. The product form of open migration processes, which contains the Jackson case, is on the platform as KellyStochasticNetworks.open_migration_equilibrium. It is a balance-equation statement about a network and does not concern QBDs. No QBD statement is on the platform.
The "if" direction of the goal looks like a computation: satisfies . But a solution of shows positive recurrence only through regularity, and on an infinite phase set that is a real hypothesis. Relating the generator condition to the eigenvector condition is the hard part. The book notes that the finite-dimensional argument (Perron–Frobenius theory for ) "fails in the case of an infinite number of phases": spectral arguments for are not available when is infinite, and every product of infinite matrices must be justified by nonnegativity. For Theorem 15.2.1, positivity of and is not visible in the hypotheses on the load. It comes from irreducibility of the network.
All declarations are in MatrixAnalytic.ProductForm. States are ℕ × ι with ι countable and arbitrary (levels from ; no finiteness of phases is assumed anywhere). The generator is qbdQ B A₀ A₁ A₂, and the hypothesis IsGeneratorC encodes the sign and zero-row-sum conditions. The continuous-time process is encoded through its jump chain and mean holding times, without measure theory. Irreducibility is that of the jump chain. Regularity (RegularCT) says that the sum of mean holding times along the jump chain diverges almost surely. Positive recurrence (PositiveRecurrentCT) says the return probability is one and the expected return time is finite. and are sums over taboo trajectories valued in , never solutions of . Defining by that equation, or positive recurrence by the existence of a stationary vector, would make the milestones circular and is ruled out. Positive recurrence and stationarity are separate objects. "Level independent of phase" is the factorization , not the geometric form, which is the conclusion. Vector equations over infinite phase sets are convergent sums; products of nonnegative matrices are computed in . The Jackson network indexes nodes by Option J with J finite, none being node 1. Its blocks are written out rate by rate, and the openness of the network ( invertible) is carried as the meaning of "the solution" of the traffic equations.
A complete development needs the theory of continuous-time chains on countable spaces through the jump chain (invariant measures, positive recurrence, the regular case), the continuous-time matrix-geometric property, and the series representation of . These are reusable well beyond this mission, and contributions of any of them are welcome.
A retailer of a seasonal or perishable product must commit to a stock level before demand is known, and must also choose the price at which to sell. The two decisions interact: the price shifts the demand distribution, and the stock level determines how much of that demand can be served. The price-setting newsvendor is the single-period model of this interaction. It goes back to Whitin (1955) and Mills (1959), and it is the building block of the joint pricing and inventory literature in operations research and economics.
Petruzzi and Dada, Pricing and the Newsvendor Problem: A Review with Extensions, Operations Research 47(2), 1999 (doi:10.1287/opre.47.2.183), unify the additive and multiplicative versions of the model and give conditions under which the joint optimum is characterized analytically. Their Theorem 1 treats additive demand. Earlier results required the demand noise to be a Pólya frequency function of order 2 (Ernst 1970) or extended this to the log-normal (Young 1978). Theorem 1 replaces those assumptions by a condition on the hazard rate that every distribution with a nondecreasing hazard rate satisfies.
Demand at price is with , where , . The noise is a random variable on the range , , with probability density (nonnegative, zero off , integrating to ), distribution function and mean . The paper requires . Stocking costs per unit; each leftover unit is disposed of at cost with (a negative is a salvage value); each unit of unmet demand costs a penalty . No sign is imposed on or .
The firm stocks units, where is the stocking factor. Leftovers occur when , shortages when . The expected profit is
With expected leftovers and expected shortages , it splits as , a riskless profit less a loss function (eqs. (1)–(3)). The riskless price is . The firm solves
For each fixed the best price is (Lemma 1), so (4) reduces to maximizing over . The hazard rate is .
The Lean development lives in the namespace PetruzziDada.Additive. The definition Model carries the data with the standing assumptions above, and defines y, F, μ, Λ, Θ, expProfit (the integral above), Ψ, L, p0, price, reducedProfit (), R (its derivative), hazard and HazardCondition.
If for and , then there is with
The optimal policy is then , . The goal leaves the density arbitrary beyond the stated condition.
Theorem 1(b) is also stated, as printed, but it is not a milestone (see Difficulty).
Theorem 1 tells a practitioner when the joint stocking and pricing problem needs only its first-order condition: one root-finding problem in replaces a two-dimensional search. The hazard condition holds for every density with a nondecreasing hazard rate, such as the uniform density on , and it tolerates a hazard rate that decreases, as long as it does not decrease faster than . The result is the analytical core of much later work on joint pricing and inventory decisions.
The theorem is proved in the paper; it has not been machine-checked. Formalizing it puts the classical price-setting newsvendor on the platform: an objective defined by an integral whose limits move with the decision, a reduction by optimizing out the price, and a unimodality argument for a derivative. The definitions (the density model, , , the hazard rate) are reusable for the multiplicative case of the same paper and for other newsvendor results.
The objective is an integral with variable limits and a density that is assumed only integrable, so eq. (5) is a Leibniz rule in which pointwise continuity of cannot be used. The derivative of the reduced objective is itself differentiable only where is, and its second derivative involves . The hazard condition, however, controls the sign of only at critical points of , and turning that local information into a global shape of on a closed interval, with a density that may jump at , is a real-analysis lemma that Mathlib does not provide in this form.
Two published steps need care. The printed proof says "", but the model allows ; Theorem 1(c) still holds then, by a different argument (finding F3). Theorem 1(b) claims that is the largest root of under the hazard condition alone, and this is false as printed: when the maximum can sit at , which need not be a root (finding F1; for uniform on , , , , , no root exists). Theorem 1(c)'s extra hypothesis is exactly what excludes this.
The distribution of is given by its density , with , off , interval-integrable on and ; the bounded range is part of the model. All integrals are interval integrals. The expected profit is the integral of p. 184, not , and optimality ranges over and every real price . The hazard rate is , which Lean evaluates to where ; the hazard condition is therefore required on instead of the printed , since is undefined. At each the condition asks for a genuine derivative of relative to (one-sided at ) with , never a junk derivative. The derivative is Mathlib's deriv; the reduced objective is differentiable everywhere, which is part of a milestone. The milestones on and add continuity, respectively differentiability, of and , which the paper uses silently; the goal adds nothing. The milestone on the endpoint values states without the printed "".
These choices rule out the trivializing formalizations: an objective defined as (which would make eq. (1) definitional and Lemma 1 a quadratic identity), optimality over alone or over all real , a hazard condition read through a junk derivative (which would reduce it to ), and a goal restricted to uniform, exponential or IFR densities.
Beyond the paper. Two variants are posed beside the faithful statements. theorem_1b_corrected (corrected, finding F1) replaces the conclusion of Theorem 1(b) by " is or the largest root"; the uniform counterexample above shows the printed conclusion fails while the corrected one holds. theorem_1c_probe (sharpness probe, finding F2) is Theorem 1(c) with optimality over all real ; for the reduced objective is with , which is unbounded, so a disproof is expected and shows that the restriction to cannot be dropped.
Contributions welcome: proofs of the milestones, general lemmas on interval integrals with moving limits against an integrable density, and a reusable unimodality lemma ("a function whose critical points are all strict local maxima rises, then falls").
Many queueing, inventory and storage models are Markov chains on a two-dimensional state space : a level (a queue length, a stock level) and a phase (the state of an arrival or service environment). When customers arrive in batches, the level can jump up by several units in one step but comes down one unit at a time; when services are grouped, it is the other way round. These two families, the M/G/1-type and GI/M/1-type chains, were developed by Neuts along separate lines (Neuts 1981; Neuts 1989, references 2 and 3), and they are the embedded chains of the classical M/G/1 queue at departures and the GI/M/1 queue at arrivals.
Chapter 13 of Latouche and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling (SIAM 1999, doi:10.1137/1.9780898719734), shows that both families are embedded in quasi-birth-and-death processes (QBDs), and derives from the QBD theory of the earlier chapters the two central results: the first-passage matrix of an M/G/1-type chain is the minimal nonnegative solution of , and the stationary distribution of a GI/M/1-type chain is matrix-geometric, . This mission formalizes those statements.
Fix a countable set of phases and two sequences of real matrices and . States are pairs , , ; the level is the set of states with first coordinate . Row vectors act on the left: is the row vector .
The M/G/1-type chain (skip-free to the left) has transition matrix (13.1): from it moves to with probability ; from , , it moves to with probability , . The GI/M/1-type chain (skip-free to the right) has transition matrix (13.2): from it moves to with probability and to with probability , . Both matrices are assumed stochastic: nonnegative entries, rows summing to one.
The M/G/1-type chain is embedded in a QBD (13.3) on the states : the level is and the phase is the pair , where counts the levels still to be climbed. A jump from to becomes the sequence , with probabilities (Table 13.1, blocks (13.4)–(13.7)). In this QBD,
with the first passage time from to , and is the QBD's matrix of first-passage probabilities from to .
A state is positive recurrent when its expected return time is finite, and a stationary probability vector is nonnegative, sums to one and satisfies .
For a stochastic M/G/1-type chain and every level , the matrix of (13.9) has finite entries and is the minimal nonnegative solution of
that is, it solves (13.10) and lies entrywise below every nonnegative real matrix with .
is the minimal nonnegative solution of (13.27), and, as printed, is for every the expected number of visits to before the first return to , starting from .
Theorem 13.1.4 turns a probabilistic object, the matrix of first-passage probabilities one level down, into the minimal solution of a matrix equation of the size of one level. Every numerical method for M/G/1-type chains, including the quadratically convergent algorithms of Bini and Meini, computes this solution. Theorem 13.1.5 (Ramaswami's formula) then gives the stationary distribution recursively from . Theorem 13.2.3 is the matrix-geometric property of GI/M/1-type chains, the origin of the matrix-analytic approach. Together these results cover the stationary analysis of batch-arrival and batch-service queues.
All four results are classical and proved in the book. None of them is formalized. Lean's Mathlib has no theory of first-passage matrices or of block-structured Markov chains. On Prove2Me the closest results are scalar ones: the geometric law of the G/M/1 arrival chain (QueueingFundamentals.GM1.arrival_point_geometric), the M/G/1 departure chain (QueueingFundamentals.MG1.*) and Foster-type classification of GI/M/1 chains (FosterQueues.GIM1.*). The matrix statements here contain those as the case of one phase.
The equation (13.10) follows formally from a first-step decomposition once is known to be well defined independent of the level. The hard part is the passage between the chain and its QBD embedding. A first passage of the QBD from down to splits into successive one-level passages, a strong-Markov decomposition that must here be carried out as an identity of sums over trajectories. Minimality cannot be read off the equation: it needs the comparison of with the iterates of the map started from , with every series over a possibly infinite phase set. For Theorem 13.1.5 the inverse has to be shown finite, which uses recurrence. Reading the interpretive clause of Theorem 13.2.3 literally is a trap (see below).
Everything lives in the namespace MatrixAnalytic.SkipFree. Chains are real matrices ℕ × ι → ℕ × ι → ℝ on a countable phase type ι, and nothing requires finitely many phases. The QBD embedding has phase type ℕ × ι. Levels are counted from . Stochasticity, irreducibility, positive recurrence (finite expected return time) and stationary probability vectors restate the platform definition mm_countable. Probabilities and expected numbers of visits (, , and the visits in (13.26)) are sums over finite trajectories of products of one-step transition probabilities, valued in . Products, powers and series of nonnegative matrices are also computed in . The book's is , and finiteness is a conclusion wherever the book asserts it. "Minimal" is entrywise, over nonnegative real matrices.
and are never defined as solutions of (13.10) or (13.27), nor as "the minimal nonnegative solution". That definition would make Theorems 13.1.4 and 13.2.3 true by construction. is the first-passage probability (13.9), and is existentially quantified with its probabilistic meaning stated.
Beyond the paper. Finding F1/F2: the interpretive clause of Theorem 13.2.3 names the wrong taboo set. With one phase, , , , the minimal solution of (13.27) is , but the expected number of visits to from before reaching is . The faithful item states the page and is expected to be disproved. The corrected variant gm1_matrix_geometric_corrected counts visits before the return to , which is what the proof's records.
Infrastructure needed: path-sum decompositions (first step, last exit, concatenation at a first-passage time) for countable chains, monotone iteration for matrix power series in , and censoring of a chain on a subset of states. All of these are reusable for the other chapters of this series. Proofs that go directly through the skip-free chain, without the QBD embedding, are welcome.