Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A retailer that sets both its replenishment quantities and its prices over a finite selling season faces a coupled decision: the price shapes the demand that the inventory must serve, and the inventory position shapes which price is worth charging. With a fixed cost per order, the classical inventory answer is the (s, S) policy of Scarf (1960): when the stock falls below a reorder point , order up to the level . Thomas (1974) asked what happens when the price is also a decision, and conjectured that an (s, S, p) policy — an (s, S) ordering rule together with a price that depends on the stock level — is optimal "under fairly general conditions". He also gave a counterexample when prices are restricted to a discrete set.
Chen and Simchi-Levi (Operations Research 52(6), 2004) settled the conjecture for the finite horizon. When demand is additive in a random shock, , the conjecture holds (§3, Theorem 3.1). When the shock is not additive, it fails, and a weaker policy class is optimal (§4, the second mission of this series). This mission formalizes the additive case.
Timeline:
There are periods . In period the firm starts with inventory , orders up to a level at cost , where is a fixed cost, a unit cost and if and otherwise, and sets a price. Demand is for a random pair with , ; in the additive case . Unmet demand is backlogged, and an end-of-period inventory costs , a convex function.
Since price and expected demand determine each other, the decision is an expected demand , with price and expected revenue , assumed concave. With , the profit-to-go functions satisfy and, for ,
where maximizes over . A function is k-convex if for all , , (Definition 2.1), and k-concave if is k-convex. Assumptions 3–5 of the paper give the stated one-sided growth limits and polynomial growth , and give demand a finite -th moment.
For additive demand and every period : attains its maximum at some , the functions and are k-concave, and there exist such that
maximizes over , , and a best expected demand exists at ; the price is of it.
The theorem identifies the structure of an optimal policy for a basic model of coordinated pricing and replenishment: two numbers per period determine the ordering decision, and the price is a function of the post-order stock. It confirms Thomas's conjecture in the additive case and tells a computation or an approximation scheme which policy class it may restrict to; §5 of the paper extends it to a nonincreasing fixed cost, the infinite horizon and Markovian demand.
The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization adds checked versions of the k-convexity toolkit (the equivalence of the two standard definitions; the (s, S) structure lemma), a checked monotone-selection argument for a parametric maximization, and a checked finite-horizon induction in which an expectation, a maximization over a continuous action and a fixed cost interact. The proof of part (a) is omitted in the paper ("similar to that of Theorem 1 in Federgruen and Heching (1999)"), so formalizing it supplies a missing argument.
The obvious argument fails at the expectation. A k-concave function composed with a shift is k-concave for a fixed , but here the demand decision depends on , and k-concavity, unlike concavity, is not preserved under an arbitrary reparametrization: Definition 2.2 is asymmetric in its two points. The inequality needed for the continuation value requires the post-demand levels to be ordered like the inventory levels . That is the content of Lemma 2, and it uses additivity; for multiplicative demand the ordering fails, and so does the theorem (§4).
The second difficulty is analytic: each step of the induction needs a continuous continuation value of polynomial growth, so that the expectation in (3) is finite and continuous, the maximum over is attained, and is coercive.
The model is a structure of real data indexed by , with periods ; the law of is a probability measure on and expectations are Bochner integrals. The formalization works in expected-demand space , equivalent to price space because is a continuous strictly decreasing bijection. Additivity is " almost surely". The profit-to-go is defined by recursion on the number of periods to go, with . Maxima are written as real suprema; every target that uses them asserts that they are attained, so the convention that an unbounded supremum is never enters. k-convexity is the platform's BertsekasKConvex (Definition 2.1); k-concavity of is k-convexity of .
Conventions and restrictions relative to the printed page:
A trivializing formalization is ruled out: the targets assert attainment of every maximum they mention and the identity between and the maximized objective, so a supremum that defaults to , or an integral of a non-integrable function, cannot make them hold vacuously; and the assumptions are satisfiable (a one-period instance with meets all of them).
A complete development needs: continuity of parametric integrals under polynomial domination; attainment of maxima over compact intervals; Topkis-style monotone selection for functions with increasing differences; the (s, S) structure lemma for k-convex functions (proved on the platform); and the closure of k-concavity under the operations above. The k-convexity results and the monotone-selection lemma are reusable for the general-demand mission of this series and for other fixed-cost inventory models. Contributions to any milestone are welcome, including proofs that rely on platform results by Topkis (Supermodularity.Monotonicity.argmax_increasing_of_increasing_differences).
The ellipsoid method is the cutting-plane algorithm that settled the polynomial-time solvability of linear programming and, more generally, of convex optimization over any set that comes with an efficient separation oracle. It was introduced for convex minimization by Shor and by Yudin and Nemirovski in the 1970s, and Khachiyan used it in 1979 to give the first polynomial-time algorithm for linear programming. Grötschel, Lovász and Schrijver later turned it into the general equivalence between separation and optimization that underlies much of combinatorial optimization.
This mission is the second of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). Its goal is the convergence guarantee of the ellipsoid method, Theorem 2.4 (p. 250), together with the geometric lemma and the steps of the proof on which it rests.
Timeline:
Write for the space of real -vectors, with the dot product . An ellipsoid is a set
where is its center and is a symmetric positive definite matrix.
A convex body is a compact convex set with non-empty interior. The objective is continuous and convex on with values in , and are such that lies in the Euclidean ball of center and radius and contains some Euclidean ball of radius . A subgradient of at is a vector with for all .
The method starts from , . At step it asks for a vector :
It then replaces by the ellipsoid given by
After iterations the output is the best of the queried centers that lie in .
For and every , , some queried center lies in , and every output satisfies
and for the explicit ellipsoid (2.5)–(2.6) works. 3. The remark before Theorem 2.4 (p. 250): a point of can leave the current ellipsoid only at a step with , and then its value exceeds . 4. Two steps reused from Theorem 2.1 (pp. 246–247): for , and on .
Theorem 2.4 bounds the oracle complexity of the ellipsoid method: accuracy needs oracle calls. Each step costs arithmetic operations plus one oracle call. With the separation oracles of linear and semidefinite programs this gives polynomial overall complexity (p. 250). The rate depends on the instance only through and , so the method needs no smoothness and no strong convexity. Lemma 2.3 is also the geometric step of the ellipsoid method for linear feasibility.
The result has a textbook proof. The work of this mission is to formalize it. The same update is published on the platform from Bertsimas and Tsitsiklis's Introduction to Linear Optimization (Theorem 8.1), with a proved volume factor of . That factor is weaker than (2.4)'s and does not give Theorem 2.4's constant. The sharper factor and the optimization version of the method (subgradient cuts, the output rule and the value bound) are not formalized on the platform.
There are two difficulties: Lemma 2.3 with the sharp constant, and the bookkeeping that turns per-step volume decrease into a value bound.
For the lemma, the volume of the explicit ellipsoid is times that of . Bounding it by rather than by the cruder needs the scalar inequality of milestone 1 for every . The reduction from a general ellipsoid to the unit ball also needs determinants under an affine map.
For the theorem, the obvious argument compares with . This only works if no cut removes an optimal point and if every removed point of is worse than a queried center. At the threshold the admissible is exactly , so a non-strict volume bound alone does not close the argument there.
Fin n → ℝ with Lebesgue measure, as in the reused Bertsimas–Tsitsiklis ellipsoid definitions (LinearOptimization.ellipsoid, ellipsoidUpdateCenter, ellipsoidUpdateMatrix, IsSubgradientOn).Fin n → ℝ is the sup norm.IsEllipsoidRun. Every theorem holds for every admissible oracle answer. The update is the published one with .Conventions and hypotheses added to the page:
A run predicate whose separation branch does not require , or that accepts with an update, would make the statements false or vacuous. Both are excluded.
Lemma 2.3's volume factor is . The weaker published factor does not prove that milestone. The published theorem LinearOptimization.ellipsoid_update_halfspace_volume is included as a reference: it supplies the containment (2.3) and positive definiteness. Contributions are welcome on every milestone. A determinant formula for the volume of an ellipsoid would be reusable well beyond this mission.
Generalization bounds in statistical learning theory control the gap between the empirical and the true performance of a predictor chosen from a class . Bartlett and Mendelson (JMLR 3, 2002) showed that this gap is governed by the Rademacher complexity of a loss class built from , and that, unlike the VC dimension, this complexity can be estimated from data. Their bounds are useful only if the Rademacher complexity of a large class can be bounded in terms of simpler classes: voting methods take convex combinations of base classifiers, neural networks compose fixed squashing functions with linear combinations, and loss classes compose a class with a Lipschitz loss. Section 3.1 of the paper collects the elementary rules for such constructions in one statement, Theorem 12. These rules are used throughout the later literature on margin bounds, boosting, and neural-network generalization (e.g. Koltchinskii and Panchenko, Ann. Statist. 2002).
This mission formalizes those rules, as stated in the published journal article (J. Mach. Learn. Res. 3 (2002), pp. 463–482), Theorem 12 on p. 469.
Let be a measurable space, a probability measure on it, and an integer. A class is a set of functions ; no boundedness is assumed.
For a sample , the empirical Rademacher complexity of (Definition 2, p. 464) is
the expectation over independent uniform random signs . The Rademacher complexity is its expectation over an i.i.d. sample from :
In the Lean development these are empiricalRademacher n F x and rademacherComplexity μ n F, both valued in .
The constructions on classes are those of §2, p. 467: is the class of convex combinations of functions from ; ; is the class of convex combinations of functions from ; ; for , ; and .
For all classes of real functions:
The goal is the conjunction, each part quantified over its own classes.
Parts 1, 3, 2 and 4 are milestones, in the order of the paper's proof. Part 7 remains a theorem item in the mission and a conjunct of the goal.
The result. Theorem 12 reduces the complexity of a constructed class to the complexities of its building blocks. Part 2 says that convex combinations come for free, which is why margin bounds for boosting depend only on the base class. Part 4 converts a complexity bound for a class into one for a Lipschitz loss composed with it, which is how the risk bounds of the paper's §2 are applied to concrete losses. Parts 1, 3 and 7 are the bookkeeping rules that combine the others; the paper uses parts 1 and 3 to show part 7 is tight.
Formalizing it. The results are proved, and part 4 is due to Ledoux and Talagrand (Probability in Banach Spaces, Springer 1991, Corollary 3.17). The platform already has a one-sided contraction lemma in a different normalization (UnderstandingML.contraction_lemma, Shalev-Shwartz and Ben-David's Lemma 26.9: per-coordinate Lipschitz maps, normalization, no absolute value, bounded nonempty sets of vectors), referenced here as supporting material, and a convex-hull identity for Mohri et al.'s empirical complexity without absolute value. None of the five parts is formalized for Definition 2's complexity (factor , absolute value inside the supremum, expectation over the sample, arbitrary classes). The mission provides machine-checked versions in exactly that normalization, reusable by the other missions of this paper and by any later development of Rademacher-complexity bounds.
Parts 1, 2, 3 and 7 are pointwise statements about finite averages of suprema, but they have to be carried through the expectation over the sample and through suprema that may be infinite. Part 2 needs the supremum of the absolute value of a linear functional over a convex hull to equal its supremum over the set, including the symmetric hull .
Part 4 is the substantial one. The natural first idea, comparing with term by term for each sign vector, fails: the inequality holds only after averaging over the signs, and only with the factor caused by the absolute value. Without the hypothesis the statement fails (a constant has but for nonempty and ), so any argument must use it.
Representation. Classes are Set (X → ℝ). Signs are averaged over all vectors Fin n → Bool (encoded ). Complexities take values in ℝ≥0∞: a class unbounded on the sample has complexity , the empty class has complexity , and is the lower Lebesgue integral against Measure.pi (fun _ : Fin n => μ) with μ a probability measure. This is the paper's meaning for arbitrary classes. A real-valued formalization would not be: a real supremum over an unbounded set and a Bochner integral of a non-integrable function both evaluate to . That would make the upper bounds false for unbounded classes and every comparison trivially satisfied for others. No boundedness hypothesis is added anywhere, since Theorem 12 is about arbitrary classes. is convexHull ℝ F (finite convex combinations, no closure); is convexHull ℝ (F ∪ -F); is c • F; enters as ENNReal.ofReal |c|, and makes consistent. The Lipschitz map in part 4 is LipschitzWith Lφ φ on all of , as printed. The classes of part 7 are indexed by Fin k and summed pointwise. At all complexities are and every part holds trivially, matching the page.
Added hypothesis. Part 7 (and its conjunct in the goal) assumes that each sample function is almost-everywhere measurable for . The paper does not discuss measurability. The lower integral is monotone and positively homogeneous without it, so parts 1–4 need no such hypothesis, but it is not additive, and part 7 needs additivity. The hypothesis holds whenever each is a countable class of measurable functions.
Omitted parts. Parts 5 and 6 of Theorem 12 are not posed. Part 5, , is false as printed: its proof (p. 470) bounds correctly but drops the factor of Definition 2, and the correct conclusion is . For , , the left side is and the printed right side is . Part 6 is derived from part 5. A corrected part 5 would not be the paper's statement, so neither is included. The remark after the theorem that parts 1–3 hold for the Gaussian complexity, and the others with an extra factor, is also not included.
Contributions welcome. Proofs of the milestones; a proof of part 4 from the platform's one-sided contraction lemma, converted to Definition 2's normalization; and general lemmas about empiricalRademacher (finiteness on finite classes, measurability for countable classes) that the other missions of this paper can reuse.
A binary classifier is judged by its misclassification probability, the chance that it mislabels a fresh example. That probability is unknown; what a learner sees is the training error, the fraction of mistakes on the sample it was trained on. A generalization bound controls the gap between the two simultaneously for every classifier in a class, so that a classifier chosen by looking at the data still has a guaranteed error. The classical bounds of Vapnik and Chervonenkis measure the class by its VC dimension, a fixed combinatorial quantity that does not depend on the data distribution, and the paper recalls evidence that such fixed complexity penalties cannot be universally effective for model selection (p. 464).
Bartlett and Mendelson's paper in the Journal of Machine Learning Research (2002) studies two data-dependent alternatives, the Rademacher and Gaussian complexities, and proves risk bounds and structural rules for them. This mission formalizes the paper's classification bound, Theorem 5(b), which replaces the VC penalty by half the Rademacher complexity of the class. The source is the published JMLR article (jmlr.org/papers/v3/bartlett02a), pp. 463–482; all page numbers below are the journal's.
Timeline. Uniform convergence of empirical frequencies with a VC-dimension rate is due to Vapnik and Chervonenkis (1971). Rademacher penalties for model selection were introduced by Koltchinskii (2001) and by Bartlett, Boucheron and Lugosi (2002), who also proved Theorem 5(a) with the maximum discrepancy. The 2002 paper proves part (b) in Appendix B (p. 480) by adapting its proof of the general risk bound, Theorem 8 (p. 467).
Let be a measurable space and a probability distribution on ; a pair is an example with label . Let be a set of -valued functions on (the classifiers), and let be an i.i.d. sample drawn from .
and the Rademacher complexity is with i.i.d. (Definition 2, p. 464). Note the factor and the absolute value.
For every , with probability at least over the sample, every satisfies
The bound is uniform: the probability that some violates it is at most .
Supporting platform items, referenced and not restated: McDiarmid's inequality for i.i.d. samples (StabGen.Uniform.mcdiarmid_inequality, open) and the symmetrization lemma in the normalization of Shalev-Shwartz and Ben-David (UnderstandingML.representativeness_le_rademacher, proved).
The result. Theorem 5(b) is a distribution-dependent risk bound for classification whose complexity term can be estimated from a single sample. The paper shows (Theorem 6, p. 465) that it is never much worse than the VC bound, since the empirical Rademacher complexity of a class is in terms of its empirical VC dimension , and it can be much better. It also serves as the template for margin bounds for large-margin classifiers, kernel machines and voting methods in Section 4 of the paper.
Formalizing it. The result is proved in the paper; no machine-checked proof is known to exist. A formal proof needs McDiarmid's inequality, a symmetrization argument with a ghost sample, and the reduction of the 0–1 loss class to the classifier class through the identity . The milestones split these, so they can be proved independently. The symmetrization milestone also corrects a printed slip (see Formalization scope).
The bounded-difference step and the final union of the two halves are short. The difficulty is in the symmetrization. The supremum over an uncountable class is not automatically measurable, so the expectations in the paper's chain need not exist as written; a proof must work with exactly the random variables it integrates and use only the measurability it is given. The exchange of a sample point with its ghost copy, the conditioning on the sample, and the replacement of by must each be justified on finite sign averages and product measures. The obvious shortcut, bounding the gap by the Rademacher complexity of the loss class , does not give the stated term: with the absolute value of Definition 2, the loss class's complexity is not , because contributes a sign sum that does not depend on .
Lean conventions:
ENNReal.ofReal on the real terms.Hypotheses added relative to the page, each necessary or a reading of the page:
UnderstandingML.representativeness_le_rademacher. They hold, for instance, for countable classes.Corrected slip: the chain on p. 480 ends "". The last equality is only "": carries an absolute value, and for the left side of that step is while . The symmetrization milestone states the chain's conclusion with , which is all Theorem 5(b) needs.
Not a valid formalization: a version with a real-valued supremum or Bochner integral for (which would read on an unbounded or non-integrable class and make the bound false or free), one that drops the absolute value or uses the normalization, or one that measures of the loss class instead of . Theorem 5(a) (maximum discrepancy, due to Bartlett, Boucheron and Lugosi) is not part of this mission.
Contributions welcome: proofs of the three milestones and the goal; the general McDiarmid inequality (the referenced open item); and reusable lemmas on measurable suprema of classifier families.
A learning algorithm picks a predictor from a class after looking at training examples, and the quantity of interest is its expected loss on a fresh example. Since depends on the data, its training error is a biased estimate of that loss, and a risk bound quantifies the bias uniformly over the class: with high probability, every has expected loss at most an observable sample average plus a complexity penalty. Classical penalties (VC dimension, covering numbers, fat-shattering dimension) are fixed in advance; data-dependent penalties such as the Rademacher complexity can be estimated from the sample itself and adapt to the distribution, which matters for model selection by complexity regularization.
Bartlett and Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results (JMLR 3, 2002, jmlr.org), state such a bound in a general decision-theoretic setting (Theorem 8, p. 467): the loss is any -valued function of an outcome and an action, and the sample average is taken of a dominating cost , which may be Lipschitz and hence amenable to the structural results of the paper's §3 even when is a discontinuous – loss. Multiclass classification with error-correcting output codes is the paper's example. The ingredients — McDiarmid's inequality (McDiarmid, 1989) and symmetrization — are standard; the paper combines them for this setting with a centred cost class. The source is the published JMLR article (pp. 463–482); all page numbers below are its printed pages.
Let be an input space, an output space and an action space with a distinguished action , each a measurable space. A probability measure on generates independent examples , and is a fresh draw from .
with independent uniform signs, and the Rademacher complexity is , the expectation over an i.i.d. sample (Definition 2, p. 464). The factor is and the absolute value is inside the supremum.
In Lean these are RadGauss.RiskBound.empiricalRademacher, rademacherComplexity, empMean, supDev (the uniform deviation ), doubleSupDev and phiTildeComp.
For every integer and every , with probability at least over the sample, every satisfies
The event is uniform over . The constant is the printed one.
The platform's Proved UnderstandingML.representativeness_le_rademacher (Shalev-Shwartz and Ben-David, Lemma 26.2) is included as a supporting reference: it is the middle inequality of milestone 5 in the , absolute-value-free normalization.
Theorem 8 bounds the expected loss of any predictor in the class, including one selected by the data, by quantities the learner can compute or estimate: the empirical cost and the Rademacher complexity of the centred cost class, which concentrates around its empirical version. Combined with the paper's structural results (§3: contraction by Lipschitz maps, convex hulls, sums), it yields margin bounds for voting methods, neural networks and kernel machines (§4) from complexities of simple base classes. Centring by matters: with the absolute value inside the supremum, can exceed by order even for a single function.
The result is proved in the paper. As far as the platform's catalog shows, it has no machine-checked proof in this normalization; McDiarmid's inequality in the non-identically distributed form, the bounded-difference step and the absolute-value Rademacher symmetrization with factor are not on the platform. A Lean proof would give a reusable risk-bound template for any loss dominated by a bounded cost.
The obvious argument — bound for a fixed by Hoeffding's inequality — does not survive the choice of after seeing the data: the deviation must be controlled uniformly over , and is typically infinite. The supremum over is a single random variable, but its expectation is not obviously small, and relating it to the Rademacher complexity requires a ghost sample and a sign-swap symmetry of the product measure. In a formal development, the supremum of an uncountable family is not automatically measurable; the expectations the argument manipulates must be genuine, not lower integrals, which is why the statements carry explicit measurability hypotheses. McDiarmid's inequality itself, for independent but not identically distributed coordinates, is a martingale-difference concentration argument that is not in Mathlib in this form.
S : Fin n → X × Y, its law the product Measure.pi (fun _ => P). "With probability at least , every satisfies …" is encoded by bounding the (outer) measure of by , with .Fin n → Bool, true ) of -valued suprema; is its Lebesgue integral. The goal is stated in , with the real terms embedded by ENNReal.ofReal (all are nonnegative). A real supremum or a Bochner integral would silently return on an unbounded class or a non-integrable integrand, making the bound trivially false or vacuous; this is ruled out by the choice of codomain.[Zero A]).UnderstandingML.representativeness_le_rademacher.Contributions welcome: a proof of McDiarmid's inequality for Measure.pi (reusable well beyond this mission), the ghost-sample symmetrization with the sign-swap invariance of , and the final assembly.
Expander graphs are sparse graphs in which every set of vertices has many neighbours. Families of them with bounded degree and expansion bounded away from zero are a basic tool of theoretical computer science: they are the main component of the sorting network of Ajtai, Komlós and Szemerédi (AKS 1983), the building block of superconcentrators and other graphs with strong connectivity properties, and an ingredient of many later constructions in coding theory, derandomization and complexity.
Expansion is hard to certify. Checking that every set of vertices has many neighbours means looking at exponentially many sets, and computing the exact expansion of a graph is coNP-complete. A spectral quantity, by contrast, is computable in polynomial time. N. Alon's paper Eigenvalues and expanders (Combinatorica 6 (1986) 83–96) proves that for regular bipartite graphs the two notions are equivalent: a graph is a strong expander if and only if the second-smallest eigenvalue of its Laplacian is bounded away from 0, with explicit constants in both directions. This is a discrete counterpart of Cheeger's inequality for Riemannian manifolds.
Timeline.
All graphs are finite and simple. For a graph and a set , is the set of neighbours of ; it may meet .
The Laplacian of is , where is the 0–1 adjacency matrix and the degree of . It is symmetric with eigenvalues , counted with multiplicity, and is its second-smallest eigenvalue. It is positive exactly when is connected.
Let be a -regular bipartite graph with and .
Part (1) of the goal combines Lemmas 3.1 and 2.4; part (2) follows from Lemma 3.3.
The result. Theorem 3.4 makes expansion of regular bipartite graphs checkable in polynomial time up to a constant-factor loss. A random regular bipartite graph can be generated and its expansion certified by computing one eigenvalue. Lemma 2.4 is one of the first discrete Cheeger inequalities. Together with Corollary 2.3 it shows that magnifiers and enlargers are the same graphs up to the constants, and it underlies the later theory of spectral expanders, including the Alon–Boppana bound and Ramanujan graphs.
The formalization. The results are proved in the paper. The work is to formalize the known proofs. That includes Tanner's eigenvalue bound, which the paper only cites, and a max-flow min-cut argument, for which Mathlib has no general theorem. No machine-checked version of Lemma 2.4, Lemma 3.1, Lemma 3.3 or Theorem 3.4 is known to exist. Lemma 2.2 is already stated and proved on the platform as part of the Alon–Milman mission.
The direction "eigenvalue gap implies expansion" is a variational argument on the spectrum of . The converse is the hard one. A first attempt bounds from below by testing the Rayleigh quotient on indicator vectors of sets. That only gives upper bounds on : any one test vector does. A lower bound has to control every vector orthogonal to the constants at once. The paper first reduces to the positive part of an eigenvector (Eq. (2.1)). It then turns the combinatorial expansion of the graph into an analytic inequality for that function, using a network flow whose existence comes from the max-flow min-cut theorem. Step (ii) of the flow conditions printed on p. 87 is false as stated: the arcs of the network absorb part of the flow. The flow argument has to be repaired before it can be formalized.
Lemma 3.1 has its own obstacle: one-sided expansion of inputs must be converted into expansion of arbitrary vertex sets that mix inputs and outputs. This needs the strong form of expansion; for ordinary expanders the lemma is false.
Graphs are SimpleGraph V on a Fintype. A bipartite graph lives on the sum type I ⊕ O, and IsIOBipartite forbids edges inside I and inside O. Cardinalities are Set.ncard. "Maximal degree " is read as G.maxDegree ≤ d; every statement is monotone in or fixes by regularity (G.IsRegularOfDegree d). The condition is written in . All constants are real, and every subtraction and division is taken in .
Reused published items:
AlonMilman.Diameter.lambda1, the second-smallest eigenvalue of G.lapMatrix ℝ, which is by convention on fewer than two vertices.AKSSorting.Core.neighbours.AlonMilman.Diameter.theorem_2_5, which carries Alon–Milman's standing hypotheses that is connected and ; outside them the inequality is trivial.The page omits a few degenerate cases, and the following hypotheses are added for them. Each is necessary, with a counterexample recorded in the item's statement:
Eq. (2.1) is stated in multiplied form, so no quotient by appears.
The closing sentences of Theorem 2.5 and Theorem 3.4 ("Thus … one can prove efficiently …") are not formalized. Read as implications between expanders they reduce to monotonicity in , because ; their content is algorithmic.
Several encodings would trivialize the mission and are excluded:
Contributions are welcome:
Every linear program comes with a second linear program, its dual, whose feasible solutions certify bounds on the optimum of the first. The duality theorem of linear programming says that these certificates are perfect: when both programs are feasible, the best bound equals the optimum. The theorem underlies the analysis of the simplex method, sensitivity analysis and shadow prices in operations research, the minimax theorem for zero-sum games, max-flow/min-cut and König-type min-max theorems in combinatorial optimization, and the primal–dual design of approximation and online algorithms.
The Farkas lemma, a theorem of the alternative for linear systems, contains the essence of duality: a system of linear equations or inequalities either has a (nonnegative) solution, or a single linear combination of its rows proves that it has none. It goes back to Farkas (1902) and Minkowski's work on finitely generated cones; the duality theorem itself is due to von Neumann (1947) and Gale, Kuhn and Tucker (1951).
This mission formalizes Chapter 6 of Matoušek and Gärtner's textbook Understanding and Using Linear Programming (Springer, 2007): the duality theorem in the book's form, weak duality, the Farkas lemma in its algebraic, geometric and three-variant forms, and the lemmas of two self-contained proofs of the Farkas lemma, one analytic (nearest points in finitely generated cones) and one via minimally infeasible systems.
Let be a real matrix with rows and columns, , . Vector inequalities are componentwise. The primal and dual linear programs are
A feasible solution of (P) is an satisfying its constraints; an optimal solution is a feasible with for every feasible . (P) is unbounded if its objective takes arbitrarily large values on feasible solutions. For the minimization (D) the notions are mirrored: an optimal has for all feasible , and (D) is unbounded if takes arbitrarily small values.
For , the convex cone generated by them is ; a primitive cone is one generated by linearly independent vectors. A system of inequalities is minimally infeasible if it has no solution but dropping any one inequality makes it solvable.
For (P) and (D) as above, exactly one of the following occurs:
LinearOptimization.farkas_lemma (Proved) and linked as a reference.Polyhedral.isClosed_conicSpan, Proved); hence it has a point nearest to any .The result. The duality theorem converts optimality into feasibility: a pair of primal and dual feasible solutions with is a short, checkable certificate that both are optimal, and the theorem guarantees such a certificate exists whenever an optimum does. It classifies every primal–dual pair into four behaviours and excludes the other five combinations of feasible-bounded, unbounded and infeasible. Later chapters of the same book rest on it: the minimax theorem for zero-sum games, the integrality of bipartite matching polytopes, the LP rounding for unrelated-machine scheduling, and the Delsarte bound for codes.
Formalizing it. All results here are classical and fully proved in the book; the work is formalization. Mathlib contains a Farkas lemma for proper cones in Hilbert spaces and closedness facts for finitely generated cones, and the platform already has Bertsimas–Tsitsiklis-style duality for a general-form minimization (LinearOptimization.lp_strong_duality) and matrix Farkas lemmas. What is missing is the textbook statement in Matoušek's inequality form (P)/(D), with its four-case exclusive classification, together with the chain of named lemmas that make two different elementary proofs of the Farkas lemma machine-checkable. The analytic chain (6.5.x) and the minimally-infeasible chain (6.6.x) are reusable independently of LP.
Weak duality is a two-line computation. The difficulty is entirely in the reverse direction, that a feasible bounded (P) forces the dual to be feasible with the same value. Any proof must use something beyond linear algebra over : either the termination of the simplex method with an anticycling rule, a topological fact (a finitely generated cone is closed), or an extremal argument (an optimal solution of an auxiliary LP). The naive geometric argument — take the nearest point of the cone to — fails without closedness, and closedness of the cone generated by a set is false for infinitely generated cones (the cone over a disc touching the origin is an open half-plane plus a point), so finiteness has to be used, which is the role of the primitive-cone decomposition. In the four-case theorem itself, the remaining obstacle is attainment: "bounded and feasible" must be upgraded to "an optimum exists" for both programs, which is not a consequence of Farkas-type statements alone.
Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; the book's indices become . The row vector is Aᵀ *ᵥ y, so is 0 ≤ Aᵀ *ᵥ y; scalar products are ⬝ᵥ.sSup/sInf is used, so no junk value of an empty or unbounded supremum enters. "Exactly one of the four cases" is ∃! k : Fin 4, DualityCase A b c k, with the book's case at index ; a plain disjunction would be weaker than the book.EuclideanSpace ℝ (Fin m), so the nearest point of Lemma 6.5.1 is Euclidean and is the inner product. The convex cone generated by is the set of nonnegative combinations (it contains , also for ).IsClosed.exists_infDist_eq_dist) are not separate targets. The Fourier–Motzkin elimination of §6.7 has no numbered result.Many design problems in control, finance and operations research are convex programs with uncertain constraints: a decision must satisfy for a parameter that is not known in advance. Enforcing the constraint for every possible (robust optimization) is often intractable or too conservative, and a chance-constrained formulation needs the distribution of , which in practice is rarely known. The scenario approach replaces the uncertain constraint by the constraints of observed samples and solves the resulting ordinary convex program. The question it answers is how much of the unseen uncertainty the resulting decision still violates.
The answer, the generalization theorem of the scenario approach, is distribution-free: the probability that the scenario solution violates more than a fraction of the uncertainty is bounded by a binomial tail that depends only on and on the number of decision variables. This mission formalizes that theorem as it is presented in Chapters 3 and 5 of Campi and Garatti's textbook Introduction to the Scenario Approach (SIAM/MOS 2018), the first mission of a series on the book.
Timeline. Calafiore and Campi introduced scenario programs and bounded the violation of their solutions through the count of support constraints (Math. Program. 2005; IEEE TAC 2006). Campi and Garatti proved in 2008 that the binomial-tail bound of Theorem 3.7 holds for every convex scenario program under existence and uniqueness of the solution, and that it is attained with equality by fully supported problems (SIAM J. Optim. 2008), which settled the tightness question. The textbook (DOI 10.1137/1.9781611975444) presents the theorem with a complete proof for fully supported problems in the plane.
Fix a cost vector , a domain , a measurable space of uncertainty instances with a probability , and a constraint set for each .
A solution is a feasible point of least cost. With i.i.d. samples its solution is denoted ; it is a random vector, a function of the sample, and is a random variable in .
For and every , under Assumptions 3.4 and 3.6,
The right-hand side is the upper tail of a Beta distribution. The statement leaves , and the constraint family completely unspecified beyond the two assumptions.
Theorem 3.7 is what makes the scenario approach usable as a design method: it certifies the reliability of a decision computed from data without any knowledge of the data-generating distribution, requiring only independence of the samples. Theorems 3.8 and 1.3 are its two most used consequences, an expected-violation bound and an explicit sample size, and later chapters of the book (constraint removal, the FAST algorithm, empirical-cost results) build on the same statement. Equality for fully supported problems shows that the bound cannot be improved for any and .
The theorem is proved in the literature; it has no machine-checked proof. A formalization produces, beyond the result itself, a reusable library of scenario programs, violation probabilities and support constraints on which the rest of the series (constraint removal, nonconvex support sets) can be stated, and it checks the measure-theoretic content that the book deliberately leaves aside ("measurability issues are glossed over throughout", p. 33).
The deterministic part, at most support constraints, is a short consequence of Helly's theorem. The probabilistic part is where the obvious approach fails. A uniform-convergence argument over all (Vapnik–Chervonenkis theory, footnote 11 of the book) gives bounds of the wrong order and can be vacuous, because it ignores that only the solution matters. The sharp bound is an exact statement about the law of , not a union bound, and problems with fewer than support constraints, or with degenerate configurations of constraints, must be shown to be no worse than fully supported ones; the book treats the general case only in the plane and refers to Campi & Garatti 2008 for general . Handling the null sets and the exchangeability of the samples under the product measure is a substantial part of the work.
EuclideanSpace ℝ (Fin d); the cost is inner ℝ c θ. A sample of size is ω : Fin m → Δ with law Measure.pi (fun _ : Fin m => P), and P is a probability measure.(P {δ | θ ∉ Θδ δ}).toReal; probabilities of events over the sample are compared in through ENNReal.ofReal.θstar : (Fin N → Δ) → EuclideanSpace ℝ (Fin d) together with the hypothesis that θstar ω solves the program for every sample; it is never an arbitrary map.θstar is measurable (the book's p. 33 convention); ; .Finset.card over Fin m.A statement in which is any feasible point of the program, or merely a measurable function of the sample, is false and does not count as a formalization of Theorem 3.7; nor does one in which Assumption 3.6 is weakened to almost every sample. Contributions of general infrastructure are welcome: exchangeability arguments for product measures, the binomial–beta identity, and Helly-type counting lemmas are reusable well beyond this mission.
Dantzig–Wolfe decomposition and column generation solve large integer programs by replacing a set of "easy" constraints with a description of its feasible points, and then pricing out the points one at a time. For linear programs this rests on the Minkowski–Weyl representation: every point of a polyhedron is a convex combination of its extreme points plus a nonnegative combination of its extreme rays. For integer programs that representation is not enough. Imposing integrality on the convex multipliers of the extreme points of does not give back the integer program, because an optimal integer point may lie in the interior of .
Lübbecke and Desrosiers, in their survey Selected Topics in Column Generation (Operations Research 53(6), 2005), present discretization (Johnson 1989, Vanderbeck 2000) as the true integer analogue of the decomposition principle. Its basis is their Theorem 1: the integer points of a rational polyhedron are generated by finitely many integer points and finitely many integer rays with integer multipliers. The paper states this result and refers its proof to Nemhauser and Wolsey, Integer and Combinatorial Optimization (1988). It underlies the integer master problem (25) of branch-and-price.
Let be an matrix and an -vector with rational entries. The polyhedron is
and its set of integer points is , the points of whose coordinates are all integers. Because , .
The recession cone of is . An integer ray of is a nonzero vector of in this cone. Extreme rays are not required.
In Lean these are polyhedronP D d, integerPoints D d, recessionConeP D and IsIntegerRay D w in the namespace Lubbecke2005.Discretization, with integer vectors cast to real vectors by castVec.
If , there exist a finite set of integer points and a finite set of integer rays of such that
Since the multipliers are nonnegative integers summing to one over , (24) says that is the union, over , of the translates of the monoid generated by the rays. No bound on or is part of the goal.
If , every point of is a vertex of . In this case convexification and discretization coincide.
The result. Theorem 1 converts an integer program into the integer master program (25) over the multipliers , with one column per generating point and per generating ray. When is bounded the rays disappear, exactly one equals one, and (25) is a linear integer program even for a nonlinear cost . The representation is what makes branching on master variables, and the passage between compact and extensive formulations, well defined in branch-and-price.
Formalizing it. The result is classical (Nemhauser–Wolsey 1988, going back to Giles and Pulleyblank and to Meyer's theorem that the integer hull of a rational polyhedron is a polyhedron). On Prove2Me, the real representation (8) is formalized as LinearOptimization.polyhedron_resolution (Bertsimas–Tsitsiklis Thm 4.15) and the integer hull theorem as LinearOptimization.integer_hull_is_polyhedron (Thm 11.3); both are included as reference items. The convexification counterpart of §3.2, that the Lagrangian dual equals the LP over , is LinearOptimization.lagrangean_dual_eq_lp_over_hull. No machine-checked statement of the integer representation (24), with integer multipliers and integer rays, was found on the platform. The mission produces that statement and, once solved, its proof.
The obvious attempt applies the real representation (8) and rounds. It fails twice. First, the extreme points of need not be integral, and an integer point written as a real combination of vertices and rays has no reason to have integer multipliers. Second, the extreme rays of generate the recession cone over , but the integer points of that cone are not in general nonnegative integer combinations of the (scaled) extreme rays; a generating set of the lattice points of a cone must usually contain non-extreme vectors. The finiteness of is also not automatic: itself is typically infinite, and taking trivializes the statement.
Rationality of the data is essential. For , every integer ray has slope below , so finitely many base points and rays generate only points with for some , while contains for every .
Fin n → ℝ; integer vectors are Fin n → ℤ cast coordinatewise. Both sides of (24) are sets of real vectors.ℚ-valued and cast to ℝ. This is an addition: the paper names no field, and the theorem is false for irrational data (see Difficulty). The cited source, Nemhauser–Wolsey, works with rational data.Fin k and Fin l for existentially chosen ; the finiteness is the content of the theorem. The multiplier vector is written as a pair of ℕ-valued vectors.A formalization with real multipliers would be the resolution theorem (8), already on the platform, and one with or infinite would be trivial; both are excluded by the statement.
Useful infrastructure: lattice points of rational polyhedral cones (Hilbert bases, Gordan's lemma), the integer hull theorem, and the real resolution theorem. A proof of Gordan's lemma for rational cones in this vocabulary would be reusable well beyond this mission. Contributions toward any of these are welcome.
The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is on every metric space with at least three points.
Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is . Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths , , . These exact values are among the few known optimal randomized ratios for server problems.
Timeline:
Fix an integer . The isosceles triangle has three points , , with
A configuration places two labelled servers on points of . A deterministic on-line algorithm assigns to every finite request sequence a configuration, computed from alone and covering the last request; its value on the empty sequence is its initial configuration. Its cost is the total distance its servers move while serving request by request. The off-line optimum from an initial configuration is the least total movement of any schedule that starts at and covers each request in turn, knowing in advance.
A randomized algorithm is a probability distribution on deterministic on-line algorithms; its expected cost is . It is -competitive against an oblivious adversary from if every algorithm in its support starts at and there is a constant such that
The request sequence is fixed in advance and does not react to the algorithm's coin flips.
Write and
In Lean this is NonuniformCompetitive.Isosceles.isoscelesRatio d.
For every and every initial configuration :
The two claims are also milestones of their own (no_better_ratio, ratio_attained).
For free real and real with
one has (lp_lower_bound); and , is nondecreasing from to and makes every constraint an equality (lp_attained).
(ratio_increases_to_e_ratio).
The theorem gives an exact optimal randomized ratio for an infinite family of metric spaces. It shows that the optimal randomized two-server ratio is not a constant: it runs from on the equilateral triangle to as the triangle becomes long and thin, where the problem resembles ski rental. With the deterministic ratio , it quantifies exactly how much randomization gains on these spaces.
The results are proved in the paper; none is formalized on Prove2Me, and no machine-checked proof of them is known. A formal proof would require the paper's phase framework (Theorems 1–3 and the appendix's Theorem 15) for server problems, which this mission does not state separately, and a concrete randomized algorithm as a measurable mixed strategy. Both would be reusable for Theorem 13 (the 3-4-5 triangle) and for other exact ratios on small metric spaces.
The phase LP milestones are finite real arithmetic. The difficulty is the passage between them and the goal. The lower bound must hold for every randomized algorithm, not only phase-based lazy ones: an arbitrary algorithm may condition on the whole history, move non-lazily, and randomize in ways that do not reduce to the probabilities . The paper handles this with Theorem 3, which says that the LP bound of phase-based algorithms bounds the competitive factor of all algorithms; its proof uses an averaging argument over histories that must be made rigorous. The upper bound needs a mixed strategy over infinitely many phases, with measurable costs, an explicit additive constant covering the first partial phase from an arbitrary initial configuration, and an accounting of across phase boundaries.
The model is the platform's published KServer_model and KServer_randomized (reference items): labelled servers Fin 2 → M; a deterministic on-line algorithm as a map from request prefixes to configurations; a randomized algorithm as a probability measure over deterministic algorithms, with the cost of each fixed sequence measurable in the random outcome; expected cost as a lower Lebesgue integral in ; the off-line optimum as a real infimum over schedules from (nonempty and bounded below by ); and IsCompetitiveFrom A C₀ c with a real additive constant.
Committed conventions:
Without the measurability field of a randomized algorithm the lower integral would under-report expected cost and the attainment claim would become easier than the paper's; the published definition includes it. The lower bound is not vacuous: the triangle hypotheses are satisfiable for every .
Welcome contributions: a formal version of the phase framework (Theorems 1–3, 15) for finite metric spaces, reusable across missions III and IV; a measurable construction of phase-based randomized algorithms; and proofs of the LP milestones.
Fictitious play is the oldest model of learning in games: each player repeatedly best-responds to the empirical frequencies of the opponents' past play. Stochastic fictitious play adds random payoff disturbances before each choice, so that players choose smoothed ("perturbed") best responses. It is a standard model in economics and in the study of learning in games (Fudenberg and Levine, 1998), and its long-run behavior is described through a deterministic mean dynamic, the perturbed best response dynamic, using stochastic approximation theory (Benaïm and Hirsch, 1999).
Supermodular games model strategic complementarities: the gain from moving to a higher strategy increases when opponents move to higher strategies. They arise in coordination, oligopoly and macroeconomic models (Milgrom and Roberts, 1990; Vives, 1990). Hofbauer and Sandholm (Econometrica 2002) show that in such games stochastic fictitious play converges almost surely whenever its mean dynamic has a unique rest point. This mission formalizes that result and the chain of lemmas behind it (Section 5 and the Appendix of the paper).
Timeline. Benaïm and Hirsch (1999) observed that supermodular games with exactly two strategies per player yield strongly monotone perturbed best response dynamics. Hofbauer and Sandholm (2002) extended this to any number of strategies by introducing stochastic dominance coordinates, and proved Theorem 6.1(iv). Benaïm (2000) supplied the low-dimensional convergence theorem used for the dimension ≤ 2 clause.
A player normal form game gives player an ordered finite strategy set and a utility on pure profiles. is the set of mixed profiles, and player 's payoff vector is .
The game is strictly supermodular if for all distinct players and all profiles with and , the difference is strictly increasing in .
Each player has a shock density on , strictly positive, whose choice function is continuously differentiable. The perturbed best response is , and the perturbed best response dynamic is
is its set of rest points in and its chain recurrent set.
In standard stochastic fictitious play the shocks have densities and are independent over time and across players. From an arbitrary initial pure profile , each player at time plays the pure strategy maximizing , where is the vector of empirical frequencies.
The stochastic dominance coordinates are , the mass on strategies above ; means each stochastically dominates . In these coordinates (P) becomes a dynamic (T) on .
For a strictly supermodular game with players and shock densities as above, if then
on every probability space, for every independent shock family with the given densities and every initial profile.
The result gives global almost-sure convergence of a stochastic learning process in a broad class of games with many strategies, where earlier results needed two strategies per player or specific payoff structures. It also shows which properties of the choice function matter: only eqs. (17)–(18), not the symmetry of its derivative used for potential and zero-sum games.
The paper's proof is complete but relies on outside results: stochastic approximation (Benaïm–Hirsch 1999, Benaïm 1999), monotone dynamical systems (Smith 1995), and the inclusion of the chain recurrent set in the global attractor (Robinson 1995). None of these, nor the Hofbauer–Sandholm theorem itself, is formalized in any proof assistant as far as known. The mission produces a machine-checked version of the theorem and of the Section 5 monotonicity theory.
The monotonicity lemmas are finite-dimensional calculus and summation by parts. The substantial steps are elsewhere. Strong monotonicity of a cooperative irreducible system (Corollary 5.5(i)) is a theorem of monotone dynamical systems that Mathlib does not have, and it must hold on the closed, non-open state space . The step from the ODE to the random process needs the stochastic approximation theorem: the empirical frequencies are an asymptotic pseudotrajectory of (P), and their limit set is almost surely internally chain transitive. Knowing that is globally asymptotically stable for (P) does not by itself give almost-sure convergence of . The limit set of the random process must be related to the chain recurrent set of (P), which is where Corollary 5.5(ii) enters.
Players are Fin p, strategies Fin (n α) (0-based, same order as the paper), with every . Mixed profiles live in the ambient space with the sup norm. The fields of (P) and (T) are defined on the whole ambient space, so partial derivatives are ordinary Fréchet derivatives. Densities are -valued. Solutions are forward solutions staying in the state space. The chain recurrent set quantifies over solutions, which are unique here because the fields are . The process is defined pathwise from the shocks, with ties in the argmax broken by the smallest index (a null event). Densities may differ across players.
A statement about the ODE (P), or about a single noise law such as logit, would be a different and much weaker theorem. The goal is about the random process , on every probability space carrying independent shocks with the given densities. Irreducibility and strong monotonicity additionally assume that two distinct players each have at least two strategies; when one player owns every stochastic dominance coordinate and has at least two of them, supermodularity holds vacuously while irreducibility fails.
A complete development needs: random utility choice functions and their derivatives; monotone and cooperative ODE theory on convex sets; the chain recurrent set and the global attractor; stochastic approximation for processes with step size . The last three are reusable well beyond this mission. Contributions to any milestone, and general-purpose lemmas on cooperative systems or stochastic approximation, are welcome.
Existence theory for elliptic, parabolic and nonlinear PDEs mostly runs through one argument: build approximate solutions, bound them in a Sobolev norm, extract a convergent subsequence, and pass to the limit. The extraction step needs a compact embedding: a bound on derivatives must buy convergence of the functions themselves in a weaker norm. On a bounded domain this is the Rellich–Kondrachov theorem. It is what makes the resolvent of the Dirichlet Laplacian compact, and so gives the Fredholm alternative and the discrete spectrum of elliptic operators on bounded domains. The companion topics of the same section, extension and trace, are how Sobolev functions are moved between a domain and all of space, and how they are given boundary values.
This mission follows Chapter 3 (§3.9–3.10) and Theorem 1.15 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014).
Timeline. Rellich proved the compactness of on bounded domains in 1930. Kondrachov extended it to and exponents below the Sobolev exponent in 1945. The compactness criterion used in the notes goes back to Kolmogorov (1931) and M. Riesz (1933); a modern account with a history is Hanche-Olsen and Holden 2010. Gagliardo characterized the traces of in 1957.
Throughout, carries Lebesgue measure, and functions are real-valued. For an open set , a test function is smooth with compact support inside . A locally integrable is the weak derivative of a locally integrable if for every test function . Here is a multi-index of order .
For and , the Sobolev space consists of the whose weak derivatives , , exist and lie in . For its norm is
and for it is the maximum of the essential suprema. The space is the closure of in this norm. For the Sobolev conjugate is .
The upper half-space is , with closure and boundary . The space consists of the functions that are smooth up to the boundary and vanish outside a compact set. Unlike , they need not vanish on .
A subset of a metric space is precompact if its closure is compact. is the space of continuous functions vanishing at infinity, with the sup norm.
In Lean the weak derivative is HasWeakDeriv (with weakDeriv and weakGradNorm) in the series' shared namespace HunterPDE.Shared; the other objects are MemW k p Ω f, sobolevNorm k p Ω f, MemW0 k p Ω f, sobolevConjugate, upperHalfSpace m, IsSmoothCompactClosedHalfSpace and boundaryPoint, in the namespace HunterPDE.Compactness.
Let be a bounded open set in , and . If satisfies for all , then
The goal is stated qualitatively (precompactness), with no constants, so it does not depend on any particular form of the Sobolev inequality.
The result itself. Rellich–Kondrachov is the source of compactness in the theory of elliptic equations. With it, the solution operator of a coercive elliptic problem on a bounded domain is compact. That yields the Fredholm alternative, the discreteness of the Dirichlet spectrum, and existence results for semilinear problems via compactness and fixed-point arguments. The trace theorem makes the boundary condition " on " meaningful for Sobolev functions, and identifies as the space in which Dirichlet problems are posed. The extension theorem transfers whole-space results to domains. Theorem 3.48 gives the uniform-norm counterpart above the critical exponent.
Formalizing it. All results here are classical and proved. The notes prove 3.45, 3.48 and the forward direction of 3.44. They describe 3.41 and 3.42 in a sentence each, and cite 1.15 without proof. Mathlib has the Lebesgue spaces Lp, Arzelà–Ascoli for bounded continuous functions, and mollification. It has no weak derivatives, no Sobolev spaces on domains, no trace, no extension operators and no Kolmogorov–Riesz criterion. A complete development would supply the first machine-checked versions of these in the notes' form, and a formal compactness theorem usable by the elliptic chapters of the same series.
The obvious route to the goal is: approximate by test functions, extend by zero, and verify the three Kolmogorov–Riesz conditions. The first two follow from the Sobolev inequality and the boundedness of . The hard parts are elsewhere. First, the Kolmogorov–Riesz criterion is not in Mathlib, and its "if" direction needs a mollification and total-boundedness argument in . Second, the -equicontinuity for above needs an interpolation between an translation estimate and the critical Sobolev embedding into , so the Gagliardo–Nirenberg–Sobolev inequality must be available for , not only for smooth compactly supported functions. Third, weak derivatives are defined by integration against test functions, and every density step has to be carried through that definition. The exponent restriction is sharp (Example 3.47 in the notes), so no argument that ignores it can succeed.
EuclideanSpace ℝ (Fin n) with volume. Open sets are Ω : Set _ with IsOpen Ω, and bounded means Bornology.IsBounded Ω. Coordinates are 0-based (i : Fin n), and multi-indices are α : Fin n → ℕ.ℝⁿ → ℝ, and only their values on the relevant set matter. weakDeriv is a chosen representative, used only where a weak derivative is assumed to exist. sobolevNorm takes values in ℝ≥0∞.sobolevNorm 1 p Ω.Ω.indicator f). The conclusion asserts both that each extension lies in and that the set of their classes in Mathlib's Lp ℝ q volume has compact closure. The hypothesis rules out .Fin.last m. The boundary is via . Extension and trace operators are maps on functions that are linear up to a.e. equality on .In best arm identification with fixed confidence, a learner samples unknown distributions (arms) sequentially and must, as early as possible, name the arm with the largest mean, while being wrong with probability at most a prescribed risk . The problem models adaptive A/B/n testing, clinical and simulation-based selection among alternatives, and the "ranking and selection" problem of operations research and simulation optimization. The quantity of interest is the sample complexity , the expected number of samples a strategy takes before stopping.
Timeline of the question this mission formalizes:
A canonical one-parameter exponential family is a family of laws , , on with density with respect to a reference measure ; is twice differentiable and strictly convex, and has mean . Bernoulli, Poisson and Gaussian laws with known variance are examples. The divergence is the Kullback–Leibler divergence between the members with means and .
A bandit model assigns a member of the family to each arm. The class consists of models with a unique optimal arm . At each round the learner picks an arm as a function of past observations, observes a reward drawn from that arm's law, and at a stopping time recommends an arm. is the number of draws of arm in the first rounds and its empirical mean.
With and the probability simplex, the characteristic time is
and the maximizer are the optimal proportions of arm draws.
Track-and-Stop combines two ingredients:
For and , Chernoff's stopping rule with combined with C-Tracking or D-Tracking satisfies
for every .
Theorem 1 of the same paper shows for every -PAC strategy, and . Theorem 14 with therefore shows that the lower bound is attained: is the exact asymptotic sample complexity of best arm identification in exponential family models, and Track-and-Stop is asymptotically optimal.
The result is proved in the paper. What is not available is a machine-checked proof for exponential families. The platform already holds a Lean development of the Gaussian case following Lattimore and Szepesvári, Bandit Algorithms, Ch. 33, stated for one existentially chosen policy with a different threshold. This mission asks for the universal statement: every run of either tracking rule, for every exponential family, with the paper's thresholds. The tracking lemmas (Lemmas 15, 7, 8) are deterministic combinatorics and reusable by any tracking-based algorithm.
The obvious argument plugs the almost-sure behaviour of Proposition 13 into an expectation. That step fails: almost-sure convergence of does not control , because on the rare events where the empirical means are far from the stopping time may be very large. Theorem 14 needs a quantitative concentration of on events whose complements have summable probability, which in turn relies on the forced exploration guaranteed by the lower bounds on (the concentration step of App. D, Lemmas 19–20).
A second obstacle is the regularity of : the tracking lemmas only transfer convergence of to convergence of through the continuity of on , proved from the characterization of in §2.2 (Proposition 6). The GLR statistic also needs its closed form (7) near , which requires the empirical means to lie in the interior of the mean space.
BanditPolicy, BanditTrajectory, TrackAndStop). uses Kullback–Leibler divergences of the arm laws over the class and takes values in . Trajectory coordinate is round . An arm never drawn has empirical mean .Best arm identification with fixed confidence is the pure-exploration counterpart of the multi-armed bandit problem. A learner faces unknown reward distributions ("arms"), samples them sequentially, and must stop and name the arm with the largest mean, being wrong with probability at most a prescribed . The question is how many samples this requires. It arises in adaptive A/B testing, in the selection of the best of several simulated systems (ranking and selection in simulation optimization), and in clinical trials that must declare the best treatment with a guaranteed error rate.
Lower bounds for this problem were first stated in terms of the gaps between means (Mannor and Tsitsiklis, 2004). Kaufmann, Cappé and Garivier (2016) replaced ad hoc changes of measure by a single "transportation" lemma relating expected sample counts, Kullback–Leibler divergences and the error probability. Garivier and Kaufmann (COLT 2016, arXiv:1602.04589v2) combine this lemma over all alternative models at once, in the spirit of Graves and Lai (1997), and obtain a lower bound whose constant is exactly matched, as , by their Track-and-Stop strategy. This mission formalizes that lower bound (Theorem 1 of the paper, p. 3).
A canonical one-parameter exponential family is given by a reference measure on , an open interval and a function , twice continuously differentiable on with , such that the laws with density with respect to are probability measures for . The mean of is . Bernoulli laws and Gaussian laws of known variance are examples.
A bandit model is a vector ; arm returns i.i.d. rewards with law and mean . Arm is the unique optimal arm if for every . Let be any set of bandit models of the family each having a unique optimal arm, and put .
A strategy consists of a sampling rule (the arm drawn at round depends, possibly with extra randomization, on the first observations), a stopping time of the natural filtration , and an -measurable decision . It is -PAC on if for every , and . is the number of draws of arm among the first rounds.
Write for the divergence between two arm laws, , and for the probability simplex on the arms. The characteristic time is defined by eq. (1):
For , every -PAC strategy on and every ,
The statement fixes no constant beyond those of the paper, and it holds for every , not only in the limit.
For every with ,
This is Lemma 1 of Kaufmann et al. (2016), which the paper quotes without proof; Theorem 1 follows from it for every alternative simultaneously.
Theorem 1 identifies as the exact problem-dependent complexity of fixed-confidence best arm identification: since , it gives , and the paper's Track-and-Stop strategy attains this rate (the subject of mission IV of this series). The bound also explains which proportions of draws an optimal strategy must use: the maximizer of eq. (1) (mission II).
Both results are proved in the literature. Neither is formalized in the paper's generality. The platform holds the textbook form of Lattimore and Szepesvári (Theorem 33.5), which is stated for an arbitrary class with the weaker constant ; for , , so Theorem 1 is strictly stronger. A formal proof here yields the transportation lemma for exponential families on the platform's infinite-horizon bandit model, which later missions (II–IV, and any lower bound by change of measure) can reuse.
The obvious proof applies the finite-horizon divergence decomposition at a deterministic horizon . That fails here: is random and unbounded, the decision is -measurable, and the relevant divergence is between the laws of the stopped observations. The step from a fixed horizon to a stopping time, together with the data-processing inequality that turns the error guarantees under two models into , is the central difficulty. A second, smaller difficulty is to identify the paper's divergence and its means with the measure-theoretic KL divergence and mean of the arm laws of the exponential family.
Lean namespace OptimalBAI.LowerBound. The bandit protocol is the platform's (BanditAlgorithm.BanditPolicy, banditTrajMeasure, IsBanditStoppingTime, IsSoundBAI, baiComplexity); is the platform's bernoulliRelativeEntropy and is trajPullCount. Conventions:
Fin K, 0-based (the paper's arm is index ); trajectory coordinate is round ;A statement with in place of , or restricted to Gaussian arms, is the platform's existing textbook theorem and does not count as this mission's goal; nor does any version that drops the almost-sure stopping clause or truncates or to real numbers.
Needed infrastructure: the transportation lemma at a stopping time (data processing for KL through an -measurable event, Wald-type identity for the stopped log-likelihood ratio), the identities "mean of " and "KL of two family members ", and . All are reusable beyond this mission. Contributions of any of these lemmas, of eq. (2) alone, or of the Gaussian and Bernoulli special cases as stepping stones are welcome.
Graphs are the most basic combinatorial model of pairwise relations: road networks, frequency interference between radio stations, schedules, circuit layouts. Chapter 5 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) introduces the vocabulary of graph theory and proves its first structural theorems: when a graph can be traversed edge by edge (Euler, 1736), when it can be toured vertex by vertex (Dirac, 1952), when it can be colored with two colors, and how far the chromatic number can drift from the size of the largest clique.
Hamiltonicity is the vertex analogue of Euler's edge-traversal problem and behaves very differently: Euler's problem has a simple parity characterization, while deciding whether a graph has a hamiltonian cycle is NP-complete (Karp, 1972). Sufficient conditions are therefore the main tool, and the minimum-degree condition of Dirac (1952) is the first and most cited of them; Ore's condition (1960) and the Bondy–Chvátal closure (1976) refine it.
A graph consists of a finite vertex set and a set of 2-element subsets of , the edges; means and are adjacent. The degree is the number of neighbours of . The mission uses Mathlib's SimpleGraph V with [Fintype V]; "a graph on vertices" means Fintype.card V = n.
AppliedComb.Graphs.IsHamiltonian).IsEulerian).IsIntervalGraph).In the book's order:
The book's proof of Theorem 5.18 uses only the pigeonhole principle, so none of these results lies on its path. The milestones are the chapter's other theorems about the same objects (cycles, degrees, colorings), and they share the goal's definitions. Cayley's formula (Theorem 5.39, labelled trees on vertices) is already on the platform as GYGraphTheory.cayley_tree_formula and is included as a reference item.
Dirac's theorem is sharp: the complete bipartite graph has minimum degree and no hamiltonian cycle. It is the starting point for the theory of degree conditions for hamiltonicity (Ore, Pósa, Chvátal) and for its extremal and random-graph analogues. Euler's theorem gives linear-time recognition of eulerian graphs; Theorem 5.21 characterizes bipartite graphs; Proposition 5.25 shows that local sparsity (no triangles) does not bound the chromatic number; Theorem 5.28 is the first step towards perfect graphs.
All of these results have been proved for a long time. What is missing is their formalization. Mathlib provides SimpleGraph, chromaticNumber, cliqueNum, degree-sum identities, and definitions of eulerian and hamiltonian walks. It contains no Dirac theorem, no converse of the eulerian degree condition, and no interval-graph theory. On the platform, FamousTheorems.two_colorable_iff_no_odd_cycle_6b is stated with odd closed walks rather than odd cycles, and triangle_free_chromatic_number asserts only rather than with exactly.
For Dirac's theorem the obvious approach, induction on (deleting a vertex), fails: deleting a vertex lowers degrees, and the hypothesis is not inherited by the smaller graph. The degree condition is global, and so is the argument that uses it. In Lean the argument also has to reverse and splice vertex sequences while keeping distinctness and every adjacency along the way. The sufficiency half of Euler's theorem has to construct a circuit that uses every edge exactly once, not just show that one exists up to parity. In Theorem 5.21 the obstruction is a cycle with distinct vertices; producing one from a failed 2-coloring takes more work than producing an odd closed walk. Proposition 5.25 needs a concrete infinite family of graphs and exact computation of both invariants. The upper bound is easy, but the lower bound is not.
SimpleGraph V on a Fintype V. The number of vertices is always Fintype.card V, never a free parameter; in Theorem 5.18 the ceiling is (n + 1) / 2 in , with Fintype.card V = n.Walk.IsHamiltonianCycle, which needs at least three vertices: under that notion Theorem 5.18 would be false for . The goal assumes nonempty, as the book's proof does ( positive). Degenerate readings are ruled out: a predicate satisfied by a cycle through only some vertices, or a statement in which is not the number of vertices, would make the goal vacuous or false, and neither is used here.chromaticNumber (-valued) and is cliqueNum; on finite graphs both agree with the book's definitions (pp. 81, 84).Second-order elliptic equations in divergence form, such as , model steady diffusion, electrostatics in inhomogeneous media and linear elasticity. They are also the stationary part of every parabolic and hyperbolic problem studied later in the same notes. When the coefficients are only bounded and measurable, classical solutions need not exist. The modern theory replaces them by weak solutions in the Sobolev space and settles existence, uniqueness and solvability by Hilbert-space methods. This mission formalizes that theory as presented in Chapter 4 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014). The chapter follows the standard development of Evans, Partial Differential Equations, Chapter 6, and of Gilbarg–Trudinger, Chapter 8.
Timeline. Riesz (1907) and Fréchet represented bounded functionals on Hilbert spaces. Fredholm (1903) proved the alternative for integral equations of the second kind, and Riesz (1918) extended it to compact operators. Lax and Milgram (1954) removed the symmetry assumption from the Riesz approach, and Gårding (1953) proved the coercivity estimate for elliptic forms. Together these give the existence and Fredholm theory for the Dirichlet problem stated here.
Let be open. A test function is a smooth with compact support in . The space is the closure of the test functions in the norm ; each element carries a function and a weak gradient , both square-integrable. is the space of bounded linear functionals on , and acts on it by .
Given coefficients with , the operator is
It is uniformly elliptic if for some , almost every and every . Its bilinear form on is
and the formal adjoint has the form . For , is a weak solution of with on if and for all . The resolvent maps to that solution.
A bounded operator on a Hilbert space is Fredholm if its kernel is finite-dimensional and its range is closed with finite-dimensional orthogonal complement. Its index is .
For bounded, uniformly elliptic and , exactly one of the following holds:
with non-unique solutions in case (2). Every kernel and equation is meant in the weak sense on .
The Fredholm alternative is the complete linear solvability theory of the Dirichlet problem for general elliptic operators on bounded domains. Uniqueness for the homogeneous problem is equivalent to existence for all data. When uniqueness fails, the obstruction is a finite set of orthogonality conditions given by the adjoint problem. This feeds directly into the spectral theory of Theorem 4.25, into eigenfunction expansions, and into the existence theory for parabolic and hyperbolic equations (Galerkin approximation in later chapters). Nonlinear elliptic problems are routinely reduced to it through linearization and the implicit function theorem.
Mathlib has Lax–Milgram for continuous coercive forms, compact operators, the Riesz representation theorem and the spectral theorem for compact self-adjoint operators. It does not have Sobolev spaces with zero boundary values as used here, elliptic bilinear forms, Fredholm operators or their index. As far as a search of the platform shows, none of these results has a machine-checked statement for elliptic operators with coefficients. The mission would give formal statements, and eventually proofs, of textbook results that are fully proved on paper.
The abstract functional analysis is close to the library. The difficulty lies in connecting it to the PDE objects. Gårding's inequality needs pointwise uniform ellipticity turned into an integral bound on the weak gradient, with the non-symmetric first-order term controlled explicitly enough to reach the stated . Compactness of the resolvent needs the Rellich–Kondrachov theorem: embeds compactly in for bounded , which is not in Mathlib in this form. The goal then relates the weak problem on to operator statements on in both directions, including the solution spaces and the adjoint's kernel. A proof that argues only on , without tracking that the solutions lie in and satisfy the weak identity for every test function, does not reach the stated result.
EuclideanSpace ℝ (Fin n) with Lebesgue measure. Coordinates are 0-based.H10 n Ω) is modelled by jets. It is the closure, in , of the pairs for smooth compactly supported with support in . Its norm is exactly the standard norm, and it is a Hilbert space. is StrongDual ℝ (H10 n Ω).Coeffs n. Admissible is membership plus a.e. symmetry. Uniform ellipticity carries .Lp ℝ 2 on .Module.finrank and is only used for Fredholm operators.finrank equality between two infinite-dimensional spaces (both in Lean) cannot stand in for the book's claim.Needed infrastructure, reusable beyond this mission: the jet model of and its Poincaré inequality, Gårding-type estimates, a Rellich–Kondrachov compactness theorem for , and Fredholm operators with index on Hilbert spaces. Contributions of any of these as separate lemmas are welcome.
Formalize , the current record from Dupont, Eisenberger, Kozlovskii, Mehrabian, Ruiz, See, Zhou, Alman, Vassilevska Williams and Balog (arXiv:2608.16884, August 2026).
The paper applies the combination-loss laser method of Alman et al. (arXiv:2404.16349), formalized here as the entry, to . That is level instead of 3, with an exact rational certificate of about parameters found by gradient-based optimization and AlphaEvolve. The authors state that the solution and verification code are being prepared for release.
The stochastic multi-armed bandit is the basic model of sequential decision making under uncertainty: a learner repeatedly chooses one of actions, observes a noisy reward for the chosen action only, and must balance exploring poorly known actions against exploiting the one that currently looks best. It underlies adaptive clinical trials, online advertising, recommendation, dynamic pricing and many simulation-optimization procedures in operations research.
The standard algorithm is UCB (Auer, Cesa-Bianchi and Fischer, 2002, doi:10.1023/A:1013689704352), which plays the arm with the largest upper confidence bound on its mean. Its confidence widths grow with the current time (or with a horizon fixed in advance), and its guarantee is on the expected regret, which grows like . Lai and Robbins (1985, doi:10.1016/0196-8858(85)90002-8) showed that logarithmic growth of the expected regret cannot be avoided by a consistent algorithm.
Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) proved a self-normalized concentration inequality for vector-valued martingales that holds uniformly over time. Section 6 of their paper applies it to the -armed bandit. The resulting confidence intervals depend on neither the horizon nor the current time. The UCB variant built on them, UCB(), has pseudo-regret bounded by a constant, independent of the horizon, on a single event of probability at least . This mission formalizes that section.
There are arms with unknown means . Write for the best mean and for the gap of arm .
Randomness lives on a probability space with a filtration . In round the learner plays an arm that is -measurable and receives the reward . The noise is -measurable and conditionally 1-sub-Gaussian:
The noise need not be independent or identically distributed across rounds, and the rewards need not be bounded.
After rounds, is the number of plays of arm and is the average reward received from it. For a confidence level the confidence width is
with when . UCB() plays, in round , an arm that maximizes ; in particular every arm is played once before any comparison is made. The pseudo-regret after rounds is
This is the linear bandit of the paper with the standard basis of as decision set and .
For every , with probability at least , for all simultaneously,
The right-hand side depends only on the gaps, and .
For any adapted choice of arms (not only UCB()) and every , with probability at least ,
The result. Theorem 7 shows that, once a confidence level is fixed, a UCB-type algorithm can stop paying for exploration after finitely many rounds: with probability the total regret over an infinite horizon is bounded. The paper notes that this does not contradict the Lai–Robbins lower bound, which concerns expected regret; on the failure event of probability the regret may grow linearly. Lemma 6 is the practical content behind this: anytime-valid confidence intervals for adaptively sampled means under martingale noise, usable for stopping rules, best-arm identification and any sequential procedure that inspects its estimates at data-dependent times.
Formalizing it. Both results are proved in the paper's appendices (F and G). No machine-checked proof of either is known to exist. The platform already has the self-normalized martingale bound for and unit sub-Gaussian noise (BanditAlgorithm.self_normalized_martingale_bound, listed here as a reference item), and UCB bounds with horizon-dependent widths and in-expectation or pathwise conclusions. Neither is Theorem 7. The mission produces a formal account of time-uniform confidence intervals for adaptively sampled arm means, and of a regret bound that is uniform in the horizon.
Two points separate this from textbook UCB analyses. First, the number of samples of an arm is itself random and depends on past noise, so a fixed-sample concentration inequality with a union bound over times does not give widths that are free of : a union bound over all costs a factor that diverges. The time-uniform event must come from a maximal (self-normalized) inequality applied to the martingale . Second, the regret statement is uniform in with constants depending on the gaps; converting a condition of the form "" into an explicit bound on requires solving an inequality in which appears both polynomially and inside a logarithm, and the explicit constants and must come out of that step.
The Lean development lives in the namespace ImprovedLinBandits.UCBDelta.
Fin d with 0 < d in the goal; means are μ : Fin d → ℝ, is ⨆ i, μ i (the maximum over a nonempty finite type).t + 1 for t : ℕ: the arm I (t + 1) is ℱ t-measurable, the noise η (t + 1) is ℱ (t + 1)-measurable and satisfies Mathlib's HasCondSubgaussianMGF (ℱ t) … (η (t + 1)) 1 P. Values at index are unused.A trivializing formalization is ruled out: the confidence event is not assumed as a hypothesis of Theorem 7, the i.i.d. bandit model is not substituted for the martingale noise model, and no bound on the means or rewards is imposed.
Useful infrastructure for solvers: the self-normalized bound of Theorem 1 in the scalar case (, , , ), a union bound over arms, and elementary inequalities inverting . Lemmas about pull counts and empirical means under adaptive sampling are reusable beyond this mission and are welcome as contributions.
Nonlinear programming algorithms are routinely advertised as finding a local minimum. Most of them only certify first-order conditions (a KKT point), and the natural next question is whether a given feasible point is in fact a local minimum. For smooth problems where the Hessian is nonsingular this is a second-order test, but in the degenerate case the test itself becomes a combinatorial question about a quadratic form restricted to a cone.
K. G. Murty and S. N. Kabadi (Math. Programming 39 (1987) 117–129) showed that this question is intractable already in its simplest instance: deciding whether is a local minimum of a quadratic form on the nonnegative orthant is NP-complete, and so is deciding whether a square integer matrix is copositive. The paper is the standard reference for the hardness of copositivity testing, which matters for copositive programming, for second-order optimality checks in constrained optimization, and for the complexity of local search in nonconvex optimization.
Let be a real square matrix of order and . The matrix is copositive if for every (coordinatewise). The paper considers the quadratic program
and the following questions, each phrased so that "yes" is the interesting answer:
The source problem is subset sum (Problem 5): given positive integers , is there with ? Let be the total number of digits in the data. The paper fixes an integer and a rational with , and defines functions of nonnegative variables :
, a homogeneous quadratic that agrees with on the set
and . The function is a quadratic form in ; the symmetric matrix , with entries computed explicitly from , is the output of the reduction.
For positive integer data and as above, with the matrix of , the following are equivalent:
This is the mathematical content of Theorems 1–3 and §4: a polynomially computable map from subset sum instances to matrices under which every one of these questions has the answer of the subset sum instance.
The result. The equivalence shows that checking local optimality of a feasible point, checking boundedness of a quadratic objective on a cone, and checking copositivity are all at least as hard as subset sum, hence NP-hard. Through (15) the same holds for local minimality and boundedness of a quartic polynomial with no constraints at all. These facts are the standard justification for why nonconvex solvers settle for KKT points, and the copositivity part underlies the hardness of copositive programming.
The formalization. The paper's claims are proved, and have been cited for decades, but the proof as printed is a sketch: several steps are stated as "clearly" or "it can be verified", and one step of the proof of Theorem 1 (p. 125) is false as written. The inequality for fails for slightly above , and the pointwise implication " on " has an explicit counterexample. The equivalence of Problems 6 and 7 itself survives numerical checks. A machine-checked proof of the goal settles the correctness of the reduction with the paper's own constants. No machine-checked proof of these statements exists on the platform.
The combinatorial direction (a subset sum solution gives a point with ) is a computation. The converse direction carries the content, in two places.
First, passing from to trades the linear penalty for a quadratic one. This is harmless on the box but not for , where is negative. The printed argument handles this coordinate by coordinate and is wrong there; a correct argument has to show that no point of with exists unless a point with does, which requires a global use of the size of .
Second, passing from to requires a quantitative gap: if on then with of only polynomially many bits. Lemma 2 provides such a gap for the unit box and integer matrices, but is not the box and has rational coefficients, so the lemma does not apply verbatim.
The remaining equivalences (Problems 1, 2, 3, 4, 11, 12 for a fixed matrix) follow from homogeneity of the quadratic form and the substitution , and are routine.
The data are natural numbers and is rational; all are cast to in and . The index is Fin n, and the variables of are indexed by Fin n ⊕ Fin n with Sum.elim y s. Standing hypotheses: and (the paper's "all positive integers"); in ; and in . The size counts decimal digits. Problem 1 is local minimality relative to the orthant, Problem 11 is unconstrained local minimality, both in the Euclidean topology. Lemma 2 is stated for integer symmetric (as §4 of the paper says, "as before … symmetric"), with Schrijver's encoding size, since the paper does not define "the size of "; the "optimum is or " is stated as a disjunction without an infimum. The milestones on over assume , which the paper assumes tacitly; the goal needs no such hypothesis.
Not formalized: membership in NP (Lemma 1), the polynomial-time computability of and its encoding size, the NP-completeness of subset sum (cited by the paper from Garey–Johnson), Theorem 4, and any of the words "NP-complete" or "NP-hard". The platform's complexity layer (Turing machines over bitstrings) has no subset sum problem and no encoding of rational matrices. The matrix has rational entries; a positive integer multiple of it is the integer matrix of Theorem 3, has the same answer to every question, and the rescaling is not formalized. The §3 standing assumption "D is not PSD" is not imposed; the constructed matrix can be PSD and the equivalence holds regardless.
The goal is about the explicit matrix , whose entries are given in the definitions; it is not about "some matrix whose quadratic form is ", and the constants and are the paper's explicit bounds, not "sufficiently large" or "for some ". A formalization that quantifies existentially over the matrix or the precision would be trivially true and is ruled out.
Contributions welcome: proofs of the matrix identity and the homogeneity arguments (milestones 6–9), a proof of Lemma 2 (which needs a Cramer/Hadamard bound on basic solutions of the linear complementarity system (9)), and a correct proof of the step. The copositivity definitions and milestones 7–9 are reusable for any later work on copositive programming.
Value-at-Risk (VaR) is the standard regulatory measure of downside risk of a portfolio: the loss level that is exceeded only with a prescribed small probability . Computing it requires the full distribution of asset returns, which is rarely known. In practice one estimates a mean vector and a covariance matrix and then assumes a Gaussian distribution, which understates the probability of large losses when returns are heavy-tailed or skewed.
El Ghaoui, Oks and Oustry (Oper. Res. 51(4), 2003) replace the distributional assumption by a worst case: the VaR is computed against every distribution consistent with the known moments. For known mean and covariance they obtain an exact closed form and several semidefinite (SDP) representations of this worst-case VaR. The SDP forms are what make the approach extend to moment uncertainty (moments only known to lie in a set, §2.2 of the paper) and to robust portfolio optimization. The equivalence between the probabilistic statement and the closed form is also a multivariate one-sided Chebyshev bound, related to Bertsimas and Popescu (SIAM J. Optim. 15(3), 2005; working paper 2000).
There are assets. Their returns over one period form a random vector , and a portfolio earns . The paper restricts to an admissible set that does not contain ; only is used.
The distribution of is unknown except for its mean and covariance matrix , with (positive definite). Let be the set of all probability distributions on with these two moments. For a loss level , the loss set is . The worst-case VaR at level is (Eq. (4))
Further notation: (Eq. (8)); for symmetric matrices, means is positive semidefinite and . The second-moment matrix is (Eq. (6))
For , , and , the following five propositions are equivalent:
In particular
The result. Proposition 2 turns the worst-case VaR into a second-order cone function of , so minimizing it over a polytope of portfolios is a second-order cone program (Eq. (12)). The SDP forms 3 and 5 are the basis of the paper's §2.2–§3: they extend, with the moments only known to lie in a convex set, to a single SDP whose value is the worst-case VaR over that set. Proposition 4 gives a deterministic reading: the worst-case VaR is the largest loss when the return vector is only known to lie in an ellipsoid, which connects distributional robustness to robust optimization with ellipsoidal uncertainty.
Formalizing it. The result is proved in the paper, with two imported steps: strong duality for the moment problem (Smith 1995; Bonnans and Shapiro 2000) and a Slater-type strong duality for the one-constraint quadratic condition. No machine-checked version is known. A formal proof would supply these steps with explicit hypotheses and would produce a Lean statement of the multivariate one-sided Chebyshev (Cantelli) bound with tightness over the full moment class.
The matrix equivalences (2 ⇔ 4 ⇔ 5 and 2 ⇔ 3) are Schur complements and finite-dimensional SDP duality. The difficulty is Proposition 1. The upper bound (Cantelli's inequality for ) handles one direction, but the converse requires tightness: for every below the closed form, a distribution on with exactly the prescribed mean and full covariance matrix that puts probability more than on the loss set. A scalar extremal distribution for does not by itself have the right covariance in the other directions, and a Gaussian does not reach the bound. The paper's route through the moment problem instead needs strong duality between a supremum over measures and an infimum over matrices, which is where the positive definiteness of enters.
EuclideanSpace ℝ (Fin n); is the inner product, and matrices are Matrix (Fin n) (Fin n) ℝ. Matrices of size are indexed by Fin n ⊕ Fin 1 and built with Matrix.fromBlocks (the helper bordered A v c is ). is PosSemidef, is PosDef, is (A * B).trace, and is written .HasMeanCov) contains every Borel probability measure on whose coordinates are square-integrable, with mean and centred covariance . It is not restricted to densities or to Gaussians: the Gaussian class gives a different constant, .IsLUB/IsGLB of one real number (no attainment is claimed). The maxima over , over and over the ellipsoid are IsGreatest.An algorithm for linear programming is strongly polynomial if the number of arithmetic operations it performs is bounded by a polynomial in the dimension of the problem alone (the number of variables and constraints), independently of the bit lengths of the numbers in the input. Many combinatorial optimization problems are linear programs over polyhedra of the form whose constraint matrix has entries , but whose objective vector is an arbitrary rational weight vector. Polynomial-time algorithms for such problems (for instance the ellipsoid-based algorithms of Grötschel, Lovász and Schrijver for maximum-weight cliques in perfect graphs, submodular flows, and matroid polyhedra) have running times that depend on the length of .
Frank and Tardos (Combinatorica 1987) remove this dependence once and for all: they replace by an integral objective whose entries have bits and which has exactly the same optimal solutions and the same optimal dual bases as over every such polyhedron. Any algorithm that is polynomial in and in the length of the objective then becomes strongly polynomial. The tool is simultaneous Diophantine approximation, used through the lattice-basis-reduction algorithm of Lenstra, Lenstra and Lovász (Math. Ann. 1982). The technique extends Tardos's strongly polynomial algorithm for linear programs with small constraint matrices (Oper. Res. 1986), which applies only to explicitly given programs.
For write and ; takes the values .
Decomposition. Fix a positive integer . A decomposition of is an expression
It satisfies condition (iii) if for the vector is nonzero and : the coefficients decrease so quickly that each term is negligible against the previous one.
Preprocessing. Given a rational and , the paper's preprocessing algorithm finds a decomposition with , condition (iii), and the size bound (ii)' , and outputs
Linear programs. Let be an matrix with entries in and . The primal program is and the dual program is . A point is -maximal if . A dual basis is a maximal set of row indices of whose rows are linearly independent; it determines at most one with supported on it (the basic dual solution), and it is an optimal dual basis if that exists and is optimal for the dual program.
For every , with , there is with
such that for every matrix with columns and every : (i) is -maximal if and only if it is -maximal; (ii) a set of rows of is an optimal dual basis for if and only if it is one for . The vector depends on only, not on or .
The result gives a general reduction: whenever a class of polyhedra with constraint matrices admits an optimization algorithm that is polynomial in and in the length of the objective, it admits a strongly polynomial one. The paper applies this to maximum-weight cliques in perfect graphs, optimization over submodular flow polyhedra, and matroid polyhedra membership, and its Section 5 applies the same rounding to the integer programming algorithms of Lenstra and Kannan. The subset-sum corollary (milestone 5) is independently useful: every rational weight function on a finite set can be replaced by an integral one with -bit entries that orders all subset sums identically.
All statements of this mission have been proved on paper since 1987. None is formalized on Prove2Me, and Mathlib contains only the one-dimensional Dirichlet approximation theorem. The mission produces a machine-checked version of the exact statements, with the explicit constants of the paper; the complexity claims (operation counts, strong polynomiality) are not part of it.
The goal combines two independent parts. The number-theoretic part (milestones 1–5) needs a multidimensional Dirichlet theorem, an induction producing the decomposition, and exact inequality chains with the constants and . The linear-programming part (milestones 6–7) needs bounds on the entries of inverses of nonsingular submatrices, the existence of optimal dual solutions supported on a dual basis, LP duality and complementary slackness. The obvious first idea, scaling to an integer vector by a common denominator, preserves every sign but gives no bound on in terms of ; the bound is the content of the theorem. Likewise, rounding each coordinate of separately to a fixed precision does not preserve the sign of when is tiny but nonzero.
Vectors are functions on Fin n: the input is rational (Fin n → ℚ) in the goal, in Theorem 3.3 and in the subset-sum corollary, as in the algorithm's input line; it is real in Theorem 3.1, Lemma 3.2 and Lemma 4.1, as on the page. Integral vectors are Fin n → ℤ, and is a Matrix (Fin m) (Fin n) ℤ with every entry in , cast to ; is unrestricted. Decompositions are indexed by as in the paper. is always the explicit sum , compared with in ; of an integer vector is a natural number (supNorm). Sign equality uses SignType.sign and includes the zero case. Condition (iii) is stated multiplicatively together with , which the paper's quotient presupposes; without Lemma 3.2 fails. An optimal dual basis is a maximal linearly independent set of row indices together with an optimal dual solution supported on it.
Two formalizations would make the goal trivial and are excluded: dropping the bound on (a multiple of then works), and letting depend on and (the goal states before ). The assumption on is part of every Section 4 statement.
A complete development needs a multidimensional pigeonhole argument, determinant and adjugate bounds for matrices, and basic LP duality (strong duality, complementary slackness, basic optimal dual solutions); the last two are reusable across linear-programming missions. Proofs of individual milestones, reusable lemmas on LP duality, and alternative proofs of Dirichlet's theorem are all welcome.
Paging is the problem of managing a fast memory that holds pages out of : when a requested page is not in fast memory (a page fault), some resident page must be evicted, and the cost of an algorithm is its number of faults. Practitioners have many eviction rules. Least-recently-used (LRU) performs well on real workloads but can be times worse than the optimal off-line schedule; the randomized marking algorithm of the same paper is -competitive and so has better worst-case guarantees. Fiat, Karp, Luby, McGeoch, Sleator and Young asked in 1991 whether one on-line algorithm can combine the advantages of several given ones, and answered the question exactly: the attainable combinations of ratios are characterized by one inequality (arXiv:cs/0205038, §6).
The question of combining on-line algorithms has since become a theme of its own: combining heuristics with worst-case-safe algorithms, and, more recently, combining machine-learned predictions with robust fallbacks, both ask for the same kind of guarantee against several reference algorithms at once.
A type consists of servers and a finite set of vertices with the uniform metric: two distinct vertices are at distance . This is paging: vertices are pages, the vertices covered by servers are the pages in fast memory, and a server move is a page fault.
A deterministic on-line algorithm of type has an initial configuration of its servers and, after each request , moves servers so that some server covers ; its configuration after a request sequence depends only on that sequence. Its cost on a request sequence is the total distance its servers travel, i.e. the number of server moves.
For algorithms and of the same type and a constant , is -competitive against if there is a constant such that for every request sequence
A sequence of positive reals is realizable if for every type and every deterministic on-line algorithms of that type there is a deterministic on-line algorithm of the same type that is -competitive against for every .
For and positive reals ,
In the order of the paper's proof:
The result. Theorem 6 is an exact characterization, not a bound: the region of simultaneously attainable ratios against arbitrary deterministic paging algorithms is . For example, any two paging algorithms can be combined into one that is -competitive against each, and no better symmetric pair is possible in general. Combined with Theorem 7 of the same paper (not part of this mission), the same region is attainable against randomized algorithms, which is how LRU's practical behaviour and the marking algorithm's worst-case guarantee can be obtained within constant factors by one algorithm.
Formalizing it. The theorem has been proved since 1991; no machine-checked proof is known. A formal proof produces a reusable notion of competitiveness of one on-line algorithm against another, built on the published KServer_model definitions, and a formal account of the scheduling fact at the core of the sufficiency proof.
Sufficiency looks like an averaging argument, but the combined algorithm cannot simulate the and follow one of them: switching between their configurations costs up to per switch, which no additive constant absorbs. The accounting has to charge each of 's faults to a specific move of a specific , and the charge must be injective; the paper's claim that is at least the number of punishments is where this happens, and it depends on how server intervals are matched. The allocation of faults to algorithms is then a deadline-scheduling problem whose feasibility is exactly , and the floor functions make the counting delicate at the boundary. The paper's own definition of punishment only counts intervals that start with a move, so the first faults of (servers on their initial vertices) need separate treatment; they are absorbed by the additive constant.
Necessity needs the right family of hard instances: the algorithms must never move at the same step, which pins the type to .
The Lean development works in the namespace CompetitivePaging.Combining and imports the published KServer_model definitions: KServer.OnlineAlgorithm k M (a configuration map from request prefixes to Fin k → M with a serving condition) and OnlineAlgorithm.cost. Committed conventions:
k : ℕ and any finite M : Type with a metric in which distinct points are at distance ; realizability quantifies over all of them, never over one fixed type;Trivializing encodings are ruled out: realizability is not stated for a single fixed type, the metric is not the metric of Fin n, and the competitive constant is not allowed to depend on the request sequence.
A complete proof needs the construction of the punishing algorithm as a KServer.OnlineAlgorithm (a lazy, injective algorithm whose moves depend on the prefix and on the 's configurations), the injective charging argument, the scheduling lemma, and the explicit shuttle algorithms. The scheduling lemma and the charging lemma are independent of paging and reusable. Proofs of any milestone are welcome, as are alternative statements of the sufficiency construction.
The Hitchcock transportation problem asks how to ship a commodity from supply points to demand points at minimum total cost. It was posed by Hitchcock in 1941 and is one of the founding problems of linear programming and network optimization; it is solved routinely in logistics, and its structure (a bipartite network with supplies, demands and per-unit costs) recurs in assignment, optimal transport and matching.
The classical algorithms for it, the Ford–Fulkerson primal–dual method among them, augment flow one path at a time. With integral data their number of augmentations is bounded only by the total supply , which is exponential in the number of binary digits used to write the data. Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems (J. ACM 19(2), 1972, doi:10.1145/321694.321699), introduced capacity scaling: solve a coarse version of the problem first, then refine one binary digit at a time. Their Theorem 9 (p. 260) bounds the total number of augmentations by a quantity proportional to times the number of bits of the data, which made the transportation problem, and through standard reductions the minimum-cost flow problem, one of the first network problems with a polynomial-time ("good") algorithm in the sense of Edmonds.
Timeline. Hitchcock (1941) posed the problem; Ford and Fulkerson (1956–1962) gave the primal–dual labeling method and the optimality conditions by node potentials; Edmonds and Karp (1972) gave the scaling method and the bound formalized here. Strongly polynomial algorithms, independent of the size of the numbers, came later (Tardos 1985; Orlin 1988).
The network of Figure 1 (p. 259) has a source , a sink , supply nodes and demand nodes , with . Its arcs are with capacity and cost ; with capacity and cost ; with capacity and cost ; and the return arc with capacity and cost . The supplies and demands are positive integers with .
A flow assigns a nonnegative number to every arc, at most the capacity, with inflow equal to outflow at every node. Write , , ; the value of is , and a maximum flow is one of largest value. Its cost is ; a flow is extreme if no flow of the same value is cheaper. A flow is pseudo-extreme if there are real with for all and whenever .
An augmenting path relative to is a sequence of distinct nodes from to in which each step either follows an arc with spare capacity or traverses backwards an arc carrying positive flow; augmenting pushes the minimum spare amount along it and raises by .
For , Problem has the same network and costs, with capacities and . Choose with every . The scaling method solves Problems in turn. Each phase performs augmentations keeping every flow pseudo-extreme, until no augmenting path is left. Problem starts from the zero flow, and Problem starts from twice the final flow of Problem .
For every run of the scaling method, the total number of flow augmentations satisfies
The bound holds for every admissible for the data and every choice of costs, and is stated with the paper's constant exactly.
The result. Theorem 9 shows that scaling reduces the number of augmentations from order to order , which is roughly the length of the binary encoding of the data. Combined with the cost of one augmentation it gives a polynomial-time algorithm for the transportation problem; through the reduction of minimum-cost flow to transportation (p. 261) it gives one for minimum-cost flow. Capacity and cost scaling became standard techniques in network optimization and in combinatorial optimization generally. Theorem 8 and the pseudo-extreme criterion are the optimality certificates for transportation, a special case of linear-programming complementary slackness.
Formalizing it. The theorem has been proved since 1972. This mission produces a machine-checked version of the bound, of the exact counting argument (eq. (6)) and of the arithmetic estimate that turns it into the stated constant, together with the potential-based optimality conditions for the transportation network. To our knowledge no machine-checked bound on the number of augmentations of a flow algorithm exists on the platform.
The obvious argument bounds the number of augmentations by the increase in flow value, since each augmentation raises the value by a positive integer. Applied to Problem 0 directly this gives only . The scaling bound needs three things that the naive count does not supply. First, doubling the final flow of Problem must give a feasible, still pseudo-extreme, starting flow for Problem (Lemma 3). Second, the gap between that start and the optimum of Problem must be small, which requires the exact maximum-flow value of each scaled problem. Third, the telescoping sum of the gaps must be estimated against with the floors handled exactly. Integrality of every intermediate flow is not assumed; it has to be carried along the run from the integral capacities and the zero start.
Everything lives in the namespace EdmondsKarp.Scaling. Nodes form an inductive type (s, t, src i, dst j). A flow is a structure with components f0, fx, fz, ret for the four arc families, real valued; the infinite capacities are encoded by the absence of an upper bound. IsMaxFlow is a predicate comparing values with every flow, not a supremum. Problem uses natural-number division for . Augmenting paths are lists of distinct nodes from s to t whose consecutive pairs have positive residual amount (resCap, valued in WithTop ℝ); they never use the return arc.
A run of the scaling method (IsScalingRun) is a family of phases for . It starts from in Problem , restarts from in Problem , and advances by one augmentation per step. Every flow is pseudo-extreme, and each phase ends with no augmenting path left. The paper's path-selection rule (minimum weight for the modified reduced costs ) is abstracted to this invariant, which the paper states for it, so every run of the paper's method is covered.
The goal compares the count, cast to , with , using Real.logb 2 and Int.floor. The constant is the printed one; neither nor a weaker constant is acceptable. Positivity of all is a hypothesis, because without it the printed bound is false (for , , , one augmentation is needed and the bound is negative). A formalization in which runs could be empty or never reach a maximum flow would trivialize the goal; the run predicate forbids this, and it is satisfiable (for instance with , , and one augmentation).
A complete development needs max-flow/min-cut for the bipartite network, integrality of flows along a run, the exact value of , the telescoping identity and floor/logarithm estimates. LP duality or complementary slackness is needed only for Theorem 8. The augmenting-path and max-flow lemmas are reusable for other bipartite flow problems. Contributions welcome: proofs of any milestone, and a formalization of the paper's exact path rule showing that it satisfies the invariant.
Machine scheduling asks how to assign jobs to machines over time so that a criterion such as the makespan , the time at which the last job completes, is as small as possible. In practice jobs also compete for scarce resources beyond the machines themselves: tools, operators, memory, power. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification of Graham, Lawler, Lenstra and Rinnooy Kan (1979) by a resource field . They then settled the complexity of every problem with parallel identical or uniform machines, unit-time jobs, precedence constraints and the criterion. Their Fig. 2 separates the maximal polynomially solvable problems from the minimal NP-hard ones, and it has been the reference map for resource-constrained scheduling since.
Brief timeline of the problems involved:
There are jobs and machines . Every job has processing time on every machine, each machine handles at most one job at a time, and jobs are not preempted. There are resources; resource has a positive integer size , the amount available at any time, and job has a nonnegative integer requirement , the amount it holds throughout its execution. A directed acyclic graph on the jobs gives the precedence constraints: if has a path from to (), then must complete before starts. The precedence is chain-like when every vertex of has indegree and outdegree at most one.
A schedule gives each job a machine and a real start time ; the job occupies and completes at . It is feasible if jobs on one machine do not overlap, precedence is respected, and at every time the jobs running at require at most of each resource . The makespan is .
The problem restricts this to , one resource () of size (), every requirement at most (), and chain-like precedence. The problem has , one resource of arbitrary size and requirements, and no precedence.
3-PARTITION: given , a positive integer and positive integers with and , can be split into disjoint 3-element sets with ?
A problem is NP-hard in the strong sense if it remains NP-hard when every number of the instance is written in unary.
The hypothesis is Garey and Johnson's theorem on 3-PARTITION, which the paper cites and does not prove. The conclusion concerns the decision version: given an instance and , is there a feasible schedule with ?
Theorem 7 is the sharpest hardness result of the paper's classification. Without resources, two-machine unit-time scheduling with arbitrary precedence is polynomial (Coffman and Graham, Acta Inform. 1972); without precedence, it is polynomial under arbitrary resources (Theorem 1 of the paper). The theorem shows that combining the weakest nontrivial versions of both constraints, chains and one unit resource, already crosses the borderline. The paper's §4.1 extends the same reduction to the and criteria.
On the formal side, the mission provides a machine-checked model of resource-constrained scheduling with real start times, a definition of NP-hardness in the strong sense on top of the platform's Turing-machine formalization of and , and 3-PARTITION as a reusable source problem. As far as the platform's corpus shows, none of Theorems 4 and 7, 3-PARTITION, or strong NP-hardness has been formalized before. Both theorems are proved in the literature; what remains is to formalize the reductions and their polynomial running time.
The combinatorial heart is the "only if" direction: a schedule of length must be shown to be rigid. Start times are arbitrary reals, so the first obstacle is to show that both machines are busy throughout , that the chain forces unit spacing, and that the primed jobs of the chains can only run in the intervals the chain leaves free of the resource. Only after this is established can the index sets be read off. Arguing on integer time slots from the start is not enough: the model allows fractional start times, and ruling them out is part of the proof.
The second obstacle is the complexity layer. NP-hardness is stated with respect to polynomial-time many-one reductions computed by one-tape Turing machines. The reduction from 3-PARTITION therefore has to be implemented and its running time bounded on unary codes. The constructed instance has jobs, which is polynomial in the unary length of the 3-PARTITION instance; this is exactly why the reduction proves hardness in the strong sense.
Fin n and machines Fin m, 0-based. Only identical machines with unit processing times are modelled. Start times are real, execution intervals are half-open, and the resource constraint is imposed at every real time. Precedence is the transitive closure of the arc list of . for an empty instance.Welcome contributions: proofs of the four milestones; a formalized polynomial-time implementation of the reduction on unary codes; general lemmas about composing polynomial-time reductions on the one-tape machine model.
The economic order quantity (EOQ) is the most widely used formula in inventory management. It assumes that demand is a deterministic constant stream. Real demand is random, and the model that accounts for this, the continuous-review policy with stochastic demand, has no closed-form optimum: for decades its optimal parameters were computed numerically, one instance at a time, which gave little insight into how the stochastic system behaves. Practitioners nevertheless kept using the EOQ quantity in stochastic systems and observed that the cost penalty was small (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), without an analytical explanation.
Zheng (Management Science 38(1), 1992) supplied that explanation. By minimising the average cost first over the reorder point and then over the order quantity, he obtained two simple optimality equations and compared the stochastic model with the EOQ model under the same cost structure. One of the results is the goal of this mission: for every leadtime-demand distribution, using the EOQ order quantity in the stochastic system raises the average cost by at most one eighth. The paper extends Federgruen and Zheng (1988), who treated the discrete-demand version of the cost function.
A single item faces demand at rate . Orders are delivered after a fixed leadtime , and stockouts are backordered. Each order costs a fixed . Inventory is held at cost rate per unit and backorders are penalised at cost rate per unit. Let be the demand during a leadtime, with mean . The newsvendor cost
is the rate at which expected inventory costs accrue at time when the inventory position at time is . It is convex, and it is assumed, as in the paper, to attain its minimum at a unique point .
A policy orders units whenever the inventory position falls to the reorder point . Its long-run average cost is
For a fixed let be an optimal reorder point, and set
is the average cost when the reorder point is chosen optimally for ; an order quantity minimising over is the optimal order quantity, and is the optimal cost.
The EOQ model is the special case in which the leadtime demand is the constant . Its cost rate is , and its optimal order quantity is
The subscript marks every object of the EOQ model (, , ).
is the stochastic cost at the EOQ quantity with the reorder point re-optimised for it. The bound holds for every leadtime-demand distribution and every value of the parameters.
In the order the goal's proof uses them:
The theorem is a distribution-free worst-case guarantee for the most common heuristic in inventory practice. It says that the EOQ formula, which needs only the mean demand rate and three cost parameters, loses at most against the true optimum, and that the loss is smaller when is close to or to . Combined with the paper's Theorem 2 (the gap is bounded as grows), it implies that the relative loss vanishes as the fixed ordering cost grows. The milestones along the way (the optimality conditions of Theorem 1, the monotonicity of the optimal reorder point, the comparison of with its EOQ counterpart) are the standard structural facts about continuous systems and are reused throughout the inventory literature.
The result is proved in the paper. No machine-checked version of it, or of the optimality conditions for the continuous cost (1), is known to exist. The platform has related but different formalizations: the discrete cost function with integer (InventoryControl_rqDiscrete), the cost under normal demand (InventoryControl_rq), and the EOQ without backorders (InventoryControl_eoq). A complete development here provides the continuous machinery for an arbitrary leadtime-demand distribution.
The paper's proofs differentiate and twice (Eqs. (4), (5)), which presupposes a leadtime demand with a smooth density. The formalization does not assume one, so that discrete demand, such as the Poisson demand of the paper's own numerical study, is covered. Every step that the paper takes through derivatives, in particular the convexity of and the slope bound , has to be established by other means: through one-sided derivatives or chord arguments for the convex function , whose kinks are where the derivative-based argument breaks. The definition of as a minimiser also means its existence and uniqueness must be proved before any property of , or can be used.
IsQRModel: , the conditions on , and the unique minimiser of (paper, p. 90). is a separate hypothesis. No density is assumed.