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.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A linear program is solved with known data, but in planning problems the data are often only known in distribution when the main decision is taken: demands, yields and requirements are revealed later, and a corrective action is taken after they are. E. M. L. Beale's 1955 paper On Minimizing a Convex Function Subject to Linear Inequalities formulates this situation in its §5, "Linear Programming with Random Coefficients", as what is now called a two-stage stochastic linear program with recourse. Beale's motivating example is the transportation problem of Hitchcock (1941) with random requirements at the destinations, where every unit of shortage or excess incurs a loss. The same model was put forward in the same year by Dantzig, Linear Programming under Uncertainty (Management Science, 1955), as the paper's note added in proof acknowledges.
Timeline:
Constants , and an matrix are given. The data , an matrix, and are random variables on a probability space : their distribution is known when the first-stage decision , , is chosen, and their values are known when the second-stage decision , , is chosen. The cost is
For a right-hand side the second-stage value is
and for fixed data the cost of a first-stage decision is . The expected cost is
The problem is to choose minimising . In Lean the value is secondStageValue D f b, the cost is cost c f D A β x, and the expected cost is expectedCost P c f D A β x, all in the namespace BealeConvexMin.RandomLP.
Assume that for every the second-stage minimum is attained for almost every outcome and that is integrable. Then
that is, is convex on the non-negative orthant. The statement fixes no distribution class: it is claimed for any known distribution of .
The result. Theorem 2 is the basic structural fact of two-stage stochastic linear programming: the first-stage problem is a convex program in , whatever the distribution of the data. It is what makes local optimality global for the first-stage problem, what justifies cutting-plane and decomposition methods that approximate from below by supporting hyperplanes, and what makes sample-average approximations convex programs. Theorem 3, joint convexity in the data, gives through Jensen's inequality the comparison between the stochastic problem and its mean-value problem that Beale draws on p. 182. The discrete reformulation (5.5)–(5.6) is the deterministic-equivalent linear program used for finitely many scenarios.
Formalizing it. The theorems are proved in the paper, and their content is classical. The mission produces machine-checked statements of the model with its implicit hypotheses made explicit (attainment of the second stage, integrability of the cost), and proofs of the three results in Lean. The platform already has related statements in other models (finite scenario sets with extended-real recourse, and a complete-recourse, finite-second-moment version); none has Beale's hypotheses, and none states convexity of for an arbitrary distribution.
The mathematics is short; the difficulty is in the encoding. The second-stage value is a minimum that may fail to exist: the second stage may be infeasible for some and some outcomes, or unbounded below. A real-valued infimum then takes an arbitrary default value, and convexity would become a statement about that default. Similarly, the mean value only exists when the cost is integrable. A faithful statement has to carry attainment and integrability exactly where the paper tacitly assumes them, on the domain the paper uses, and no stronger condition (such as complete recourse or moment bounds) that the paper does not make. In the discrete reformulation, the minimum over the whole family has to be matched with the probability-weighted sum of per-scenario minima.
Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, inner products dotProduct, and is the componentwise order. The random data are functions A : Ω → Matrix (Fin m) (Fin n) ℝ and β : Ω → Fin m → ℝ on a measurable space with a probability measure P; no measurability of the data is assumed beyond integrability of the cost.Many computations in scientific computing, statistics and machine learning need the trace of a matrix that is never formed explicitly: may be for a large sparse , an inverse , or a product of operators, and the only access to it is the ability to compute products for chosen vectors . Examples are log-determinant estimation in Gaussian process regression, counting triangles in graphs through , computing charge densities in electronic structure calculations, and generalized cross-validation in regularized regression. For such matrices the diagonal entries are not available, and computing them one at a time costs matrix–vector products.
Randomized trace estimators replace this by a small number of products: draw random vectors from a fixed distribution with and average the quadratic forms. Hutchinson (1989) introduced the estimator with Rademacher vectors and computed its variance; Silver and Röder (1997) used Gaussian vectors. Before Avron and Toledo (2011), the analyses of these estimators were variance computations, which do not say how many samples guarantee a given relative accuracy with a given probability. Avron and Toledo gave the first such sample bounds for several estimators, stated in terms of an guarantee; this mission formalizes their bound for the Gaussian estimator. Later work (Roosta-Khorasani and Ascher 2015; Cortinovis and Kressner 2022) sharpened these bounds and extended them to indefinite matrices.
Let be symmetric positive semi-definite, and write . Fix a number of samples . Let be random vectors whose entries are independent standard normal random variables. The Gaussian trace estimator (Definition 3.1) is
Each term has expectation , so is unbiased. A randomized trace estimator is an -approximator of (Definition 4.1) if
that is, if its relative error is at most except on an event of probability at most .
The analysis uses the eigenvalues of , listed with multiplicity, and the polynomial , where ranges over subsets of ; it satisfies .
For every symmetric positive semi-definite , every , every and every natural number with
the estimator is an -approximator of . The sample count depends on neither nor .
The theorem gives a number of matrix–vector products, , that suffices for a relative-error guarantee on the trace of any positive semi-definite matrix, independent of its dimension and spectrum. It is the reference row of the paper's Table I, against which the Hutchinson, normalized Rayleigh-quotient and unit-vector estimators are compared, and it is the form in which trace estimation enters the analysis of randomized algorithms for log-determinants, spectral densities and matrix functions.
The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The mission produces a machine-checked version with the constant and the range of made explicit, and with the misprints of the printed argument resolved (see Formalization scope). It also produces reusable pieces: the moment generating function of a Gaussian quadratic form, and the bound on elementary symmetric sums by powers of the power sum. Sharper constants, the removal of the restriction , or a direct formalization of the lower tail through a tail bound are welcome as further theorems.
Unbiasedness and the variance formula do not give the result: Chebyshev's inequality with yields , with a polynomial rather than logarithmic dependence on . A logarithmic bound needs exponential moments of , and the exponential moment of is finite only for below ; the argument has to choose inside that range uniformly in the spectrum, using only . The second obstacle is distributional: is not a sum of independent terms in the coordinates of , and reducing it to a weighted sum of independent variables requires the rotation invariance of the standard Gaussian vector. The paper proves only the upper tail with an explicit constant and states that the lower tail follows "using the same technique"; that step has to be supplied.
Matrices are Matrix (Fin n) (Fin n) ℝ; "symmetric positive semi-definite" is A.PosSemidef, "symmetric" is A.IsHermitian, and eigenvalues are Matrix.IsHermitian.eigenvalues. The sample space is Fin M → Fin n → ℝ with the product measure of copies of gaussianReal 0 1, so the law of the samples is constructed, not assumed; . Probabilities are Measure.real; the moment generating function is Mathlib's mgf; the variance is Mathlib's variance, and Lemma 5.1 asserts square integrability so that neither the integral nor the variance takes its default value. The sample count is a natural number ; and are real.
Corrections of the printed text, each recorded in the item's Formalization Note:
A formalization that makes the goal trivial is ruled out: the estimator's law is the explicit product Gaussian measure rather than a hypothesis, ranges over all natural numbers above the threshold, and the approximator predicate is evaluated on the genuine event .
A complete development needs rotation invariance of the standard Gaussian on (Mathlib's stdGaussian_map), the moment generating function of a squared standard normal, independence of products of Gaussian vectors, and a Chernoff bound from the moment generating function. The Gaussian quadratic-form results (milestones 1 and 2) are reusable for the other Gaussian estimators of the paper, such as the rank estimator of Lemma 5.3. Proofs of any milestone, alternative proofs of the lower tail, and helper lemmas on moment generating functions are welcome.
Retailers of fashion and seasonal goods sell at a premium price early in the season and mark down later. When customers anticipate the markdown, some of them wait, and the seller's pricing problem becomes a game between the seller and a population of forward-looking (strategic) customers. Aviv and Pazgal (MSOM 10(3), 2008) study this game in a model with limited inventory, stochastic arrivals and valuations that decline over the season, under two classes of seller policies: contingent pricing, where the discount depends on the inventory left, and announced fixed-discount pricing, where the seller commits to both prices upfront. Their numerical study (§7.3) compares the two classes and finds that precommitment can raise expected revenue by up to about 8%.
That comparison needs, for every announced price path, the customers' equilibrium response. Theorem 2 of the paper (p. 348) supplies it: a threshold purchasing policy, pinned down by a scalar fixed-point equation for the probability that a waiting customer is served. This mission formalizes Theorem 2. A companion mission of the same series formalizes Theorem 1, the contingent-pricing counterpart.
A seller has units to sell over a season , split at a fixed time with . Customers arrive by a Poisson process with rate . Customer has a base valuation drawn from a continuous distribution (tail ), and at time values the product at , where the decline factor is common to all customers.
Under an announced price path the seller commits to a premium price on and a discount price from on; does not depend on the remaining inventory. Customers know the initial inventory but not the current one.
A customer arriving at buys immediately if and only if (i) the current surplus is nonnegative and (ii) it is at least the expected surplus of waiting,
where is the probability that a unit will be allocated to the customer at time . Units left at are rationed at random among the customers who request one.
For a threshold function on the paper defines three segment rates: , the expected number of customers who buy at ; , those who could buy at but wait and want to buy at ; and , those whose valuation was below and who want to buy at . Each is times an integral over of at scaled prices (p. 345). With the Poisson probabilities, the allocation probability of units is
For let
and suppose solves
Then, when all other customers use (so that a waiting customer is served with the probability on the right of (8)), every customer arriving at buys immediately if and only if : the symmetric threshold profile is a Nash equilibrium.
Theorem 2 reduces the customers' equilibrium under an announced path to a single scalar . Everything downstream in §5 and §7 rests on it: the seller's expected revenue (p. 348) is written in terms of , the seller's optimal announced path maximizes it, and the comparison between announced and contingent pricing uses the resulting value . The theorem also explains the qualitative prediction of the model: the threshold exceeds exactly when the announced discount is deep relative to the decline of valuations, and it rises with the perceived availability .
The result is proved in the paper; to the best of our search it has no machine-checked proof. A formal development contributes the model objects (segment rates for threshold policies, the allocation probability for random rationing among Poisson requesters) in a form reusable by the rest of the series and by other strategic-customer pricing models, and a checked proof of the equilibrium property. The existence of a solution to (8) is not proved in the paper and is a natural further target.
The best-response part of the argument is elementary once the availability is known. The substance of the statement lies in the availability itself: the probability that a waiting customer is served is not a free parameter but the one generated, through (8), by the other customers' use of the same threshold. A formalization must connect the segment rates, the Poisson counts and random rationing into one expression and keep the fixed-point coupling between and intact; dropping it turns the theorem into a one-line inequality about an arbitrary . The division by also degenerates when and , and has to be excluded explicitly.
The Lean development lives in namespace SeasonalPricing.Announced. Conventions:
μ : Measure ℝ with IsProbabilityMeasure μ, = ProbabilityTheory.cdf μ, and continuity of (the paper's "continuous distribution") is a hypothesis of the goal. No support condition on is imposed; the statement quantifies over every real base valuation .tsum) as printed, not its closed form.availability is the right-hand side of (8), with built from by (7).Readings of the paper's informal words:
A formalization in which is an arbitrary number in , not tied to (8), is ruled out: it is the best-response lemma alone, not Theorem 2. Contributions welcome: proofs of the two milestones and the goal; lemmas such as and summability of its series; the closed form of printed on p. 346; and an existence result for (8).
In high-dimensional regression the number of candidate predictors can far exceed the number of observations . A regression function can then be estimated only if it is well approximated by a combination of a few elements of a large dictionary. The Lasso is the most widely used estimator in this regime. The question this mission formalizes is how well the Lasso predicts when the truth is not assumed to be sparse, or even to lie in the span of the dictionary.
A sparsity oracle inequality answers it. It bounds the prediction error of the estimator by the error of the best sparse approximation of the truth, which only an oracle knowing the truth could compute, plus a remainder proportional to the sparsity of that approximation times . Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) proved such an inequality for the Lasso under their restricted eigenvalue (RE) condition. Earlier oracle inequalities for Lasso-type estimators in fixed design (Bunea, Tsybakov and Wegkamp, 2006–2007) required the Gram matrix to be positive definite or to satisfy a mutual-coherence condition. The RE condition is weaker and allows , and it is now the standard hypothesis in this literature.
A dictionary is evaluated at fixed points . This gives the design matrix and, for an unknown regression function , the vector . The observations are
Nothing is assumed about . For the empirical norm is , and for we write . The column norms are assumed nonzero, with and . The support of is and its sparsity is .
The Lasso is any minimiser of
and .
Assumption RE holds with constant if, for every with and every with ,
The paper's is the largest such constant.
Fix , , , , and let RE hold with constant . With probability at least , every Lasso solution satisfies, simultaneously for all with ,
The theorem says that, up to the factor and a remainder of order , the Lasso predicts as well as the best -sparse linear combination of the dictionary. This is the case even when is not sparse and not in the span of the dictionary. The remainder is the parametric rate for parameters, inflated by and by the ill-posedness factor . Together with Theorem 5.1 of the same paper (mission II of this series), it shows that the Lasso and the Dantzig selector are within the same distance of the sparse oracle. The oracle inequality is used in aggregation, in model selection, and as a black box in later sparse-estimation papers.
The result is proved in the paper. It has not been formalized: at the time of writing, no Lasso oracle inequality and no probabilistic Lasso bound exist on Prove2Me or in Mathlib. What this mission contributes is a machine-checked proof of the paper's Theorem 6.1 with an explicit constant . The paper leaves unspecified, and its proof fixes the value used here. The mission also formalizes the Gaussian-tail step (B.4) and the deterministic basic inequality (B.1), both of which are shared with the paper's other Lasso results.
There is no sparse truth, so the usual argument does not apply. That argument places the error in the RE cone and reads off a rate. Here the competitor is arbitrary, and the approximation error can dominate the penalty terms, in which case the error is not in the cone. The RE assumption can be used only where the error does lie in a cone, and the cone constant available there depends on and on the column-norm ratio , because the penalty is weighted while RE is stated for unweighted vectors. What RE then yields is an inequality quadratic in with a cross term, not the form directly, and the constant is determined by how that cross term is absorbed. On the probabilistic side, the whole argument must run on one event of probability at least . That event may depend neither on nor on the choice of minimiser. The Lasso need not have a unique solution.
Matrix (Fin n) (Fin M) ℝ) and the target only through , which is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, independent random variables, each with law gaussianReal 0 σ², and .Classical non-cooperative game theory randomizes with objective, independent devices: each player spins a private wheel whose odds everyone agrees on. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) asks what changes when the randomizing events are ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. The paper introduced correlated equilibrium, and it also separates two effects that the classical model fuses: subjectivity (players disagree about probabilities) and correlation (players peg their choices on common or dependent events).
This mission formalizes the paper's result on subjectivity without correlation. Example 2.3 of the paper exhibits a three-person game in which strategies pegged on subjective but mutually secret events form an equilibrium that every player prefers to every classical mixed equilibrium. Proposition 5.1 shows that this cannot happen with two players.
A game has a finite set of players, a finite set of pure strategies for each player, a finite set of outcomes and an outcome function from onto . Player has a utility ; write for .
A randomizing structure consists of a set of states of the world with a -field of events, a sub--field for each player (the events is informed about), and a probability measure on for each player (the subjective probability of ). A strategy of is a map whose level sets lie in . For a profile of strategies the payoff of is
computed under player 's own beliefs. An equilibrium point is a profile with for every player and every strategy of .
An event is -secret if and every other player regards as independent of every event in the -field generated by the , : . A strategy is mixed if its level sets are -secret, and objective if each level set has the same probability under every . A measure is non-atomic on a -field if every event of of positive measure contains an event of of strictly smaller positive measure; a roulette is a sub--field of on which every is non-atomic. Throughout, Assumption II holds: every player has a -field of -secret events on which every is non-atomic.
For distributions on the classical payoff is , and is a Nash equilibrium point if no player gains by switching to another distribution.
Let and assume
Then for every equilibrium point in mixed strategies there is an equilibrium point in objective mixed strategies with
The game need not be zero-sum.
The result. Proposition 5.1 isolates correlation as the source of the new equilibrium payoffs of the subjective model in two-person games: disagreement about probabilities alone, with strategies pegged on secret events, reproduces only payoffs already achievable by classical mixed strategies (by Proposition 4.3, only Nash equilibrium payoffs). The paper uses it to explain Example 2.9, where two zero-sum players both expect more than the value, as an effect of subjectivity combined with correlation. Proposition 4.3 is the bridge that embeds classical Nash theory in the subjective model; with Nash's theorem it gives existence of equilibrium points in every game.
Formalizing it. The results are proved in the paper; to our knowledge none of them has been machine-checked. The mission produces a reusable measure-theoretic model of randomized strategies with private information and subjective beliefs (secret events, mixed and objective strategies, roulettes), a non-atomicity notion relative to a sub--field, and the Lyapunov-type construction of Lemma 7.1, none of which exists in Mathlib at the pinned revision.
The equilibrium conditions quantify over all strategies of the deviator, i.e. all -measurable maps, and the deviator may know events on which the opponent's mixed strategy is pegged. The obvious computation of as a sum of products of marginal probabilities is valid only because the opponent's strategy is pegged on secret events, which is the content of Lemma 7.3; for correlated strategies it fails, and Example 2.9 shows the proposition then fails. A second obstacle is that the replacement must reproduce player 2's beliefs about , while player 1's own equilibrium condition is stated under ; condition (5.2) is what transfers " is played with positive probability" from one player's beliefs to the other's. Constructing objective strategies with prescribed probabilities (Lemmas 7.1 and 4.1) needs the convexity of the range of a non-atomic vector measure (Lyapunov's theorem), which is not in Mathlib.
Players are a finite type (Fin 2 in the goal, players ); the and are finite types, and is surjective. The -field is an explicit parameter mΩ of the structure RandomizingStructure ι Ω mΩ, which carries the and the probability measures . Probabilities are -valued Mathlib measures. Utilities and are data (Assumption I is used only to compare lotteries by expected utility; the uniqueness of is not encoded). is a Bochner integral; for strategy profiles the integrand has finitely many values and is measurable, hence integrable. Non-atomicity on a sub--field is defined directly; Mathlib's NoAtoms (singletons are null) would trivialize Assumption II and is not used. "Mixed" means pegged on the family of all -secret events, not on the -field of Assumption II. Classical distributions, and Nash equilibrium points are AGT.IsLottery, AGT.expectedPayoff and AGT.IsMixedNash from the published definition agt_games.
A formalization that restricted deviations to mixed or objective strategies, or dropped "mixed" from the hypothesis on , would state a different theorem and is ruled out.
Useful contributions: Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures (or the special case needed for Lemma 7.1), the factorization of Lemma 7.3, and the payoff identities used in the proof of Proposition 4.3. The model definitions are shared in meaning with the companion mission on two-person zero-sum games.
In high-dimensional linear regression one observes with a design matrix whose number of columns may far exceed the sample size . The two standard estimators of a sparse , the Lasso (Tibshirani, 1996) and the Dantzig selector (Candès and Tao, 2007), both come with error bounds of order for an -sparse , but only under a condition on : since has a non-trivial kernel when , some form of restricted invertibility is unavoidable.
Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 2009) introduced the restricted eigenvalue (RE) condition, which asks for invertibility of only on a cone of approximately sparse vectors. It is weaker than the conditions used before it and has since become the default assumption in the sparse-estimation literature. Section 4 of the paper relates RE to the earlier conditions:
This mission formalizes those implications.
Fix integers and and a matrix with columns . The Gram matrix is . For and , is the vector equal to on and off ; , are the and Euclidean norms; is the number of non-zero coordinates of ; is the complement of .
The cone condition for and is
Assumption RE holds with constant if for every with and every satisfying (4.1). For , let be a set of indices outside carrying the largest , and ; Assumption RE replaces by .
The restricted eigenvalues are and , the minimum and maximum of over with . The restricted correlations are the maximum of over disjoint index sets with and non-zero . Two constants are attached to them:
is the orthogonal projector in onto the span of the columns , .
For integers , , and , if Assumption 2 holds, then , RE and RE hold with constant , and for every with and every satisfying (4.1)
Assumption 2 involves no correlations, only extreme eigenvalues of small principal submatrices of .
For and , Assumption 1 implies the same conclusions with and constant .
For and , each of
(Assumptions 3, 4, 5) implies RE, with the constants , and respectively.
The milestones are the steps of the proof in Appendix A — the projection inequality (A.1), the block bound (A.2), the shelling bound (A.3), the Candès–Tao correlation bound used for part (i) — followed by part (i) and the three coherence-type implications.
RE with and is the hypothesis of the paper's prediction and bounds for the Lasso and the Dantzig selector (Theorems 5.1, 6.1, 7.1, 7.2), and RE is the hypothesis of its bounds. Assumptions 1–5 are stated through quantities that are standard in compressed sensing and random matrix theory, so known bounds for , and of random designs transfer, through this mission's theorems, to every result stated under RE. Lemma 4.1 also shows that RE is weaker than the Candès–Tao condition used for the Dantzig selector.
The results are proved in the paper; parts of Lemma 4.1's proof (the correlation bound for part (i)) are cited from Candès and Tao without proof. None of these results is formalized: the platform has pairwise-incoherence and restricted-nullspace statements from Wainwright's textbook (a different conclusion and normalization) and restricted isometry definitions, but neither restricted eigenvalues , restricted correlations , nor the RE condition in this form.
The naive attempt to bound from below splits and applies an eigenvalue bound to each part. This fails: can have up to non-zero coordinates, and no condition on - or -sparse submatrices controls directly. The cone condition bounds only the norm of , while eigenvalue conditions speak about norms of sparse vectors; bridging the two with the right constant , and keeping track of how the leading block interacts with the rest through the projector , is where the work lies. For part (i), the interaction between disjoint sparse blocks has to be controlled by rather than by .
Matrix (Fin n) (Fin M) ℝ; vectors are Fin M → ℝ and Fin n → ℝ; . The projector is Mathlib's orthogonal projection on EuclideanSpace ℝ (Fin n) onto the span of the columns indexed by .RE X s c0 κ asserts the RE inequality with constant for all admissible and . The paper's is the largest such (the minimum is attained), so "RE holds with " is exactly " is a witness". This avoids a real infimum over an empty set when .sInf/sSup over nonempty bounded sets (a basis vector for ; two disjoint singletons for , since ), so they equal the paper's attained min/max. , , are natural numbers; is written .Generalized pattern search (GPS) is a class of derivative-free methods for minimizing a function that can only be evaluated, not differentiated. Such objectives arise in engineering design, where one evaluation is an expensive simulation that may fail and return no value at all. The helicopter rotor design problem of Booker et al. is one example: no value was returned for roughly 66% of the trial points (Booker et al., 1999). A method for such problems has to tolerate objectives that are discontinuous or take the value .
Earlier convergence theory for GPS assumed continuous differentiability of the objective on a neighbourhood of the level set. Torczon established it for unconstrained problems (SIAM J. Optim. 7, 1997), and Lewis and Torczon extended it to bound constraints (1999) and to finitely many linear constraints (SIAM J. Optim. 10, 2000). Audet and Dennis (SIAM J. Optim. 13, 2003) replaced these analyses with a single argument. Its conclusions are local and are graded by the smoothness of the objective at the limit point only, through Clarke's generalized directional derivative. That paper is the source of this mission. Its analysis is the basis of the later mesh adaptive direct search (MADS) theory (Audet, Dennis, SIAM J. Optim. 17, 2006).
The problem is
with and in . The algorithm works with the barrier function , equal to on and to elsewhere.
The algorithm uses a finite set of directions , the columns of the product of a nonsingular and an integer matrix . The directions form a positive spanning set: their nonnegative combinations give all of . At iteration , with iterate and mesh size parameter , the mesh is . A poll set is drawn from a positive spanning subset . Each iteration ends in one of two ways:
Here is rational and are integers. The assumptions are A1 , A2 is rational, and A3 all iterates lie in a compact set. A refining subsequence is an infinite set of mesh local optimizers along which (Definition 3.5). For Lipschitz near , Clarke's derivative is
Assume A1–A3. Let be the limit of a refining subsequence, and let be a direction polled at a feasible point for infinitely many in the subsequence. If is Lipschitz near , then
Theorem 3.7 gives a first-order conclusion at a limit point from a local hypothesis at that point alone. It does not require smoothness elsewhere, finiteness of elsewhere, or continuity. It turns the heuristic "the method stopped improving on ever finer meshes" into a statement about generalized derivatives. The unconstrained stationarity result (Theorem 3.9) and the linearly constrained KKT result (Theorem 3.14) follow from it, and they recover the Torczon and Lewis–Torczon theorems under weaker smoothness assumptions. The chain Lemma 3.2 → Lemma 3.3 → Proposition 3.4 → Theorem 3.6 shows that the goal's hypothesis is always met. Every run satisfying A1 and A3 has a refining subsequence, which rests on the rationality of and on the integer structure of .
All results in this mission are proved in the source paper. None of them has, to the best of our knowledge, a machine-checked proof. The mission contributes a formal model of the GPS algorithm class as a class of runs, a formal Clarke directional derivative, and checked proofs of the mesh-refinement chain and the main theorem.
Given a refining subsequence, the goal is a comparison of limsups: the poll inequalities give nonnegative difference quotients at the points , which converge to . The difficulty lies in two places. First, the objective is extended-valued, and the barrier hides at infeasible poll points, where the poll inequality says nothing. The hypothesis on has to supply feasibility, and the Lipschitz hypothesis has to supply finiteness near . Second, the existence of refining subsequences is not a compactness argument alone. Coarsening is allowed, so need not decrease, and with an irrational or a direction set that is not an integer lattice image (for instance in ) the meshes can be dense and can be positive. The lattice argument behind Proposition 3.4 is where the integrality hypotheses are used.
Points of are Fin n → ℝ, takes values in WithTop ℝ, and the bounds are EReal-valued, so gives . The barrier is defined by cases, never by extended addition. Directions are the columns of G * Zbar indexed by Fin p, and is a Finset (Fin p). A GPS run is a structure of sequences and a per-iteration predicate "mesh local optimizer", subject to exactly the two update rules above, , rational and the exponent bounds. The SEARCH step, the choice of and the exponents are left free, since the paper allows any strategy. A subsequence is a strictly increasing map . The Clarke derivative of a real function is an EReal-valued limit superior along , . " Lipschitz near " means that agrees near with a real function Lipschitz there, and the conclusions are stated for every such function. Strict differentiability is the directional notion of Section 3.4 of the paper.
The goal is not trivialized by an empty run class: Theorem 3.6, on the same class, asserts that refining subsequences exist. The mesh-local-optimizer branch requires the complete poll inequality over . The Clarke limit superior cannot take a default value. The direction must be polled at feasible points infinitely often, which is the paper's " was evaluated".
Contributions welcome: proofs of any milestone, and reusable lemmas on positive spanning sets, lattice points in compact sets, and the Clarke derivative (for instance, that it equals under strict differentiability).
Maximizing a submodular set function without constraints contains Max Cut, Max Directed Cut, maximum facility location and several graph and hypergraph cut problems as special cases, and it appears in operations research wherever a value exhibits diminishing returns but is not monotone (profit that combines coverage with a cost, for example). These problems are NP-hard, so the question is which fraction of the optimum an efficient algorithm can guarantee when the function is accessible only through a value oracle that returns for a queried set .
Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor approximation algorithms for maximizing a general nonnegative submodular function. The simplest of them returns a uniformly random set and achieves of the optimum; this mission is about the next one, a nonadaptive algorithm: it decides all of its oracle queries before seeing any answer, then computes a set from the answers. Such an algorithm can be run in one round of parallel queries. The paper shows that this restricted access already beats and reaches .
Timeline. For Max Directed Cut, a random cut achieves . Feige, Mirrokni and Vondrák (FOCS 2007; journal version 2011) proved for a random set and nonadaptively for general nonnegative submodular functions, and by adaptive local search, and that requires exponentially many queries. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012, SIAM J. Comput. 2015) later reached the optimal with a randomized double-greedy algorithm.
Let be a finite ground set with elements. A function is submodular (Definition 1.1) if
Throughout, is nonnegative, the paper's standing assumption, and .
For , denotes the random subset of containing each element independently with probability ; is a uniformly random subset. For a set , is the analogous random subset of . The averaged marginal value of an element (Definition 2.4) is
Algorithm NA (p. 1139):
Given the estimates, the expected value NA returns is .
For every nonnegative submodular and every estimate with for all ,
The printed theorem says "at least "; the term is what the proof establishes (p. 1140, last display).
Milestones 3–7 are the displayed steps of the proof of Theorem 2.6, stated for arbitrary sets where the page's argument does not use the optimality of .
The theorem shows that nonadaptive access, a fixed batch of polynomially many value queries followed by a computation, suffices for a -approximation of unconstrained nonnegative submodular maximization, strictly better than the of any algorithm that must return one of its queried sets (the paper shows is optimal in that class, §4.2). The quantity generalizes the in-degree/out-degree test for Max Directed Cut to arbitrary submodular functions, and Lemmas 2.2 and 2.3 are general sampling inequalities for submodular functions that the paper reuses for its adaptive smooth local search.
Formalizing it produces machine-checked versions of Lemmas 2.2 and 2.3 as statements about exact finite averages, a reusable expectation operator on product-distributed random subsets, and a checked version of the argument with its explicit error term. The result is proved in the paper; to our knowledge none of it has been formalized in a proof assistant.
The two regimes the proof separates, " is already good" and "one of , is large", must be tied to the value of a uniformly random set, whereas the elements of and are chosen from estimated averages, not from the optimal set . The natural attempt, comparing with element by element, fails because is not monotone: adding elements of to can decrease the value. The accuracy of the estimates must also be propagated through a sum over up to elements, which is where the error term comes from. The sampling lemmas require handling expectations over pairs of independent random subsets of possibly overlapping sets.
Fintype X with DecidableEq, assumed Nonempty, so and the divisions by and are genuine; sets are Finset X; is real valued with nonnegativity as an explicit hypothesis. Lemmas 2.2 and 2.3 are stated for real with no sign condition, as printed.Finset.univ.sup' _ f, the true maximum over all subsets.Welcome contributions: proofs of Lemmas 2.2 and 2.3 (reusable for mission IV of this series), the identity , and general lemmas about the operator (splitting a uniform random set along a partition).
The continuous-review policy is the standard replenishment rule of inventory theory: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point , order a fixed order quantity . It is used in practice and taught in every operations management course, usually after the deterministic economic order quantity (EOQ) model, which is the same system with a constant demand stream.
Practitioners and textbooks rely on a robustness property of the EOQ: its cost is very insensitive to the choice of order quantity. If the order quantity is off by a factor , the cost rises only by the factor ; ordering 50% too much costs about 8% extra. The insensitivity of the stochastic system to its control parameters had been observed numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), but, as Zheng notes, no analytical result on it was known.
Timeline:
Demands arrive at rate ; orders arrive after a fixed leadtime ; all stockouts are backordered. Each order costs ; holding costs accrue at rate per unit in stock and penalty costs at rate per unit backordered. The leadtime demand has distribution with finite mean .
The inventory cost rate at inventory position is
assumed to attain its minimum at a unique point . The long-run average cost of the policy is
For fixed let be a reorder point minimizing , and let
is the cost of the order quantity when the reorder point is always chosen optimally for it. An optimal order quantity minimizes over , and .
The EOQ model is the same system with the constant leadtime demand . Its cost rate is , and , , are the objects above at , with optimum and .
The goal holds for every demand distribution satisfying the standing assumptions and every optimal . Both regimes, and , are included.
In the order the proof uses them:
In the EOQ model the relative cost of a scaled order quantity is exactly (Eq. (25) of the paper). Theorem 4 shows that the stochastic system is at least as forgiving. The bound holds for every leadtime-demand distribution with a unique newsvendor minimizer, and it does not depend on the parameters , , , or . Because the reorder point is re-optimized for each quantity, the bound applies to the practical question of how much a misestimated lot size costs when the safety stock is set correctly.
Together with the other results of the paper (the bound for the EOQ heuristic and the bounds between and , which are separate missions of this series), it gives a closed-form account of why the EOQ is a good heuristic for stochastic systems.
The result has a complete published proof. It has not been machine-checked. The work that remains is a formal proof for general distributions: the paper differentiates and twice, and a formal proof has to replace those derivatives with arguments that need no density.
is defined through an inner minimization over the reorder point, so its shape in is controlled by the implicitly defined function rather than by directly. The obvious approach would bound with the reorder point fixed at . That approach is the wrong comparison: it bounds a larger quantity, and the resulting bound depends on the distribution.
The paper's proof uses three properties of : that it is convex, that its slope never exceeds the EOQ slope , and that it dominates . The paper obtains these from the derivatives and under a smooth demand distribution. Without a density, is only an argmin and need not be differentiable, so none of these three properties can be read off a derivative formula; the asymptotic slope in particular depends on the finite mean and on the behaviour of at .
The mission is set in Lean 4 with Mathlib. All objects are real valued.
QRModel bundles , a probability measure on with integrable identity, , almost surely, and the unique-minimizer hypothesis on . is implicit in the paper and made explicit here. No density is assumed; deterministic and discrete demands are allowed, and the paper's own numerical study uses Poisson demand.IsOptQty Q, meaning and for all . Its existence is asserted in the Eq. (8) milestone, so the goal is not vacuous. "" is a real with real division . In Lemma 9 the integral is oriented, as on the page.A complete development needs the following:
These facts about newsvendor cost functions are reusable in the other missions of this series. Contributions of any of them as separate lemmas are welcome.
The continuous-review policy is the standard control rule for a single stocked item with random demand: whenever the inventory position falls to the reorder point , an order of fixed size is placed. It is implemented in a large share of commercial inventory systems. Choosing the two parameters jointly has traditionally required numerical search (Hadley and Whitin, 1963; Federgruen and Zheng, 1992). In practice the order quantity is therefore often taken from the deterministic economic order quantity (EOQ) formula with backorders, and the reorder point is then set for the random demand.
Zheng (1992) turned this practice into a question with an exact answer: how does the optimal order quantity of the stochastic model compare with the EOQ quantity computed from the same cost data and the same mean demand? Its Theorem 2 answers it with a two-sided bound. This mission formalizes that theorem. Companion missions of the same series formalize the paper's cost bounds (Theorem 3), the flatness of the cost curve (Theorem 4) and the bound on the cost of using the EOQ quantity (Theorem 5).
Demand arrives at rate and replenishment orders arrive after a fixed leadtime . Shortages are backordered. Holding costs accrue at rate per unit held, backorder penalties at rate per unit short, and every order costs . The leadtime demand is a nonnegative random variable with law and mean . The expected inventory cost rate at inventory position is the newsvendor cost
assumed, as in the paper, to attain its minimum at a unique point . The long-run average cost of the policy is
For each , let be an optimal reorder point, i.e. a minimizer of . The analysis runs through the curves
and through the cost of order quantity with the reorder point set optimally. The optimal order quantity is the minimizer of over .
The EOQ model is the case of a constant leadtime demand . Its cost rate is , and the same construction gives , , and the optimal quantity
For , let , , be the positive solutions of
Each has exactly one positive solution, and
Moreover, with and the demand law fixed, is nondecreasing on and converges to a finite constant as .
The milestones are the paper's own numbered results that feed Theorem 2, listed in the order the argument uses them:
The result. Theorem 2 says that the EOQ formula always underestimates the optimal order quantity when leadtime demand is random. The underestimate is bounded by , a quantity that stays bounded however large the ordering cost is. So the relative error of the EOQ quantity vanishes as grows. The first inequality, , is also an ingredient of the paper's Theorem 3 (cost bounds) and Theorem 5 (the EOQ quantity raises costs by at most ). The explicit bounds , , bracket and give a search interval for it.
Formalizing it. The theorem has been proved on paper since 1992. No machine-checked version of it, or of the continuous-review cost of Eq. (1), exists on this platform. The inventory items already here treat the discrete cost with integer order quantities, a normally distributed demand, or the EOQ without backorders. This mission provides a machine-checked version of the paper's optimality conditions for a general demand distribution. The paper's argument differentiates twice, i.e. it tacitly assumes a density. The formal statements do not, so a formal proof must redo those steps with one-sided (convexity) arguments. The printed argument for the limit in part (b) shows only that a derivative tends to zero. A complete proof of convergence is part of the work.
The obvious route to compares the two cost curves and directly. It fails because pointwise, and a pointwise inequality between two convex functions says nothing about the order of their minimizers. The stochastic curve is defined only implicitly, as evaluated at a minimizer of a parametric integral, so its growth relative to the linear has to be established before any comparison of order quantities. For part (b), a vanishing derivative does not imply convergence ( also has a vanishing derivative), so the printed proof of the limit does not go through as written.
Without a density, need not be differentiable. Every derivative in the paper's proofs (of , and ) must be replaced by monotonicity or chord arguments.
The Lean development uses the namespace ZhengQR.OrderQty. Its conventions:
Infrastructure needed includes the following. Much of it is reusable for any single-item inventory model:
Contributions welcome: proofs of the milestones in any order, general lemmas on the newsvendor cost, and a complete convergence argument for part (b).
Firms that can buy the same item from two suppliers, a cheap slow one and a fast expensive one, face the dual-sourcing inventory problem: how much to order from each source in every period when demand is random and unmet demand is backlogged. Global sourcing (offshore regular supply plus a near-shore express supply) is the standard example (Allon and Van Mieghem 2010). When the two lead times differ by more than one period, the optimal policy depends on the whole pipeline of outstanding orders. No simple optimal policy is known, and dynamic programming is intractable for long lead times.
The tailored base-surge (TBS) policy orders a constant amount from the slow source and uses the fast source to bring the expedited inventory position up to a fixed level. It is simple, and it is used in practice. Janakiraman, Seshadri and Sheopuri (JSS, Management Science 2015) showed that its best parameters solve a convex program that does not depend on the regular lead time, and they conjectured, with numerical support, that TBS is near-optimal when that lead time is long.
Timeline:
Let be a nonnegative random variable with finite mean that is not almost surely constant. Demands are i.i.d. copies of . The regular source has lead time , the express source has lead time , and . In period the controller orders and ; then arrives and is realized, so the on-hand inventory evolves as and may be negative. Initially nothing is on order and , where the are further i.i.d. copies of and , .
The per-period cost is with , where and is the express premium (the regular unit cost is normalized to ). An admissible policy chooses the two orders in period as deterministic measurable functions of . Its long-run average cost is
With the expedited inventory position , the TBS policy orders and . A best TBS pair minimizes over and (first in through , then in ).
The constants and are explicit functionals of the law of and of . They are built from , , , the mean absolute deviation , and the large-deviation quantities of (p. 441).
For all , and ,
The threshold does not depend on , so the statement gives an explicit, inverse-polynomial rate. Its limit form is Corollary 1 of the paper.
In the order the proof uses them:
The theorem shows that one of the simplest dual-sourcing heuristics is asymptotically optimal as the regular lead time grows. This is the regime where exact dynamic programming is hopeless. The best TBS parameters come from a convex program independent of , so the result yields an algorithm whose running time does not grow with and whose optimality gap is bounded explicitly for every finite . It extends the lower-bounding technique of Xin and Goldberg's lost-sales work (Operations Research 2016) from a static to a dynamic relaxation.
Formalization adds the following. To the best of available knowledge, none of the objects involved (average-cost inventory control with backlog, TBS policies, Lindley-type maxima of random walks with their Spitzer identity) exists in Mathlib or on the platform. The paper's proof defers several ingredients to the literature or omits them: Lemma 1, Eq. (3), Lemma 3, and the details of Lemmas 5 and 7. A complete formal proof must supply them. The result is proved on paper but not formalized anywhere.
An optimal dual-sourcing policy need not be stationary, its induced Markov chain need not have a stationary distribution, and the inventory is unbounded below. The natural argument would compare the optimal policy's steady state with the TBS steady state, and it fails at its first step. Theorem 2 replaces the steady state by a vector with a few distributional properties, built from time averages. That construction, and the independence structure it must carry, is the central technical step. The conditional Jensen step then leads to a single-source problem with possibly negative demand, where textbook interchange-of-limits theorems do not apply directly. Finally, bounding away from requires a quantitative lower bound on the growth of random-walk maxima under only a first-moment assumption.
Conventions of the Lean development (namespace XinGoldbergTBS.Asymptotic):
Lemma 1, Eq. (3) and Lemma 3 are results the paper quotes from Sheopuri et al. (2010), JSS and Scarf (1960). Proposition 1 (conditional-expectation form of the bound) is not included.
A trivializing formalization is ruled out: ranges over the full admissible class, the constants are definitions rather than hypotheses, and the goal includes an existence clause.
Reusable beyond this mission: average-cost inventory models with lead times, discounted single-source backlog value functions, and Spitzer-type identities for random-walk maxima. Contributions to any milestone are welcome.
A Markovian decision process (Howard, 1960) models a controller who, in each of finitely many states, picks a decision, earns a reward and moves to a random next state according to known transition probabilities. In applications (inventory control, equipment replacement, quality control) those probabilities are estimated, not known. Satia and Lave (Operations Research 21(3), 1973) treat the uncertainty in two ways: a game-theoretic formulation, in which each unknown row only lies in a given set, and a Bayesian formulation, going back to Silver (1963) and Martin (1967), in which the controller holds a prior on the unknown matrix and learns from observed transitions.
The Bayesian problem is the natural one but its state includes the whole prior, so it cannot be solved exactly beyond small cases. The paper's contribution in the Bayesian part is a pair of computable bounds on the Bayesian optimal return in terms of the two game-theoretic values (max-max and max-min). This mission formalizes those bounds and the chain of facts they rest on.
There are states and, in state , a finite nonempty set of decisions. A transition under decision earns and rewards are discounted by , . The row of transition probabilities is unknown; it is known to lie in a closed convex nonempty set of probability vectors, and .
A prior is a probability distribution on matrices whose rows are all probability vectors. Its means are . After a transition under decision the prior is replaced by the Bayes transformation (Eq. (8)), with the normalizing constant. The Bayesian optimal return solves the recursion
The max-max and max-min values , solve
with max for and min for . Finally , the prior probability that the true matrix lies in .
The Lean development lives in the namespace SatiaLave.Bayes: UncertainMDP, IsPrior, pbar, bayes, SolvesEq10, SolvesVplus, SolvesVminus, alpha, rmax, rmin, policyValue.
For every bounded solution of (10), all solutions , , every prior and every state ,
together with the existence of , and . Both halves are the paper's printed statements.
The result. The bounds sandwich an intractable quantity between two quantities computable by finite algorithms (the max-max and max-min policy-iteration procedures of the same paper), weighted by a single prior probability . When the prior concentrates on () the bounds become : the Bayesian return lies between the pessimistic and optimistic robust values. They are the upper and lower bounds on the return that the paper's implicit-enumeration method (the decision tree of its Fig. 2 and Proposition 12) uses to compare decisions. The Jensen step is a value-of-information inequality (Bayesian optimal return is at most the expected full-information optimal return), which recurs throughout Bayesian control and bandit theory.
Formalizing it. The results are proved on paper (Propositions 6 and 8 by reference to Martin's book and Satia's thesis, Propositions 9 and 10 in the text); none is machine-checked. The mission produces a Lean model of Bayes-adaptive Markov decision processes with priors as measures, the Bayes transformation and its fixed-point recursion, and the link between the Bayesian and the robust (rectangular) formulations. Martin's existence-uniqueness theorem and the convexity of the Bayesian value are reusable for any Bayes-adaptive model.
The prior space is infinite-dimensional and not a vector space, so the recursion (10) lives on a space of measures, and the usual finite-state arguments do not apply verbatim. Proposition 8 gives convexity only along finite mixtures, while the proof of Proposition 9 applies Jensen's inequality to the integral mixture of point masses; bridging the two, or proving the value-of-information inequality directly, is the central step. The paper also restricts the point masses to , which cannot represent a prior with mass outside ; the formal statement integrates over every transition matrix, as the next line of the paper's display requires. Measurability of is not automatic, since is only characterized by a functional equation.
Fintype S; decisions a dependent family D i of nonempty finite types. A matrix is P : (i : S) → D i → S → ℝ with the product Borel -algebra.bayes then returns . That posterior is always multiplied by in (10), so the choice is immaterial.⨆/⨅ over a nonempty bounded set. "Obviously " is stated for every pure stationary policy , not only a max-min optimal one. The policy return is the componentwise series .Welcome contributions: the Banach fixed-point argument for (10) on bounded functions of priors; lemmas that bayes maps priors to priors and that point masses are fixed; continuity of the known- optimal value in ; a general Jensen inequality for functions convex along mixtures of probability measures.
Semidefinite programming (SDP) optimizes a linear function over the intersection of the cone of positive semidefinite matrices with an affine subspace. It contains linear programming as the diagonal case and is the computational core of relaxations in combinatorial optimization, control theory and polynomial optimization. Its standard duality theory, however, is weaker than that of linear programming. The Lagrangian dual of an SDP can have a strictly positive duality gap, can fail to attain its optimal value, and an infeasible semidefinite system need not have a certificate of infeasibility of the naive Farkas form. All the classical strong duality theorems for SDP therefore assume a constraint qualification such as Slater's condition (a strictly feasible point).
M. V. Ramana (1997, Math. Program. 77, 129–162) constructed a dual, the Extended Lagrange–Slater Dual (ELSD), whose size is polynomial in the data and which enjoys every property of linear programming duality for every SDP, with no constraint qualification. The same construction yields an exact theorem of the alternative for semidefinite feasibility and the complexity consequence that semidefinite feasibility lies in NP if and only if it lies in co-NP in the Turing model.
Timeline:
Let be natural numbers, the space of real matrices, and the symmetric ones. On the inner product is . For symmetric , means is positive semidefinite. The data are symmetric and . The primal SDP is
with feasible region , a spectrahedron. Define by and write for " and ".
For let be the set of tuples of real matrices with and, for ,
The need not be symmetric. and are the sets of last components and ; . The ELSD is
and Weak-ELSD is the same program with . For the milestones: the polar , the algebraic polar , and .
For all data :
Propositions 7(vi) and 7(vii) (facts on PSD matrices), Lemma 9 (annihilation ), weak duality over every , Lemma 10 (nested subspaces), Lemma 13 (), Corollary 14, Claims 17 and 16, the central Theorem 12,
the translation invariance of (§2.5), and system (14) (dual attainment at value 0). Theorems 19–21 (Farkas lemma for SDP, optimality condition, primal attainment) are further items stated on the same definitions.
The Duality Theorem gives SDP a dual with the full strength of linear programming duality for every instance, at polynomial size. Consequences in the paper: an exact theorem of the alternative for semidefinite feasibility (Theorem 19); semidefinite characterizations of optimality of a given point and of primal attainment (Theorems 20, 21); and the complexity results that semidefinite feasibility is in NP iff it is in co-NP in the Turing model and in NP ∩ co-NP in the Blum–Shub–Smale model (Theorem 25, not part of this mission). Theorem 12 separately gives an exact semidefinite description of the polar of any spectrahedron containing the origin.
The results are proved on paper and are classical. No machine-checked version is known to exist; the platform's existing SDP duality theorem assumes Slater's condition. A formalization would provide the first constraint-qualification-free SDP duality in Lean, together with reusable infrastructure on PSD matrices (range inclusion, ) and on polars of convex sets.
The obvious route to SDP strong duality separates the primal's value from the image of the PSD cone under a linear map and invokes a closed-cone Farkas lemma. That step fails: the linear image of the PSD cone need not be closed, which is exactly why Lagrangian duality has gaps. In this mission the obstruction reappears as the non-closedness of the algebraic polar (Lemma 13 only gives ). The difficulty is to show that finitely many, and at most , corrections by the sets close (Claims 16, 17), and to control dimensions in doing so. A proof by assuming closedness, strict feasibility or a Slater point is a different theorem.
Everything lives in the namespace ExactSDPDuality.ELSD, in one definition file. Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin m → ℝ; "" is Mathlib's PosSemidef (which over ℝ includes symmetry); is the entrywise sum on all of ; is the dot product. The data carry symmetry hypotheses in every statement, as the paper assumes throughout. is encoded by sequences with , so ; for the index is . Optimal values are least upper and greatest lower bounds of the value sets, never real sSup/sInf. The polar is the one-sided polar. In §2.4 statements the standing assumption is a hypothesis. In Claim 16 the index satisfies , the range where is introduced, and is the rank of the span of .
Theorems 20 and 21 are printed with ; both are false as printed (counterexamples in the items) and are stated with the corrected that the paper's derivation from Theorem 6 gives.
Trivializing formalizations are ruled out: no Slater or other constraint qualification appears; the dual is the ELSD built from the recursively defined , not the Lagrangian dual or an arbitrary subspace; the range over all of , not only symmetric matrices (the paper's Example 4 needs a nonsymmetric ).
Needed infrastructure: PSD matrix facts (Proposition 7), bipolar theorem for closed convex sets containing the origin (Proposition 11), closedness arguments for linear images of cones, and dimension counting of subspaces of . Contributions of any milestone, of these general lemmas, and of alternative proofs (for instance via facial reduction) are welcome.
Many problems in optimization and equilibrium modelling reduce to a system of equations with that is continuous and locally Lipschitz but not differentiable. Complementarity problems rewritten through the min or Fischer–Burmeister functions, Karush–Kuhn–Tucker systems of nonlinear programs, and the gradients of augmented Lagrangians all have this form. Newton's method cannot be applied verbatim, because need not exist.
Qi and Sun (Math. Programming 58 (1993) 353–367) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and proved that the resulting method converges under a condition they called semismoothness, extending Mifflin's notion (SIAM J. Control Optim. 15 (1977)) from functionals to maps. The paper has two convergence results. Theorem 3.2 is local: near a semismooth root with nonsingular generalized Jacobian the method converges superlinearly. Theorem 3.3, the target of this mission, is global in the Newton–Kantorovich sense: explicit constants on a ball around the starting point guarantee that the iteration never leaves , that has exactly one zero in , and that the iterates converge to it with a computable error bound. The authors describe it as "an extension of the classical Newton-Kantorovich theorem" (p. 361), which is stated for smooth maps in Ortega and Rheinboldt's monograph.
Timeline.
Work in with the Euclidean norm ; for a linear map , is the induced operator norm. Let be locally Lipschitz. Write for the set of points where is differentiable and for the derivative at .
In Lean these are NonsmoothNewton.Global.clarkeJac, dirDeriv, SemismoothAt and IsNewtonRun, over EuclideanSpace ℝ (Fin n).
Fix , , the closed ball , and constants with .
Assume is semismooth at every point of and, for all and : is nonsingular,
with and . Then every run of (3.2) from stays in , every is nonsingular, has a unique zero in , , and
The theorem certifies, from data checkable on a single ball, that a solution exists, where it is, that it is unique there, and how far the current iterate is from it; (3.4) is an a-posteriori stopping criterion. It holds for every choice of , which is what implementations need, since they compute one element of and not the whole set. The result underlies the global and semilocal analysis of semismooth Newton methods for complementarity problems, variational inequalities and nonsmooth KKT systems, a line that continued through the 1990s and 2000s.
The theorem is proved on paper; no machine-checked version is known. The platform has no Newton–Kantorovich theorem, smooth or nonsmooth, and no Clarke generalized Jacobian. A complete formalization would supply both, and the definitions layer here (generalized Jacobian, one-sided directional derivative, semismoothness, Newton runs) is shared with the two companion missions on Qi and Sun's local convergence theorem and on semismoothness of augmented Lagrangian gradients.
The Newton map is set-valued: depends on the choice of , so the Banach fixed-point theorem for a single contraction does not apply directly, and the argument must hold for every sequence of choices. The contraction estimate needs both consecutive steps to start inside , so containment in and the geometric decay of the steps must be established together. Identifying the limit as a zero requires a uniform bound on , which is not a hypothesis: it has to come from local Lipschitz continuity through the structure of the generalized Jacobian. Uniqueness uses an element , whose existence rests on Rademacher's theorem. Finally, the directional derivative in the hypotheses is only meaningful because semismoothness makes it exist.
The space is EuclideanSpace ℝ (Fin n), so the norm is Euclidean, as in the paper (p. 356), and is the operator norm. Local Lipschitzness is global (LocallyLipschitz F), the standing assumption of Section 3. Conventions:
fderiv along sequences in ; no closure is taken (the limit set is compact for locally Lipschitz ).Ring.inverse is not used.dirDeriv, a limUnder along , used only at points of , where semismoothness makes the limit exist.The goal is the full four-part conclusion: containment, existence, uniqueness, and convergence with (3.4). A formalization that proves only that the iterates converge to some zero, or that treats as possibly empty so that the hypotheses become vacuous, is not the theorem. The hypotheses are satisfiable by genuinely nonsmooth maps, e.g. on with a ball containing the kink.
A complete development needs: nonemptiness and local boundedness of the generalized Jacobian (Rademacher's theorem, available in Mathlib as LipschitzWith.ae_differentiableAt); geometric-series and Cauchy-sequence arguments in a complete space. The generalized-Jacobian facts are reusable well beyond this mission. Contributions of any of the milestones, or of these general facts as separate lemmas, are welcome.
Many problems in optimization and equilibrium modelling reduce to a system of equations whose map is Lipschitz but not differentiable: reformulations of nonlinear complementarity problems through the componentwise minimum or the Fischer–Burmeister function, Karush–Kuhn–Tucker systems of constrained programs, and gradients of augmented Lagrangians all have kinks. Newton's method, , is the standard fast local solver for smooth systems, but it needs a derivative at every iterate.
Qi and Sun (Math. Programming 58, 1993) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and showed that the resulting method converges locally superlinearly under a regularity condition they called semismoothness, extending Mifflin's notion for functionals (Mifflin, SIAM J. Control Optim. 15, 1977) to vector-valued maps. This theorem is the foundation of the family of semismooth Newton methods used in complementarity, variational inequalities and PDE-constrained optimization.
Timeline. Robinson (1988) and Pang (Math. OR 15, 1990) studied Newton methods built on B-derivatives, with convergence proved under a strong Fréchet derivative at the solution; Kummer (1988) gave an abstract framework for Newton methods for nonsmooth equations; Qi and Sun (1993) proved local superlinear convergence for the generalized-Jacobian iteration under semismoothness and nonsingularity of , with order under -order semismoothness.
Let be locally Lipschitz. By Rademacher's theorem is differentiable on a set of full measure; write for the Jacobian at . The generalized Jacobian is
the convex hull of all limits of Jacobians along sequences of differentiability points converging to . The one-sided directional derivative is .
is semismooth at if it is Lipschitz near and, for every , the limit of over , , exists. For , is -order semismooth at if in addition for , .
For , the nonsmooth Newton method is
where any element of may be chosen at each step. A run is a pair of sequences , with and for all . A root () is regular when every is nonsingular.
Let be locally Lipschitz, , semismooth at , and every nonsingular. Then there is such that every with is nonsingular, a Newton step from such a stays within of , and every run with satisfies
The goal asserts only the shape of the convergence (superlinear) and fixes no constants.
If moreover is -order semismooth at , , there are and with
for every run started within of .
The milestones follow the paper's route: Proposition 2.1 (the limit in the definition of semismoothness is the directional derivative), Lemma 2.2 (Lipschitz continuity of and its realisation by an element of ), Theorem 2.3 (semismoothness is equivalent to and to the corresponding condition at differentiability points), the Remark's expansion (2.17), Proposition 3.1 (uniform invertibility near a regular point), the order- sentence of Theorem 3.2, and Corollary 2.5 (strong Fréchet differentiability implies semismoothness).
The theorem gives a locally superlinearly convergent method for Lipschitz equations with no smoothness beyond semismoothness at the root. Convex, smooth and subsmooth functions are semismooth, as are sums and scalar products of semismooth functions (the paper, citing Mifflin), and later work showed that the complementarity and KKT reformulations on which semismooth Newton solvers are built are semismooth as well; the order- variant gives local quadratic convergence for strongly semismooth maps. Mission II of this series treats the paper's global convergence theorem on a ball, and Mission III the semismoothness of augmented Lagrangian gradients, which supplies the application.
The results are proved in the paper. No machine-checked version of the generalized Jacobian, of semismoothness or of the nonsmooth Newton method is known to exist in Mathlib or on this platform; the platform's formalized Newton results concern one-dimensional functions (MetodosNumericos.newton_local_convergence) and smooth convex minimization. A complete development would provide the first formal library for Clarke's generalized Jacobian and semismooth maps.
The classical Newton proof compares with its linearization and uses continuity of the Jacobian at . Here neither is available: need not be differentiable at or at any iterate, the element is chosen arbitrarily from a set, and need not be close to any fixed linear map. The comparison has to go through the directional derivative , which is only positively homogeneous, not linear. The analytic content therefore sits in Section 2: showing that semismoothness, defined through a limit over a set-valued map, controls uniformly in the direction, and that is small. Both rest on Clarke's mean-value inclusion and on compactness and upper semicontinuity of , none of which is in Mathlib. The superlinear rate also requires a uniform bound on in a whole neighbourhood, not just at .
Everything lives in the namespace NonsmoothNewton.Local. Section 2 results are stated for maps between finite-dimensional real normed spaces (the paper's is the Euclidean instance); Section 3 results use EuclideanSpace ℝ (Fin n). Conventions fixed by the Lean statements:
fderiv; the generalized Jacobian is the convex hull (no closure) of limits of fderiv along sequences of differentiability points.lineDeriv; its value is a limUnder, used only where existence is a hypothesis or a consequence.IsUnit in the ring of continuous linear endomorphisms; is a two-sided inverse of operator norm at most .IsLittleO along atTop; the printed Theorem 3.2 states only well-definedness and convergence. "Order " is pinned as with and uniform over runs. Every in (2.8), (2.9) and (2.17) is its – form with a non-strict inequality , and every is an explicit constant and radius.HasStrictFDerivAt, which corrects the misprint for in the paper's display (2.16).A trivializing formalization is ruled out: the update is not written with a junk inverse (which would make a singular step "well defined"), the generalized Jacobian is the paper's nonempty set rather than one that could be empty, and the theorem quantifies over every run rather than asserting that some run converges.
A complete development needs Clarke's mean-value inclusion (2.2), compactness and upper semicontinuity of for locally Lipschitz maps (via Rademacher's theorem, available in Mathlib), and perturbation bounds for inverses of linear maps. The generalized-Jacobian and semismoothness layer is reusable beyond this mission, in particular for Missions II and III of this series. Contributions of proofs of any milestone, and of general lemmas about , are welcome.
Connecting a set of terminals by a network of direct links of least total length is one of the oldest problems of combinatorial optimization. R. C. Prim's 1957 paper in the Bell System Technical Journal (DOI) was motivated by the rate structure for Bell System leased-line services, in which the charge for connecting a set of terminals depends on the length of a shortest network connecting them. The paper states two local construction principles, P1 and P2, and shows that any sequence of their applications produces a shortest network, first for points in the plane and then for arbitrary connected labelled graphs with arbitrary real edge lengths. The paper's §V specialization of the principles, growing a single fragment, is what is now called Prim's algorithm, and its §IV statement is the form of the minimum spanning tree theorem used throughout network design, clustering and approximation algorithms.
Timeline. O. Borůvka (1926) solved the problem for an electrical network in Moravia; V. Jarník (1930) gave the single-fragment procedure; J. B. Kruskal (1956, Proc. AMS 7, 48–50) proved that adding globally shortest links avoiding cycles yields a shortest spanning tree; Prim (1957) gave the more permissive principles P1 and P2, which contain both the Jarník procedure and Kruskal's rule as special orders of application; E. W. Dijkstra (1959) rediscovered the single-fragment procedure.
Let be a finite set of terminals and a simple graph on , the labelled graph whose edges are the possible links. Each edge carries a real length ; lengths may be negative, zero, or tie. For a finite set of links, denotes the graph on whose edges are the links of .
Only edges of are possible links; in Prim's distance table a missing edge has length .
For every finite connected graph and every ,
This is the sentence "P1 and P2 will provide a SSS for any connected labelled graph with any set of real edge lengths." It fixes nothing about the order of applications, the component chosen, or the tie-breaking.
The goal is the correctness theorem of a whole family of greedy minimum spanning tree procedures at once: Jarník–Prim (one growing fragment), Kruskal (globally shortest link first) and Borůvka-style interleavings all produce sequences of P1/P2 applications. Because lengths are arbitrary reals, it also covers maximum spanning trees by a sign change (p. 1397) and graphs that are not complete.
The result is classical and fully proved in the literature. What this mission adds is a machine-checked statement in exactly Prim's generality. Mathlib has spanning trees of connected graphs (SimpleGraph.Connected.exists_isTree_le) and the edge count of trees, but no minimum spanning tree theory. Existing Prove2Me items on minimum spanning trees are either restricted to complete graphs with distance matrices or state a cut property in existence form at a single vertex; none states Prim's principles or his necessary conditions.
The obvious argument, "each link P1 or P2 adds belongs to the shortest network", uses a unique shortest network, and that fails with ties: when two links tie, a P1/P2 link need not lie in a given SSS. Prim's own treatment of ties (§III) is an informal perturbation argument; the formal statement must hold for every tie-breaking choice made during a construction, not only for a generic perturbed instance. Negative lengths remove the easy reading "shortest connected spanning subgraph": the minimum must range over trees only. The statements also involve the component structure of as it changes during a construction, and tree paths in an arbitrary, not necessarily complete, graph.
Namespace ShortestConnection.Principles, Mathlib SimpleGraph. Conventions:
Fintype with decidable equality; is a SimpleGraph V (at most one link per pair, no loops, which is Prim's setting). Lengths are w : Sym2 V → ℝ; only values on edges of matter.Finset (Sym2 V); linkGraph F is SimpleGraph.fromEdgeSet F. A spanning subtree requires ↑F ⊆ G.edgeSet and (linkGraph F).IsTree.linkGraph F; the P2 condition is a single inequality against every -edge leaving it, which is equivalent to "nearest neighbor and shortest link" in Prim's sense.List (Sym2 V) checked entrywise against l.take i; complete means length Fintype.card V - 1 (natural subtraction, used only for nonempty ).sInf of the lengths of spanning subtrees; continuity is in the product topology.Implicit hypotheses made explicit: connected (hence ) wherever an SSS or a complete construction is involved; at least two terminals for Necessary Condition 1; nonempty and for Necessary Condition 2; pairwise distinct edge lengths only in milestone 4, as in the paper's temporary assumption.
The goal's existence clause rules out a vacuous formalization in which no complete construction exists; the step predicates are defined from lengths and components only, never through shortest spanning subtrees, and they are not restricted to one growing fragment or to the globally shortest link.
Needed infrastructure: tree exchange (adding an edge to a spanning tree creates one cycle; removing any other cycle edge yields a spanning tree), component counts under edge addition, and minima of finitely many continuous functions. The exchange and counting lemmas are reusable for any matroid-greedy or spanning-tree mission. Contributions of intermediate lemmas, and proofs of the milestones in any order, are welcome.
Quasi-Newton methods minimize a smooth function on by moving along , where is the gradient and is an approximation of the inverse Hessian built from observed gradient differences. The BFGS update is the most widely used way of building , but it stores a dense matrix, which is prohibitive for large .
Nocedal's 1980 paper (Math. Comp. 35, 773–782) proposed keeping only the last correction pairs and rebuilding the matrix from a simple initial matrix at every step. The resulting method, called SQN in the paper, is now known as L-BFGS, and it is the default large-scale unconstrained optimizer in many numerical libraries and in machine learning. The paper's main theoretical claim is that this truncation does not destroy the finite termination of BFGS on quadratics.
Timeline:
Let be a symmetric positive definite matrix and , and let , a strictly convex quadratic with gradient and unique minimizer .
Exact line search. Along a direction from , the step minimizes .
BFGS update. For a pair with and , the BFGS update of is
Special BFGS matrices. Fix symmetric positive definite and a number of stored corrections. Given pairs , the special matrix is updated by the pairs , oldest first (the paper's (4)–(5)). Only the most recent pairs enter, and the matrix is rebuilt from .
SQN. Starting from , with :
with the exact step and the special matrix built from the last pairs.
PCG with fixed preconditioner . , , with .
For every , every symmetric positive definite and , every , and every ,
where are the SQN iterates. The statement fixes no constant beyond the dimension bound .
The result shows that storing only correction pairs costs nothing on quadratics: for any , SQN terminates in at most steps, like full BFGS and conjugate gradients. It explains why L-BFGS with small is competitive, and it is the model case for later analyses of limited-memory methods (their linear convergence on uniformly convex functions, and their relation to Krylov methods). Property (b) is the reason one expects efficiency to grow with : the matrix satisfies the secant equation on the most recent directions.
The claims are classical and generally accepted, but the paper argues them in a few lines ("it is straightforward to show"), deferring the PCG facts (15)–(16) to a reference. No machine-checked proof of the termination of BFGS, L-BFGS or preconditioned conjugate gradients is known to this mission. A formalization would provide a verified model of L-BFGS on quadratics and a reusable development of conjugate-direction methods with a preconditioner.
The obvious route, "SQN is BFGS and BFGS terminates", fails: SQN discards old corrections, so the classical BFGS argument (hereditary secant conditions on all past directions) does not apply once more than steps have been taken. The paper asserts the identity of SQN with preconditioned conjugate gradients in one sentence ("using a similar argument as for the SCG"), and the PCG relations it relies on are quoted from a technical report. The other difficulty is bookkeeping: the window of stored pairs shifts, the matrix is a nested product, and the runs must remain meaningful after the minimizer is reached.
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, is dotProduct, and is Matrix.vecMulVec. Symmetric positive definiteness is Matrix.PosDef. Indices are 0-based, as in the paper. The exact line search is the closed-form step . The iterations have no stopping rule: once the gradient vanishes the direction and step are zero and the iterate stays at the minimizer (Lean's ). Past that point the zero pair stored by SQN leaves the BFGS step unchanged. The hypotheses are exactly the paper's: , , and exact line searches. need not be diagonal.
Two misprints are corrected and flagged in the items: the denominator of in (13) is (as in (12) and p. 778), and the second relation of (16) is stated for (as used on p. 778), since it fails for .
Ruled out: SQN is defined through its own matrices (4)–(5), rebuilt from and the last pairs. It is not defined through the PCG recurrence, not by one BFGS update of the previous matrix, and not with a stop rule that returns . The standing assumption is not a hypothesis of any statement about a run (it fails after termination and would make the goal vacuous). With SQN is steepest descent and the goal is false, so is required.
Needed infrastructure: algebra of rank-one updates and of Matrix.PosDef under congruence, conjugate-direction lemmas for quadratics, and the fact that mutually -orthogonal vectors in include a zero vector. The PCG results (milestones 5–7) are reusable beyond this mission. Proofs of any milestone, or of the goal directly, are welcome.
Newton's method is the standard second-order algorithm for unconstrained minimization, but without safeguards it has no global guarantee: far from a minimizer the Newton step can increase the objective, and at a point where the Hessian is indefinite the step can head for a saddle point or a maximum. The usual repairs (line search, trust regions, Levenberg–Marquardt damping) come with convergence proofs, but for nonconvex objectives those proofs typically give no rate at all, or only the rate of the gradient method.
Nesterov and Polyak (Math. Program. 108 (2006) 177–205) proposed to regularize the second-order Taylor model of the objective with a cubic term and to take as the next iterate a global minimizer of the regularized model. They showed that the resulting method has a global worst-case rate of convergence to points satisfying the second-order necessary conditions, for every objective with a Lipschitz continuous Hessian and without any convexity. That rate, for the gradient norm, is better than the of the gradient method. It became the reference point for the complexity theory of nonconvex second-order optimization: adaptive variants (Cartis, Gould and Toint, Math. Program. 127 (2011) 245–295) and lower bounds showing that iterations are optimal among second-order methods (Carmon, Duchi, Hinder and Sidford, Math. Program. 184 (2020) 71–120) are stated against it.
This mission formalizes the general convergence result of that paper, Theorem 1 of Section 3, together with the properties of the cubic step from Section 2 on which it rests.
Let be a closed convex set with nonempty interior, and let be twice differentiable on with gradient and Hessian . A starting point is fixed, and is assumed to contain the level set in its interior. Assumption 1: the Hessian is Lipschitz continuous on in the spectral norm, for all , with .
For a parameter the cubic model of at is
The cubic-regularized Newton step is any global minimizer of over ; it exists because the model is continuous and coercive. Write and .
The cubic regularization of Newton method (3.3) fixes , starts at and, for , chooses such that , then sets . The choice always passes the test.
Write for the smallest eigenvalue of a symmetric matrix . The measure of local optimality is
It is nonnegative and vanishes exactly when and .
If for all , then every run of method (3.3) satisfies, for every ,
The constant and the exponent are the paper's; the statement holds for every admissible choice of the parameters and of the global minimizers .
Inequality (3.4) is a global, dimension-free complexity bound for reaching approximate second-order stationarity. It controls both the gradient norm, , and the most negative curvature, , along the best iterate, from a single scalar potential . The second claim of Theorem 1 gives the asymptotic counterpart: every limit point satisfies the second-order necessary conditions. Section 4 of the paper derives its faster rates for star-convex and gradient-dominated functions from the same Section 2 lemmas.
The result is proved on paper and widely cited; to our knowledge no machine-checked proof of it or of the Section 2 lemmas exists. A formalization adds a checked statement of the method with its exact constants, and reusable facts about global minimizers of cubic models (Proposition 1 in particular) that the companion missions on star-convex, gradient-dominated and locally quadratic convergence also rely on.
Most steps are short inequalities, but two are not. Proposition 1 is a statement about a global minimizer of a nonconvex function: the first- and second-order conditions of a local minimizer give only , which is weaker. The natural first attempt, "take the second-order optimality condition of the model at ", therefore fails. The paper proves it in Section 5.1 through a one-dimensional dual characterization of the minimizer.
The second is Lemma 2's second claim, used for (2.12): showing that stays in requires a boundary argument along the segment from to , since the Taylor bounds are only available inside . The remaining work is calculus in : the integral form of Taylor's theorem for the gradient under a Lipschitz Hessian, and eigenvalue perturbation for the second entry of .
The space is EuclideanSpace ℝ (Fin n) for arbitrary n : ℕ. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every x ∈ F. At boundary points of this asks for two-sided derivatives, a mild strengthening of "twice differentiable on ". The Lipschitz condition uses the operator norm, which is the spectral norm. is represented by the predicate IsCubicStep (global minimizer of cubicModel), and every lemma is stated for every such minimizer. The run predicate IsCubicNewtonRun is 0-based. It writes as plus the model value at , which is the minimum because attains it. is lamMin, the Rayleigh-quotient infimum over the unit sphere, which equals the smallest eigenvalue for the (symmetric) Hessian. The lower bound is required on only. The minimum over is written as the existence of an index attaining the bound.
A stationary point of the cubic model is not an admissible step, and the run must keep the test and the acceptance test. Replacing the step by any point with makes the goal false, and dropping the square root in makes Lemma 5 false. The statements rule out all three. Lemma 5 carries the hypothesis , which its printed proof uses and which holds at every iterate.
A complete development needs the Taylor bounds (2.2)–(2.3) for vector-valued derivatives on convex sets, and first- and second-order optimality for the cubic model. It also needs a proof of Proposition 1 (Section 5.1 or any other correct argument) and eigenvalue perturbation via Rayleigh quotients. The cubic-model lemmas and Proposition 1 are reusable across the whole series. Proofs of any milestone, alternative proofs of Proposition 1, and general Mathlib-level lemmas about Rayleigh quotients are welcome.
A maximal independent set (MIS) of a graph is a set of vertices, no two adjacent, to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be found fast in parallel was a central question of parallel complexity in the early 1980s: an MIS algorithm is a subroutine for maximal matching, vertex colouring with colours, and many other symmetry-breaking tasks.
Luby's algorithm is the standard textbook example of a randomized parallel algorithm and remains the basis of distributed MIS algorithms in the LOCAL model. Its analysis rests on one statement, Theorem 1 of the paper, which this mission formalizes.
All algorithms in the paper run the same loop on a finite simple undirected input graph with vertices. The current graph is , initially . For the neighbourhood is . One execution of the loop body selects a set independent in , adds it to the output, and replaces by the subgraph induced on . The loop stops when is empty.
For write for its neighbours and for its degree. The two Monte Carlo select steps are:
Let be the number of edges of before the -th execution of the loop body. The number of edges eliminated by that execution is : exactly the edges of with at least one endpoint in . For the paper uses the weight .
For the current graph and ,
The constants are those printed in the paper. No connectivity, degree or size condition on is assumed.
Theorem 1 says that each round removes, in expectation, a constant fraction of the remaining edges. From it the paper derives that the expected number of rounds of either algorithm is , and hence that MIS has a Monte Carlo algorithm running in expected time on a CRCW P-RAM and on an EREW P-RAM with processors. Algorithm B and the proof of part (2) are also the basis of the paper's deterministic algorithm: the analysis of Lemma B uses only pairwise independence of the coins. The companion mission (A Simple Parallel Algorithm for the Maximal Independent Set Problem II) formalizes that derandomization and reuses the statements of milestones 2, 5 and 6.
The results are proved in the paper and reproduced in textbooks (e.g. Motwani and Raghavan, Randomized Algorithms), but not formalized: no statement of Theorem 1, Lemma A or Lemma B was found on the platform. A formal proof would make the per-round analysis of a standard parallel randomized algorithm reusable. That includes the degree-weighted counting of milestone 6 and the Bonferroni-type bound of the Technical Lemma, both of which recur in later analyses of distributed symmetry breaking.
The obvious argument tries to show that a fixed vertex enters with good probability. That fails, because a high-degree vertex rarely wins against all its neighbours. The analysis instead bounds the probability that a vertex is removed, i.e. lands in . This event is a union over neighbours of dependent events, so the first Bonferroni inequality alone does not give a lower bound: the pairwise-intersection terms must be controlled. The union bound can also be very lossy when is large, which is why the conclusion involves a minimum with a constant.
A second obstacle is the passage from vertices to edges: vertices of small can have high degree while contributing little probability. The per-vertex bounds therefore have to be summed with degree weights and redistributed over edges. For Algorithm A there is an additional complication: priorities from can collide, so the argument about a uniformly random order holds only on the event that is injective. That event appears as the factor .
SimpleGraph V on a finite type with decidable adjacency, and . The degree is SimpleGraph.degree, is neighborFinset, and is edgeFinset.card.Theorem 1 is false for arbitrary distributions of priorities or coins. A formalization that takes "Pr" as an unconstrained parameter, conditions on the event of interest, or replaces by does not state the paper's theorem.
A complete development needs finite product probability spaces, inclusion–exclusion (Bonferroni) inequalities for finite unions, the symmetry of uniform priorities conditioned on injectivity, and degree-sum identities (SimpleGraph.sum_degrees_eq_twice_card_edges). The Technical Lemma and milestones 5 and 6 are reusable beyond this mission. Proofs of any milestone, and alternative proofs of Lemmas A and B, are welcome.
The Critical-Path Method (CPM) was introduced by J. E. Kelley, Jr. (Remington Rand) and M. R. Walker (du Pont) in Critical-Path Planning and Scheduling (Proc. Eastern Joint Computer Conference, 1959, pp. 160–173, doi:10.1145/1460299.1460318). Together with PERT, developed at the same time for the Polaris programme, it became the standard way to plan and schedule large projects in construction, maintenance and engineering, and it is taught in every introductory operations research course.
The paper reduces project scheduling to arithmetic on a directed acyclic graph: the earliest and latest times of the project's events are computed by two recursions, and the jobs whose timing has no slack, the critical jobs, are singled out by an equation. Its central structural claim is that critical jobs, when they exist, form a path from the start of the project to its end. The paper states this without proof ("a detailed development being reserved for a separate paper", p. 161). This mission formalizes that claim and the facts about the two recursions on which it rests.
A project network has events labelled with : event is the origin and event the terminus. A job is an arrow from an event to an event , written job ; the jobs form a finite set of ordered pairs of events. Two standing assumptions of the paper (pp. 161–162) are part of the model:
Each job has a real duration . The earliest event times are given by display (1) of the paper,
and, for a project completion time , the latest event times by display (2),
The maximum time available for job is . The job is critical if this equals its duration, , and a floater if it exceeds it. A critical path is a contiguous path of critical jobs from origin to terminus: events with every a critical job of .
In the Lean development these are ProjectNetwork n (with field P), earliest N y, latest N y λ, maxTimeAvailable, IsCritical, IsFloater and IsCriticalPath, in the namespace CriticalPath.Events.
For every project network, durations and completion time ,
This is the paper's "A project will contain critical jobs only when . If a project does contain critical jobs, then it also contains at least one contiguous path of critical jobs through the project diagram from origin to terminus." Only the "only when" direction is asserted, as on the page.
The result. The theorem is what makes the method's name meaningful: it says that the jobs without slack are not scattered but line up along an origin–terminus path, and that such jobs exist only when the project is scheduled at its earliest possible completion time. Project managers use this to decide which jobs to watch, which to expedite, and which may slip; the delay statement (milestone 4) is the quantitative form of that advice. The characterisations of (1) and (2) as least and greatest feasible schedules are the bridge between CPM and linear programming: they identify and with extreme solutions of the system of difference constraints , which the paper's own §3 uses to build the project cost curve.
Formalizing it. The results are classical and folklore, but the paper proves none of them, and textbook treatments usually define the critical path as a longest path, which makes the goal a tautology. This mission states the claims with the paper's own definitions: criticality by the float equation, event times by the recursions. To the best of current knowledge no machine-checked version of these statements for activity-on-arrow networks exists; the platform has a related activity-on-node development (Brucker and Knust, Complex Scheduling) in which the critical path is defined as a longest path.
The recursions (1) and (2) are local: each event looks only at its immediate predecessors or successors. The goal is global: from one critical job it asserts a statement about the whole completion time and a whole origin–terminus path. The float equation mixes a quantity computed forward from the origin with one computed backward from the terminus, and neither recursion alone says anything about the other. The naive reading "a critical job lies on a longest path" is not available as a definition: it is, in substance, what has to be established from the recursions. The formal overhead is the well-founded recursion on the labels, in both directions, and the bookkeeping of lists of events forming a path.
Events are Fin (n + 1), origin 0, terminus Fin.last n, with 1 ≤ n. Jobs are a Finset of ordered pairs, so there is at most one job per ordered pair. The standing assumptions (labels increase along jobs; origin precedes and terminus follows every event, via Relation.ReflTransGen) are fields of the structure ProjectNetwork and are never dropped. Durations and times are real numbers; durations are a function Fin (n+1) → Fin (n+1) → ℝ read only on jobs of P, with no sign condition, as in the paper's deterministic case.
The event times are defined by the recursions (1) and (2) themselves, by well-founded recursion on the label with Finset.sup'/Finset.inf' over the predecessor/successor set; these sets are nonempty by the standing assumptions, so no fallback value exists. The latest times are defined for every real ; the paper's assumption is a hypothesis of every theorem that uses them.
Disclosed readings: "earliest time occurance" (milestone 1) and "latest time … relative to a fixed project completion time" (milestone 2) are read as least and greatest vectors satisfying the job constraints (the paper's constraint (8), p. 165); milestone 3 is the fact implicit in the dichotomy "critical or floater"; "comparable delay" (milestone 4) is read as an exact delay of in for .
A trivializing formalization is ruled out: defining a critical job or path through longest paths, or taking and as arbitrary functions satisfying (1) and (2), would make the goal a restatement of its definitions; here criticality is the float equation and the times are computed by the recursions. Dropping the reachability assumptions would make (2) ill-defined at events without successors.
Contributions welcome: proofs of the milestones, general lemmas on longest paths in finite labelled DAGs and on difference constraints , which are reusable for the companion mission on the project cost curve.
Bin packing asks how to place a list of items with sizes in into as few unit-capacity bins as possible. It models the cutting of stock material, the packing of files onto tracks of a disc and the assignment of jobs to machines with a common deadline. Deciding the optimum is NP-hard, so in practice simple rules are used, and the question is how far they can stray from the optimum in the worst case.
Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3(4), 1974) gave the first sharp worst-case bounds for the four classical rules. For First-Fit Decreasing (FFD), the rule that sorts the items into nonincreasing order and then places each into the first bin with room, they announced the bound , whose full proof in Johnson's thesis exceeds 75 pages. To show the method, Section 4 of the paper proves a simpler bound in detail: when no item exceeds , FFD uses at most bins. That result is the subject of this mission.
Timeline:
A list is a finite sequence of real numbers in ; values may repeat. A bin has capacity ; its level is the sum of the numbers in it. The optimum is the least number of bins into which the elements of can be placed with no bin level exceeding .
First-Fit places in order into bins , each initially at level : goes into the bin of least index whose level satisfies . First-Fit Decreasing first arranges into nonincreasing order and then runs First-Fit. is the number of bins it uses.
The proof uses a weight on finite sets of elements. For an integer , is a -piece if , and a -bin is a bin whose largest element is a -piece. Set . A pair obeys relation if is a -piece and ; then , and otherwise . For a partition of into one- and two-element sets, with each pair ordered (earlier, later) in the nonincreasing order,
BASIC is the set of elements of that are -pieces lying in a -bin of the FFD packing of , for some ; SURPLUS is the rest of .
The constants are those printed in the paper. The multiplicative constant is best possible.
A companion item states the Remark after Theorem 4.1: for every there is a list with all elements below , and .
Theorem 4.1 shows the weighting-function method in its simplest nontrivial form: a weight whose total is within a constant of the algorithm's bin count, and which no feasible bin can exceed by more than the target ratio. The same method, with more elaborate weights, gives the bound for FFD, and it is the model for later worst-case analyses of packing heuristics. The Remark shows that is exact for items in , and the Corollary on p. 322 extends the analysis to the asymptotic ratio when items are bounded by .
The source proof is partial. The billing argument behind Claim 4.2.2 is given only when two auxiliary conditions (G1) and (G2) hold ("The more intricate argument here omitted", p. 321), and Lemma 4.3 is checked in four of about seventy-four cases ("leaving the remaining 70-odd, more or less routine, cases to the ambitious reader", p. 321). Complete details are in Johnson's thesis. The theorem itself is established. A formalization therefore gives the first complete, checked proof in a single place. The finite case analysis of Lemma 4.3 is well suited to machine checking. No machine-checked proof of any FFD bound is known to exist.
The obvious weight alone fails. Claim 4.2.1 shows that covers the FFD bins, but many sets of elements with sum at most have , for example two -pieces, a -piece and a -piece. The pair discounts of repair Lemma 4.3, but they must then be paid for in Lemma 4.2, for every partition. That is Claim 4.2.2: a charge from each discounted pair to distinct SURPLUS elements that are no larger. The charge is straightforward only when no member of a pair obeying relation lies in a bin of type . In general a pair's larger element may already have been charged by a smaller relation, and the paper omits the argument that handles this. Lemma 4.3 is elementary but has many cases, each determined by the piece types in and the relations they obey.
A list is L : List ℝ with IsList L ( for each element) in every statement. is optBins L, the least such that some map from positions to Fin b has every bin sum at most . The First-Fit run keeps the nonempty bins as a List (List ℝ), and opens a new bin at the end exactly when no existing bin fits, which is the paper's "least ". The fit test is . FFD is First-Fit on sortDesc L, the mergeSort into nonincreasing order; ties do not affect the bin count. Indices are -based.
sorts into nonincreasing order and minimises over the involutions of its positions: fixed points are singletons, and a pair is oriented (larger, smaller). The minimum is over a finite nonempty set, so it is attained. BASIC is a set of positions of sortDesc L, and each position's bin is its bin in the final FFD packing. In , is the piece type of the first element. Sums are over Finset.Icc 2 (N - 1) with .
The goal's range is . The restriction to belongs only to the proof, through Lemma 3.3. Stating the goal for , weakening or , or making an unattained infimum would each change the theorem. Only the FFD half of Lemma 3.3 is stated. Claim 4.2.1 is stated with Lemma 4.2's standing hypothesis . The Remark's printed range is a misprint: its FFD packing needs , and the companion item states only the existence claim.
Infrastructure needed: a usable API for the First-Fit run (the invariants of the fold, bin levels, the order of bins), a lemma that FFD bins receive items in nonincreasing order, and a decision procedure for Lemma 4.3's case analysis over piece types. The model file and the weight file are reusable for the bound (mission 3 of this series) and for the bounded- corollaries. Contributions of proofs of Lemma 4.3 by computer-checked case enumeration, and of the missing general case of Claim 4.2.2, are especially welcome.
Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models table formatting, the placement of program segments on pages, and the allocation of files to disc tracks, and it is NP-complete, so exact solutions require search in general. Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3 (1974)) therefore studied four simple placement heuristics and bounded how far each can be from the optimum in the worst case. Their paper is one of the founding results of the worst-case analysis of approximation algorithms.
This mission concerns the two decreasing heuristics, which sort the items from largest to smallest before placing them. For them the paper proves that at most of the optimum, plus an additive constant, is ever used, and that the factor cannot be improved.
Timeline.
A list is a finite sequence of real numbers in ; values may repeat. A bin has capacity ; its level is the sum of the numbers placed in it. The optimum is the least number of bins into which the elements of can be distributed so that no bin has level exceeding .
The bins start empty and the elements are placed one at a time, in list order.
and are the numbers of bins that receive at least one element.
Two auxiliary notions from the paper's proof also appear among the milestones. The position of an element in a packing means that it is the -th element placed into bin . The weight of a collection of elements is defined through -pieces, the elements in . Each element has the weight . A pair with a -piece and has the discounted weight , and any other pair has . is the least total weight over all ways of grouping into singletons and pairs.
For every list ,
The constants are the paper's. Both halves are part of the goal.
The bound makes FFD and BFD, which run in time, the reference heuristics for off-line bin packing. The bound and its proof technique of weighting functions were the model for the analysis of many later packing and scheduling heuristics. Theorem 3.1 shows that the factor is exact, so together with the goal it determines , where is the largest ratio over lists with .
The result is proved, but the source proves it only in part. The paper gives complete proofs of Lemma 3.3, Theorem 3.4 and Theorem 3.1. For the reduced assertion it gives only an outline, whose central inequalities involve maps the paper never defines, and it refers to the thesis for the details. Lemma 4.2 is proved in the paper through two claims. A formal proof of the goal must therefore either formalize one of the later complete proofs (Baker 1985, Yue 1991, Dósa 2007) or reconstruct the thesis argument. No machine-checked proof of the bound is present in Mathlib or on the platform.
The obvious approach, used for First-Fit in Section 2 of the same paper, assigns each element a weight depending only on its size, so that every bin of the algorithm's packing weighs at least and every bin of an optimal packing weighs at most the target ratio. For FFD no weighting of single elements works at ratio . Summing over the elements overcharges the FFD packing: a set of elements fitting into one bin can carry total -weight well above . The paper's remedy is a weight defined on pairs, , which discounts elements that could share a bin with a larger one. Even with , the bins of FFD whose largest element exceeds do not fit the scheme. Handling them requires a case analysis that the paper only sketches and that runs to more than 75 pages in the thesis.
The BFD half cannot be obtained by bounding BFD by FFD in general: there are lists with . Theorem 3.4 works only because Lemma 3.3 first removes all elements below .
Lists are L : List ℝ with the predicate IsList L ( for every element), assumed by every statement. is optBins L, the least b : ℕ admitting a map from the items to Fin b with every bin sum at most . A run keeps the nonempty bins as a List (List ℝ) in index order and opens a new bin at the end exactly when no nonempty bin fits, which matches the paper's "least " over infinitely many empty bins. The fit test is non-strict. FFD and BFD are FF and BF applied to sortDesc L, a stable merge sort into nonincreasing order. They are defined for every list, so the goal is stated for arbitrary, unsorted . Positions are -based pairs (bin, place in bin) read off the run.
sorts its argument into nonincreasing order, so index is the position in that order. It then minimizes over involutions of the positions, which encode the partitions into one- and two-element sets. Weights are real-valued; the paper's use of rationals is incidental. The range hypotheses are exactly the paper's: is closed in Theorem 3.4, is open at , and Lemma 4.2 has .
A weakened goal, such as with a larger , a bound for sorted lists only, or the FFD half alone, is a different theorem and does not close the mission. Claims 3.4.1–3.4.4 and 3.4.7 and the inequalities , of the outline are not stated: they concern the paper's step-by-step construction and the undefined maps , .
A complete development needs basic lemmas about FF and BF runs (levels stay at most , a new bin opens only when nothing fits, runs on prefixes). It also needs invariance of FFD and BFD under permutations of equal elements, the monotonicity of under deletion, and . These are reusable in the other missions of this series. Proofs of individual milestones, alternative complete proofs of the goal, and sharper additive constants are all welcome.
Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It is one of the first problems studied through the worst-case analysis of approximation algorithms, and it models storage allocation, paging and file placement on tracks, as well as cutting-stock problems in operations research. Deciding the optimum exactly is NP-hard, so the practical question is how badly simple rules can do. The two simplest on-line rules, First-Fit and Best-Fit, are still the baseline against which every later bin-packing heuristic is measured.
Timeline:
A list is a finite sequence of real numbers in ; values may repeat. A bin has capacity , and its level is the sum of the numbers in it. The optimum is the minimum number of bins into which the elements of can be placed so that no bin contains numbers whose sum exceeds .
Both rules place in this order into bins , each initially at level , and never move an element once placed.
and are the numbers of nonempty bins at the end. The worst-case ratio at optimum is
The analysis also uses a weighting function , piecewise linear with on , on , on and on , and the coarseness of a bin of a completed packing: the largest over the bins of smaller index, and for the first bin.
The goal fixes only the asymptotic ratio and leaves the additive constants free, so it is the statement that survives the later improvements of the constants.
A companion item, not a milestone, records the explicit list of Fig. 3 (p. 307) with and .
The result fixes the worst-case behaviour of the two simplest bin-packing heuristics: neither ever uses more than about more bins than an optimal packing, and both can be forced to. The weighting-function technique introduced for this bound became the standard method for analysing bin-packing heuristics, including First-Fit Decreasing, Harmonic-type algorithms and on-line lower bounds, and the constant is the reference point for later on-line algorithms.
The theorem is proved, and its constants have since been sharpened. No machine-checked proof of any of these results is known. This mission produces a Lean model of on-line bin packing (the optimum, the First-Fit and Best-Fit runs with their placement history, and the worst-case ratio) that the other missions of this paper and later bin-packing formalizations can reuse. It also produces formal proofs of the weighting-function bounds, of the upper bound and of the lower-bound construction.
The first idea, charging each bin its level, gives only : at most one bin is at most half full. The ratio comes from bins that are more than half full but far from full, and a bound on the total size of the elements cannot see them. No property of the final packing alone suffices: the bins that are far from full can only be controlled through the order in which the rule opened and filled them, so the argument depends on the dynamics of the run. On the lower-bound side, the natural periodic list (sizes near , p. 301) gives only the ratio ; reaching needs a list on which both rules waste space in every medium bin, for every , while is still known exactly.
A list is L : List ℝ with the hypothesis IsList L (every element in ), and every statement assumes it. is optBins L, the least b : ℕ for which some assignment Fin L.length → Fin b has every bin sum at most . A run is a fold over the list that keeps only the nonempty bins, in index order, each with its contents in placement order. A new bin is opened at the end exactly when no nonempty bin fits, which is the paper's "least " over infinitely many initially empty bins, since elements are positive. The fit test is the non-strict , and Best-Fit breaks ties by least index. The placement history (the bin chosen for each element and that bin's level just before) is read off the run on the prefix of the list. Indices are -based. Coarseness is computed in the completed packing. is a function ℝ → ℝ and is only ever applied to elements of . and are suprema in the extended nonnegative reals , and the limit is taken there.
A real-valued supremum would be on an empty or unbounded family, and the limit statement would then say nothing about the algorithms. The extended-real supremum rules this trivialization out. Every claim is stated for the concrete First-Fit run and the concrete Best-Fit run, not for an abstract rule with the properties used in the proof.
Claim 2.2.4 is printed with alternative (i) " and ", which is false: First-Fit on gives a counterexample. The mission states it with , which is what the paper's proof establishes and what the main proof uses. The milestone text keeps the printed version.
The model definitions are reusable for any on-line bin-packing rule, since the run is parameterized by the choice rule. Contributions welcome: proofs of the milestones, general lemmas about the runs (levels stay at most , at most one bin is at most half full, the history determines the final packing), and the computation of for the explicit lists of Theorem 2.1 and Fig. 3.
Many operational systems move between a finite number of states at random times: a machine alternates between working and repair, a queue between occupancy levels, an inventory between stock positions. When the time spent in a state is not exponential and not a fixed period, neither discrete-time Markov decision processes nor continuous-time Markov chains describe the system faithfully. William S. Jewell's 1963 paper Markov-Renewal Programming. I extends Howard's Markov decision processes to Markov-renewal processes (also called semi-Markov processes), in which the time between transitions is a random variable whose law depends on the current state, the next state, and the decision taken. The resulting model, now called a semi-Markov decision process, is standard in maintenance, queueing control and reliability.
Timeline:
A Markov-renewal program has a finite set of states (the paper's ) and a finite, nonempty set of alternatives (the paper's ), each available in every state. For each alternative and states it specifies:
The Laplace–Stieltjes transform is the expected discount over one interval. The average one-step return is , and for a vector of returns the test quantity is
A stationary policy is a map ; a nonstationary policy is a sequence of such maps, being used at the -th transition. The -step return of a policy, with boundary rewards , is the test quantity of applied to the -step return of the shifted policy; the optimal -step return of equation (6) replaces by a maximum over . The value-determination equations (15) of a stationary policy are .
The algorithm of Fig. 1 alternates two steps: solve (15) for the current policy, then in every state pick an alternative maximizing the test quantity, keeping the old alternative if it still attains the maximum. It stops when two successive policies are identical.
For every : (15) has a unique solution for every stationary policy, and every run of Fig. 1 reaches with , where
for every state and all boundary rewards, every limit existing. This is the paper's "the algorithm of Fig. 1 produces an optimal, stationary policy that is as good as any optimal, nonstationary policy".
The result says that the infinite-step discounted Markov-renewal program is solved exactly, in finitely many cycles, by a finite-dimensional algorithm, and that the answer is a stationary policy. As the paper notes, this matters operationally because a nonstationary policy is hard to follow. The sojourn distributions enter only through the numbers , so the same algorithm serves any sojourn-time law. For fixed the model is a discounted Markov decision process whose discount factor depends on the transition, which contains Howard's and Blackwell's constant-discount problem as the case of intervals of fixed length (p. 943).
The results are classical and proved in the literature. The paper itself refers the proofs to Howard and Blackwell. Machine-checked versions exist on this platform for finite stochastic shortest path and constant-discount problems (Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.2.2 and 7.3.1, mission Dynamic Programming and Optimal Control VII). No formal treatment of Markov-renewal programs, of transition-dependent discounting, or of the retention rule of Fig. 1 is known to exist. The mission produces a verified policy-iteration theorem for semi-Markov decision processes, with an explicit termination bound and the comparison against nonstationary policies.
The discount over one transition, , varies with , and , so the problem is not a constant- contraction of textbook form; the relevant bound is that every row of sums to less than one, which rests on . Entries in alone, the paper's stated justification of Claim (a), do not make invertible: the matrix with every entry has entries in , yet minus it is singular.
Finite termination is not automatic either. If the improvement step may switch between tied maximizers, the iterates can cycle forever between two policies with equal returns; the retention rule of Fig. 1 excludes this, and Claim (b) must deliver a strict increase in some state, with no decrease anywhere, to rule out revisiting a policy. Comparing with nonstationary policies requires controlling returns of arbitrary policy sequences, whose limits must be shown to exist, not assumed.
Reusable infrastructure: bounds for substochastic matrices with row sums below one (invertibility, Neumann series, nonnegative inverse), convergence of iterated Bellman operators with transition-dependent discount, and the policy-iteration termination argument with a tie-breaking rule. Proofs of any milestone and alternative arguments are welcome.
The conjugate gradient method (cg-method) of Hestenes and Stiefel is the standard iterative solver for linear systems with a symmetric positive definite matrix . It is used for the large sparse systems of finite-element and finite-difference discretizations, as the inner solver of Newton-type and interior-point methods in optimization, and as the prototype of the Krylov subspace methods. Its original 1952 paper (Hestenes and Stiefel, J. Res. NBS 49(6), 1952) already presented it as two things at once: a direct method that reaches the exact solution in at most steps, and a method of successive approximations whose intermediate estimates are useful in their own right.
The second view needs a guarantee that the intermediate estimates actually approach the solution. The method is built to decrease the -weighted error , and the residual need not decrease (Section 18 of the paper, p. 432, notes that it can increase at every step). Theorem 6:3 of the paper supplies the guarantee in the plain Euclidean length: the distance from the estimate to the solution decreases strictly at every step, by an exactly computable amount. This mission formalizes that theorem together with the relations from Sections 5 and 6 of the paper on which its proof rests.
Timeline:
Let be a real matrix that is symmetric and positive definite, let , and let be the solution of . Write and . From an arbitrary starting point , the cg-method (5:1) computes estimates , residuals and direction vectors by
The error vector of is . The error function (4:5) is , which is nonnegative and vanishes only at . The Rayleigh quotient (4:12) of a vector is . The Lean development names these cgIter A k x₀ i (with fields .x, .r, .p), cgAlpha for , errorFun A h x and rayleigh A z.
For every step that the method performs, that is, every with ,
The paper writes the step from to ; the Lean statement shifts the index by one. The goal holds for every dimension , every symmetric positive definite , every and every .
The theorem is what makes an early stop of the cg-method safe in the norm a user usually cares about. Every intermediate estimate is closer to the solution, in Euclidean distance, than the previous one, and the identity (6:5) states by how much. It also separates the cg-method from methods that minimize the residual: the -norm error, the Euclidean error and the residual behave differently, and only the first two are monotone along cg.
The results are proved in the 1952 paper. They have not been formalized: the Prove2Me library has no statement of the conjugate gradient recursion (5:1), and Mathlib has none either. What this mission adds is a machine-checked version of the paper's Section 6 argument for the recursion exactly as printed, including the case analysis at termination that the paper leaves implicit, and a reusable Lean definition of the cg iteration with its basic identities.
The obvious argument does not reach the conclusion. The method decreases at every step, but a decrease in this -weighted norm does not imply a decrease in the Euclidean norm: for a single step along an arbitrary direction, even the best step for can lengthen the Euclidean error. So the theorem cannot be proved one step at a time from the local minimization property. It depends on how the current direction relates to all the later directions of the same run, and those relations in turn rest on the mutual orthogonality of the residuals and the conjugacy of the directions, which are established by an induction over the whole run.
A second difficulty is bookkeeping at the end of the run. The recursion divides by and by , which vanish after termination. Every milestone has to hold, or be guarded, past that point, and the goal needs the hypothesis exactly because the strict inequality fails once .
Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), is Matrix.mulVec (*ᵥ), and the standing assumption is A.PosDef, which in Mathlib includes symmetry. The solution is a variable with the hypothesis A *ᵥ h = k. Indices are 0-based. The cg recursion is the definition cgIter, which computes (5:1b)–(5:1f) literally and in order; it has no stopping rule, and Lean's convention makes it stay at with once . Lengths appear squared, as . The milestones are stated for every index without a termination guard, because both sides of each identity vanish after termination; only the goal carries .
Two formalizations would trivialize the goal and are ruled out. The goal does not assume termination () or any bound on : it quantifies over every cg run and every step that takes place. And it is about the Euclidean length , not the error function (that is Theorem 6:1, a different and weaker statement) and not the residual.
A complete development needs Theorem 5:1 (orthogonality of residuals, conjugacy of directions) for the literal recursion, the identities (5:2) and (5:3c), and the positivity of for . These are reusable for any further work on the cg-method, including the sister mission on finite termination. Proofs of any milestone, and alternative proofs of Theorem 6:3 through the Krylov-subspace characterization, are welcome.