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?
Two estimators dominate sparse high-dimensional regression, where the number of candidate regressors can far exceed the sample size . The Lasso (Tibshirani, 1996) minimises a least-squares criterion plus an penalty. The Dantzig selector (Candès and Tao, 2007) minimises the norm of the coefficients subject to a bound on the correlation between the residual and the regressors, and is computed by a linear program. They were proposed independently and first analysed under different assumptions: sparsity oracle inequalities for the Lasso (Bunea, Tsybakov and Wegkamp, 2007) and bounds for the Dantzig selector under a uniform uncertainty principle (Candès and Tao, 2007). A practitioner choosing between them needs to know whether guarantees for one say anything about the other.
Bickel, Ritov and Tsybakov (arXiv:0801.1095; Ann. Statist. 37(4), 2009, doi:10.1214/08-AOS620) analyse both estimators in parallel under one assumption on the design, the restricted eigenvalue condition. Their main message is that, under sparsity, the two estimators "exhibit similar behavior" (p. 2). Section 5 makes this precise: the prediction losses of the two estimators are close. The result holds in a nonparametric model: the regression function need not be a combination of the regressors. This mission formalizes that comparison, Theorem 5.1 of the paper.
Let be real functions (the dictionary) on a set , and fixed design points, with and . The design matrix is . Observations are , where is an unknown function and are independent with . Write , and , so .
The empirical norm of is . Every column has , and . For , has value vector . The support is and the sparsity is . For , agrees with on and vanishes elsewhere.
Fix . The Lasso is any minimiser of
With , the Dantzig constraint is . The Dantzig selector is any vector of smallest that satisfies it. The estimators are and .
Assumption RE with , asks that
Throughout, , where is the natural logarithm.
Assume RE with , and let . With probability at least , every Lasso solution with and every Dantzig selector satisfy
The proof uses one probabilistic event and two one-sided deterministic inequalities.
Assume for all and RE. With probability at least , whenever ,
The result. Theorem 5.1 bounds the gap between the two prediction losses by the rate of a sparse regression with parameters. The bound carries a factor that measures how ill-conditioned the Gram matrix is on sparse vectors. A prediction bound for one estimator therefore transfers to the other at this cost. The paper uses this transfer in Proposition 6.3, which combines Theorem 5.1 with the Lasso oracle inequality of Section 6 to derive an oracle inequality for the Dantzig selector. The theorem requires no assumption relating to the dictionary.
Formalizing it. The result has been proved since 2009, and this mission formalizes that proof. None of the objects involved exists on Prove2Me yet: the weighted Lasso, the Dantzig selector and the Gaussian noise events. The Wainwright series on the platform defines a differently normalised Lasso with an unweighted penalty, a single fixed support and a different restricted eigenvalue condition, so it cannot be reused here. A machine-checked proof would also confirm the paper's constants, and the thresholds and , which appear in all later analyses.
Each estimator is defined only implicitly, as the solution of an optimisation problem, and neither need be unique. Comparing their losses directly gives plus with . A crude bound on the cross term, , yields an error proportional to . This does not produce the sparse rate unless is controlled by . That control needs to lie in the restricted eigenvalue cone at the support of the random, data-dependent vector . The restricted eigenvalue condition must therefore hold uniformly over supports of size at most ; a condition for one fixed support does not suffice. The probabilistic part is a union bound over Gaussian coordinates, and it must be arranged so that a single event serves every minimiser of both programs.
The dictionary and the design points enter every statement only through and , so the Lean statements take X : Matrix (Fin n) (Fin M) ℝ and f : Fin n → ℝ directly, and is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, mutually independent random variables with law gaussianReal 0 σ², and . The Lasso and the Dantzig selector are predicates (IsLasso, IsDantzig), and every theorem is stated for every solution. The Dantzig constraint is written coordinatewise as . The Lasso penalty and the Dantzig constraint are weighted by , and the Dantzig objective is unweighted, exactly as in the paper. Theorem 5.1 does not normalise the columns.
RE is stated through a witness: a real with on the cone, for all . The paper's is attained, so it is the largest witness. Every bound decreases in , so this reading is equivalent to the paper's and avoids a real infimum over an empty set. "With probability at least " becomes the existence of a measurable event with on which the conclusion holds for every Lasso solution and every Dantzig selector. The condition is imposed inside the event, per realisation. The milestones (B.2), (B.10), (B.15) and (B.17) are stated deterministically, on the noise events and as predicates on the noise vector; this is how the proof uses them. (B.4) is stated for every , which is stronger than the paper's and still true.
The goal cannot be made vacuous. For the probability bound is positive. Lasso solutions exist because and every , and Dantzig selectors exist because the Lasso is feasible. RE with holds for .
A complete development needs:
The noise-event lemmas and the Lasso optimality condition can be reused by the companion missions on this paper. Proofs of any milestone are welcome, including proofs that route (B.4) through Mathlib's sub-Gaussian API.
Classical non-cooperative game theory randomizes with objective, independent devices: each player spins a private wheel whose odds everyone agrees on. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) asks what changes when the randomizing events are ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. The paper introduced correlated equilibrium, and it also separates two effects that the classical model fuses: subjectivity (players disagree about probabilities) and correlation (players peg their choices on common or dependent events).
This mission formalizes the paper's result on subjectivity without correlation. Example 2.3 of the paper exhibits a three-person game in which strategies pegged on subjective but mutually secret events form an equilibrium that every player prefers to every classical mixed equilibrium. Proposition 5.1 shows that this cannot happen with two players.
A game has a finite set of players, a finite set of pure strategies for each player, a finite set of outcomes and an outcome function from onto . Player has a utility ; write for .
A randomizing structure consists of a set of states of the world with a -field of events, a sub--field for each player (the events is informed about), and a probability measure on for each player (the subjective probability of ). A strategy of is a map whose level sets lie in . For a profile of strategies the payoff of is
computed under player 's own beliefs. An equilibrium point is a profile with for every player and every strategy of .
An event is -secret if and every other player regards as independent of every event in the -field generated by the , : . A strategy is mixed if its level sets are -secret, and objective if each level set has the same probability under every . A measure is non-atomic on a -field if every event of of positive measure contains an event of of strictly smaller positive measure; a roulette is a sub--field of on which every is non-atomic. Throughout, Assumption II holds: every player has a -field of -secret events on which every is non-atomic.
For distributions on the classical payoff is , and is a Nash equilibrium point if no player gains by switching to another distribution.
Let and assume
Then for every equilibrium point in mixed strategies there is an equilibrium point in objective mixed strategies with
The game need not be zero-sum.
The result. Proposition 5.1 isolates correlation as the source of the new equilibrium payoffs of the subjective model in two-person games: disagreement about probabilities alone, with strategies pegged on secret events, reproduces only payoffs already achievable by classical mixed strategies (by Proposition 4.3, only Nash equilibrium payoffs). The paper uses it to explain Example 2.9, where two zero-sum players both expect more than the value, as an effect of subjectivity combined with correlation. Proposition 4.3 is the bridge that embeds classical Nash theory in the subjective model; with Nash's theorem it gives existence of equilibrium points in every game.
Formalizing it. The results are proved in the paper; to our knowledge none of them has been machine-checked. The mission produces a reusable measure-theoretic model of randomized strategies with private information and subjective beliefs (secret events, mixed and objective strategies, roulettes), a non-atomicity notion relative to a sub--field, and the Lyapunov-type construction of Lemma 7.1, none of which exists in Mathlib at the pinned revision.
The equilibrium conditions quantify over all strategies of the deviator, i.e. all -measurable maps, and the deviator may know events on which the opponent's mixed strategy is pegged. The obvious computation of as a sum of products of marginal probabilities is valid only because the opponent's strategy is pegged on secret events, which is the content of Lemma 7.3; for correlated strategies it fails, and Example 2.9 shows the proposition then fails. A second obstacle is that the replacement must reproduce player 2's beliefs about , while player 1's own equilibrium condition is stated under ; condition (5.2) is what transfers " is played with positive probability" from one player's beliefs to the other's. Constructing objective strategies with prescribed probabilities (Lemmas 7.1 and 4.1) needs the convexity of the range of a non-atomic vector measure (Lyapunov's theorem), which is not in Mathlib.
Players are a finite type (Fin 2 in the goal, players ); the and are finite types, and is surjective. The -field is an explicit parameter mΩ of the structure RandomizingStructure ι Ω mΩ, which carries the and the probability measures . Probabilities are -valued Mathlib measures. Utilities and are data (Assumption I is used only to compare lotteries by expected utility; the uniqueness of is not encoded). is a Bochner integral; for strategy profiles the integrand has finitely many values and is measurable, hence integrable. Non-atomicity on a sub--field is defined directly; Mathlib's NoAtoms (singletons are null) would trivialize Assumption II and is not used. "Mixed" means pegged on the family of all -secret events, not on the -field of Assumption II. Classical distributions, and Nash equilibrium points are AGT.IsLottery, AGT.expectedPayoff and AGT.IsMixedNash from the published definition agt_games.
A formalization that restricted deviations to mixed or objective strategies, or dropped "mixed" from the hypothesis on , would state a different theorem and is ruled out.
Useful contributions: Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures (or the special case needed for Lemma 7.1), the factorization of Lemma 7.3, and the payoff identities used in the proof of Proposition 4.3. The model definitions are shared in meaning with the companion mission on two-person zero-sum games.
The continuous-review policy — order a fixed quantity whenever the inventory position falls to the reorder point — is the textbook policy for a single item with random demand and a positive replenishment leadtime (Hadley and Whitin 1963). Its optimal parameters have no closed form, so practice routinely falls back on the deterministic economic order quantity (EOQ) model with backorders, whose optimum is explicit. How much the deterministic model misjudges the stochastic system's cost is therefore a practical question, and before Zheng (1992) it had been studied only numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978).
Zheng's paper answers it analytically. This mission targets its Theorem 3, which brackets the optimal cost of the stochastic model by the optimal cost of the EOQ model with the same parameters.
Demands arrive at rate and orders arrive after a fixed leadtime . Each order costs ; holding and backorder costs accrue at rates and per unit per unit time. The leadtime demand is a nonnegative random variable with . The inventory cost rate at inventory position is the newsvendor cost
assumed to attain its minimum at a unique point .
For order quantity and reorder point , the long-run average cost is
Let be a reorder point minimizing , and define for , , and . The optimal order quantity minimizes over , and . Write and
the controllable cost, so that ; . The constant is the newsboy cost.
The EOQ model is the same construction with demand constant at : , with functions , , optimal quantity and optimal cost .
All three inequalities are part of the goal. The weaker remark after the proof, , drops the factor and is not the goal.
Theorem 3 says that randomness of leadtime demand raises the total optimal cost above the EOQ's, yet the controllable part of that cost — the part the order quantity actually trades off — is smaller than the EOQ's cost, scaled by . Combined with (Theorem 2 of the paper), the gap is at most the newsboy cost , independent of , so the EOQ cost is a good proxy when is large relative to . The same machinery yields the paper's Theorem 5, that using in the stochastic model costs at most more than the optimum.
The result was proved in 1992; no machine-checked proof is known to exist. Formalizing it requires the continuous model as a whole — optimal reorder points, the one-variable reduction through , and the area function — none of which is in Mathlib. The companion missions of this series formalize Theorems 2, 4 and 5 of the same paper on the same model.
The middle inequality compares minima of two different functions: pointwise follows from Jensen's inequality, but only after the reorder point of each model is chosen optimally, so the comparison has to pass through the definition of as a minimum over . The outer inequalities depend on Lemma 8, whose proof uses convexity of and a slope comparison (Lemmas 4 and 7). The paper argues these through first and second derivatives of and , which exist only when the leadtime demand has a smooth distribution; the formal statements assume no density, so a proof must either avoid derivatives or handle one-sided ones. Existence of optimal reorder points and of is asserted in the paper without a separate argument.
Everything lives in the namespace ZhengQR.CostBounds. The machinery (qrCost, reorderPt, idealPt, Hfun, Cfun, Afun, H0fun, C0fun, IsOptQty) is defined for an arbitrary and instantiated at the stochastic and at . A structure QRModel holds the parameters, the demand distribution (a probability measure on ) and the standing assumptions.
Conventions committed to:
A formalization in which were an arbitrary number, or an arbitrary positive real, would make the goal false or empty; both are tied to the model above.
Needed infrastructure: existence of minimizers of convex coercive functions on , differentiation of parametric integrals , and properties of the newsvendor cost (convexity, coercivity, Jensen). Most of it is reusable for any continuous-review inventory model. Proofs of any milestone, and of lemmas the paper uses but this mission does not list (Lemmas 2–5, 7), are welcome.
Howard's finite Markovian decision process (MDP) models a controller who, at each instant, observes the state of a system, chooses a decision, collects a reward and moves to a random next state with known transition probabilities. Howard's policy-iteration algorithm computes an optimal policy, and the model has been applied to inventory control, equipment replacement, quality control and marketing. Its weak point is the requirement that every transition probability be known exactly: in applications these numbers are estimated and are hard to measure.
Satia and Lave (Operations Research 21(3), 1973) relax this requirement. In their game-theoretic formulation, the controller knows only a set of admissible probability rows for every state–decision pair, and nature chooses the rows adversarially. This is the model now called a robust MDP with (s,a)-rectangular uncertainty, studied later by Iyengar (Math. Oper. Res. 2005) and Nilim and El Ghaoui (Oper. Res. 2005), who reprove and extend the dynamic-programming results for it. The paper gives a policy-iteration algorithm for the max-min criterion and proves that it terminates at an optimal policy. This mission formalizes that part of the paper (pp. 728–732).
Timeline:
There are finitely many states and, in state , a finite nonempty set of decisions . A transition under decision earns reward ; rewards are discounted by with . For every pair there is a nonempty, closed, convex set of probability rows , , . Nature's choice is a matrix : one row for every pair.
A pure stationary policy selects . Under its present value is the unique solution of equations (5),
Nature's minimum is , and the max-min return of criterion (2) is . A policy is max-min optimal if in every state.
The algorithm alternates two routines. Phase 1 (nature's policy evaluation) fixes , computes from the current rows, replaces each row at by a minimizer of over (6), and stops when the minima reproduce . Phase 2 (policy improvement) chooses in each state a decision maximizing the test quantity (7),
at , keeping on ties; if the algorithm terminates.
Along every run of Phase 2 steps,
and the terminal policy attains the solution of the equations (4) and is -optimal for every .
The goal certifies a complete algorithm for the max-min problem: it computes a policy that is optimal against the worst admissible transition probabilities, in all states at once, in finitely many improvement steps. Propositions 1 and 2 show that the dynamic-programming equations (4) characterize the max-min value and that neither side gains from randomization. The known-transition case (every a single row) recovers Howard's policy iteration.
On the platform, Howard-type policy iteration for known transitions has been formalized (the Bertsekas Dynamic Programming and Optimal Control missions); nothing with uncertain transitions exists. The results of this paper are proved in the literature (Satia's thesis, and in greater generality by Iyengar and by Nilim and El Ghaoui); none has a machine-checked proof. This mission produces the first formal robust-MDP model and robust policy-iteration theorem on the platform.
The obvious argument copies Howard's improvement lemma. It fails at two points. First, the value of a policy is itself the result of an inner optimization by nature, so comparing two policies requires comparing two different worst-case transition matrices; the matrix minimizing against is not the one minimizing against . Second, the proof of Proposition 4 as printed shows only that nature's values decrease and converge; that the limit is nature's optimum, over a continuum of admissible rows, needs a separate argument. Finally, Proposition 1 involves randomized strategies and probability measures on the uncertainty sets, and reducing them to pure strategies is the content of Propositions 1 and 2, not a definitional convenience.
States are a finite type S (nonemptiness is not needed: every statement is unchanged in meaning at and trivially true at ), decisions a family D : S → Type* of finite nonempty types. The model fixes these conventions and readings:
Equation (4) must not be collapsed to in its definition: that would make Proposition 2 true by definition. Similarly, the Phase 2 relation always has a successor and algorithm runs exist from every policy, so the goal is not vacuous.
Needed infrastructure: Neumann series for with stochastic , monotonicity of policy evaluation, existence of minimizers of linear functions on compact subsets of the simplex, and the contraction argument for the robust Bellman operator. These are reusable for any robust or known-transition MDP development. Proofs of any milestone, alternative arguments for Propositions 1 and 2, and extensions to the max-max criterion are welcome.
The traveling salesman problem with the triangle inequality asks for a shortest closed tour through points whose distances form a metric. It is NP-hard, so in practice tours are built by fast construction heuristics, and the natural question is how far such a tour can be from optimal in the worst case. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the standard heuristics. Their results are reproduced in textbooks on approximation algorithms and combinatorial optimization, and they are the reference point against which later guarantees (Christofides' algorithm, the double-tree -approximation) are compared.
The simplest heuristic studied is the nearest neighbor algorithm (Bellmore and Nemhauser, 1968; the "next best method" of Gavett, 1965): from the current node, always move to the closest node not yet visited, and return to the start at the end. The paper shows that this greedy rule is never worse than logarithmic (Theorem 1) and that the logarithm cannot be removed (Theorem 2). This mission is about Theorem 2, the lower bound.
A traveling salesman graph on nodes is a complete graph with a distance that is symmetric, , nonnegative, , and satisfies the triangle inequality . A tour lists the nodes in a visiting order and returns to ; its length is the sum of the distances along it. OPTIMAL is the least length of a tour.
The nearest neighbor algorithm starts at an arbitrary node ; having reached , it moves to a node that minimizes over the nodes not yet visited, breaking ties arbitrarily; after the last node it returns to . The length of the resulting tour is written NEARNEIBER. Because the start node and the ties are free, one instance has in general several nearest-neighbor tours. A lower bound needs only one of them; an upper bound must hold for all.
The instances of the proof are built from a recursive family of weighted graphs. With (so ), the graph is a triangle with unit weights, and consists of two copies of joined through one new node by two edges of length and two edges of length . Each has nodes and a path from its start node to its middle node through every node, of length with , . The graph adds two closing edges to , and is the complete graph on the same nodes whose distance is the shortest-path distance of .
For each there is a traveling salesman graph with nodes and a nearest-neighbor tour on it such that
The statement is existential in both the instance and the run of the algorithm, exactly as in the paper.
The instance for is .
Theorem 1 of the same paper shows for every nearest-neighbor tour on every traveling salesman graph. Theorem 2 shows that this bound has the right order: no constant-factor guarantee holds for the nearest neighbor rule, and the gap between the two constants ( against ) is all that remains. This separates the nearest neighbor rule from the insertion rules analysed later in the same paper, of which nearest and cheapest insertion are within a factor of optimal. It is the standard example of a natural greedy heuristic whose approximation ratio grows with .
The upper bound, Theorem 1, is already on Prove2Me with a machine-checked proof (SupplyChainTheory.nearest_neighbor_bound); its statement notes that the lower-bound instances are not formalized there. This mission supplies them: an explicit recursive family of metric instances, the shortest-path computations that certify it, and the arithmetic of its ratio. The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The construction (a recursively defined weighted graph with a closed-form shortest-path table) is also a reusable pattern for other worst-case lower bounds of greedy heuristics.
The arithmetic ((2.12) and the final inequality) is routine. The content is in properties a) and b). A shortest-path distance is an infimum over all walks, and property a) asks that no detour through the recursive structure is shorter than the direct edge, at every level of the recursion. The paper handles this by an induction on (2.13)–(2.17) that tracks only seven nodes per level, and argues that distances inside a copy of are not shortened by embedding it into . Property b) then needs that at each step of the chosen node is at least as close as every unvisited node, including nodes in the other copy and nodes reached through the start or right nodes; ties occur, and the claim is only that some resolution of them follows . Checking small cases by computer does not give either property for all .
Nodes of an instance are Fin n, a tour is a permutation of Fin n, the tour length is the sum over consecutive pairs including the closing edge, and OPTIMAL is a minimum over the finite set of permutations. The model is the paper's: symmetric, nonnegative distances with the triangle inequality. The distance structure also carries , a normalization not in the paper; the diagonal never enters a tour length. A nearest-neighbor tour is a permutation in which each step goes to a node at least as close as every unvisited node, from an arbitrary start with arbitrary ties.
Ratios are multiplied out: the goal is together with , the paper's standing assumption (1.1). is Real.logb 2 of , as printed. Because of the strict inequality and the conjunct , the all-zero distance does not satisfy the goal, so the statement cannot be met by a degenerate instance.
In the construction the nodes of , , are numbered from left to right (start node , middle node , right node ); in the left copy comes first, then the new node, then the right copy. Graphs are edge lists with real weights and is defined in exactly as in (2.11). The shortest-path distance is the infimum of walk weights over an inductive walk predicate; it would be for two nodes with no connecting walk, a case that does not arise because every and is connected. is defined by its difference equation; its identification with the length of the tour along is milestone 7. All construction statements assume .
A complete development needs a small library for shortest-path distances of finite weighted edge lists (symmetry, triangle inequality, attainment, behaviour under relabelling and under gluing two graphs at a few nodes); this part is reusable beyond the mission. Contributions welcome: proofs of any milestone, and such general shortest-path lemmas as separate theorems. Theorem 1 is not part of this mission.
Semidefinite programming (SDP) optimizes a linear function over the intersection of the cone of positive semidefinite matrices with an affine subspace. It contains linear programming as the diagonal case and is the computational core of relaxations in combinatorial optimization, control theory and polynomial optimization. Its standard duality theory, however, is weaker than that of linear programming. The Lagrangian dual of an SDP can have a strictly positive duality gap, can fail to attain its optimal value, and an infeasible semidefinite system need not have a certificate of infeasibility of the naive Farkas form. All the classical strong duality theorems for SDP therefore assume a constraint qualification such as Slater's condition (a strictly feasible point).
M. V. Ramana (1997, Math. Program. 77, 129–162) constructed a dual, the Extended Lagrange–Slater Dual (ELSD), whose size is polynomial in the data and which enjoys every property of linear programming duality for every SDP, with no constraint qualification. The same construction yields an exact theorem of the alternative for semidefinite feasibility and the complexity consequence that semidefinite feasibility lies in NP if and only if it lies in co-NP in the Turing model.
Timeline:
Let be natural numbers, the space of real matrices, and the symmetric ones. On the inner product is . For symmetric , means is positive semidefinite. The data are symmetric and . The primal SDP is
with feasible region , a spectrahedron. Define by and write for " and ".
For let be the set of tuples of real matrices with and, for ,
The need not be symmetric. and are the sets of last components and ; . The ELSD is
and Weak-ELSD is the same program with . For the milestones: the polar , the algebraic polar , and .
For all data :
Propositions 7(vi) and 7(vii) (facts on PSD matrices), Lemma 9 (annihilation ), weak duality over every , Lemma 10 (nested subspaces), Lemma 13 (), Corollary 14, Claims 17 and 16, the central Theorem 12,
the translation invariance of (§2.5), and system (14) (dual attainment at value 0). Theorems 19–21 (Farkas lemma for SDP, optimality condition, primal attainment) are further items stated on the same definitions.
The Duality Theorem gives SDP a dual with the full strength of linear programming duality for every instance, at polynomial size. Consequences in the paper: an exact theorem of the alternative for semidefinite feasibility (Theorem 19); semidefinite characterizations of optimality of a given point and of primal attainment (Theorems 20, 21); and the complexity results that semidefinite feasibility is in NP iff it is in co-NP in the Turing model and in NP ∩ co-NP in the Blum–Shub–Smale model (Theorem 25, not part of this mission). Theorem 12 separately gives an exact semidefinite description of the polar of any spectrahedron containing the origin.
The results are proved on paper and are classical. No machine-checked version is known to exist; the platform's existing SDP duality theorem assumes Slater's condition. A formalization would provide the first constraint-qualification-free SDP duality in Lean, together with reusable infrastructure on PSD matrices (range inclusion, ) and on polars of convex sets.
The obvious route to SDP strong duality separates the primal's value from the image of the PSD cone under a linear map and invokes a closed-cone Farkas lemma. That step fails: the linear image of the PSD cone need not be closed, which is exactly why Lagrangian duality has gaps. In this mission the obstruction reappears as the non-closedness of the algebraic polar (Lemma 13 only gives ). The difficulty is to show that finitely many, and at most , corrections by the sets close (Claims 16, 17), and to control dimensions in doing so. A proof by assuming closedness, strict feasibility or a Slater point is a different theorem.
Everything lives in the namespace ExactSDPDuality.ELSD, in one definition file. Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin m → ℝ; "" is Mathlib's PosSemidef (which over ℝ includes symmetry); is the entrywise sum on all of ; is the dot product. The data carry symmetry hypotheses in every statement, as the paper assumes throughout. is encoded by sequences with , so ; for the index is . Optimal values are least upper and greatest lower bounds of the value sets, never real sSup/sInf. The polar is the one-sided polar. In §2.4 statements the standing assumption is a hypothesis. In Claim 16 the index satisfies , the range where is introduced, and is the rank of the span of .
Theorems 20 and 21 are printed with ; both are false as printed (counterexamples in the items) and are stated with the corrected that the paper's derivation from Theorem 6 gives.
Trivializing formalizations are ruled out: no Slater or other constraint qualification appears; the dual is the ELSD built from the recursively defined , not the Lagrangian dual or an arbitrary subspace; the range over all of , not only symmetric matrices (the paper's Example 4 needs a nonsymmetric ).
Needed infrastructure: PSD matrix facts (Proposition 7), bipolar theorem for closed convex sets containing the origin (Proposition 11), closedness arguments for linear images of cones, and dimension counting of subspaces of . Contributions of any milestone, of these general lemmas, and of alternative proofs (for instance via facial reduction) are welcome.
Many problems in optimization and equilibrium modelling reduce to a system of equations with that is continuous and locally Lipschitz but not differentiable. Complementarity problems rewritten through the min or Fischer–Burmeister functions, Karush–Kuhn–Tucker systems of nonlinear programs, and the gradients of augmented Lagrangians all have this form. Newton's method cannot be applied verbatim, because need not exist.
Qi and Sun (Math. Programming 58 (1993) 353–367) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and proved that the resulting method converges under a condition they called semismoothness, extending Mifflin's notion (SIAM J. Control Optim. 15 (1977)) from functionals to maps. The paper has two convergence results. Theorem 3.2 is local: near a semismooth root with nonsingular generalized Jacobian the method converges superlinearly. Theorem 3.3, the target of this mission, is global in the Newton–Kantorovich sense: explicit constants on a ball around the starting point guarantee that the iteration never leaves , that has exactly one zero in , and that the iterates converge to it with a computable error bound. The authors describe it as "an extension of the classical Newton-Kantorovich theorem" (p. 361), which is stated for smooth maps in Ortega and Rheinboldt's monograph.
Timeline.
Work in with the Euclidean norm ; for a linear map , is the induced operator norm. Let be locally Lipschitz. Write for the set of points where is differentiable and for the derivative at .
In Lean these are NonsmoothNewton.Global.clarkeJac, dirDeriv, SemismoothAt and IsNewtonRun, over EuclideanSpace ℝ (Fin n).
Fix , , the closed ball , and constants with .
Assume is semismooth at every point of and, for all and : is nonsingular,
with and . Then every run of (3.2) from stays in , every is nonsingular, has a unique zero in , , and
The theorem certifies, from data checkable on a single ball, that a solution exists, where it is, that it is unique there, and how far the current iterate is from it; (3.4) is an a-posteriori stopping criterion. It holds for every choice of , which is what implementations need, since they compute one element of and not the whole set. The result underlies the global and semilocal analysis of semismooth Newton methods for complementarity problems, variational inequalities and nonsmooth KKT systems, a line that continued through the 1990s and 2000s.
The theorem is proved on paper; no machine-checked version is known. The platform has no Newton–Kantorovich theorem, smooth or nonsmooth, and no Clarke generalized Jacobian. A complete formalization would supply both, and the definitions layer here (generalized Jacobian, one-sided directional derivative, semismoothness, Newton runs) is shared with the two companion missions on Qi and Sun's local convergence theorem and on semismoothness of augmented Lagrangian gradients.
The Newton map is set-valued: depends on the choice of , so the Banach fixed-point theorem for a single contraction does not apply directly, and the argument must hold for every sequence of choices. The contraction estimate needs both consecutive steps to start inside , so containment in and the geometric decay of the steps must be established together. Identifying the limit as a zero requires a uniform bound on , which is not a hypothesis: it has to come from local Lipschitz continuity through the structure of the generalized Jacobian. Uniqueness uses an element , whose existence rests on Rademacher's theorem. Finally, the directional derivative in the hypotheses is only meaningful because semismoothness makes it exist.
The space is EuclideanSpace ℝ (Fin n), so the norm is Euclidean, as in the paper (p. 356), and is the operator norm. Local Lipschitzness is global (LocallyLipschitz F), the standing assumption of Section 3. Conventions:
fderiv along sequences in ; no closure is taken (the limit set is compact for locally Lipschitz ).Ring.inverse is not used.dirDeriv, a limUnder along , used only at points of , where semismoothness makes the limit exist.The goal is the full four-part conclusion: containment, existence, uniqueness, and convergence with (3.4). A formalization that proves only that the iterates converge to some zero, or that treats as possibly empty so that the hypotheses become vacuous, is not the theorem. The hypotheses are satisfiable by genuinely nonsmooth maps, e.g. on with a ball containing the kink.
A complete development needs: nonemptiness and local boundedness of the generalized Jacobian (Rademacher's theorem, available in Mathlib as LipschitzWith.ae_differentiableAt); geometric-series and Cauchy-sequence arguments in a complete space. The generalized-Jacobian facts are reusable well beyond this mission. Contributions of any of the milestones, or of these general facts as separate lemmas, are welcome.
Bin packing asks how to place a list of items with sizes in into as few unit-capacity bins as possible. It models the cutting of stock material, the packing of files onto tracks of a disc and the assignment of jobs to machines with a common deadline. Deciding the optimum is NP-hard, so in practice simple rules are used, and the question is how far they can stray from the optimum in the worst case.
Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3(4), 1974) gave the first sharp worst-case bounds for the four classical rules. For First-Fit Decreasing (FFD), the rule that sorts the items into nonincreasing order and then places each into the first bin with room, they announced the bound , whose full proof in Johnson's thesis exceeds 75 pages. To show the method, Section 4 of the paper proves a simpler bound in detail: when no item exceeds , FFD uses at most bins. That result is the subject of this mission.
Timeline:
A list is a finite sequence of real numbers in ; values may repeat. A bin has capacity ; its level is the sum of the numbers in it. The optimum is the least number of bins into which the elements of can be placed with no bin level exceeding .
First-Fit places in order into bins , each initially at level : goes into the bin of least index whose level satisfies . First-Fit Decreasing first arranges into nonincreasing order and then runs First-Fit. is the number of bins it uses.
The proof uses a weight on finite sets of elements. For an integer , is a -piece if , and a -bin is a bin whose largest element is a -piece. Set . A pair obeys relation if is a -piece and ; then , and otherwise . For a partition of into one- and two-element sets, with each pair ordered (earlier, later) in the nonincreasing order,
BASIC is the set of elements of that are -pieces lying in a -bin of the FFD packing of , for some ; SURPLUS is the rest of .
The constants are those printed in the paper. The multiplicative constant is best possible.
A companion item states the Remark after Theorem 4.1: for every there is a list with all elements below , and .
Theorem 4.1 shows the weighting-function method in its simplest nontrivial form: a weight whose total is within a constant of the algorithm's bin count, and which no feasible bin can exceed by more than the target ratio. The same method, with more elaborate weights, gives the bound for FFD, and it is the model for later worst-case analyses of packing heuristics. The Remark shows that is exact for items in , and the Corollary on p. 322 extends the analysis to the asymptotic ratio when items are bounded by .
The source proof is partial. The billing argument behind Claim 4.2.2 is given only when two auxiliary conditions (G1) and (G2) hold ("The more intricate argument here omitted", p. 321), and Lemma 4.3 is checked in four of about seventy-four cases ("leaving the remaining 70-odd, more or less routine, cases to the ambitious reader", p. 321). Complete details are in Johnson's thesis. The theorem itself is established. A formalization therefore gives the first complete, checked proof in a single place. The finite case analysis of Lemma 4.3 is well suited to machine checking. No machine-checked proof of any FFD bound is known to exist.
The obvious weight alone fails. Claim 4.2.1 shows that covers the FFD bins, but many sets of elements with sum at most have , for example two -pieces, a -piece and a -piece. The pair discounts of repair Lemma 4.3, but they must then be paid for in Lemma 4.2, for every partition. That is Claim 4.2.2: a charge from each discounted pair to distinct SURPLUS elements that are no larger. The charge is straightforward only when no member of a pair obeying relation lies in a bin of type . In general a pair's larger element may already have been charged by a smaller relation, and the paper omits the argument that handles this. Lemma 4.3 is elementary but has many cases, each determined by the piece types in and the relations they obey.
A list is L : List ℝ with IsList L ( for each element) in every statement. is optBins L, the least such that some map from positions to Fin b has every bin sum at most . The First-Fit run keeps the nonempty bins as a List (List ℝ), and opens a new bin at the end exactly when no existing bin fits, which is the paper's "least ". The fit test is . FFD is First-Fit on sortDesc L, the mergeSort into nonincreasing order; ties do not affect the bin count. Indices are -based.
sorts into nonincreasing order and minimises over the involutions of its positions: fixed points are singletons, and a pair is oriented (larger, smaller). The minimum is over a finite nonempty set, so it is attained. BASIC is a set of positions of sortDesc L, and each position's bin is its bin in the final FFD packing. In , is the piece type of the first element. Sums are over Finset.Icc 2 (N - 1) with .
The goal's range is . The restriction to belongs only to the proof, through Lemma 3.3. Stating the goal for , weakening or , or making an unattained infimum would each change the theorem. Only the FFD half of Lemma 3.3 is stated. Claim 4.2.1 is stated with Lemma 4.2's standing hypothesis . The Remark's printed range is a misprint: its FFD packing needs , and the companion item states only the existence claim.
Infrastructure needed: a usable API for the First-Fit run (the invariants of the fold, bin levels, the order of bins), a lemma that FFD bins receive items in nonincreasing order, and a decision procedure for Lemma 4.3's case analysis over piece types. The model file and the weight file are reusable for the bound (mission 3 of this series) and for the bounded- corollaries. Contributions of proofs of Lemma 4.3 by computer-checked case enumeration, and of the missing general case of Claim 4.2.2, are especially welcome.
Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models cutting stock, memory allocation, file placement and the loading of trucks, and it is NP-hard, so in practice lists are packed by simple rules that look at one item at a time. The two most widely used rules are First-Fit and Best-Fit, and the question that Johnson, Demers, Ullman, Garey and Graham answered in 1974 is how far from optimal they can be in the worst case.
Their headline answer is that both rules use at most about times the optimal number of bins, and that is asymptotically attained. The lists that force this ratio use items larger than . When all items are known to be small, which is typical of memory and storage applications, the guarantee is much better, and this mission is about that refinement: the paper's Theorem 2.3 and its corollary, which determine the asymptotic worst-case ratio of First-Fit and Best-Fit exactly as a function of the largest allowed item size .
Timeline. Ullman (1971) introduced the worst-case analysis of First-Fit with a bound. Garey, Graham and Ullman (1972) and Johnson's thesis (MIT, 1973) extended it to Best-Fit and to the decreasing variants. The 1974 SIAM paper collects these results; Theorem 2.3 there is the parametric bound for items of size at most . The additive constants in the unrestricted bound were sharpened over the following four decades, culminating in Dósa and Sgall's proof (2013) that .
A list is a finite sequence of real numbers in . Its optimum is the least number of bins into which the elements of can be placed so that no bin contains numbers whose sum exceeds . The level of a bin is the sum of the numbers in it. For a real , write when every element of is at most .
First-Fit () considers bins , all initially empty, and places in that order: goes into the bin of least index whose level satisfies . Best-Fit () is the same except that, among the bins with , it chooses one of largest level (least index among ties). and denote the numbers of nonempty bins at the end.
The restricted worst-case ratios are
Throughout, and , an integer with and .
The goal is stated as a limit, which is the stable form of the result: it is unaffected by any improvement of the additive constants below.
For each there is a list with and ; likewise for .
If no element of exceeds , then in the First-Fit packing every bin except possibly the last contains at least elements, and all but at most two bins have level at least .
For every list ,
The theorem gives an exact, parametric description of how the worst case of the two greedy rules improves as items shrink: the asymptotic ratio is when items are at most , when at most , and tends to as the maximum item size tends to . Combined with the bound for unrestricted lists, it shows that the bad behaviour of First-Fit is caused entirely by items larger than . Such parametric bounds are the standard way bin-packing heuristics are compared in the literature on online and semi-online packing, and the construction in part (i) is a reusable template for lower-bound lists.
The paper proves the First-Fit upper bound and the lower bound (the verification of the lower-bound construction is left to the reader). The Best-Fit upper bound is stated but not proved: the paper says only that "a similar, but slightly more complicated, argument can be used". A formal proof of the goal therefore requires supplying that argument. None of these results is known to have a machine-checked proof; Mathlib contains no bin-packing development.
For First-Fit the upper bound is a counting argument, but it rests on a property of the run, not of the final packing: an item that went into a later bin did not fit into an earlier bin at the moment it was placed. Turning that into a statement about the final levels requires an invariant maintained through the whole sequence of placements.
The Best-Fit upper bound is harder because that property fails: Best-Fit may put a small item into a fuller, later bin while an earlier, lighter bin still has room, so a light early bin and a light later bin can coexist longer than under First-Fit. The paper gives no argument for this case.
The lower bound requires computing the exact behaviour of both algorithms on a specific interleaved list with item sizes perturbed by powers of , and computing exactly for that list, which needs a matching lower bound on the optimum.
A list is L : List ℝ with the hypothesis IsList L (every element in ); is the additional hypothesis ∀ a ∈ L, a ≤ α. is optBins L, a sInf in ℕ over numbers of bins admitting a feasible assignment; the hypothesis IsList makes the set nonempty. The runs ffPack L and bfPack L are folds over the list that keep the nonempty bins in the order they were opened, each with its contents; an item that fits nowhere opens a new bin at the end, which is the paper's "least " over infinitely many empty bins. Comparisons are exact (classical decidability on ℝ), and , are the lengths of the final bin lists. is Nat.floor α⁻¹, cast before any division.
The ratios , are suprema taken in ℝ≥0∞: an unbounded family would give , never a default value, and at the only admissible list is empty and the value is . The goal is a Tendsto … atTop (𝓝 (1 + (⌊α⁻¹⌋₊)⁻¹)) statement in ℝ≥0∞. A real-valued sSup would have returned on an unbounded family and made a false bound look provable; that encoding is ruled out. The upper bounds keep the additive constant and the lower bound the subtractive exactly as printed.
The two proof steps are stated under the proof's own hypothesis "no element exceeding ", which is weaker than .
A complete development needs invariants of the First-Fit and Best-Fit folds, a lower bound , and exact evaluation of both runs on the construction of part (i). Lemmas about the fold encoding of First-Fit and Best-Fit and about are reusable in the companion missions on the , and bounds of the same paper. Contributions on the Best-Fit upper bound are especially welcome, since the source gives no proof.
Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It is one of the first problems studied through the worst-case analysis of approximation algorithms, and it models storage allocation, paging and file placement on tracks, as well as cutting-stock problems in operations research. Deciding the optimum exactly is NP-hard, so the practical question is how badly simple rules can do. The two simplest on-line rules, First-Fit and Best-Fit, are still the baseline against which every later bin-packing heuristic is measured.
Timeline:
A list is a finite sequence of real numbers in ; values may repeat. A bin has capacity , and its level is the sum of the numbers in it. The optimum is the minimum number of bins into which the elements of can be placed so that no bin contains numbers whose sum exceeds .
Both rules place in this order into bins , each initially at level , and never move an element once placed.
and are the numbers of nonempty bins at the end. The worst-case ratio at optimum is
The analysis also uses a weighting function , piecewise linear with on , on , on and on , and the coarseness of a bin of a completed packing: the largest over the bins of smaller index, and for the first bin.
The goal fixes only the asymptotic ratio and leaves the additive constants free, so it is the statement that survives the later improvements of the constants.
A companion item, not a milestone, records the explicit list of Fig. 3 (p. 307) with and .
The result fixes the worst-case behaviour of the two simplest bin-packing heuristics: neither ever uses more than about more bins than an optimal packing, and both can be forced to. The weighting-function technique introduced for this bound became the standard method for analysing bin-packing heuristics, including First-Fit Decreasing, Harmonic-type algorithms and on-line lower bounds, and the constant is the reference point for later on-line algorithms.
The theorem is proved, and its constants have since been sharpened. No machine-checked proof of any of these results is known. This mission produces a Lean model of on-line bin packing (the optimum, the First-Fit and Best-Fit runs with their placement history, and the worst-case ratio) that the other missions of this paper and later bin-packing formalizations can reuse. It also produces formal proofs of the weighting-function bounds, of the upper bound and of the lower-bound construction.
The first idea, charging each bin its level, gives only : at most one bin is at most half full. The ratio comes from bins that are more than half full but far from full, and a bound on the total size of the elements cannot see them. No property of the final packing alone suffices: the bins that are far from full can only be controlled through the order in which the rule opened and filled them, so the argument depends on the dynamics of the run. On the lower-bound side, the natural periodic list (sizes near , p. 301) gives only the ratio ; reaching needs a list on which both rules waste space in every medium bin, for every , while is still known exactly.
A list is L : List ℝ with the hypothesis IsList L (every element in ), and every statement assumes it. is optBins L, the least b : ℕ for which some assignment Fin L.length → Fin b has every bin sum at most . A run is a fold over the list that keeps only the nonempty bins, in index order, each with its contents in placement order. A new bin is opened at the end exactly when no nonempty bin fits, which is the paper's "least " over infinitely many initially empty bins, since elements are positive. The fit test is the non-strict , and Best-Fit breaks ties by least index. The placement history (the bin chosen for each element and that bin's level just before) is read off the run on the prefix of the list. Indices are -based. Coarseness is computed in the completed packing. is a function ℝ → ℝ and is only ever applied to elements of . and are suprema in the extended nonnegative reals , and the limit is taken there.
A real-valued supremum would be on an empty or unbounded family, and the limit statement would then say nothing about the algorithms. The extended-real supremum rules this trivialization out. Every claim is stated for the concrete First-Fit run and the concrete Best-Fit run, not for an abstract rule with the properties used in the proof.
Claim 2.2.4 is printed with alternative (i) " and ", which is false: First-Fit on gives a counterexample. The mission states it with , which is what the paper's proof establishes and what the main proof uses. The milestone text keeps the printed version.
The model definitions are reusable for any on-line bin-packing rule, since the run is parameterized by the choice rule. Contributions welcome: proofs of the milestones, general lemmas about the runs (levels stay at most , at most one bin is at most half full, the history determines the final packing), and the computation of for the explicit lists of Theorem 2.1 and Fig. 3.
In stochastic linear optimization under bandit feedback a learner repeatedly chooses a decision from a fixed set and observes only the noisy cost of that one decision, whose expectation is a fixed but unknown linear function . The model covers online routing, ad and product selection with feature vectors, and any sequential decision problem whose decision set is too large to enumerate but whose expected cost is linear in a known representation. The multi-armed bandit is the special case where is the set of standard basis vectors.
Dani, Hayes and Kakade (COLT 2008) analysed the algorithm ConfidenceBall₂, a generalization of Auer's LinRel (JMLR 2002), and proved that its regret is with high probability for an arbitrary compact decision set, and that this is optimal up to logarithmic factors. Their confidence-ellipsoid construction became the template for later linear bandit algorithms (OFUL, LinUCB), and the ellipsoid-plus-potential analysis is the standard argument of the field (Lattimore and Szepesvári, Bandit Algorithms, Chapters 19–20).
Timeline: Auer (2002) introduced LinRel for finite decision sets; Dani, Hayes and Kakade (2008) extended it to arbitrary compact sets with the bound and a matching lower bound; Rusmevichientong and Tsitsiklis (Math. Oper. Res. 2010) studied linearly parameterized bandits with dimension-dependent regret bounds; Abbasi-Yadkori, Pál and Szepesvári (NeurIPS 2011) sharpened the confidence ellipsoids with self-normalized martingale bounds.
Fix and a compact decision set whose standard basis is a barycentric spanner: each and every lies in the cube . The paper's Section 5 adopts these coordinates without loss of generality. An unknown vector satisfies for , and minimises .
On round the learner plays , measurable with respect to the information before round , and observes a loss with . The regret after rounds is
ConfidenceBall₂ maintains the design matrix , the least-squares estimate , the radius
and the confidence ellipsoid . It plays the optimistic decision . The analysis uses the width , the error , and the noise .
For with and noise ,
A single event covers every horizon, so the bound is anytime.
The result gives a regret bound for linear bandits over an arbitrary compact decision set that depends on the dimension rather than on , holds uniformly over horizons, and requires no gap between the best and second-best decision. With the paper's lower bound it shows that the price of bandit feedback, compared with full information, is a factor . The two components, a confidence theorem for a least-squares ellipsoid under martingale noise and a deterministic potential argument on , are reused in the analysis of most optimistic linear and generalized-linear bandit algorithms.
The theorem has a published proof but, to our knowledge, no machine-checked one. The platform already has the elliptical potential lemma (BanditAlgorithm.elliptical_potential_lemma, Lattimore–Szepesvári Lemma 19.4), the matrix determinant lemma and the Woodbury identity, which cover the linear-algebra layer; the LinUCB regret theorem there (BanditAlgorithm.linear_bandit_linucb_regret_bound) is pathwise given confidence, for a different algorithm, so the probabilistic half is new. Formalization also settles the printed constants, three of which need correction (below).
The deterministic half is linear algebra. The difficulty is the confidence theorem. Hoeffding–Azuma applied to would need a deterministic step bound, and the natural one gives only a regret. The step sizes of are bounded in terms of the random widths , so the argument must control the conditional variances pathwise and apply Freedman's inequality, whose event is random. The escape indicator , which switches the martingale off after the first failure of confidence, is what makes the variance bound hold on every path, and the induction that turns Lemma 14 into Theorem 5 must be carried out on a single event for all simultaneously. Freedman's inequality itself is not in Mathlib.
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, rounds are indexed in ℕ. The spanner is the standard basis, as in Section 5 of the paper (the algorithm is equivariant under the linear change of coordinates). The probability model is a probability space with a general filtration ; is -measurable and is -measurable. The argmin is encoded as a joint minimiser over , which admits every tie-break and is required on every outcome; measurability of is a hypothesis, not derived from the selection. The optimum is a hypothesis (, minimising), not an sInf.
Corrections of the printed statements, each labelled in the item's Formalization Note:
A regret bound for an arbitrary decision sequence under the assumption for all is Theorem 6, not the goal; the goal carries the ConfidenceBall₂ selection rule, the conditional-mean and measurability hypotheses, and as the algorithm's own parameter. The hypotheses are jointly satisfiable, for example by a finite with a fixed tie-break and i.i.d. costs in .
Needed infrastructure: Freedman's inequality for a filtration (reusable across all of bandit theory), the potential lemma (available), and measurability of the algorithm's statistics. Contributions of alternative proofs of Theorem 5, for example via self-normalized bounds, are welcome.
Minimizing the average completion time of jobs that arrive over time is one of the basic objectives of machine scheduling: it measures how long, on average, a job waits in the system. On a single machine with release dates and no preemption (written ), the problem is strongly NP-hard, so research has focused on approximation algorithms whose guarantees are stated against every feasible schedule.
The standard route runs through the preemptive relaxation. When jobs may be interrupted and resumed, the shortest-remaining-processing-time rule (SRPT) produces an optimal schedule, and its value is a lower bound for every nonpreemptive schedule. The question is how to turn that preemptive schedule into a nonpreemptive one without losing too much.
Timeline:
An instance has jobs . Job has a processing time , a release date , and, where the objective is weighted, a weight . There is one machine.
A nonpreemptive schedule assigns each job a start time such that the intervals are pairwise disjoint. Its completion times are .
A preemptive schedule specifies, for each time , which job runs at , if any. Job runs only at times , receives exactly units of processing in total, and finishes by some finite time. Its completion time is the first time by which all of has been processed. For , its -point is the first time by which units have been processed.
For a job , denotes the idle time of before . denotes the fraction of processed before . The paper writes for the set of jobs with , and also for their total processing time.
One-machine list scheduling in a given order runs the jobs nonpreemptively in that order. Each job starts at the later of its release date and the completion of the previous job in the list. An -schedule is list scheduling in nondecreasing order of the -points . denotes the completion times of an -schedule.
Random- draws from a distribution on and outputs the -schedule. Best- outputs the -schedule of smallest total completion time .
Let be optimal among preemptive schedules for . Then there is such that every -schedule derived from satisfies
Since Best- returns a schedule no worse than this -schedule, Best- is an -approximation.
Companion statements, not milestones:
The bound shows that conversion from the preemptive relaxation can beat the factor 2 of the natural ordering. It does so by exploiting that no single instance is bad for many values of at once. The -point technique was also used with LP relaxations, for example by Goemans (SODA 1997) and by Schulz and Skutella. The randomized version is an optimal randomized on-line algorithm for . Lemma 2.3 is a statement about any preemptive schedule, so it applies wherever a good preemptive or fractional schedule is available.
All results of the mission are proved in the paper, except that the proof of Theorem 2.6, part 2 is omitted there. No machine-checked proof of them is known. A complete development would give a verified model of preemptive one-machine schedules, -points and list scheduling, together with the averaging argument over . These are reusable for the later results of the same paper and for the -point literature.
The obvious argument bounds each job's -schedule completion time directly against its preemptive completion time. That argument loses a factor (Theorem 2.1), which is at least 2 for every fixed . The improvement needs Lemma 2.3. There the charge to each job depends on how much of it was done by relative to , and the idle time is not inflated at all. Proving Lemma 2.3 requires reasoning about a preemptive schedule as a measure on time, and about how moving pieces of jobs changes completion times. A proof that treats the preemptive schedule as a finite list of pieces must first show that nothing is lost by this discretization.
The averaging step needs the expectation over to be an honest integral. The map must be shown integrable, which requires a fixed rule for ties between equal -points.
Fin n, time is real, and . The paper admits only in its tightness instances.
Option (Fin n) (none = idle). Each job's run set is measurable, lies in , is bounded above, and has Lebesgue measure .Contributions are welcome at every level. The calculus milestone and Lemma 2.2 are good first targets.
In the predict-then-optimize paradigm a model first predicts the cost vector of a linear optimization problem from contextual features, and the prediction is then fed to an optimization solver that returns a decision. Examples include routing with predicted travel times and portfolio choice with predicted returns. The quality of a prediction is judged by the decision it produces. The Smart Predict-then-Optimize (SPO) loss of Elmachtoub and Grigas (Management Science 2022) measures exactly that: the excess cost of acting on the prediction instead of on the true cost vector.
El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) ask when a model with small empirical SPO loss also has small expected SPO loss. The SPO loss is non-convex and discontinuous, so standard Lipschitz-contraction arguments do not apply to it directly. Their Section 4 introduces a margin version of the SPO loss, in the spirit of the margin theory of Koltchinskii and Panchenko (Ann. Statist. 2002) for classification. They show that it is Lipschitz under a geometric condition on the feasible region, and derive a generalization bound in terms of the multivariate Rademacher complexity of the hypothesis class. This mission formalizes that bound.
Decisions live in with a norm ; cost vectors are linear functionals with the dual norm . The feasible region is nonempty, compact and convex, and throughout Section 4 it is not a singleton. An optimization oracle maps each cost vector to some minimizer . The SPO loss of a prediction against the realized cost is
and the linear optimization gap is , with and for the set of possible true costs.
A cost vector is degenerate if has more than one optimal solution; is the set of degenerate costs. The distance to degeneracy is . The region has the strength property with parameter if
For the -margin SPO loss equals when and otherwise. It dominates the SPO loss.
Data are drawn from a distribution on features and costs in , and is a class of prediction functions . The SPO risk is and the empirical margin risk is . The multivariate empirical Rademacher complexity is with i.i.d. Rademacher vectors , and is its expectation over the sample.
In the set-up, under the strength property with and for fixed , for every , with probability at least over an i.i.d. sample of size , for all :
Theorem 3 is stated for a general norm, as in the paper. Eq. (7), Theorem 4 and the goal are Euclidean. The paper's Theorem 5 (p. 20), a version of the goal uniform over , is not part of this mission.
The bound replaces the loss-class complexity of the SPO loss, which is controlled only through combinatorial dimensions (Natarajan dimension in the polyhedral case, Section 3 of the paper), by the multivariate Rademacher complexity of itself. For norm-bounded linear hypothesis classes this complexity has mild, even logarithmic, dependence on the dimensions and (Section 4.4). The result applies to every feasible region with the strength property. By Section 5 of the paper these include strongly convex sets and polytopes, where can also be computed. When most predictions stay far from degeneracy, and the bound is much sharper than the combinatorial one. It is also a strict generalization of margin bounds for binary classification (Example 7).
The theorem is proved in the paper, which imports two external tools without proof: the Rademacher generalization bound of Bartlett and Mendelson, applied to the margin loss, and Maurer's inequality. To our knowledge none of these results has a machine-checked proof. The mission produces a checked proof of the margin bound and a Lean statement of Maurer's inequality. It also formalizes the strength property and the Lipschitz estimates of Theorem 3, which the companion missions on strongly convex sets and polytopes rely on.
The SPO loss is discontinuous in at degenerate predictions. The standard route, scalar Ledoux–Talagrand contraction applied to the loss class, therefore fails at the first step. It would fail even for a Lipschitz loss, because it relates the loss class only to a scalar class, and is vector valued. Lipschitz continuity of the margin loss needs the oracle to be stable away from . Convexity and compactness of alone do not give that: for an ball with the strength property fails for every (p. 14). The vector contraction inequality of Maurer (2016) is a nontrivial probabilistic inequality, and its constant must not depend on the dimension . The final concentration step is McDiarmid's inequality for a supremum over a possibly uncountable class, which in a formal proof needs measurability of that supremum.
The decision space is a finite-dimensional real normed space E. Cost vectors and predictions are continuous linear functionals, StrongDual ℝ E, whose operator norm is the paper's dual norm. In the statements E = EuclideanSpace ℝ (Fin d), where the dual norm is Euclidean. Every statement carries the standing assumptions: nonempty, compact, convex and not a singleton, an arbitrary oracle (no tie-breaking rule), and , . The Lipschitz-like bounds of Theorem 3(a)–(b) are stated multiplied out, because the paper reads as . Expectations over signs are finite averages over sign patterns. and are suprema over a nonempty bounded containing the cost almost surely. "With probability at least " is the statement that the outer -measure of the failure event is at most .
Added hypotheses, all disclosed in the statements: the multivariate Rademacher sums are bounded above (almost surely in the goal) and is integrable, since otherwise Lean's junk value would replace an infinite complexity and make the bound false rather than vacuous. Hypotheses and measurable, and the uniform deviation and margin Rademacher suprema a.e.-measurable, are also added; the paper is silent on measurability. A singleton would make empty and the strength property hold for free; this is excluded explicitly, so the strength property is not vacuous.
A complete development needs the Bartlett–Mendelson symmetrization bound for bounded losses, McDiarmid's inequality, Maurer's inequality, and the Lipschitz and distance-to-degeneracy facts of Section 4.1. Maurer's inequality and the multivariate Rademacher complexity are reusable across vector-valued learning theory. Proofs of any milestone, and of Maurer's inequality in particular, are welcome.
The uncapacitated facility location (UFL) problem is one of the basic models of location theory and operations research: a firm chooses which warehouses, plants or servers to open, paying a fixed cost for each open site and a service cost for every client according to its distance to the nearest open site. It is also a standard test case for approximation algorithms.
Local search is the simplest of these and the one most used in practice: start from any set of open facilities and repeatedly add, drop or exchange one facility while this lowers the cost. The question is how bad a solution can be when no such move helps. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) answered it for UFL with an exact constant.
Timeline. Korupolu, Plaxton and Rajaraman (SODA 1998, J. Algorithms 2000) analysed local search with add, drop and swap moves and proved a locality gap of at most 5; their analysis contains the service cost bound restated here as Lemma 4.1. Charikar and Guha (FOCS 1999) proved a locality gap of 3 for a different local search, in which one facility is added and any number are dropped. Arya et al. (STOC 2001; journal version 2004) proved that the add/drop/swap neighbourhood itself has locality gap at most 3, and gave an instance showing that 3 cannot be improved (§4.3).
A metric instance consists of a finite set of clients, a finite set of facilities, and a distance on that is nonnegative, symmetric and satisfies the triangle inequality. The cost of serving client by facility is ; the distance between two facilities is also available. Each facility has an opening cost .
A solution is a nonempty set of open facilities. Every client is served by its nearest open facility, so
The neighbourhood of is the set of solutions reachable by adding one facility, dropping one facility, or swapping one open facility for another:
is locally optimum if for every . The locality gap is the supremum, over all instances, of the ratio between the cost of a worst local optimum and the cost of a global optimum.
The proofs use the following notation, which appears in the milestones but not in the goal. Fix a second solution and nearest-facility assignments , ; write , , , and . A facility captures if ; is good if it captures no facility of and bad otherwise. The proof of the facility cost bound uses a permutation of the clients that maps each onto itself, moves every client of a non-capturing block out of that block (Property 3.1), and fixes every client of a capturing block that it would map into the same block.
This is the locality gap bound of Theorem 4.3 (p. 557) in its strongest printed form: is any solution, not only an optimal one.
A companion item, not a milestone, states the bound in the proof of Theorem 4.4 with : a local optimum of the instance with facility costs costs at most in the original instance.
The result. Theorem 4.3 shows that the simplest local search for metric UFL is within a factor 3 of optimal at every local optimum, with no LP and no rounding, and the tight example of §4.3 shows the analysis cannot be improved for this neighbourhood. Because Lemmas 4.1 and 4.2 hold against every solution , scaling the facility costs before running local search trades the two bounds against each other and gives the guarantee of Theorem 4.4. The same capture-and-reassign technique is used for k-median (§3) and capacitated facility location (§5).
Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of any locality gap bound for facility location is known to this mission. A formal development would check the reassignment arguments, which are stated case by case in the paper, and would produce reusable Lean infrastructure for metric facility location instances, nearest-facility costs and neighbourhood-based local optimality.
The service cost bound is routine; the facility cost bound is where the work lies. The natural first idea, closing a facility and sending each of its clients to the facility of nearest to that client's optimal facility, fails when serves most of the clients of some : the nearest facility of to may be itself, so the client has nowhere to go. The proof separates good facilities, which can be dropped, from bad ones, which must be swapped with a captured facility, and pays for the clients that cannot be moved through the distance between and its nearest captured facility. The combinatorial core is the construction of a permutation within each that avoids every non-capturing block and has fixed points only where they are unavoidable.
Clients and facilities are finite types Cl and Fa. The distance is a real-valued function on Cl ⊕ Fa that is nonnegative, symmetric and satisfies the triangle inequality; is not assumed, since the paper neither states nor uses it. Opening costs are a function f : Fa → ℝ with 0 ≤ f i, and demands are unit, as in the paper.
Solutions are nonempty Finsets. The service cost is (Finset.inf') and is defined only for nonempty sets, so no junk value for enters. Accordingly the drop move is considered only when a facility remains open; with at least one client, cannot serve anyone and is not a solution. Local optimality is required for all moves of : every added facility, every dropped facility and every swap, not only the moves used in the proof. The goal is stated as the multiplied-out inequality for every nonempty , never as a ratio, since may be .
In the milestones, the nearest-facility assignments , are arbitrary among the nearest ones (ties broken arbitrarily), and the family of bijections is a single permutation of the clients with . Inequality (5) assumes at least one client, which the paper assumes implicitly: with no clients and it would read . The goal and Lemma 4.2 need no such assumption.
A statement that assumes local optimality only for the moves the proof uses, that fixes to be a global optimum defined by hypotheses, or that allows the empty set a zero service cost would be a different theorem; none of these is used.
Needed infrastructure: sums over nearest-facility assignments and their fibers , the permutation , and bookkeeping of the three kinds of moves. The instance, cost and local optimality definitions are reusable for other local search analyses of metric location problems. Proofs of any milestone are welcome, as are alternative proofs of the goal.
Bilinear programs, which minimize an objective containing a term over constraints on and , model pooling and blending in petroleum refining, location–allocation, certain dynamic production problems and many other applications (Konno 1971, surveyed in Al-Khayyal and Falk 1983, p. 274). The term is not convex, so such problems can have local minima that are not global. For example, has local solutions at and . When and are constrained separately, a solution lies at an extreme point of the feasible region, and vertex-enumeration and cutting-plane methods apply. When the constraints couple and , this property is lost.
Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) gave a branch-and-bound algorithm for this jointly constrained case. It lower-bounds the objective on each box by the convex envelope of the bilinear term, and they proved that it converges to a global solution. The closed form of that envelope, found independently by McCormick (1976) and now called the McCormick envelope, underlies the bilinear relaxations of modern global solvers.
Timeline:
Fix and a box with coordinate rectangles . Problem is
with , convex (and continuous) on their boxes, closed and convex, and . Its optimal value is .
The convex envelope of a function over a set is the pointwise supremum of all convex functions that underestimate on . For a box , the node function is convex and lies below on . The subproblem at node , minimizing over , is a convex program.
A run of the algorithm is a sequence of stages. Stage has the single open node . At stage the Best Bound Rule selects an open node whose subproblem value is least, and the stage point is its subproblem solution. The best lower bound is and the best upper bound is . The selected node is then split. The algorithm picks the coordinate with the largest gap and replaces the rectangle by the four subrectangles cut out by the point (Figure 1 of the paper). All other rectangles are kept. The stage function assigns to each point of the least node value among the open boxes containing it.
For every run,
In attack order:
Theorem 4 of the paper, on the envelope of with concave , is included as a further target.
The convergence theorem certifies that the algorithm computes the global optimum of a nonconvex problem. It is not a local search. Its ingredients carry over to spatial branch-and-bound in general: envelopes that are exact on the boundary of their box, a subdivision at the relaxation's solution, and best-bound selection. Theorem 2 and its separable extension are the building block of McCormick relaxations, used for bilinear terms throughout global optimization.
As far as is known, none of these results is formalized. The mission produces a formal model of a spatial branch-and-bound procedure with rectangular subdivision at the relaxation solution, together with the convex-envelope facts it rests on. The paper's convergence proof is informal and, as printed, passes through two claims that do not hold (see Formalization scope). A machine-checked proof of the convergence theorem would settle the result on firm ground.
The algorithm splits at the relaxation's solution, not at the midpoint, so the boxes of a run need not shrink to points. The usual "exhaustive subdivision" argument, in which the diameters of nested boxes tend to zero, does not apply. What makes the gap close is Theorem 3: after a split, the split point sits on the boundary of the new rectangles in the split coordinate, where the envelope is exact. That exactness has to be carried from the selected points to their accumulation points, across coordinates that may be split finitely or infinitely often. The obvious route through a continuous limit of the stage functions is not available, because the stage functions are not continuous in general.
Vectors are Fin n → ℝ, points are pairs in (Fin n → ℝ) × (Fin n → ℝ), and boxes are four bound vectors, degenerate boxes allowed. The convex envelope is the paper's definition, the real supremum of values of convex minorants, and is used only at points of convex boxes. The McCormick closed form is Theorem 2, a target, and is not built into any definition. A run is a predicate on four sequences: open nodes as a multiset of boxes, selected node, branching index, stage point. Stages are numbered from and runs are infinite: the stopping test is ignored, so a run stopped by the paper is a prefix of one. The optional pruning of p. 278 is omitted, and ties are arbitrary. The optimal value enters through IsMinOn, not through an infimum. The Euclidean distance on is written out explicitly.
Hypotheses and corrections relative to the page:
Two trivializations are excluded. The goal is not a statement about an arbitrary sequence of boxes and points whose gap tends to zero: it quantifies over runs of the algorithm as defined, and a separate well-posedness item, run_exists, asserts that runs exist for every instance. Theorem 2 is about the supremum of convex minorants, not about a function defined by the closed form.
Reusable beyond this mission: the convex envelope and its bilinear closed form, and the box-splitting model. Contributions welcome: proofs of the envelope theorems, a proof of run_exists, and a convergence proof that avoids the false intermediate claims.
The Riemann mapping theorem says that every simply connected region of the complex plane other than the plane itself can be mapped one-to-one and conformally onto the open unit disk. It is the central existence theorem of geometric function theory: it reduces questions about analytic functions on an arbitrary simply connected region to questions on the disk, and it shows that, up to conformal equivalence, there are only two simply connected regions in the plane — the plane and the disk.
In L. V. Ahlfors' textbook Complex Analysis (3rd ed., McGraw-Hill, 1979) the theorem is Theorem 1 of Chapter 6, §1.1 (p. 230). Its proof draws on much of the preceding theory: the general form of Cauchy's theorem (through the existence of logarithms and roots on simply connected regions, Ch. 4, §4.4), Schwarz's lemma (Ch. 4, §3.4), Hurwitz's theorem (Ch. 5, §1.1) and the theory of normal families (Ch. 5, §5). This mission is the first of a series formalizing capstone results of the book.
Timeline (as recorded by Ahlfors, p. 229–230). The theorem was formulated by B. Riemann (1851). A related theorem from which it can be derived was proved earlier by W. F. Osgood; the first successful proof of the mapping theorem itself is credited to P. Koebe. The proof in the book is a shorter variant of Koebe's original proof.
A region is a nonempty, open, connected subset of the complex plane (Ch. 3, §1.3, Definition 4). The extended plane is , the one-point compactification of . A region is simply connected if its complement with respect to the extended plane, , is connected (Ch. 4, §4.2, Definition 1). This is Ahlfors' definition; it is not the usual "every loop is contractible" definition, although the two agree for plane regions. The point always lies in the complement, so, for example, a disk, a half-plane and a parallel strip are simply connected, while the punctured plane and the exterior of a circle are not.
A function is analytic in if it is complex-differentiable at every point of (equivalently, it has a convergent power-series expansion around every point of ). It is univalent in if it is one-to-one there. We write for the open unit disk.
A family of functions on is normal in if every sequence of members of has a subsequence which converges uniformly on every compact subset of (Ch. 5, §5.1, Definition 2); the limit need not belong to .
Let be a simply connected region with and let . Then there is an analytic function in with
and any two functions with these properties agree on .
The mapping theorem is the entry point to the conformal-mapping part of complex analysis: the uniqueness statement identifies the conformal automorphisms of a simply connected region with those of the disk, and the existence statement is the base case of the uniformization theorem for Riemann surfaces. It also yields the purely topological fact that any simply connected plane region is homeomorphic to a disk.
The theorem is classical and fully proved in the literature. What this mission adds is a machine-checked proof in Lean 4 / Mathlib, together with machine-checked versions of the supporting results listed above in the book's own formulations. Mathlib already contains related material (for example, Cauchy integral formulas and a derivative bound of Schwarz type, Complex.norm_deriv_le_div_of_mapsTo_ball); it should be reused wherever it applies.
The obvious approach — write down the map — is not available: for a general region there is no formula, and the map is obtained from an extremal problem (maximize over univalent maps into the disk). Three steps are delicate: showing that the competing family is nonempty (this uses the existence of a square root on , i.e. the general Cauchy theorem, applied with Ahlfors' complement-connectedness definition); showing that an extremal function exists and is still univalent (this needs normal families and Hurwitz's theorem, neither of which is a direct consequence of pointwise convergence); and showing that the extremal function is onto (a second square-root construction combined with a Schwarz-lemma-type estimate). Uniqueness requires the classification of the automorphisms of the disk.
All statements live in the namespace AhlforsComplexAnalysis, shared by the whole book series. Functions are total maps ; "analytic in " is Mathlib's AnalyticOnNhd ℂ f Ω (analytic at every point of ), and values of outside are unconstrained. Consequently the uniqueness part of the goal is stated as agreement on (Set.EqOn f g Ω), not as equality of functions. The condition is written as and , with the complex derivative deriv f. The extended plane is Mathlib's OnePoint ℂ; "connected" is Mathlib's IsConnected (nonempty and preconnected). Uniform convergence on compact subsets is stated literally: for each compact , uniform convergence on .
The hypothesis is essential and cannot be dropped: by Liouville's theorem no nonconstant bounded analytic function on exists. The hypotheses are satisfiable (for example by , ), so the goal is not vacuous.
Needed infrastructure beyond Mathlib likely includes: the equivalence of Ahlfors' simple connectivity with the vanishing of winding numbers (Ch. 4, Theorem 14) and the general Cauchy theorem on such regions; Montel's theorem in the form above; Hurwitz's theorem. These pieces are reusable well beyond this mission, and contributions of any of them — as well as proofs of the milestones — are welcome.
Rotations of three-dimensional space are the most frequently used nontrivial Lie group in physics. Quantum mechanics requires more than the rotation group itself: particles of half-integer spin, such as the electron, transform under a group in which a rotation by acts as . That group is , the double covering group of . W. Siegel's graduate text Fields (arXiv:hep-th/9912205) introduces spin through this covering in Chapter II, Section A ("Two components", pp. 110–116). It encodes a 3-vector as a traceless hermitian matrix, reads the dot and cross products off the matrix product, and realizes rotations as conjugation by unitary matrices.
This mission is the first in a series formalizing results from Fields. It covers the algebra of §IIA1–IIA3, which ends with the statement that the map is two-to-one.
Let be the complex matrices, the conjugate transpose, the transpose and the entrywise complex conjugate.
In the Lean development these are SiegelFields.IsThreeVector, vecToMatrix, basisMatrix, matC and rotationOf. Components are indexed by .
Concretely: for all ; ; every element of is some ; and exactly when or .
The covering is the basic reason spinors exist. It gives the spin- representation, explains why a rotation acts as on fermions, and is the first instance of the low-dimensional Lie algebra identifications that Siegel lists in §IC5 (such as and ). Later chapters of Fields build spinor index notation, the Lorentz group and supersymmetry on this material.
The mathematics is classical and fully proved. What this mission adds is a machine-checked version stated in the book's own conventions: its basis, its normalization of the norm () and its matrix . The result is a dictionary between Siegel's matrix notation and Mathlib's matrix groups that later missions in the series can import.
Most milestones are identities about matrices and can be checked entrywise. The substantive parts of the goal are surjectivity onto and the kernel computation. Showing that every rotation is some requires constructing from , for example from an axis and an angle or by generating from simpler rotations. It cannot be done by an entrywise identity. Pinning the kernel to requires showing that a unitary matrix commuting with all of is scalar, and then combining this with . Showing rather than needs either a connectedness argument or an explicit formula.
Matrix.specialUnitaryGroup (Fin 2) ℂ and is Matrix.specialOrthogonalGroup (Fin 3) ℝ. Unitary matrices are Matrix.unitaryGroup (Fin 2) ℂ.rotationOf U is defined for every matrix and takes the real part of a trace. The statements restrict to the unitary or special unitary group, where that trace is real.crossProduct on Fin 3 → ℝ. The book's basis corresponds to the cyclically relabelled Pauli matrices , which preserves orientation.Contributions welcome: proofs of the matrix identities, a proof of surjectivity, and connections to Mathlib's quaternion and unit-sphere API.
The Virasoro–Shapiro amplitude is the tree-level scattering amplitude of four tachyons in the closed bosonic string. Together with the Veneziano amplitude for open strings it is historically the first formula of string theory: both were written down around 1968–69 as closed-form guesses with striking properties, before anyone knew they described strings (Veneziano 1968, Virasoro 1969, Shapiro 1970). In David Tong's Cambridge Part III lecture notes on string theory, the amplitude is reduced in Section 6.2.2 to a single integral over the complex plane, and the whole physical content of the answer (the symmetry in the Mandelstam variables, the infinite tower of poles at the string masses, the soft high-energy behaviour) is read off from the closed form of that integral in terms of Euler's Gamma function, eq. (6.11). The evaluation itself is carried out in the Appendix, Section 6.5.
For complex numbers define the Virasoro–Shapiro integral
where, following Tong's convention, for (twice Lebesgue measure on ). Powers of the positive reals and are . The integral converges absolutely exactly when
the three conditions controlling integrability near , near and at respectively. denotes Euler's Gamma function, defined by for (eq. (6.26)) and continued analytically.
In the physics application and are determined by the tachyon momenta, and the three Gamma-function ratios become and its analogues (eq. (6.12)).
For with ,
The result. Eq. (6.11) is what turns the four-point function (6.10) into the Virasoro–Shapiro amplitude (6.12). Every property Tong extracts in Section 6.2.3 — the manifest symmetry, the poles at reproducing the closed-string mass formula, and the exponential fall-off at high energy — is a property of the Gamma-function expression, not of the raw integral. The same integral (with general exponents) is the basic building block of Coulomb-gas computations in two-dimensional conformal field theory (Dotsenko–Fateev 1984).
Formalizing it. The identity is classical and its proof is elementary but analytically delicate. No machine-checked proof of the complex-plane integral is known to the mission author. A formal proof requires a reusable toolkit: Fubini–Tonelli manipulations of absolutely convergent iterated integrals with complex powers, two-dimensional Gaussian integrals, and a polar/affine change of variables on . The Beta integral (milestone 1) is already in Mathlib.
Each step of the textbook computation interchanges the order of integration in an integral with integrable but unbounded singularities at , and at infinity, so each interchange must be justified by absolute convergence under exactly the three conditions above. The naive approach of applying Fubini directly to the original integrand in Cartesian coordinates does not factor; the proof in the notes instead introduces two auxiliary Gamma-function integrals, making the integral four-dimensional before any variable is integrated out, and the justification of Tonelli for that four-dimensional integrand is the main technical point.
The integral is TongString.virasoroShapiroIntegral a b, defined as 2 * ∫ z : ℂ, (‖z‖ : ℂ) ^ (2a-2) * (‖1-z‖ : ℂ) ^ (2b-2), the integral being the Bochner integral against Lebesgue measure on ; the factor implements . Complex powers are Mathlib's principal-branch cpow applied to non-negative real bases, which agrees with for (the point , is a null set). The parameters are complex; the notes use real Mandelstam-type exponents, which are a special case. Since the Bochner integral of a non-integrable function is in Lean, every statement carries the convergence hypotheses; with them the integral is a genuine absolutely convergent integral, so the goal cannot be satisfied vacuously. The Gamma function is Mathlib's Complex.Gamma.
Contributions welcome: proofs of any milestone, and general lemmas on iterated integrals over with complex-power weights, which are reusable for other Selberg- and Dotsenko–Fateev-type integrals.
The MDL and Occam principles of Chapter 7 rank hypotheses by description length and pay for a hypothesis according to its rank. Chapter 31 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), generalizes this to the PAC-Bayesian approach of McAllester: prior knowledge is a prior distribution over the class, the learner outputs a posterior , read as the randomized predictor that draws , and the price of is its Kullback–Leibler divergence from . The PAC-Bayes theorem (Theorem 31.1) says that with probability , simultaneously for every posterior, the generalization loss exceeds the training loss by at most . Its proof is a compact and elegant argument: Markov's inequality for an exponential moment, a change of measure from to by Jensen's inequality, an exchange of expectations that is possible because the prior does not depend on the sample, and a moment bound for the deviation of a single hypothesis. The bound suggests the learning rule of Remark 31.1, minimize plus the divergence penalty, which is regularized risk minimization in disguise, and for a finite class with a uniform prior it recovers an Occam-type bound (Exercise 2).
is a measurable space of hypotheses, a jointly measurable loss, a distribution over , and a prior probability measure on . For a posterior , , and , and is the Kullback–Leibler divergence, a real number when and the log-density is -integrable.
For and , with probability at least over , every probability measure with finite divergence satisfies
The identity (§31.1); the moment bound of the proof (p. 417); Exercise 2, the bound for a finite class with the uniform prior.
PAC-Bayes bounds are among the tightest generalization bounds known in practice, and the reason is visible in Theorem 31.1: the complexity term is not a property of the class but of the posterior actually chosen, measured against a prior, so a learner that stays close to its prior generalizes even in a huge class. The theorem is the ancestor of a large literature (Seeger, Langford, Catoni, Maurer) and of modern nonvacuous bounds for neural networks. Formally it is a pleasant target: the change-of-measure inequality is the Donsker–Varadhan inequality, of independent value, and the moment bound is a sharp sub-Gaussian fact. On the platform, the mission introduces Gibbs risks and the Kullback–Leibler divergence between measures on a class, ending the book's series with its last learning principle.
The Gibbs risk identity is Fubini for a bounded jointly measurable function. The moment bound is the delicate step: the book derives it from Hoeffding's tail bound through Exercise 1, whose one-sided hypothesis is not enough (a constant negative variable satisfies it with an unbounded moment), and even the two-sided tail integrates only to ; the claim is nevertheless true, for instance by writing for a standard Gaussian and applying Hoeffding's lemma to the sample mean, which gives . Theorem 31.1 then follows the book: Markov's inequality on with , the change of measure (31.2) by Jensen's inequality for applied to the density (the Donsker–Varadhan inequality, which needs and an integrable log-density), the exchange of expectations (31.4) by Fubini, the moment bound, and finally Jensen for in (31.6); formally the supremum over all posteriors is handled by proving the bound for each on the event , whose complement has probability at most by Markov, which sidesteps any measurability question about . Exercise 2 is the theorem with , for which .
The class is an arbitrary measurable space, priors and posteriors are probability measures on it, and is Mathlib's Radon–Nikodym derivative; the divergence is a Bochner integral, so the theorem quantifies over posteriors whose log-density is -integrable, exactly the posteriors with a finite divergence, for which the bound has content, and no junk value can make a case false. Posteriors may depend on the sample: the statement bounds the outer measure of the set of samples for which some admissible violates the bound. The loss is jointly measurable so that and are measurable and the Gibbs risks are genuine integrals; is forced by the denominator . The moment bound is stated as the claim the proof needs rather than as Exercise 1, whose printed hypothesis is insufficient; the item text records this. Exercise 2 is stated as a simultaneous bound over the finite class, the form in which the theorem delivers it.
Not stated: Remark 31.1 (a learning rule, not a theorem), Exercise 1 as printed, and the second part of Exercise 2.
A feedforward neural network is a directed acyclic graph of neurons, each computing a fixed scalar activation of a weighted sum of its inputs; fixing the graph and the activation and letting the weights vary gives a hypothesis class. Chapter 20 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), studies these classes through the book's three lenses. Approximation: every Boolean function is implemented by a network of depth 2 (Claim 20.1), but only at exponential size (Theorem 20.2), while a sign neuron implements conjunctions and disjunctions (Lemma 20.4), the bridge to Boolean circuits and hence to everything computable in bounded time. Estimation: the VC dimension of the class of sign networks over a graph with edges is (Theorem 20.6), so the sample complexity is governed by the number of weights. Optimization: training is NP-hard even for tiny networks, and the practical answer is SGD with the gradient computed by backpropagation, whose correctness the chapter derives from the chain rule.
A layered graph has layers , every edge joining to ; holds the inputs and a constant neuron outputting . With weights and an activation , the outputs are computed layer by layer, and . The class (20.1); for binary classification the output layer is a single neuron and is the sign function, so is a set of -valued predictors on . The size of the network is , its depth . The growth function extends to classes with any finite codomain (p. 275), and the proof of Theorem 20.6 uses two of its properties, stated as Exercises 3 and 4: the growth function of a product class is at most the product of the growth functions, and likewise for a composition class. For backpropagation the activation is any differentiable and the loss is ; the backward pass sets and .
The VC dimension of is . Explicitly, for a layered graph of depth at least with a single output neuron,
stated as: every satisfies this bound (so the VC dimension is finite).
Claim 20.1 (the depth-2 graph with whose sign class contains every function ); Theorem 20.2 (every sign network implementing all functions has ); Lemma 20.4 (conjunction and disjunction as sign neurons); Exercise 4 (growth function of a composition); the correctness of backpropagation (§20.6: the partial derivative for the edge is ). Further items: Exercise 3 (growth function of a product) and the intermediate bound of the proof of Theorem 20.6.
Theorem 20.6 is the reason networks are learnable at all in the book's sense: by the fundamental theorem, a class with finite VC dimension is agnostic PAC learnable with sample complexity linear in that dimension, and here the dimension is essentially the number of tunable parameters. The proof technique, due to Kakade and Tewari's lecture notes, is a composition-and-product argument on growth functions that applies to any layered class of threshold units and is reusable well beyond this chapter. Theorem 20.2 is the matching negative fact on expressive power, and it is a corollary of the same bound: a class that shatters points needs edges. Backpropagation's correctness is the one theorem about training the chapter can offer, given the hardness results, and it is the algorithm every practitioner runs.
Claim 20.1 and Lemma 20.4 are explicit constructions: the neuron detects because otherwise, and the output neuron takes the disjunction; formally one must build the weight function and evaluate the forward pass on the inputs. Exercises 3 and 4 are counting: a restricted product is determined by its two restricted factors, and a restricted composition on is determined by and , with . Theorem 20.6 then needs: the class of one neuron is the class of homogenous halfspaces on its incoming coordinates, of VC dimension at most (Mission VI), Sauer's lemma in the form for every (Mission IV; for use ), the layer class as a product and the network as a composition of layer classes, and finally the arithmetic , which replaces the book's appeal to Lemma A.2 (for one has ). Theorem 20.2 follows from the goal with . Backpropagation is a chain-rule computation in a single real variable: the loss as a function of one weight is a composition of finitely many differentiable maps, and the derivative unwinds to the backward recursion; the formal effort is in the induction along layers with the natural-number indexing of the model.
Layers and neurons are indexed by natural numbers: a LayeredGraph records the depth, the layer widths and, for each , the finite set of edges as pairs within the layer widths. Weights are functions on all index triples, and only those on edges are used, so the class is the image of all weight functions, as in (20.1). The forward computation netOutput is a recursion on the layer index; netInput is . The sign activation returns with , the book's convention elsewhere, and a neuron with no incoming edges outputs (p. 270). The binary class signNetClass n G is Bool-valued, true iff the output neuron's input is positive, and is stated for graphs of depth at least (for depth the edges out of the input layer would be used but not counted in ). Growth functions with finite codomain are growthY, an sSup over restriction sizes, well defined because the codomains are finite; the Bool case is Mission IV's growth, and VC dimension and shattering are Mission IV's. Theorem 20.6 and Theorem 20.2 are given with explicit constants derived from the proof, since statements have no formal content; the drafter verified numerically for up to and at , and . Backpropagation is stated for an arbitrary layered graph (phantom edges have weight , p. 279), any differentiable activation, and one edge at a time as a HasDerivAt of the loss in that weight; is defined by recursion on . The book's layer indices in (20.3) are shifted by one in the statement.
Not stated: Theorem 20.3 (Turing machines), Theorem 20.5 and Exercise 1 (sigmoid approximation, which needs a convention for outputs in that the chapter leaves open), Theorem 20.7 and Exercise 6 (NP-hardness), Exercise 5 (the sigmoid lower bound, which assumes an exact threshold), the sigmoid half of Theorem 20.2, and the SGD pseudocode of §20.6, which is a heuristic without a stated guarantee.
Whether the gravitational field must be quantized is a long-standing foundational question. A well-known family of arguments tries to settle it by consistency alone: if a classical field were coupled to a quantum system, some basic principle — momentum conservation, the uncertainty relations, or the impossibility of superluminal signalling — would allegedly be violated. The two best-known versions are the gedanken experiment of Eppley and Hannah (1977) and the measurement-theoretic argument of DeWitt (1962).
Albers, Kiefer and Reginatto (Phys. Rev. D 78, 064051 (2008)) re-examine both arguments. Their paper is largely conceptual, but several of its steps are precise, checkable mathematical claims. This mission collects those claims and makes them machine-checkable.
Timeline.
Photon pair and detector (Sec. II). Each photon carries a polarization qubit with orthonormal basis (horizontal) and (vertical). A detector with state space (an arbitrary complex inner-product space) is coupled to photon 1. Before the measurement the joint state of photon 1, photon 2 and the detector is
and after the detector has measured photon 1 it is
The reduced density operator of photon 2 is obtained from by tracing out photon 1 and the detector; the paper asserts that for both states it equals
Mass cube and gravitational wave (Sec. III B). The disturbance of the averaged energy density of the scattered wave depends on the cube's edge length and speed , with sensitivities and . With and the uncertainty has a strictly positive lower bound.
DeWitt's argument (Sec. V). A system observable reconstructed from apparatus data has uncertainty , where is the coupling constant.
For all unit vectors ,
The goal is the precise content of the paper's rebuttal of the superluminal-signalling branch of the Eppley–Hannah argument: the state of photon 2 accessible to a probe (such as a classical gravitational wave) is the same whether or not photon 1 has been measured, so a probe of photon 2 alone cannot tell whether photon 1 was measured. Milestones 3–6 are the quantitative estimates the paper uses in Sec. III B (a coupling to a test body obeying the uncertainty principle transfers a minimum uncertainty to the classical wave) and Sec. V (DeWitt's limitation on a single observable, Eq. (64)).
The results are elementary once stated; the value of the mission is to pin the paper's claims down exactly, including the hypotheses under which they hold. None of the statements has, to our knowledge, a machine-checked proof on the platform.
The goal and Milestones 1–2 need a workable representation of the partial trace over a factor that is an arbitrary (possibly infinite-dimensional) inner-product space; the cross terms between the two branches vanish because the two branches are orthogonal on photon 1, not because of any property of the detector states. Milestones 3–6 are single-variable optimization statements; the main care is in the side conditions (positivity, excluding and ).
The book The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) develops a perturbative, physics-style theory of wide deep neural networks. Every later computation in the book, from the statistics of preactivations at initialization to the neural tangent kernel, reduces to Gaussian expectations of polynomials. The single tool that evaluates these expectations is Wick's theorem (eq. 1.45), which the authors ask the reader to "put a box around". This mission formalizes Chapter 1, §1.1 (Gaussian Integrals), culminating in that theorem. It is the first mission of a series formalizing the book, all in the Lean namespace DeepLearningTheory.
Fix and a symmetric positive-definite real matrix , the covariance. Write for its inverse. The zero-mean multivariable Gaussian distribution with covariance (eq. 1.31) has density on
and the expectation of an observable is (eqs. 1.36, 1.46), an integral against Lebesgue measure. A pairing of the labels is a partition into unordered pairs; equivalently, a fixed-point-free involution of pairing with . There are pairings.
For all indices (repetitions allowed),
Wick's theorem (also known as Isserlis' theorem, 1918) is used throughout the book: the Gaussianity of the first layer (Chapter 4), the four-point correlators of deep linear networks (Chapter 3), and all perturbative expansions around the infinite-width limit are evaluated by Wick contractions. A machine-checked version stated in the book's own density-based conventions gives later missions of this series a dependable foundation. The result is classical; the work remaining is its formalization in exactly this form. A related statement for general (possibly degenerate) Gaussian measures already exists on the platform as FeynmanWick.wick_theorem_gaussian; the present mission keeps the book's formulation via the explicit density and a positive-definite covariance.
The book's derivation differentiates the generating function (1.41) times at , which requires justifying differentiation under the integral sign and organizing the combinatorics of the product rule into pairings. Both the analytic step (dominated convergence for Gaussian tails, in dimensions) and the combinatorial step (a bijection between surviving terms and pairings, with the normalization) are routine on paper but need care in Lean. Computing the normalization (1.30) itself requires diagonalizing and a linear change of variables.
Fin N → ℝ with Lebesgue measure; is a Matrix (Fin N) (Fin N) ℝ with K.PosDef (which includes symmetry). The inverse is Mathlib's K⁻¹.gaussianDensity K z and gaussExpect K F are exactly the book's and ; gaussQuadForm K z is .pairings (2m) is the finite set of fixed-point-free involutions of Fin (2m); the product is over labels with , so each pair contributes once.A magnetohydrodynamic (MHD) equilibrium is a magnetic field and a scalar pressure on a region of satisfying
Under the substitution these are exactly the equations of a steady incompressible Euler flow, with replaced by the Bernoulli function, so every statement in this mission is simultaneously a statement about stationary solutions of the 3D Euler equations. Magnetic confinement of a fusion plasma requires equilibria whose pressure surfaces are nested tori, because forces to be constant on the surfaces swept out by field lines.
Whether such equilibria exist without a continuous symmetry has been open since Grad, who conjectured in 1967 that smooth toroidal equilibria with non-constant pressure do not exist unless the configuration is symmetric (for instance axisymmetric), and restated the claim in 1985 as the assertion that, apart from the symmetric exceptions, there are no families of solutions depending smoothly on a parameter. Modern formulations of the conjecture appear in the work of Constantin–Drivas–Ginsberg (2021), Enciso–Luque–Peralta-Salas (2025) and Cardona–Duignan–Perrella (2025, Conjecture 2.5). Partial results have always relaxed something: Lortz (1970) obtained non-symmetric toroidal equilibria only with mirror symmetry and vanishing rotational transform; Bruno–Laurence (1996) and Enciso–Luque–Peralta-Salas (2025) allow discontinuous pressure and current sheets; Weitzner–Sengupta (2020) work in a topological torus rather than true toroidal geometry; near-axis and high-aspect-ratio expansions (Mercier 1964, Garren–Boozer 1991) give only approximate solutions.
Landreman (2026) exhibits explicit, fully non-axisymmetric, smooth analytic solutions on a genuine solid torus, with exact nested flux surfaces, finite aspect ratio and non-zero rotational transform. This mission formalizes the first of the two families presented there — the family with uniform rotational transform — in Lean 4.
Fix a parameter and set , . For a Cartesian point (written in the paper) define
and the vector field
The natural domain is the open set , on which and all the expressions above are smooth. With
the flux label and the pressure are
where is an arbitrary constant. The level sets of are the pressure surfaces. For the region is a solid torus bounded by a -surface, and this is the plasma domain.
Field lines are described by a second coordinate system. For labels with , putting and , the position map is
The curve is an integral curve of , the pair labels the field line, and acts as a toroidal angle of period . The magnetic axis is the field line , , on which ; it is the non-planar closed curve .
The goal theorem asserts that for every , every and every constant , the pair above is a smooth equilibrium on that is genuinely three-dimensional:
together with smoothness of and on and the failure of axisymmetry: there is a rotation about the axis and a point of whose image lies in and carries a different pressure.
The milestones are the individual equations of Section 2 of the paper: divergence-freedom, the tension identity , force balance, invariance of along , the field-line position map and its Jacobian , the expressions and in field-line labels, the magnetic axis, the enclosed volume , the uniform rotational transform , and the averages and .
The solutions contradict the strict formulation of Grad's conjecture used in the recent literature (for example Conjecture 2.5 of Cardona–Duignan–Perrella), since they are smooth, have non-constant pressure, exact nested toroidal flux surfaces, no continuous Euclidean symmetry, finite aspect ratio and non-zero rotational transform, and they form continuous families parameterized by and . Because MHD equilibrium is isomorphic to steady Euler flow, the same objects are explicit non-symmetric stationary Euler flows with invariant tori. They also serve as exact benchmarks for numerical equilibrium codes, where analytic three-dimensional solutions with known flux surfaces are otherwise unavailable.
The paper's derivations are elementary but long: they are algebraic identities among square roots and rational functions, verified in the paper by hand and by supporting numerical scripts. A machine-checked development removes the remaining doubt about sign conventions and domains, which is precisely what a counterexample to a conjecture requires. Nothing in this development is currently formalized in Mathlib: there is no curl, no divergence, and no notion of MHD equilibrium, so the mission also produces a small reusable vector-calculus layer on .
Force balance is an identity between derivatives of expressions containing and division by ; differentiating it directly produces large expressions whose simplification needs the domain hypotheses ( and positive radicand) at every step, so field_simp-style automation must be driven with those side conditions in hand. The statements about field-line coordinates require knowing that the position map is a diffeomorphism onto its image, which the paper establishes by a covering argument rather than by computation. The transform is the hardest milestone: it is a winding-number statement about the poloidal displacement of a field line relative to the magnetic axis, and the paper's proof is a continuity-in- argument, which in Lean needs an honest treatment of continuous angle lifts. The volume and average identities need the change of variables theorem with the constant Jacobian over a solid torus.
Points of space are Fin 3 → ℝ; partial derivatives are fderiv applied to the standard basis vector, and gradient, divergence, curl, cross product, the directional derivative and the tension are defined from it in the first definition file. Squared length is , so the Pi-type norm is never used. All the paper's objects — , , , , , , , , , , , , , , rotation about the axis, and the complex poloidal displacement used for the transform — are given in the second definition file, in the same notation as this description. Smoothness is ContDiffOn ℝ ⊤; volumes are the Lebesgue measure on Fin 3 → ℝ; integrals are Bochner integrals.
Everything is stated with the explicit field of Section 2 rather than an abstract existence claim, so no statement can be satisfied by a degenerate or symmetric configuration. The equilibrium conditions are asserted pointwise on , which is open and non-empty for , so no milestone is vacuous. Contributions of the auxiliary calculus lemmas (differentiability of , and on , and the product and quotient rules in this partialD formulation) are welcome and reusable by the companion family of Section 3, which is not part of this mission.
Chapter 3 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks how many random examples suffice to learn a concept from an infinite class. The cardinality bound of Occam's Razor is useless there, yet the rectangle game of Chapter 1 shows that some infinite classes are learnable from a finite sample. The answer is the Vapnik–Chervonenkis dimension: the size of the largest set on which the class realizes every labeling. Sauer's lemma says that a class of VC dimension realizes only labelings on any points, polynomially many rather than , and the ε-net theorem of Blumer, Ehrenfeucht, Haussler and Warmuth turns this into a sample bound: a consistent hypothesis from a class of VC dimension is probably approximately correct once is of order . A matching lower bound shows that examples are necessary. The chapter thus gives a single combinatorial parameter that characterizes, up to a logarithmic factor, the sample complexity of learning any class in the distribution-free model.
For a class of concepts and a finite , is the set of dichotomies of realized by ; is shattered if all are realized; is the supremum of the sizes of shattered sets, possibly ; is the largest over ; and is defined by , . For a target the error regions are for in the hypothesis class, and a set of points is an ε-net if it meets every error region of weight at least under the target distribution . Samples, their product law, consistency and the error of a hypothesis are those of Mission I.
Let be a class of VC dimension at most , well-behaved for the target (the double-sample event of the proof is null-measurable), and . The points of a random sample of examples of a target fail to be an ε-net for the error regions with probability at most
so any algorithm that outputs a hypothesis in consistent with its sample has error greater than with at most that probability; with and the probability is at most ; and, if is nonempty, every class contained in for whose targets is well-behaved is PAC learnable using .
Lemma 3.1 (Sauer's lemma, ); Lemma 3.2 (); the polynomial bound of p. 57; Theorem 3.5 (the lower bound, in the two explicit forms of its proof).
Theorem 3.3 is the fundamental theorem of PAC learning: it replaces in Occam's Razor by the VC dimension and thereby covers rectangles, halfspaces, polygons, neural networks with a fixed architecture, and every class whose dichotomies grow polynomially. Its proof, the double sample and random partition argument, is the origin of symmetrization in empirical process theory. Sauer's lemma is a cornerstone of extremal combinatorics with independent proofs by Sauer, Shelah and Vapnik–Chervonenkis, and the lower bound of Theorem 3.5 shows that the upper bound is tight to within , so the VC dimension genuinely characterizes sample complexity. None of these is machine-checked. Formalizing them puts on the platform the VC dimension, the growth function and the ε-net theorem with explicit constants, stated on the same sample law as the rest of this series, and the first information-theoretic lower bound for learning.
Sauer's lemma is a double induction on and through the auxiliary class of dichotomies whose two extensions to a distinguished point are both realized, which needs care with the identification of dichotomies of and of . The ε-net theorem needs: the reduction from a failed ε-net on the first half to a region hit at least times by the second half, which is a Chebyshev bound on a binomial variable and is where enters; the exchangeability of the draws with a random partition into two halves; the counting bound ; and Sauer's lemma applied to the error regions, whose growth function equals that of . The explicit constants require the numerical inequality under the two stated conditions. The lower bound is a probabilistic argument with a random target: conditional on the sample, the labels of unseen points are fair coins, so the number of errors on them is binomial and exceeds half its range with probability at least ; the refined bound scales this construction to a region of weight and uses Markov's inequality to bound the number of draws landing in it. Measurability of the failure sets is avoided by stating outer-measure bounds, except for the double-sample event, which the proof integrates: it is assumed null-measurable (the well-behavedness of Blumer et al., without which the theorem is false for a class of VC dimension on ). For the lower bound it is avoided by working over a finitely supported distribution on a space with measurable singletons.
The VC dimension is a supremum in , the growth function a supremum in (bounded by ), and the book's recurrence, with its closed form and polynomial bound stated as separate theorems. The goal is stated for a hypothesis class (Theorem 3.4), Theorem 3.3 being the case ; it carries the exact bound of the proof, the explicit constants of Blumer et al. in place of the book's , the requirement of the proof's Chebyshev step, measurability of the hypotheses and the target, well-behavedness of for the target, and . PAC learnability of the subclasses of needs nonempty, since no algorithm outputs hypotheses in the empty class. The lower bound is stated for every deterministic learning function, on an instance space with measurable singletons, for a class shattering some set of points, with the explicit constants derived in the proof sketch (: error with probability ; and : error with probability ). Running time is not modelled. The composition bound for layered networks (Theorems 3.6 and 3.7) is not stated.
Trivializing readings are excluded: the ε-net event ranges over every hypothesis of , the failure bounds are uniform over all consistent learners, and the lower bound holds for every learning function. Welcome contributions: Sauer's lemma, the closed form and the bound, the random-partition counting lemma, and the binomial median inequality used in the lower bound.
A decision-maker has projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number , computable for each bandit process from its own data and its own current state , such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.
The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.
A bandit process (§2.3–2.4) is a Markov reward process on a countable state space : transition probabilities , a bounded reward received each time the continuation control is applied in state , and a discount factor ; the freeze control leaves the state unchanged and yields nothing. The law of the process started at is and is its state at process time . A stopping time is a past-measurable rule for switching from continuation to freezing, taking values in . For such , is the expected discounted reward and the expected discounted time; their ratio (2.7) is the equivalent constant reward rate of that portion of . The Gittins index is
and, equivalently, the fair charge (2.5): the greatest rent per period for which continuing for one or more periods, paying each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted -valued maps on trajectories, and gittinsIndex P r a x is (2.6).
The supremum in (2.6) is attained. For the initial state , the attaining stopping rule may be taken to be "stop at the first time at which the state lies in " for any set with
and every such rule has .
Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at .
Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.
Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.
The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge , whose value function satisfies , together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities and . That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is , not , because restarting forever is free.
The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; . The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes everywhere, so and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time of a set, with when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over , a nonempty set bounded above. The restart iteration is stated as a limit, with the value : for a nonnegative index this is the book's , and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under , written as events of measure one.
Two trivializing readings are excluded: the index is never taken over all -valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.