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?
Expander graphs are sparse graphs in which every set of vertices has many neighbours. Families of them with bounded degree and expansion bounded away from zero are a basic tool of theoretical computer science: they are the main component of the sorting network of Ajtai, Komlós and Szemerédi (AKS 1983), the building block of superconcentrators and other graphs with strong connectivity properties, and an ingredient of many later constructions in coding theory, derandomization and complexity.
Expansion is hard to certify. Checking that every set of vertices has many neighbours means looking at exponentially many sets, and computing the exact expansion of a graph is coNP-complete. A spectral quantity, by contrast, is computable in polynomial time. N. Alon's paper Eigenvalues and expanders (Combinatorica 6 (1986) 83–96) proves that for regular bipartite graphs the two notions are equivalent: a graph is a strong expander if and only if the second-smallest eigenvalue of its Laplacian is bounded away from 0, with explicit constants in both directions. This is a discrete counterpart of Cheeger's inequality for Riemannian manifolds.
Timeline.
All graphs are finite and simple. For a graph and a set , is the set of neighbours of ; it may meet .
The Laplacian of is , where is the 0–1 adjacency matrix and the degree of . It is symmetric with eigenvalues , counted with multiplicity, and is its second-smallest eigenvalue. It is positive exactly when is connected.
Let be a -regular bipartite graph with and .
Part (1) of the goal combines Lemmas 3.1 and 2.4; part (2) follows from Lemma 3.3.
The result. Theorem 3.4 makes expansion of regular bipartite graphs checkable in polynomial time up to a constant-factor loss. A random regular bipartite graph can be generated and its expansion certified by computing one eigenvalue. Lemma 2.4 is one of the first discrete Cheeger inequalities. Together with Corollary 2.3 it shows that magnifiers and enlargers are the same graphs up to the constants, and it underlies the later theory of spectral expanders, including the Alon–Boppana bound and Ramanujan graphs.
The formalization. The results are proved in the paper. The work is to formalize the known proofs. That includes Tanner's eigenvalue bound, which the paper only cites, and a max-flow min-cut argument, for which Mathlib has no general theorem. No machine-checked version of Lemma 2.4, Lemma 3.1, Lemma 3.3 or Theorem 3.4 is known to exist. Lemma 2.2 is already stated and proved on the platform as part of the Alon–Milman mission.
The direction "eigenvalue gap implies expansion" is a variational argument on the spectrum of . The converse is the hard one. A first attempt bounds from below by testing the Rayleigh quotient on indicator vectors of sets. That only gives upper bounds on : any one test vector does. A lower bound has to control every vector orthogonal to the constants at once. The paper first reduces to the positive part of an eigenvector (Eq. (2.1)). It then turns the combinatorial expansion of the graph into an analytic inequality for that function, using a network flow whose existence comes from the max-flow min-cut theorem. Step (ii) of the flow conditions printed on p. 87 is false as stated: the arcs of the network absorb part of the flow. The flow argument has to be repaired before it can be formalized.
Lemma 3.1 has its own obstacle: one-sided expansion of inputs must be converted into expansion of arbitrary vertex sets that mix inputs and outputs. This needs the strong form of expansion; for ordinary expanders the lemma is false.
Graphs are SimpleGraph V on a Fintype. A bipartite graph lives on the sum type I ⊕ O, and IsIOBipartite forbids edges inside I and inside O. Cardinalities are Set.ncard. "Maximal degree " is read as G.maxDegree ≤ d; every statement is monotone in or fixes by regularity (G.IsRegularOfDegree d). The condition is written in . All constants are real, and every subtraction and division is taken in .
Reused published items:
AlonMilman.Diameter.lambda1, the second-smallest eigenvalue of G.lapMatrix ℝ, which is by convention on fewer than two vertices.AKSSorting.Core.neighbours.AlonMilman.Diameter.theorem_2_5, which carries Alon–Milman's standing hypotheses that is connected and ; outside them the inequality is trivial.The page omits a few degenerate cases, and the following hypotheses are added for them. Each is necessary, with a counterexample recorded in the item's statement:
Eq. (2.1) is stated in multiplied form, so no quotient by appears.
The closing sentences of Theorem 2.5 and Theorem 3.4 ("Thus … one can prove efficiently …") are not formalized. Read as implications between expanders they reduce to monotonicity in , because ; their content is algorithmic.
Several encodings would trivialize the mission and are excluded:
Contributions are welcome:
Every linear program comes with a second linear program, its dual, whose feasible solutions certify bounds on the optimum of the first. The duality theorem of linear programming says that these certificates are perfect: when both programs are feasible, the best bound equals the optimum. The theorem underlies the analysis of the simplex method, sensitivity analysis and shadow prices in operations research, the minimax theorem for zero-sum games, max-flow/min-cut and König-type min-max theorems in combinatorial optimization, and the primal–dual design of approximation and online algorithms.
The Farkas lemma, a theorem of the alternative for linear systems, contains the essence of duality: a system of linear equations or inequalities either has a (nonnegative) solution, or a single linear combination of its rows proves that it has none. It goes back to Farkas (1902) and Minkowski's work on finitely generated cones; the duality theorem itself is due to von Neumann (1947) and Gale, Kuhn and Tucker (1951).
This mission formalizes Chapter 6 of Matoušek and Gärtner's textbook Understanding and Using Linear Programming (Springer, 2007): the duality theorem in the book's form, weak duality, the Farkas lemma in its algebraic, geometric and three-variant forms, and the lemmas of two self-contained proofs of the Farkas lemma, one analytic (nearest points in finitely generated cones) and one via minimally infeasible systems.
Let be a real matrix with rows and columns, , . Vector inequalities are componentwise. The primal and dual linear programs are
A feasible solution of (P) is an satisfying its constraints; an optimal solution is a feasible with for every feasible . (P) is unbounded if its objective takes arbitrarily large values on feasible solutions. For the minimization (D) the notions are mirrored: an optimal has for all feasible , and (D) is unbounded if takes arbitrarily small values.
For , the convex cone generated by them is ; a primitive cone is one generated by linearly independent vectors. A system of inequalities is minimally infeasible if it has no solution but dropping any one inequality makes it solvable.
For (P) and (D) as above, exactly one of the following occurs:
LinearOptimization.farkas_lemma (Proved) and linked as a reference.Polyhedral.isClosed_conicSpan, Proved); hence it has a point nearest to any .The result. The duality theorem converts optimality into feasibility: a pair of primal and dual feasible solutions with is a short, checkable certificate that both are optimal, and the theorem guarantees such a certificate exists whenever an optimum does. It classifies every primal–dual pair into four behaviours and excludes the other five combinations of feasible-bounded, unbounded and infeasible. Later chapters of the same book rest on it: the minimax theorem for zero-sum games, the integrality of bipartite matching polytopes, the LP rounding for unrelated-machine scheduling, and the Delsarte bound for codes.
Formalizing it. All results here are classical and fully proved in the book; the work is formalization. Mathlib contains a Farkas lemma for proper cones in Hilbert spaces and closedness facts for finitely generated cones, and the platform already has Bertsimas–Tsitsiklis-style duality for a general-form minimization (LinearOptimization.lp_strong_duality) and matrix Farkas lemmas. What is missing is the textbook statement in Matoušek's inequality form (P)/(D), with its four-case exclusive classification, together with the chain of named lemmas that make two different elementary proofs of the Farkas lemma machine-checkable. The analytic chain (6.5.x) and the minimally-infeasible chain (6.6.x) are reusable independently of LP.
Weak duality is a two-line computation. The difficulty is entirely in the reverse direction, that a feasible bounded (P) forces the dual to be feasible with the same value. Any proof must use something beyond linear algebra over : either the termination of the simplex method with an anticycling rule, a topological fact (a finitely generated cone is closed), or an extremal argument (an optimal solution of an auxiliary LP). The naive geometric argument — take the nearest point of the cone to — fails without closedness, and closedness of the cone generated by a set is false for infinitely generated cones (the cone over a disc touching the origin is an open half-plane plus a point), so finiteness has to be used, which is the role of the primitive-cone decomposition. In the four-case theorem itself, the remaining obstacle is attainment: "bounded and feasible" must be upgraded to "an optimum exists" for both programs, which is not a consequence of Farkas-type statements alone.
Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; the book's indices become . The row vector is Aᵀ *ᵥ y, so is 0 ≤ Aᵀ *ᵥ y; scalar products are ⬝ᵥ.sSup/sInf is used, so no junk value of an empty or unbounded supremum enters. "Exactly one of the four cases" is ∃! k : Fin 4, DualityCase A b c k, with the book's case at index ; a plain disjunction would be weaker than the book.EuclideanSpace ℝ (Fin m), so the nearest point of Lemma 6.5.1 is Euclidean and is the inner product. The convex cone generated by is the set of nonnegative combinations (it contains , also for ).IsClosed.exists_infDist_eq_dist) are not separate targets. The Fourier–Motzkin elimination of §6.7 has no numbered result.Many design problems in control, finance and operations research are convex programs with uncertain constraints: a decision must satisfy for a parameter that is not known in advance. Enforcing the constraint for every possible (robust optimization) is often intractable or too conservative, and a chance-constrained formulation needs the distribution of , which in practice is rarely known. The scenario approach replaces the uncertain constraint by the constraints of observed samples and solves the resulting ordinary convex program. The question it answers is how much of the unseen uncertainty the resulting decision still violates.
The answer, the generalization theorem of the scenario approach, is distribution-free: the probability that the scenario solution violates more than a fraction of the uncertainty is bounded by a binomial tail that depends only on and on the number of decision variables. This mission formalizes that theorem as it is presented in Chapters 3 and 5 of Campi and Garatti's textbook Introduction to the Scenario Approach (SIAM/MOS 2018), the first mission of a series on the book.
Timeline. Calafiore and Campi introduced scenario programs and bounded the violation of their solutions through the count of support constraints (Math. Program. 2005; IEEE TAC 2006). Campi and Garatti proved in 2008 that the binomial-tail bound of Theorem 3.7 holds for every convex scenario program under existence and uniqueness of the solution, and that it is attained with equality by fully supported problems (SIAM J. Optim. 2008), which settled the tightness question. The textbook (DOI 10.1137/1.9781611975444) presents the theorem with a complete proof for fully supported problems in the plane.
Fix a cost vector , a domain , a measurable space of uncertainty instances with a probability , and a constraint set for each .
A solution is a feasible point of least cost. With i.i.d. samples its solution is denoted ; it is a random vector, a function of the sample, and is a random variable in .
For and every , under Assumptions 3.4 and 3.6,
The right-hand side is the upper tail of a Beta distribution. The statement leaves , and the constraint family completely unspecified beyond the two assumptions.
Theorem 3.7 is what makes the scenario approach usable as a design method: it certifies the reliability of a decision computed from data without any knowledge of the data-generating distribution, requiring only independence of the samples. Theorems 3.8 and 1.3 are its two most used consequences, an expected-violation bound and an explicit sample size, and later chapters of the book (constraint removal, the FAST algorithm, empirical-cost results) build on the same statement. Equality for fully supported problems shows that the bound cannot be improved for any and .
The theorem is proved in the literature; it has no machine-checked proof. A formalization produces, beyond the result itself, a reusable library of scenario programs, violation probabilities and support constraints on which the rest of the series (constraint removal, nonconvex support sets) can be stated, and it checks the measure-theoretic content that the book deliberately leaves aside ("measurability issues are glossed over throughout", p. 33).
The deterministic part, at most support constraints, is a short consequence of Helly's theorem. The probabilistic part is where the obvious approach fails. A uniform-convergence argument over all (Vapnik–Chervonenkis theory, footnote 11 of the book) gives bounds of the wrong order and can be vacuous, because it ignores that only the solution matters. The sharp bound is an exact statement about the law of , not a union bound, and problems with fewer than support constraints, or with degenerate configurations of constraints, must be shown to be no worse than fully supported ones; the book treats the general case only in the plane and refers to Campi & Garatti 2008 for general . Handling the null sets and the exchangeability of the samples under the product measure is a substantial part of the work.
EuclideanSpace ℝ (Fin d); the cost is inner ℝ c θ. A sample of size is ω : Fin m → Δ with law Measure.pi (fun _ : Fin m => P), and P is a probability measure.(P {δ | θ ∉ Θδ δ}).toReal; probabilities of events over the sample are compared in through ENNReal.ofReal.θstar : (Fin N → Δ) → EuclideanSpace ℝ (Fin d) together with the hypothesis that θstar ω solves the program for every sample; it is never an arbitrary map.θstar is measurable (the book's p. 33 convention); ; .Finset.card over Fin m.A statement in which is any feasible point of the program, or merely a measurable function of the sample, is false and does not count as a formalization of Theorem 3.7; nor does one in which Assumption 3.6 is weakened to almost every sample. Contributions of general infrastructure are welcome: exchangeability arguments for product measures, the binomial–beta identity, and Helly-type counting lemmas are reusable well beyond this mission.
Dantzig–Wolfe decomposition and column generation solve large integer programs by replacing a set of "easy" constraints with a description of its feasible points, and then pricing out the points one at a time. For linear programs this rests on the Minkowski–Weyl representation: every point of a polyhedron is a convex combination of its extreme points plus a nonnegative combination of its extreme rays. For integer programs that representation is not enough. Imposing integrality on the convex multipliers of the extreme points of does not give back the integer program, because an optimal integer point may lie in the interior of .
Lübbecke and Desrosiers, in their survey Selected Topics in Column Generation (Operations Research 53(6), 2005), present discretization (Johnson 1989, Vanderbeck 2000) as the true integer analogue of the decomposition principle. Its basis is their Theorem 1: the integer points of a rational polyhedron are generated by finitely many integer points and finitely many integer rays with integer multipliers. The paper states this result and refers its proof to Nemhauser and Wolsey, Integer and Combinatorial Optimization (1988). It underlies the integer master problem (25) of branch-and-price.
Let be an matrix and an -vector with rational entries. The polyhedron is
and its set of integer points is , the points of whose coordinates are all integers. Because , .
The recession cone of is . An integer ray of is a nonzero vector of in this cone. Extreme rays are not required.
In Lean these are polyhedronP D d, integerPoints D d, recessionConeP D and IsIntegerRay D w in the namespace Lubbecke2005.Discretization, with integer vectors cast to real vectors by castVec.
If , there exist a finite set of integer points and a finite set of integer rays of such that
Since the multipliers are nonnegative integers summing to one over , (24) says that is the union, over , of the translates of the monoid generated by the rays. No bound on or is part of the goal.
If , every point of is a vertex of . In this case convexification and discretization coincide.
The result. Theorem 1 converts an integer program into the integer master program (25) over the multipliers , with one column per generating point and per generating ray. When is bounded the rays disappear, exactly one equals one, and (25) is a linear integer program even for a nonlinear cost . The representation is what makes branching on master variables, and the passage between compact and extensive formulations, well defined in branch-and-price.
Formalizing it. The result is classical (Nemhauser–Wolsey 1988, going back to Giles and Pulleyblank and to Meyer's theorem that the integer hull of a rational polyhedron is a polyhedron). On Prove2Me, the real representation (8) is formalized as LinearOptimization.polyhedron_resolution (Bertsimas–Tsitsiklis Thm 4.15) and the integer hull theorem as LinearOptimization.integer_hull_is_polyhedron (Thm 11.3); both are included as reference items. The convexification counterpart of §3.2, that the Lagrangian dual equals the LP over , is LinearOptimization.lagrangean_dual_eq_lp_over_hull. No machine-checked statement of the integer representation (24), with integer multipliers and integer rays, was found on the platform. The mission produces that statement and, once solved, its proof.
The obvious attempt applies the real representation (8) and rounds. It fails twice. First, the extreme points of need not be integral, and an integer point written as a real combination of vertices and rays has no reason to have integer multipliers. Second, the extreme rays of generate the recession cone over , but the integer points of that cone are not in general nonnegative integer combinations of the (scaled) extreme rays; a generating set of the lattice points of a cone must usually contain non-extreme vectors. The finiteness of is also not automatic: itself is typically infinite, and taking trivializes the statement.
Rationality of the data is essential. For , every integer ray has slope below , so finitely many base points and rays generate only points with for some , while contains for every .
Fin n → ℝ; integer vectors are Fin n → ℤ cast coordinatewise. Both sides of (24) are sets of real vectors.ℚ-valued and cast to ℝ. This is an addition: the paper names no field, and the theorem is false for irrational data (see Difficulty). The cited source, Nemhauser–Wolsey, works with rational data.Fin k and Fin l for existentially chosen ; the finiteness is the content of the theorem. The multiplier vector is written as a pair of ℕ-valued vectors.A formalization with real multipliers would be the resolution theorem (8), already on the platform, and one with or infinite would be trivial; both are excluded by the statement.
Useful infrastructure: lattice points of rational polyhedral cones (Hilbert bases, Gordan's lemma), the integer hull theorem, and the real resolution theorem. A proof of Gordan's lemma for rational cones in this vocabulary would be reusable well beyond this mission. Contributions toward any of these are welcome.
The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is on every metric space with at least three points.
Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is . Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths , , . These exact values are among the few known optimal randomized ratios for server problems.
Timeline:
Fix an integer . The isosceles triangle has three points , , with
A configuration places two labelled servers on points of . A deterministic on-line algorithm assigns to every finite request sequence a configuration, computed from alone and covering the last request; its value on the empty sequence is its initial configuration. Its cost is the total distance its servers move while serving request by request. The off-line optimum from an initial configuration is the least total movement of any schedule that starts at and covers each request in turn, knowing in advance.
A randomized algorithm is a probability distribution on deterministic on-line algorithms; its expected cost is . It is -competitive against an oblivious adversary from if every algorithm in its support starts at and there is a constant such that
The request sequence is fixed in advance and does not react to the algorithm's coin flips.
Write and
In Lean this is NonuniformCompetitive.Isosceles.isoscelesRatio d.
For every and every initial configuration :
The two claims are also milestones of their own (no_better_ratio, ratio_attained).
For free real and real with
one has (lp_lower_bound); and , is nondecreasing from to and makes every constraint an equality (lp_attained).
(ratio_increases_to_e_ratio).
The theorem gives an exact optimal randomized ratio for an infinite family of metric spaces. It shows that the optimal randomized two-server ratio is not a constant: it runs from on the equilateral triangle to as the triangle becomes long and thin, where the problem resembles ski rental. With the deterministic ratio , it quantifies exactly how much randomization gains on these spaces.
The results are proved in the paper; none is formalized on Prove2Me, and no machine-checked proof of them is known. A formal proof would require the paper's phase framework (Theorems 1–3 and the appendix's Theorem 15) for server problems, which this mission does not state separately, and a concrete randomized algorithm as a measurable mixed strategy. Both would be reusable for Theorem 13 (the 3-4-5 triangle) and for other exact ratios on small metric spaces.
The phase LP milestones are finite real arithmetic. The difficulty is the passage between them and the goal. The lower bound must hold for every randomized algorithm, not only phase-based lazy ones: an arbitrary algorithm may condition on the whole history, move non-lazily, and randomize in ways that do not reduce to the probabilities . The paper handles this with Theorem 3, which says that the LP bound of phase-based algorithms bounds the competitive factor of all algorithms; its proof uses an averaging argument over histories that must be made rigorous. The upper bound needs a mixed strategy over infinitely many phases, with measurable costs, an explicit additive constant covering the first partial phase from an arbitrary initial configuration, and an accounting of across phase boundaries.
The model is the platform's published KServer_model and KServer_randomized (reference items): labelled servers Fin 2 → M; a deterministic on-line algorithm as a map from request prefixes to configurations; a randomized algorithm as a probability measure over deterministic algorithms, with the cost of each fixed sequence measurable in the random outcome; expected cost as a lower Lebesgue integral in ; the off-line optimum as a real infimum over schedules from (nonempty and bounded below by ); and IsCompetitiveFrom A C₀ c with a real additive constant.
Committed conventions:
Without the measurability field of a randomized algorithm the lower integral would under-report expected cost and the attainment claim would become easier than the paper's; the published definition includes it. The lower bound is not vacuous: the triangle hypotheses are satisfiable for every .
Welcome contributions: a formal version of the phase framework (Theorems 1–3, 15) for finite metric spaces, reusable across missions III and IV; a measurable construction of phase-based randomized algorithms; and proofs of the LP milestones.
Fictitious play is the oldest model of learning in games: each player repeatedly best-responds to the empirical frequencies of the opponents' past play. Stochastic fictitious play adds random payoff disturbances before each choice, so that players choose smoothed ("perturbed") best responses. It is a standard model in economics and in the study of learning in games (Fudenberg and Levine, 1998), and its long-run behavior is described through a deterministic mean dynamic, the perturbed best response dynamic, using stochastic approximation theory (Benaïm and Hirsch, 1999).
Supermodular games model strategic complementarities: the gain from moving to a higher strategy increases when opponents move to higher strategies. They arise in coordination, oligopoly and macroeconomic models (Milgrom and Roberts, 1990; Vives, 1990). Hofbauer and Sandholm (Econometrica 2002) show that in such games stochastic fictitious play converges almost surely whenever its mean dynamic has a unique rest point. This mission formalizes that result and the chain of lemmas behind it (Section 5 and the Appendix of the paper).
Timeline. Benaïm and Hirsch (1999) observed that supermodular games with exactly two strategies per player yield strongly monotone perturbed best response dynamics. Hofbauer and Sandholm (2002) extended this to any number of strategies by introducing stochastic dominance coordinates, and proved Theorem 6.1(iv). Benaïm (2000) supplied the low-dimensional convergence theorem used for the dimension ≤ 2 clause.
A player normal form game gives player an ordered finite strategy set and a utility on pure profiles. is the set of mixed profiles, and player 's payoff vector is .
The game is strictly supermodular if for all distinct players and all profiles with and , the difference is strictly increasing in .
Each player has a shock density on , strictly positive, whose choice function is continuously differentiable. The perturbed best response is , and the perturbed best response dynamic is
is its set of rest points in and its chain recurrent set.
In standard stochastic fictitious play the shocks have densities and are independent over time and across players. From an arbitrary initial pure profile , each player at time plays the pure strategy maximizing , where is the vector of empirical frequencies.
The stochastic dominance coordinates are , the mass on strategies above ; means each stochastically dominates . In these coordinates (P) becomes a dynamic (T) on .
For a strictly supermodular game with players and shock densities as above, if then
on every probability space, for every independent shock family with the given densities and every initial profile.
The result gives global almost-sure convergence of a stochastic learning process in a broad class of games with many strategies, where earlier results needed two strategies per player or specific payoff structures. It also shows which properties of the choice function matter: only eqs. (17)–(18), not the symmetry of its derivative used for potential and zero-sum games.
The paper's proof is complete but relies on outside results: stochastic approximation (Benaïm–Hirsch 1999, Benaïm 1999), monotone dynamical systems (Smith 1995), and the inclusion of the chain recurrent set in the global attractor (Robinson 1995). None of these, nor the Hofbauer–Sandholm theorem itself, is formalized in any proof assistant as far as known. The mission produces a machine-checked version of the theorem and of the Section 5 monotonicity theory.
The monotonicity lemmas are finite-dimensional calculus and summation by parts. The substantial steps are elsewhere. Strong monotonicity of a cooperative irreducible system (Corollary 5.5(i)) is a theorem of monotone dynamical systems that Mathlib does not have, and it must hold on the closed, non-open state space . The step from the ODE to the random process needs the stochastic approximation theorem: the empirical frequencies are an asymptotic pseudotrajectory of (P), and their limit set is almost surely internally chain transitive. Knowing that is globally asymptotically stable for (P) does not by itself give almost-sure convergence of . The limit set of the random process must be related to the chain recurrent set of (P), which is where Corollary 5.5(ii) enters.
Players are Fin p, strategies Fin (n α) (0-based, same order as the paper), with every . Mixed profiles live in the ambient space with the sup norm. The fields of (P) and (T) are defined on the whole ambient space, so partial derivatives are ordinary Fréchet derivatives. Densities are -valued. Solutions are forward solutions staying in the state space. The chain recurrent set quantifies over solutions, which are unique here because the fields are . The process is defined pathwise from the shocks, with ties in the argmax broken by the smallest index (a null event). Densities may differ across players.
A statement about the ODE (P), or about a single noise law such as logit, would be a different and much weaker theorem. The goal is about the random process , on every probability space carrying independent shocks with the given densities. Irreducibility and strong monotonicity additionally assume that two distinct players each have at least two strategies; when one player owns every stochastic dominance coordinate and has at least two of them, supermodularity holds vacuously while irreducibility fails.
A complete development needs: random utility choice functions and their derivatives; monotone and cooperative ODE theory on convex sets; the chain recurrent set and the global attractor; stochastic approximation for processes with step size . The last three are reusable well beyond this mission. Contributions to any milestone, and general-purpose lemmas on cooperative systems or stochastic approximation, are welcome.
Existence theory for elliptic, parabolic and nonlinear PDEs mostly runs through one argument: build approximate solutions, bound them in a Sobolev norm, extract a convergent subsequence, and pass to the limit. The extraction step needs a compact embedding: a bound on derivatives must buy convergence of the functions themselves in a weaker norm. On a bounded domain this is the Rellich–Kondrachov theorem. It is what makes the resolvent of the Dirichlet Laplacian compact, and so gives the Fredholm alternative and the discrete spectrum of elliptic operators on bounded domains. The companion topics of the same section, extension and trace, are how Sobolev functions are moved between a domain and all of space, and how they are given boundary values.
This mission follows Chapter 3 (§3.9–3.10) and Theorem 1.15 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014).
Timeline. Rellich proved the compactness of on bounded domains in 1930. Kondrachov extended it to and exponents below the Sobolev exponent in 1945. The compactness criterion used in the notes goes back to Kolmogorov (1931) and M. Riesz (1933); a modern account with a history is Hanche-Olsen and Holden 2010. Gagliardo characterized the traces of in 1957.
Throughout, carries Lebesgue measure, and functions are real-valued. For an open set , a test function is smooth with compact support inside . A locally integrable is the weak derivative of a locally integrable if for every test function . Here is a multi-index of order .
For and , the Sobolev space consists of the whose weak derivatives , , exist and lie in . For its norm is
and for it is the maximum of the essential suprema. The space is the closure of in this norm. For the Sobolev conjugate is .
The upper half-space is , with closure and boundary . The space consists of the functions that are smooth up to the boundary and vanish outside a compact set. Unlike , they need not vanish on .
A subset of a metric space is precompact if its closure is compact. is the space of continuous functions vanishing at infinity, with the sup norm.
In Lean the weak derivative is HasWeakDeriv (with weakDeriv and weakGradNorm) in the series' shared namespace HunterPDE.Shared; the other objects are MemW k p Ω f, sobolevNorm k p Ω f, MemW0 k p Ω f, sobolevConjugate, upperHalfSpace m, IsSmoothCompactClosedHalfSpace and boundaryPoint, in the namespace HunterPDE.Compactness.
Let be a bounded open set in , and . If satisfies for all , then
The goal is stated qualitatively (precompactness), with no constants, so it does not depend on any particular form of the Sobolev inequality.
The result itself. Rellich–Kondrachov is the source of compactness in the theory of elliptic equations. With it, the solution operator of a coercive elliptic problem on a bounded domain is compact. That yields the Fredholm alternative, the discreteness of the Dirichlet spectrum, and existence results for semilinear problems via compactness and fixed-point arguments. The trace theorem makes the boundary condition " on " meaningful for Sobolev functions, and identifies as the space in which Dirichlet problems are posed. The extension theorem transfers whole-space results to domains. Theorem 3.48 gives the uniform-norm counterpart above the critical exponent.
Formalizing it. All results here are classical and proved. The notes prove 3.45, 3.48 and the forward direction of 3.44. They describe 3.41 and 3.42 in a sentence each, and cite 1.15 without proof. Mathlib has the Lebesgue spaces Lp, Arzelà–Ascoli for bounded continuous functions, and mollification. It has no weak derivatives, no Sobolev spaces on domains, no trace, no extension operators and no Kolmogorov–Riesz criterion. A complete development would supply the first machine-checked versions of these in the notes' form, and a formal compactness theorem usable by the elliptic chapters of the same series.
The obvious route to the goal is: approximate by test functions, extend by zero, and verify the three Kolmogorov–Riesz conditions. The first two follow from the Sobolev inequality and the boundedness of . The hard parts are elsewhere. First, the Kolmogorov–Riesz criterion is not in Mathlib, and its "if" direction needs a mollification and total-boundedness argument in . Second, the -equicontinuity for above needs an interpolation between an translation estimate and the critical Sobolev embedding into , so the Gagliardo–Nirenberg–Sobolev inequality must be available for , not only for smooth compactly supported functions. Third, weak derivatives are defined by integration against test functions, and every density step has to be carried through that definition. The exponent restriction is sharp (Example 3.47 in the notes), so no argument that ignores it can succeed.
EuclideanSpace ℝ (Fin n) with volume. Open sets are Ω : Set _ with IsOpen Ω, and bounded means Bornology.IsBounded Ω. Coordinates are 0-based (i : Fin n), and multi-indices are α : Fin n → ℕ.ℝⁿ → ℝ, and only their values on the relevant set matter. weakDeriv is a chosen representative, used only where a weak derivative is assumed to exist. sobolevNorm takes values in ℝ≥0∞.sobolevNorm 1 p Ω.Ω.indicator f). The conclusion asserts both that each extension lies in and that the set of their classes in Mathlib's Lp ℝ q volume has compact closure. The hypothesis rules out .Fin.last m. The boundary is via . Extension and trace operators are maps on functions that are linear up to a.e. equality on .In best arm identification with fixed confidence, a learner samples unknown distributions (arms) sequentially and must, as early as possible, name the arm with the largest mean, while being wrong with probability at most a prescribed risk . The problem models adaptive A/B/n testing, clinical and simulation-based selection among alternatives, and the "ranking and selection" problem of operations research and simulation optimization. The quantity of interest is the sample complexity , the expected number of samples a strategy takes before stopping.
Timeline of the question this mission formalizes:
A canonical one-parameter exponential family is a family of laws , , on with density with respect to a reference measure ; is twice differentiable and strictly convex, and has mean . Bernoulli, Poisson and Gaussian laws with known variance are examples. The divergence is the Kullback–Leibler divergence between the members with means and .
A bandit model assigns a member of the family to each arm. The class consists of models with a unique optimal arm . At each round the learner picks an arm as a function of past observations, observes a reward drawn from that arm's law, and at a stopping time recommends an arm. is the number of draws of arm in the first rounds and its empirical mean.
With and the probability simplex, the characteristic time is
and the maximizer are the optimal proportions of arm draws.
Track-and-Stop combines two ingredients:
For and , Chernoff's stopping rule with combined with C-Tracking or D-Tracking satisfies
for every .
Theorem 1 of the same paper shows for every -PAC strategy, and . Theorem 14 with therefore shows that the lower bound is attained: is the exact asymptotic sample complexity of best arm identification in exponential family models, and Track-and-Stop is asymptotically optimal.
The result is proved in the paper. What is not available is a machine-checked proof for exponential families. The platform already holds a Lean development of the Gaussian case following Lattimore and Szepesvári, Bandit Algorithms, Ch. 33, stated for one existentially chosen policy with a different threshold. This mission asks for the universal statement: every run of either tracking rule, for every exponential family, with the paper's thresholds. The tracking lemmas (Lemmas 15, 7, 8) are deterministic combinatorics and reusable by any tracking-based algorithm.
The obvious argument plugs the almost-sure behaviour of Proposition 13 into an expectation. That step fails: almost-sure convergence of does not control , because on the rare events where the empirical means are far from the stopping time may be very large. Theorem 14 needs a quantitative concentration of on events whose complements have summable probability, which in turn relies on the forced exploration guaranteed by the lower bounds on (the concentration step of App. D, Lemmas 19–20).
A second obstacle is the regularity of : the tracking lemmas only transfer convergence of to convergence of through the continuity of on , proved from the characterization of in §2.2 (Proposition 6). The GLR statistic also needs its closed form (7) near , which requires the empirical means to lie in the interior of the mean space.
BanditPolicy, BanditTrajectory, TrackAndStop). uses Kullback–Leibler divergences of the arm laws over the class and takes values in . Trajectory coordinate is round . An arm never drawn has empirical mean .Best arm identification with fixed confidence is the pure-exploration counterpart of the multi-armed bandit problem. A learner faces unknown reward distributions ("arms"), samples them sequentially, and must stop and name the arm with the largest mean, being wrong with probability at most a prescribed . The question is how many samples this requires. It arises in adaptive A/B testing, in the selection of the best of several simulated systems (ranking and selection in simulation optimization), and in clinical trials that must declare the best treatment with a guaranteed error rate.
Lower bounds for this problem were first stated in terms of the gaps between means (Mannor and Tsitsiklis, 2004). Kaufmann, Cappé and Garivier (2016) replaced ad hoc changes of measure by a single "transportation" lemma relating expected sample counts, Kullback–Leibler divergences and the error probability. Garivier and Kaufmann (COLT 2016, arXiv:1602.04589v2) combine this lemma over all alternative models at once, in the spirit of Graves and Lai (1997), and obtain a lower bound whose constant is exactly matched, as , by their Track-and-Stop strategy. This mission formalizes that lower bound (Theorem 1 of the paper, p. 3).
A canonical one-parameter exponential family is given by a reference measure on , an open interval and a function , twice continuously differentiable on with , such that the laws with density with respect to are probability measures for . The mean of is . Bernoulli laws and Gaussian laws of known variance are examples.
A bandit model is a vector ; arm returns i.i.d. rewards with law and mean . Arm is the unique optimal arm if for every . Let be any set of bandit models of the family each having a unique optimal arm, and put .
A strategy consists of a sampling rule (the arm drawn at round depends, possibly with extra randomization, on the first observations), a stopping time of the natural filtration , and an -measurable decision . It is -PAC on if for every , and . is the number of draws of arm among the first rounds.
Write for the divergence between two arm laws, , and for the probability simplex on the arms. The characteristic time is defined by eq. (1):
For , every -PAC strategy on and every ,
The statement fixes no constant beyond those of the paper, and it holds for every , not only in the limit.
For every with ,
This is Lemma 1 of Kaufmann et al. (2016), which the paper quotes without proof; Theorem 1 follows from it for every alternative simultaneously.
Theorem 1 identifies as the exact problem-dependent complexity of fixed-confidence best arm identification: since , it gives , and the paper's Track-and-Stop strategy attains this rate (the subject of mission IV of this series). The bound also explains which proportions of draws an optimal strategy must use: the maximizer of eq. (1) (mission II).
Both results are proved in the literature. Neither is formalized in the paper's generality. The platform holds the textbook form of Lattimore and Szepesvári (Theorem 33.5), which is stated for an arbitrary class with the weaker constant ; for , , so Theorem 1 is strictly stronger. A formal proof here yields the transportation lemma for exponential families on the platform's infinite-horizon bandit model, which later missions (II–IV, and any lower bound by change of measure) can reuse.
The obvious proof applies the finite-horizon divergence decomposition at a deterministic horizon . That fails here: is random and unbounded, the decision is -measurable, and the relevant divergence is between the laws of the stopped observations. The step from a fixed horizon to a stopping time, together with the data-processing inequality that turns the error guarantees under two models into , is the central difficulty. A second, smaller difficulty is to identify the paper's divergence and its means with the measure-theoretic KL divergence and mean of the arm laws of the exponential family.
Lean namespace OptimalBAI.LowerBound. The bandit protocol is the platform's (BanditAlgorithm.BanditPolicy, banditTrajMeasure, IsBanditStoppingTime, IsSoundBAI, baiComplexity); is the platform's bernoulliRelativeEntropy and is trajPullCount. Conventions:
Fin K, 0-based (the paper's arm is index ); trajectory coordinate is round ;A statement with in place of , or restricted to Gaussian arms, is the platform's existing textbook theorem and does not count as this mission's goal; nor does any version that drops the almost-sure stopping clause or truncates or to real numbers.
Needed infrastructure: the transportation lemma at a stopping time (data processing for KL through an -measurable event, Wald-type identity for the stopped log-likelihood ratio), the identities "mean of " and "KL of two family members ", and . All are reusable beyond this mission. Contributions of any of these lemmas, of eq. (2) alone, or of the Gaussian and Bernoulli special cases as stepping stones are welcome.
Graphs are the most basic combinatorial model of pairwise relations: road networks, frequency interference between radio stations, schedules, circuit layouts. Chapter 5 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) introduces the vocabulary of graph theory and proves its first structural theorems: when a graph can be traversed edge by edge (Euler, 1736), when it can be toured vertex by vertex (Dirac, 1952), when it can be colored with two colors, and how far the chromatic number can drift from the size of the largest clique.
Hamiltonicity is the vertex analogue of Euler's edge-traversal problem and behaves very differently: Euler's problem has a simple parity characterization, while deciding whether a graph has a hamiltonian cycle is NP-complete (Karp, 1972). Sufficient conditions are therefore the main tool, and the minimum-degree condition of Dirac (1952) is the first and most cited of them; Ore's condition (1960) and the Bondy–Chvátal closure (1976) refine it.
A graph consists of a finite vertex set and a set of 2-element subsets of , the edges; means and are adjacent. The degree is the number of neighbours of . The mission uses Mathlib's SimpleGraph V with [Fintype V]; "a graph on vertices" means Fintype.card V = n.
AppliedComb.Graphs.IsHamiltonian).IsEulerian).IsIntervalGraph).In the book's order:
The book's proof of Theorem 5.18 uses only the pigeonhole principle, so none of these results lies on its path. The milestones are the chapter's other theorems about the same objects (cycles, degrees, colorings), and they share the goal's definitions. Cayley's formula (Theorem 5.39, labelled trees on vertices) is already on the platform as GYGraphTheory.cayley_tree_formula and is included as a reference item.
Dirac's theorem is sharp: the complete bipartite graph has minimum degree and no hamiltonian cycle. It is the starting point for the theory of degree conditions for hamiltonicity (Ore, Pósa, Chvátal) and for its extremal and random-graph analogues. Euler's theorem gives linear-time recognition of eulerian graphs; Theorem 5.21 characterizes bipartite graphs; Proposition 5.25 shows that local sparsity (no triangles) does not bound the chromatic number; Theorem 5.28 is the first step towards perfect graphs.
All of these results have been proved for a long time. What is missing is their formalization. Mathlib provides SimpleGraph, chromaticNumber, cliqueNum, degree-sum identities, and definitions of eulerian and hamiltonian walks. It contains no Dirac theorem, no converse of the eulerian degree condition, and no interval-graph theory. On the platform, FamousTheorems.two_colorable_iff_no_odd_cycle_6b is stated with odd closed walks rather than odd cycles, and triangle_free_chromatic_number asserts only rather than with exactly.
For Dirac's theorem the obvious approach, induction on (deleting a vertex), fails: deleting a vertex lowers degrees, and the hypothesis is not inherited by the smaller graph. The degree condition is global, and so is the argument that uses it. In Lean the argument also has to reverse and splice vertex sequences while keeping distinctness and every adjacency along the way. The sufficiency half of Euler's theorem has to construct a circuit that uses every edge exactly once, not just show that one exists up to parity. In Theorem 5.21 the obstruction is a cycle with distinct vertices; producing one from a failed 2-coloring takes more work than producing an odd closed walk. Proposition 5.25 needs a concrete infinite family of graphs and exact computation of both invariants. The upper bound is easy, but the lower bound is not.
SimpleGraph V on a Fintype V. The number of vertices is always Fintype.card V, never a free parameter; in Theorem 5.18 the ceiling is (n + 1) / 2 in , with Fintype.card V = n.Walk.IsHamiltonianCycle, which needs at least three vertices: under that notion Theorem 5.18 would be false for . The goal assumes nonempty, as the book's proof does ( positive). Degenerate readings are ruled out: a predicate satisfied by a cycle through only some vertices, or a statement in which is not the number of vertices, would make the goal vacuous or false, and neither is used here.chromaticNumber (-valued) and is cliqueNum; on finite graphs both agree with the book's definitions (pp. 81, 84).Second-order elliptic equations in divergence form, such as , model steady diffusion, electrostatics in inhomogeneous media and linear elasticity. They are also the stationary part of every parabolic and hyperbolic problem studied later in the same notes. When the coefficients are only bounded and measurable, classical solutions need not exist. The modern theory replaces them by weak solutions in the Sobolev space and settles existence, uniqueness and solvability by Hilbert-space methods. This mission formalizes that theory as presented in Chapter 4 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014). The chapter follows the standard development of Evans, Partial Differential Equations, Chapter 6, and of Gilbarg–Trudinger, Chapter 8.
Timeline. Riesz (1907) and Fréchet represented bounded functionals on Hilbert spaces. Fredholm (1903) proved the alternative for integral equations of the second kind, and Riesz (1918) extended it to compact operators. Lax and Milgram (1954) removed the symmetry assumption from the Riesz approach, and Gårding (1953) proved the coercivity estimate for elliptic forms. Together these give the existence and Fredholm theory for the Dirichlet problem stated here.
Let be open. A test function is a smooth with compact support in . The space is the closure of the test functions in the norm ; each element carries a function and a weak gradient , both square-integrable. is the space of bounded linear functionals on , and acts on it by .
Given coefficients with , the operator is
It is uniformly elliptic if for some , almost every and every . Its bilinear form on is
and the formal adjoint has the form . For , is a weak solution of with on if and for all . The resolvent maps to that solution.
A bounded operator on a Hilbert space is Fredholm if its kernel is finite-dimensional and its range is closed with finite-dimensional orthogonal complement. Its index is .
For bounded, uniformly elliptic and , exactly one of the following holds:
with non-unique solutions in case (2). Every kernel and equation is meant in the weak sense on .
The Fredholm alternative is the complete linear solvability theory of the Dirichlet problem for general elliptic operators on bounded domains. Uniqueness for the homogeneous problem is equivalent to existence for all data. When uniqueness fails, the obstruction is a finite set of orthogonality conditions given by the adjoint problem. This feeds directly into the spectral theory of Theorem 4.25, into eigenfunction expansions, and into the existence theory for parabolic and hyperbolic equations (Galerkin approximation in later chapters). Nonlinear elliptic problems are routinely reduced to it through linearization and the implicit function theorem.
Mathlib has Lax–Milgram for continuous coercive forms, compact operators, the Riesz representation theorem and the spectral theorem for compact self-adjoint operators. It does not have Sobolev spaces with zero boundary values as used here, elliptic bilinear forms, Fredholm operators or their index. As far as a search of the platform shows, none of these results has a machine-checked statement for elliptic operators with coefficients. The mission would give formal statements, and eventually proofs, of textbook results that are fully proved on paper.
The abstract functional analysis is close to the library. The difficulty lies in connecting it to the PDE objects. Gårding's inequality needs pointwise uniform ellipticity turned into an integral bound on the weak gradient, with the non-symmetric first-order term controlled explicitly enough to reach the stated . Compactness of the resolvent needs the Rellich–Kondrachov theorem: embeds compactly in for bounded , which is not in Mathlib in this form. The goal then relates the weak problem on to operator statements on in both directions, including the solution spaces and the adjoint's kernel. A proof that argues only on , without tracking that the solutions lie in and satisfy the weak identity for every test function, does not reach the stated result.
EuclideanSpace ℝ (Fin n) with Lebesgue measure. Coordinates are 0-based.H10 n Ω) is modelled by jets. It is the closure, in , of the pairs for smooth compactly supported with support in . Its norm is exactly the standard norm, and it is a Hilbert space. is StrongDual ℝ (H10 n Ω).Coeffs n. Admissible is membership plus a.e. symmetry. Uniform ellipticity carries .Lp ℝ 2 on .Module.finrank and is only used for Fredholm operators.finrank equality between two infinite-dimensional spaces (both in Lean) cannot stand in for the book's claim.Needed infrastructure, reusable beyond this mission: the jet model of and its Poincaré inequality, Gårding-type estimates, a Rellich–Kondrachov compactness theorem for , and Fredholm operators with index on Hilbert spaces. Contributions of any of these as separate lemmas are welcome.
Formalize , the current record from Dupont, Eisenberger, Kozlovskii, Mehrabian, Ruiz, See, Zhou, Alman, Vassilevska Williams and Balog (arXiv:2608.16884, August 2026).
The paper applies the combination-loss laser method of Alman et al. (arXiv:2404.16349), formalized here as the entry, to . That is level instead of 3, with an exact rational certificate of about parameters found by gradient-based optimization and AlphaEvolve. The authors state that the solution and verification code are being prepared for release.
The stochastic multi-armed bandit is the basic model of sequential decision making under uncertainty: a learner repeatedly chooses one of actions, observes a noisy reward for the chosen action only, and must balance exploring poorly known actions against exploiting the one that currently looks best. It underlies adaptive clinical trials, online advertising, recommendation, dynamic pricing and many simulation-optimization procedures in operations research.
The standard algorithm is UCB (Auer, Cesa-Bianchi and Fischer, 2002, doi:10.1023/A:1013689704352), which plays the arm with the largest upper confidence bound on its mean. Its confidence widths grow with the current time (or with a horizon fixed in advance), and its guarantee is on the expected regret, which grows like . Lai and Robbins (1985, doi:10.1016/0196-8858(85)90002-8) showed that logarithmic growth of the expected regret cannot be avoided by a consistent algorithm.
Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) proved a self-normalized concentration inequality for vector-valued martingales that holds uniformly over time. Section 6 of their paper applies it to the -armed bandit. The resulting confidence intervals depend on neither the horizon nor the current time. The UCB variant built on them, UCB(), has pseudo-regret bounded by a constant, independent of the horizon, on a single event of probability at least . This mission formalizes that section.
There are arms with unknown means . Write for the best mean and for the gap of arm .
Randomness lives on a probability space with a filtration . In round the learner plays an arm that is -measurable and receives the reward . The noise is -measurable and conditionally 1-sub-Gaussian:
The noise need not be independent or identically distributed across rounds, and the rewards need not be bounded.
After rounds, is the number of plays of arm and is the average reward received from it. For a confidence level the confidence width is
with when . UCB() plays, in round , an arm that maximizes ; in particular every arm is played once before any comparison is made. The pseudo-regret after rounds is
This is the linear bandit of the paper with the standard basis of as decision set and .
For every , with probability at least , for all simultaneously,
The right-hand side depends only on the gaps, and .
For any adapted choice of arms (not only UCB()) and every , with probability at least ,
The result. Theorem 7 shows that, once a confidence level is fixed, a UCB-type algorithm can stop paying for exploration after finitely many rounds: with probability the total regret over an infinite horizon is bounded. The paper notes that this does not contradict the Lai–Robbins lower bound, which concerns expected regret; on the failure event of probability the regret may grow linearly. Lemma 6 is the practical content behind this: anytime-valid confidence intervals for adaptively sampled means under martingale noise, usable for stopping rules, best-arm identification and any sequential procedure that inspects its estimates at data-dependent times.
Formalizing it. Both results are proved in the paper's appendices (F and G). No machine-checked proof of either is known to exist. The platform already has the self-normalized martingale bound for and unit sub-Gaussian noise (BanditAlgorithm.self_normalized_martingale_bound, listed here as a reference item), and UCB bounds with horizon-dependent widths and in-expectation or pathwise conclusions. Neither is Theorem 7. The mission produces a formal account of time-uniform confidence intervals for adaptively sampled arm means, and of a regret bound that is uniform in the horizon.
Two points separate this from textbook UCB analyses. First, the number of samples of an arm is itself random and depends on past noise, so a fixed-sample concentration inequality with a union bound over times does not give widths that are free of : a union bound over all costs a factor that diverges. The time-uniform event must come from a maximal (self-normalized) inequality applied to the martingale . Second, the regret statement is uniform in with constants depending on the gaps; converting a condition of the form "" into an explicit bound on requires solving an inequality in which appears both polynomially and inside a logarithm, and the explicit constants and must come out of that step.
The Lean development lives in the namespace ImprovedLinBandits.UCBDelta.
Fin d with 0 < d in the goal; means are μ : Fin d → ℝ, is ⨆ i, μ i (the maximum over a nonempty finite type).t + 1 for t : ℕ: the arm I (t + 1) is ℱ t-measurable, the noise η (t + 1) is ℱ (t + 1)-measurable and satisfies Mathlib's HasCondSubgaussianMGF (ℱ t) … (η (t + 1)) 1 P. Values at index are unused.A trivializing formalization is ruled out: the confidence event is not assumed as a hypothesis of Theorem 7, the i.i.d. bandit model is not substituted for the martingale noise model, and no bound on the means or rewards is imposed.
Useful infrastructure for solvers: the self-normalized bound of Theorem 1 in the scalar case (, , , ), a union bound over arms, and elementary inequalities inverting . Lemmas about pull counts and empirical means under adaptive sampling are reusable beyond this mission and are welcome as contributions.
Nonlinear programming algorithms are routinely advertised as finding a local minimum. Most of them only certify first-order conditions (a KKT point), and the natural next question is whether a given feasible point is in fact a local minimum. For smooth problems where the Hessian is nonsingular this is a second-order test, but in the degenerate case the test itself becomes a combinatorial question about a quadratic form restricted to a cone.
K. G. Murty and S. N. Kabadi (Math. Programming 39 (1987) 117–129) showed that this question is intractable already in its simplest instance: deciding whether is a local minimum of a quadratic form on the nonnegative orthant is NP-complete, and so is deciding whether a square integer matrix is copositive. The paper is the standard reference for the hardness of copositivity testing, which matters for copositive programming, for second-order optimality checks in constrained optimization, and for the complexity of local search in nonconvex optimization.
Let be a real square matrix of order and . The matrix is copositive if for every (coordinatewise). The paper considers the quadratic program
and the following questions, each phrased so that "yes" is the interesting answer:
The source problem is subset sum (Problem 5): given positive integers , is there with ? Let be the total number of digits in the data. The paper fixes an integer and a rational with , and defines functions of nonnegative variables :
, a homogeneous quadratic that agrees with on the set
and . The function is a quadratic form in ; the symmetric matrix , with entries computed explicitly from , is the output of the reduction.
For positive integer data and as above, with the matrix of , the following are equivalent:
This is the mathematical content of Theorems 1–3 and §4: a polynomially computable map from subset sum instances to matrices under which every one of these questions has the answer of the subset sum instance.
The result. The equivalence shows that checking local optimality of a feasible point, checking boundedness of a quadratic objective on a cone, and checking copositivity are all at least as hard as subset sum, hence NP-hard. Through (15) the same holds for local minimality and boundedness of a quartic polynomial with no constraints at all. These facts are the standard justification for why nonconvex solvers settle for KKT points, and the copositivity part underlies the hardness of copositive programming.
The formalization. The paper's claims are proved, and have been cited for decades, but the proof as printed is a sketch: several steps are stated as "clearly" or "it can be verified", and one step of the proof of Theorem 1 (p. 125) is false as written. The inequality for fails for slightly above , and the pointwise implication " on " has an explicit counterexample. The equivalence of Problems 6 and 7 itself survives numerical checks. A machine-checked proof of the goal settles the correctness of the reduction with the paper's own constants. No machine-checked proof of these statements exists on the platform.
The combinatorial direction (a subset sum solution gives a point with ) is a computation. The converse direction carries the content, in two places.
First, passing from to trades the linear penalty for a quadratic one. This is harmless on the box but not for , where is negative. The printed argument handles this coordinate by coordinate and is wrong there; a correct argument has to show that no point of with exists unless a point with does, which requires a global use of the size of .
Second, passing from to requires a quantitative gap: if on then with of only polynomially many bits. Lemma 2 provides such a gap for the unit box and integer matrices, but is not the box and has rational coefficients, so the lemma does not apply verbatim.
The remaining equivalences (Problems 1, 2, 3, 4, 11, 12 for a fixed matrix) follow from homogeneity of the quadratic form and the substitution , and are routine.
The data are natural numbers and is rational; all are cast to in and . The index is Fin n, and the variables of are indexed by Fin n ⊕ Fin n with Sum.elim y s. Standing hypotheses: and (the paper's "all positive integers"); in ; and in . The size counts decimal digits. Problem 1 is local minimality relative to the orthant, Problem 11 is unconstrained local minimality, both in the Euclidean topology. Lemma 2 is stated for integer symmetric (as §4 of the paper says, "as before … symmetric"), with Schrijver's encoding size, since the paper does not define "the size of "; the "optimum is or " is stated as a disjunction without an infimum. The milestones on over assume , which the paper assumes tacitly; the goal needs no such hypothesis.
Not formalized: membership in NP (Lemma 1), the polynomial-time computability of and its encoding size, the NP-completeness of subset sum (cited by the paper from Garey–Johnson), Theorem 4, and any of the words "NP-complete" or "NP-hard". The platform's complexity layer (Turing machines over bitstrings) has no subset sum problem and no encoding of rational matrices. The matrix has rational entries; a positive integer multiple of it is the integer matrix of Theorem 3, has the same answer to every question, and the rescaling is not formalized. The §3 standing assumption "D is not PSD" is not imposed; the constructed matrix can be PSD and the equivalence holds regardless.
The goal is about the explicit matrix , whose entries are given in the definitions; it is not about "some matrix whose quadratic form is ", and the constants and are the paper's explicit bounds, not "sufficiently large" or "for some ". A formalization that quantifies existentially over the matrix or the precision would be trivially true and is ruled out.
Contributions welcome: proofs of the matrix identity and the homogeneity arguments (milestones 6–9), a proof of Lemma 2 (which needs a Cramer/Hadamard bound on basic solutions of the linear complementarity system (9)), and a correct proof of the step. The copositivity definitions and milestones 7–9 are reusable for any later work on copositive programming.
Value-at-Risk (VaR) is the standard regulatory measure of downside risk of a portfolio: the loss level that is exceeded only with a prescribed small probability . Computing it requires the full distribution of asset returns, which is rarely known. In practice one estimates a mean vector and a covariance matrix and then assumes a Gaussian distribution, which understates the probability of large losses when returns are heavy-tailed or skewed.
El Ghaoui, Oks and Oustry (Oper. Res. 51(4), 2003) replace the distributional assumption by a worst case: the VaR is computed against every distribution consistent with the known moments. For known mean and covariance they obtain an exact closed form and several semidefinite (SDP) representations of this worst-case VaR. The SDP forms are what make the approach extend to moment uncertainty (moments only known to lie in a set, §2.2 of the paper) and to robust portfolio optimization. The equivalence between the probabilistic statement and the closed form is also a multivariate one-sided Chebyshev bound, related to Bertsimas and Popescu (SIAM J. Optim. 15(3), 2005; working paper 2000).
There are assets. Their returns over one period form a random vector , and a portfolio earns . The paper restricts to an admissible set that does not contain ; only is used.
The distribution of is unknown except for its mean and covariance matrix , with (positive definite). Let be the set of all probability distributions on with these two moments. For a loss level , the loss set is . The worst-case VaR at level is (Eq. (4))
Further notation: (Eq. (8)); for symmetric matrices, means is positive semidefinite and . The second-moment matrix is (Eq. (6))
For , , and , the following five propositions are equivalent:
In particular
The result. Proposition 2 turns the worst-case VaR into a second-order cone function of , so minimizing it over a polytope of portfolios is a second-order cone program (Eq. (12)). The SDP forms 3 and 5 are the basis of the paper's §2.2–§3: they extend, with the moments only known to lie in a convex set, to a single SDP whose value is the worst-case VaR over that set. Proposition 4 gives a deterministic reading: the worst-case VaR is the largest loss when the return vector is only known to lie in an ellipsoid, which connects distributional robustness to robust optimization with ellipsoidal uncertainty.
Formalizing it. The result is proved in the paper, with two imported steps: strong duality for the moment problem (Smith 1995; Bonnans and Shapiro 2000) and a Slater-type strong duality for the one-constraint quadratic condition. No machine-checked version is known. A formal proof would supply these steps with explicit hypotheses and would produce a Lean statement of the multivariate one-sided Chebyshev (Cantelli) bound with tightness over the full moment class.
The matrix equivalences (2 ⇔ 4 ⇔ 5 and 2 ⇔ 3) are Schur complements and finite-dimensional SDP duality. The difficulty is Proposition 1. The upper bound (Cantelli's inequality for ) handles one direction, but the converse requires tightness: for every below the closed form, a distribution on with exactly the prescribed mean and full covariance matrix that puts probability more than on the loss set. A scalar extremal distribution for does not by itself have the right covariance in the other directions, and a Gaussian does not reach the bound. The paper's route through the moment problem instead needs strong duality between a supremum over measures and an infimum over matrices, which is where the positive definiteness of enters.
EuclideanSpace ℝ (Fin n); is the inner product, and matrices are Matrix (Fin n) (Fin n) ℝ. Matrices of size are indexed by Fin n ⊕ Fin 1 and built with Matrix.fromBlocks (the helper bordered A v c is ). is PosSemidef, is PosDef, is (A * B).trace, and is written .HasMeanCov) contains every Borel probability measure on whose coordinates are square-integrable, with mean and centred covariance . It is not restricted to densities or to Gaussians: the Gaussian class gives a different constant, .IsLUB/IsGLB of one real number (no attainment is claimed). The maxima over , over and over the ellipsoid are IsGreatest.An algorithm for linear programming is strongly polynomial if the number of arithmetic operations it performs is bounded by a polynomial in the dimension of the problem alone (the number of variables and constraints), independently of the bit lengths of the numbers in the input. Many combinatorial optimization problems are linear programs over polyhedra of the form whose constraint matrix has entries , but whose objective vector is an arbitrary rational weight vector. Polynomial-time algorithms for such problems (for instance the ellipsoid-based algorithms of Grötschel, Lovász and Schrijver for maximum-weight cliques in perfect graphs, submodular flows, and matroid polyhedra) have running times that depend on the length of .
Frank and Tardos (Combinatorica 1987) remove this dependence once and for all: they replace by an integral objective whose entries have bits and which has exactly the same optimal solutions and the same optimal dual bases as over every such polyhedron. Any algorithm that is polynomial in and in the length of the objective then becomes strongly polynomial. The tool is simultaneous Diophantine approximation, used through the lattice-basis-reduction algorithm of Lenstra, Lenstra and Lovász (Math. Ann. 1982). The technique extends Tardos's strongly polynomial algorithm for linear programs with small constraint matrices (Oper. Res. 1986), which applies only to explicitly given programs.
For write and ; takes the values .
Decomposition. Fix a positive integer . A decomposition of is an expression
It satisfies condition (iii) if for the vector is nonzero and : the coefficients decrease so quickly that each term is negligible against the previous one.
Preprocessing. Given a rational and , the paper's preprocessing algorithm finds a decomposition with , condition (iii), and the size bound (ii)' , and outputs
Linear programs. Let be an matrix with entries in and . The primal program is and the dual program is . A point is -maximal if . A dual basis is a maximal set of row indices of whose rows are linearly independent; it determines at most one with supported on it (the basic dual solution), and it is an optimal dual basis if that exists and is optimal for the dual program.
For every , with , there is with
such that for every matrix with columns and every : (i) is -maximal if and only if it is -maximal; (ii) a set of rows of is an optimal dual basis for if and only if it is one for . The vector depends on only, not on or .
The result gives a general reduction: whenever a class of polyhedra with constraint matrices admits an optimization algorithm that is polynomial in and in the length of the objective, it admits a strongly polynomial one. The paper applies this to maximum-weight cliques in perfect graphs, optimization over submodular flow polyhedra, and matroid polyhedra membership, and its Section 5 applies the same rounding to the integer programming algorithms of Lenstra and Kannan. The subset-sum corollary (milestone 5) is independently useful: every rational weight function on a finite set can be replaced by an integral one with -bit entries that orders all subset sums identically.
All statements of this mission have been proved on paper since 1987. None is formalized on Prove2Me, and Mathlib contains only the one-dimensional Dirichlet approximation theorem. The mission produces a machine-checked version of the exact statements, with the explicit constants of the paper; the complexity claims (operation counts, strong polynomiality) are not part of it.
The goal combines two independent parts. The number-theoretic part (milestones 1–5) needs a multidimensional Dirichlet theorem, an induction producing the decomposition, and exact inequality chains with the constants and . The linear-programming part (milestones 6–7) needs bounds on the entries of inverses of nonsingular submatrices, the existence of optimal dual solutions supported on a dual basis, LP duality and complementary slackness. The obvious first idea, scaling to an integer vector by a common denominator, preserves every sign but gives no bound on in terms of ; the bound is the content of the theorem. Likewise, rounding each coordinate of separately to a fixed precision does not preserve the sign of when is tiny but nonzero.
Vectors are functions on Fin n: the input is rational (Fin n → ℚ) in the goal, in Theorem 3.3 and in the subset-sum corollary, as in the algorithm's input line; it is real in Theorem 3.1, Lemma 3.2 and Lemma 4.1, as on the page. Integral vectors are Fin n → ℤ, and is a Matrix (Fin m) (Fin n) ℤ with every entry in , cast to ; is unrestricted. Decompositions are indexed by as in the paper. is always the explicit sum , compared with in ; of an integer vector is a natural number (supNorm). Sign equality uses SignType.sign and includes the zero case. Condition (iii) is stated multiplicatively together with , which the paper's quotient presupposes; without Lemma 3.2 fails. An optimal dual basis is a maximal linearly independent set of row indices together with an optimal dual solution supported on it.
Two formalizations would make the goal trivial and are excluded: dropping the bound on (a multiple of then works), and letting depend on and (the goal states before ). The assumption on is part of every Section 4 statement.
A complete development needs a multidimensional pigeonhole argument, determinant and adjugate bounds for matrices, and basic LP duality (strong duality, complementary slackness, basic optimal dual solutions); the last two are reusable across linear-programming missions. Proofs of individual milestones, reusable lemmas on LP duality, and alternative proofs of Dirichlet's theorem are all welcome.
Paging is the problem of managing a fast memory that holds pages out of : when a requested page is not in fast memory (a page fault), some resident page must be evicted, and the cost of an algorithm is its number of faults. Practitioners have many eviction rules. Least-recently-used (LRU) performs well on real workloads but can be times worse than the optimal off-line schedule; the randomized marking algorithm of the same paper is -competitive and so has better worst-case guarantees. Fiat, Karp, Luby, McGeoch, Sleator and Young asked in 1991 whether one on-line algorithm can combine the advantages of several given ones, and answered the question exactly: the attainable combinations of ratios are characterized by one inequality (arXiv:cs/0205038, §6).
The question of combining on-line algorithms has since become a theme of its own: combining heuristics with worst-case-safe algorithms, and, more recently, combining machine-learned predictions with robust fallbacks, both ask for the same kind of guarantee against several reference algorithms at once.
A type consists of servers and a finite set of vertices with the uniform metric: two distinct vertices are at distance . This is paging: vertices are pages, the vertices covered by servers are the pages in fast memory, and a server move is a page fault.
A deterministic on-line algorithm of type has an initial configuration of its servers and, after each request , moves servers so that some server covers ; its configuration after a request sequence depends only on that sequence. Its cost on a request sequence is the total distance its servers travel, i.e. the number of server moves.
For algorithms and of the same type and a constant , is -competitive against if there is a constant such that for every request sequence
A sequence of positive reals is realizable if for every type and every deterministic on-line algorithms of that type there is a deterministic on-line algorithm of the same type that is -competitive against for every .
For and positive reals ,
In the order of the paper's proof:
The result. Theorem 6 is an exact characterization, not a bound: the region of simultaneously attainable ratios against arbitrary deterministic paging algorithms is . For example, any two paging algorithms can be combined into one that is -competitive against each, and no better symmetric pair is possible in general. Combined with Theorem 7 of the same paper (not part of this mission), the same region is attainable against randomized algorithms, which is how LRU's practical behaviour and the marking algorithm's worst-case guarantee can be obtained within constant factors by one algorithm.
Formalizing it. The theorem has been proved since 1991; no machine-checked proof is known. A formal proof produces a reusable notion of competitiveness of one on-line algorithm against another, built on the published KServer_model definitions, and a formal account of the scheduling fact at the core of the sufficiency proof.
Sufficiency looks like an averaging argument, but the combined algorithm cannot simulate the and follow one of them: switching between their configurations costs up to per switch, which no additive constant absorbs. The accounting has to charge each of 's faults to a specific move of a specific , and the charge must be injective; the paper's claim that is at least the number of punishments is where this happens, and it depends on how server intervals are matched. The allocation of faults to algorithms is then a deadline-scheduling problem whose feasibility is exactly , and the floor functions make the counting delicate at the boundary. The paper's own definition of punishment only counts intervals that start with a move, so the first faults of (servers on their initial vertices) need separate treatment; they are absorbed by the additive constant.
Necessity needs the right family of hard instances: the algorithms must never move at the same step, which pins the type to .
The Lean development works in the namespace CompetitivePaging.Combining and imports the published KServer_model definitions: KServer.OnlineAlgorithm k M (a configuration map from request prefixes to Fin k → M with a serving condition) and OnlineAlgorithm.cost. Committed conventions:
k : ℕ and any finite M : Type with a metric in which distinct points are at distance ; realizability quantifies over all of them, never over one fixed type;Trivializing encodings are ruled out: realizability is not stated for a single fixed type, the metric is not the metric of Fin n, and the competitive constant is not allowed to depend on the request sequence.
A complete proof needs the construction of the punishing algorithm as a KServer.OnlineAlgorithm (a lazy, injective algorithm whose moves depend on the prefix and on the 's configurations), the injective charging argument, the scheduling lemma, and the explicit shuttle algorithms. The scheduling lemma and the charging lemma are independent of paging and reusable. Proofs of any milestone are welcome, as are alternative statements of the sufficiency construction.
The Hitchcock transportation problem asks how to ship a commodity from supply points to demand points at minimum total cost. It was posed by Hitchcock in 1941 and is one of the founding problems of linear programming and network optimization; it is solved routinely in logistics, and its structure (a bipartite network with supplies, demands and per-unit costs) recurs in assignment, optimal transport and matching.
The classical algorithms for it, the Ford–Fulkerson primal–dual method among them, augment flow one path at a time. With integral data their number of augmentations is bounded only by the total supply , which is exponential in the number of binary digits used to write the data. Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems (J. ACM 19(2), 1972, doi:10.1145/321694.321699), introduced capacity scaling: solve a coarse version of the problem first, then refine one binary digit at a time. Their Theorem 9 (p. 260) bounds the total number of augmentations by a quantity proportional to times the number of bits of the data, which made the transportation problem, and through standard reductions the minimum-cost flow problem, one of the first network problems with a polynomial-time ("good") algorithm in the sense of Edmonds.
Timeline. Hitchcock (1941) posed the problem; Ford and Fulkerson (1956–1962) gave the primal–dual labeling method and the optimality conditions by node potentials; Edmonds and Karp (1972) gave the scaling method and the bound formalized here. Strongly polynomial algorithms, independent of the size of the numbers, came later (Tardos 1985; Orlin 1988).
The network of Figure 1 (p. 259) has a source , a sink , supply nodes and demand nodes , with . Its arcs are with capacity and cost ; with capacity and cost ; with capacity and cost ; and the return arc with capacity and cost . The supplies and demands are positive integers with .
A flow assigns a nonnegative number to every arc, at most the capacity, with inflow equal to outflow at every node. Write , , ; the value of is , and a maximum flow is one of largest value. Its cost is ; a flow is extreme if no flow of the same value is cheaper. A flow is pseudo-extreme if there are real with for all and whenever .
An augmenting path relative to is a sequence of distinct nodes from to in which each step either follows an arc with spare capacity or traverses backwards an arc carrying positive flow; augmenting pushes the minimum spare amount along it and raises by .
For , Problem has the same network and costs, with capacities and . Choose with every . The scaling method solves Problems in turn. Each phase performs augmentations keeping every flow pseudo-extreme, until no augmenting path is left. Problem starts from the zero flow, and Problem starts from twice the final flow of Problem .
For every run of the scaling method, the total number of flow augmentations satisfies
The bound holds for every admissible for the data and every choice of costs, and is stated with the paper's constant exactly.
The result. Theorem 9 shows that scaling reduces the number of augmentations from order to order , which is roughly the length of the binary encoding of the data. Combined with the cost of one augmentation it gives a polynomial-time algorithm for the transportation problem; through the reduction of minimum-cost flow to transportation (p. 261) it gives one for minimum-cost flow. Capacity and cost scaling became standard techniques in network optimization and in combinatorial optimization generally. Theorem 8 and the pseudo-extreme criterion are the optimality certificates for transportation, a special case of linear-programming complementary slackness.
Formalizing it. The theorem has been proved since 1972. This mission produces a machine-checked version of the bound, of the exact counting argument (eq. (6)) and of the arithmetic estimate that turns it into the stated constant, together with the potential-based optimality conditions for the transportation network. To our knowledge no machine-checked bound on the number of augmentations of a flow algorithm exists on the platform.
The obvious argument bounds the number of augmentations by the increase in flow value, since each augmentation raises the value by a positive integer. Applied to Problem 0 directly this gives only . The scaling bound needs three things that the naive count does not supply. First, doubling the final flow of Problem must give a feasible, still pseudo-extreme, starting flow for Problem (Lemma 3). Second, the gap between that start and the optimum of Problem must be small, which requires the exact maximum-flow value of each scaled problem. Third, the telescoping sum of the gaps must be estimated against with the floors handled exactly. Integrality of every intermediate flow is not assumed; it has to be carried along the run from the integral capacities and the zero start.
Everything lives in the namespace EdmondsKarp.Scaling. Nodes form an inductive type (s, t, src i, dst j). A flow is a structure with components f0, fx, fz, ret for the four arc families, real valued; the infinite capacities are encoded by the absence of an upper bound. IsMaxFlow is a predicate comparing values with every flow, not a supremum. Problem uses natural-number division for . Augmenting paths are lists of distinct nodes from s to t whose consecutive pairs have positive residual amount (resCap, valued in WithTop ℝ); they never use the return arc.
A run of the scaling method (IsScalingRun) is a family of phases for . It starts from in Problem , restarts from in Problem , and advances by one augmentation per step. Every flow is pseudo-extreme, and each phase ends with no augmenting path left. The paper's path-selection rule (minimum weight for the modified reduced costs ) is abstracted to this invariant, which the paper states for it, so every run of the paper's method is covered.
The goal compares the count, cast to , with , using Real.logb 2 and Int.floor. The constant is the printed one; neither nor a weaker constant is acceptable. Positivity of all is a hypothesis, because without it the printed bound is false (for , , , one augmentation is needed and the bound is negative). A formalization in which runs could be empty or never reach a maximum flow would trivialize the goal; the run predicate forbids this, and it is satisfiable (for instance with , , and one augmentation).
A complete development needs max-flow/min-cut for the bipartite network, integrality of flows along a run, the exact value of , the telescoping identity and floor/logarithm estimates. LP duality or complementary slackness is needed only for Theorem 8. The augmenting-path and max-flow lemmas are reusable for other bipartite flow problems. Contributions welcome: proofs of any milestone, and a formalization of the paper's exact path rule showing that it satisfies the invariant.
Machine scheduling asks how to assign jobs to machines over time so that a criterion such as the makespan , the time at which the last job completes, is as small as possible. In practice jobs also compete for scarce resources beyond the machines themselves: tools, operators, memory, power. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification of Graham, Lawler, Lenstra and Rinnooy Kan (1979) by a resource field . They then settled the complexity of every problem with parallel identical or uniform machines, unit-time jobs, precedence constraints and the criterion. Their Fig. 2 separates the maximal polynomially solvable problems from the minimal NP-hard ones, and it has been the reference map for resource-constrained scheduling since.
Brief timeline of the problems involved:
There are jobs and machines . Every job has processing time on every machine, each machine handles at most one job at a time, and jobs are not preempted. There are resources; resource has a positive integer size , the amount available at any time, and job has a nonnegative integer requirement , the amount it holds throughout its execution. A directed acyclic graph on the jobs gives the precedence constraints: if has a path from to (), then must complete before starts. The precedence is chain-like when every vertex of has indegree and outdegree at most one.
A schedule gives each job a machine and a real start time ; the job occupies and completes at . It is feasible if jobs on one machine do not overlap, precedence is respected, and at every time the jobs running at require at most of each resource . The makespan is .
The problem restricts this to , one resource () of size (), every requirement at most (), and chain-like precedence. The problem has , one resource of arbitrary size and requirements, and no precedence.
3-PARTITION: given , a positive integer and positive integers with and , can be split into disjoint 3-element sets with ?
A problem is NP-hard in the strong sense if it remains NP-hard when every number of the instance is written in unary.
The hypothesis is Garey and Johnson's theorem on 3-PARTITION, which the paper cites and does not prove. The conclusion concerns the decision version: given an instance and , is there a feasible schedule with ?
Theorem 7 is the sharpest hardness result of the paper's classification. Without resources, two-machine unit-time scheduling with arbitrary precedence is polynomial (Coffman and Graham, Acta Inform. 1972); without precedence, it is polynomial under arbitrary resources (Theorem 1 of the paper). The theorem shows that combining the weakest nontrivial versions of both constraints, chains and one unit resource, already crosses the borderline. The paper's §4.1 extends the same reduction to the and criteria.
On the formal side, the mission provides a machine-checked model of resource-constrained scheduling with real start times, a definition of NP-hardness in the strong sense on top of the platform's Turing-machine formalization of and , and 3-PARTITION as a reusable source problem. As far as the platform's corpus shows, none of Theorems 4 and 7, 3-PARTITION, or strong NP-hardness has been formalized before. Both theorems are proved in the literature; what remains is to formalize the reductions and their polynomial running time.
The combinatorial heart is the "only if" direction: a schedule of length must be shown to be rigid. Start times are arbitrary reals, so the first obstacle is to show that both machines are busy throughout , that the chain forces unit spacing, and that the primed jobs of the chains can only run in the intervals the chain leaves free of the resource. Only after this is established can the index sets be read off. Arguing on integer time slots from the start is not enough: the model allows fractional start times, and ruling them out is part of the proof.
The second obstacle is the complexity layer. NP-hardness is stated with respect to polynomial-time many-one reductions computed by one-tape Turing machines. The reduction from 3-PARTITION therefore has to be implemented and its running time bounded on unary codes. The constructed instance has jobs, which is polynomial in the unary length of the 3-PARTITION instance; this is exactly why the reduction proves hardness in the strong sense.
Fin n and machines Fin m, 0-based. Only identical machines with unit processing times are modelled. Start times are real, execution intervals are half-open, and the resource constraint is imposed at every real time. Precedence is the transitive closure of the arc list of . for an empty instance.Welcome contributions: proofs of the four milestones; a formalized polynomial-time implementation of the reduction on unary codes; general lemmas about composing polynomial-time reductions on the one-tape machine model.
The economic order quantity (EOQ) is the most widely used formula in inventory management. It assumes that demand is a deterministic constant stream. Real demand is random, and the model that accounts for this, the continuous-review policy with stochastic demand, has no closed-form optimum: for decades its optimal parameters were computed numerically, one instance at a time, which gave little insight into how the stochastic system behaves. Practitioners nevertheless kept using the EOQ quantity in stochastic systems and observed that the cost penalty was small (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), without an analytical explanation.
Zheng (Management Science 38(1), 1992) supplied that explanation. By minimising the average cost first over the reorder point and then over the order quantity, he obtained two simple optimality equations and compared the stochastic model with the EOQ model under the same cost structure. One of the results is the goal of this mission: for every leadtime-demand distribution, using the EOQ order quantity in the stochastic system raises the average cost by at most one eighth. The paper extends Federgruen and Zheng (1988), who treated the discrete-demand version of the cost function.
A single item faces demand at rate . Orders are delivered after a fixed leadtime , and stockouts are backordered. Each order costs a fixed . Inventory is held at cost rate per unit and backorders are penalised at cost rate per unit. Let be the demand during a leadtime, with mean . The newsvendor cost
is the rate at which expected inventory costs accrue at time when the inventory position at time is . It is convex, and it is assumed, as in the paper, to attain its minimum at a unique point .
A policy orders units whenever the inventory position falls to the reorder point . Its long-run average cost is
For a fixed let be an optimal reorder point, and set
is the average cost when the reorder point is chosen optimally for ; an order quantity minimising over is the optimal order quantity, and is the optimal cost.
The EOQ model is the special case in which the leadtime demand is the constant . Its cost rate is , and its optimal order quantity is
The subscript marks every object of the EOQ model (, , ).
is the stochastic cost at the EOQ quantity with the reorder point re-optimised for it. The bound holds for every leadtime-demand distribution and every value of the parameters.
In the order the goal's proof uses them:
The theorem is a distribution-free worst-case guarantee for the most common heuristic in inventory practice. It says that the EOQ formula, which needs only the mean demand rate and three cost parameters, loses at most against the true optimum, and that the loss is smaller when is close to or to . Combined with the paper's Theorem 2 (the gap is bounded as grows), it implies that the relative loss vanishes as the fixed ordering cost grows. The milestones along the way (the optimality conditions of Theorem 1, the monotonicity of the optimal reorder point, the comparison of with its EOQ counterpart) are the standard structural facts about continuous systems and are reused throughout the inventory literature.
The result is proved in the paper. No machine-checked version of it, or of the optimality conditions for the continuous cost (1), is known to exist. The platform has related but different formalizations: the discrete cost function with integer (InventoryControl_rqDiscrete), the cost under normal demand (InventoryControl_rq), and the EOQ without backorders (InventoryControl_eoq). A complete development here provides the continuous machinery for an arbitrary leadtime-demand distribution.
The paper's proofs differentiate and twice (Eqs. (4), (5)), which presupposes a leadtime demand with a smooth density. The formalization does not assume one, so that discrete demand, such as the Poisson demand of the paper's own numerical study, is covered. Every step that the paper takes through derivatives, in particular the convexity of and the slope bound , has to be established by other means: through one-sided derivatives or chord arguments for the convex function , whose kinks are where the derivative-based argument breaks. The definition of as a minimiser also means its existence and uniqueness must be proved before any property of , or can be used.
IsQRModel: , the conditions on , and the unique minimiser of (paper, p. 90). is a separate hypothesis. No density is assumed.In stochastic optimization the law of a random return is rarely known exactly, while its mean and variance can be estimated. A robust mean-covariance decision maker therefore evaluates a utility by its worst case
Popescu (Operations Research 55(1), 2007) shows that for large classes of utilities this infinite-dimensional problem collapses to a one-dimensional one. The paper projects multivariate problems to a single dimension (the subject of the first mission of this series) and then asks for which the univariate worst case sits on laws with two support points. This mission formalizes the answer the paper gives for utilities whose marginal utility is decreasing and changes curvature once, with finite limits: log-logistic utilities used in statistics and classification, and catenary-type utilities , each plus a concave quadratic.
The result has a bounded-support precursor: Birge and Dulá (Annals of Operations Research 30, 1991, Theorem 5.1, as cited on p. 102 of Popescu 2007) proved an analogous two-point statement for functions on a bounded interval. Popescu's Proposition 5 is the unbounded version on the whole real line.
Let .
and (lemma1Quad).
partnerPoint) and (prop5Gap).If is differentiable, is inverse S-shaped, and the limits and exist and are finite, then
The result. Through the paper's Proposition 4, two-point support turns the worst-case expected utility over all laws with mean and variance into a minimization over a single parameter of . Combined with the projection property of the paper's Section 2, this gives tractable robust counterparts of multivariate stochastic programs whose objective depends on a linear combination of random returns. Proposition 5 is the paper's sufficient condition that places a concrete class of utilities in this regime; it is also closed under adding any quadratic.
Formalizing it. The result is proved on paper; no machine-checked version is known. The formalization produces a checked characterization of two-point support (Lemma 1), a reusable encoding of convex-concave and S-shaped functions, and a proof of Proposition 5. The printed final step of the paper's proof is incomplete (see Difficulty), so a complete formal proof requires an argument the paper does not spell out.
Conditions (a) and (b) of Lemma 1 come from a sign change of on : the two limits in milestone 4 need a l'Hôpital-type argument and the continuity of a monotone derivative. The central difficulty is condition (c): showing that the quadratic built from a pair lies below on the whole line. The obvious argument takes any zero of and counts the intersections of the linear with the inverse S-shaped . This fails when is affine on an interval: a zero of can then produce a quadratic that coincides with on but crosses above just left of . A proof must therefore choose the zero of , or the pair , with care, and the curvature hypotheses are not strict.
ℝ → ℝ; is deriv u, and the goal assumes Differentiable ℝ u. Finite limits are Tendsto (deriv u) atBot (𝓝 l) and Tendsto (deriv u) atTop (𝓝 l) for some real l; the one-sided limit at is along 𝓝[<] μ.StrictMono); the paper writes "nondecreasing" for the weak notion. Convexity and concavity are ConvexOn/ConcaveOn on the open half-lines Set.Iio x₀, Set.Ioi x₀, as printed.Useful infrastructure: l'Hôpital's rule at infinity (Analysis/Calculus/LHopital), Darboux's theorem for derivatives, the intermediate value theorem, and one-sided limits of monotone functions. The shape definitions of Definition 2 are reusable for S-shaped value functions elsewhere (prospect theory, sigmoidal utilities). Proofs of the milestones, of the goal, and alternative arguments for condition (c) are all welcome. Related platform work: Wasserstein Distributionally Robust Optimization II.
Online convex optimization is a repeated game between a learner and an adversary. In each round the learner commits to a point of a convex set ; only then is a convex cost function revealed, and the learner pays . The learner is judged by its regret: its total cost minus the total cost of the best fixed point chosen in hindsight. The model covers online portfolio selection, online regression, prediction with expert advice and the analysis of stochastic gradient methods, and it is the standard language of online learning theory.
Zinkevich (ICML 2003) showed that projected gradient descent with step sizes of order has regret for any convex costs with gradients bounded by on a set of diameter , and this rate cannot be improved for linear costs. Hazan, Agarwal and Kale (Machine Learning 69, 2007) asked what curvature buys. Their first result, the subject of this mission, is that the same algorithm with the faster step sizes has regret only logarithmic in once every cost function is -strongly convex. The paper's other three results (the Online Newton Step, Follow the Approximate Leader and Exponentially Weighted Online Optimization, for exp-concave costs) are the subject of the other missions of this series.
Fix and a nonempty, closed, bounded, convex set , with the Euclidean norm (§2.1, p. 171).
IsProj P y z).(IsOGDRun P η f x).
For , cost functions that are -strongly convex on with gradients bounded by on , and any run of Online Gradient Descent whose step after round is , for every and every :
This is LogRegretOCO.OGD.ogd_regret_bound. The constant is the paper's, and at the bound reads .
UnderstandingML.projection_lemma, and is reused as a reference item.The last step of the argument is the harmonic-sum bound , which Mathlib already provides (harmonic_le_one_add_log).
The result. Theorem 1 separates two regimes of online convex optimization: regret for general convex costs and for strongly convex ones, with an algorithm that costs one gradient and one projection per round. Through the online-to-batch conversion, the same step-size schedule gives the rate of stochastic gradient descent on strongly convex objectives. The theorem is also the reference point for the paper's weaker exp-concavity assumption, under which the other three algorithms obtain regret.
Formalizing it. The result is proved and well known; what this mission adds is a machine-checked proof with the paper's exact constant. The Prove2Me platform holds a statement of the textbook version of this theorem (Hazan, Introduction to Online Convex Optimization, Theorem 3.3), OnlineConvexOpt.FirstOrder.online_gradient_descent_strongly_convex_regret, but it is Disproved: its regret is written with a real infimum over the decision set, which Lean evaluates to a junk value. No proved version of the logarithmic bound is on the platform. The strong-convexity inequality, the one-step projected-gradient inequality and the telescoping argument are reusable by every later formalization of gradient methods on the platform.
The argument is short, and its difficulty lies in the bookkeeping. The telescoping sum of squared distances cancels exactly only with the right step-size indexing: the step taken after round must be . Reading Fig. 1 literally with makes the step after round equal to , and the sum then leaves an uncancelled term that the printed bound does not contain. Strong convexity is a statement about the Hessian, so the curvature inequality (1) needs a second-order Taylor expansion along a segment of ; convexity of keeps the segment inside the set where the Hessian bound holds. The projection step needs the obtuse-angle property of Euclidean projection onto a convex set.
Points are EuclideanSpace ℝ (Fin n), so is the Euclidean norm (the sup norm of Fin n → ℝ would change the gradient bound). Cost functions are functions on all of , as the paper's use of gradients and Hessians presupposes; the gradient is Mathlib's gradient, and the Hessian quadratic form is the second Fréchet derivative applied to . Rounds are 1-based: x 0, f 0 and η 1 are never read, and sums run over Finset.Icc 1 T. The run of the algorithm is a predicate on the whole trajectory, required at every round; the projection is a predicate (nearest point of ), which is unique for nonempty closed convex .
Choices and corrections relative to the printed text:
η (t + 1) = 1 / (H * t) for on the step sizes of Fig. 1.A regret bound written with a real ⨅/sInf over , or a bound for an arbitrary sequence satisfying Eq. (2) instead of a run of the paper's algorithm, would not be Theorem 1; the goal quantifies over every comparator in and carries the run predicate, the Hessian hypothesis and the gradient bound. The hypotheses are jointly satisfiable: on the closed unit ball, with meets all of them.
Contributions welcome: proofs of the two inequalities and of the goal; a general projection lemma for positive semidefinite (Lemma 8 in full, needed by the Online Newton Step mission) is reusable beyond this mission.
In many operational problems (shortest paths, assignment, planning) the decision solves a linear program whose cost vector is unknown at decision time and is predicted from contextual features. The predict-then-optimize pipeline fits a model that maps a feature vector to a predicted cost vector , and then acts on the decision that is optimal for . Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed to measure the quality of such a model not by the prediction error but by the SPO loss (Smart Predict-then-Optimize loss): the excess true cost of the decision induced by the prediction over the best decision in hindsight.
The question is whether a small SPO loss on the training sample implies a small SPO loss on new data, uniformly over the models a training procedure may return. The SPO loss is neither convex nor continuous in the prediction, so the standard Lipschitz-based bounds for regression do not apply. El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3, Mathematics of Operations Research 2023; a preliminary version appeared at NeurIPS 2019) give the first such generalization bounds. This mission formalizes their first one, for polyhedral feasible regions, which treats every vertex of the feasible region as a class label of a multiclass classification problem. The bound has since been used by later work, e.g. Hu, Kallus and Mao (Fast rates for contextual linear optimization, Management Science 2022), who sharpen it by a factor (as noted on p. 4 of the paper).
A feasible region is nonempty, compact and convex. For a cost vector the nominal problem is . An optimization oracle is a fixed map with for every ; nothing is assumed about how it breaks ties. The SPO loss of a prediction when the realized cost is is
The linear optimization gap is , and for a set of cost vectors ; the SPO loss of a cost in lies in .
Data are pairs drawn from a distribution on . A hypothesis class is a family of predictors . The SPO risk is , and on an i.i.d. sample the empirical SPO risk is . The empirical Rademacher complexity with respect to the SPO loss is
with independent uniform signs , and is its expectation over the sample.
The decisions induced by form the class . A class N-shatters a finite set if there are two labelings that differ at every point of such that every mixture of them (follow on a subset , on the rest) is realized by some member of . The Natarajan dimension is the largest size of an N-shattered set. When is a polyhedron, denotes its finite set of extreme points.
For a polyhedral and every , with probability at least over an i.i.d. sample of size , every satisfies
UnderstandingML.natarajan_lemma): a class from an -point set to labels with Natarajan dimension has at most members.The bound controls the out-of-sample decision cost of every predictor in the class, not only of an empirical risk minimizer, so it applies to any training procedure (SPO+ surrogate minimization, decision trees, heuristics) that returns a member of . Its dependence on the feasible region is only through and : the number of vertices of a combinatorial polytope is typically exponential in , and enters only logarithmically. For linear predictors the paper's Corollary 2 bounds by , giving a rate of order .
The results are proved in the paper; this mission formalizes them. No statement about predict-then-optimize or the SPO loss is known to have a machine-checked proof. The platform already has the Natarajan lemma (proved) and several Massart-type lemmas for generic classes; this mission connects that multiclass machinery to decision losses, and its Theorem 1 is a reusable Rademacher generalization bound for a loss with range .
The obvious route through Lipschitz contraction fails: the SPO loss jumps when the prediction crosses a point where the optimum is not unique, so the Rademacher complexity of the composed class cannot be bounded by that of times a Lipschitz constant. Any argument through the finitely many vertices of needs the decisions to take finitely many values on a sample, i.e. the oracle to return vertices; for an oracle that returns a non-vertex optimal point under ties, may take infinitely many values on a sample. On the probabilistic side, the passage from the empirical to the expected complexity and the McDiarmid concentration step (Theorem 1) require the suprema over an uncountable class to be measurable, which the paper does not discuss.
Lean works in = EuclideanSpace ℝ (Fin d); cost vectors and decisions live in the same space and is the inner product. The standing assumptions of §2 are hypotheses of every theorem: nonempty, compact and convex; an arbitrary oracle (a hypothesis IsOracle S w, never a specific selection); nonempty and bounded, with the cost component of in almost surely (or, for fixed-sample statements, every ); . "Polyhedron" means the solution set of finitely many linear inequalities; with compactness it is a polytope, and is the cardinality of Set.extremePoints ℝ S. The expectation over signs is the exact average over the sign vectors; and are Bochner integrals. "With probability at least " is stated as: the product measure of the set of samples on which some violates the bound is at most .
The formalization commits to the following disclosed additions:
A formalization that let be an sSup in , or chose a specific tie-breaking oracle inside the definitions, would prove a different and in part trivial statement; both are excluded.
Infrastructure needed: McDiarmid's bounded-differences inequality and symmetrization for the product measure; Massart's finite-class lemma (a proved version is on the platform as RademacherMassart.rad_le_massart, with its own normalization); the Natarajan lemma (proved, UnderstandingML.natarajan_lemma, stated with its own but identical notion of N-shattering over finite types); finiteness and nonemptiness of the extreme points of a nonempty polytope. Theorem 1 and the Massart step do not use polyhedrality and are reusable for any bounded decision loss. Contributions of these infrastructure lemmas are welcome.
In Witten's cubic open string field theory (Witten 1986) the interaction glues half-strings together, and in the usual center-of-mass variables the action contains infinitely many time derivatives. Such a theory has no evident initial value formulation, which obstructs a Hamiltonian treatment and a direct discussion of causality.
Erler and Gross (2004) show that after a unitary change of basis in which the string field depends on the lightcone component of the string midpoint (and on transverse center-of-mass coordinates), the cubic vertex contains no derivatives with respect to lightcone time. This reduces to five linear relations among the Neumann coefficients of the three-string vertex, the midpoint identities (A.6)–(A.10) of the paper. One of them, (A.8), is a closed numerical identity: a specific infinite series built from Neumann coefficients equals , where is the zero-mode Neumann coefficient. This mission formalizes that identity and the chain of intermediate results the paper uses to prove it (Appendix B), together with a divergence statement from Section 2 explaining why other midpoint bases fail.
Define real constants () by the expansion
For real the left side is , so is the -th Taylor coefficient of at (e.g. ). The even Neumann vector and the vector are
In Lean these are ErlerGross.neumannA, ErlerGross.neumannMEven (with neumannMEven n ) and ErlerGross.betaVec. Two auxiliary objects appear in the proof: the (B.3) terms
(ErlerGross.b3Term) and the -basis integrand
(ErlerGross.kappaIntegrand), which arises from the continuous spectrum of the Neumann matrices (Rastelli–Sen–Zwiebach 2001).
formalized as: the series converges absolutely (Lean HasSum) to .
In the paper, (A.8) is one of the relations which, together with (A.6), (A.7), (A.9), (A.10), removes lightcone-time derivatives from the cubic vertex. This is what gives the theory an initial value formulation in lightcone time and makes the Hamiltonian BRST quantization of Section 4 possible. Unlike the other four identities, which are relations between distributions and are verified in the paper's spectral basis, (A.8) is an equality of real numbers. It can therefore be checked completely in Lean.
A complete formalization would produce a machine-checked proof of a Neumann-coefficient identity. It would also add reusable material: Taylor coefficients of , the integral, and digamma-type evaluations of rational series.
The goal defines through Taylor coefficients, which have no closed form. The paper does not sum the series in the mode basis. It moves to the continuous basis of the Neumann spectrum and closes a contour. That step rests on eigenvector expansions and the principal-value distribution , neither of which is in Mathlib. A direct route has to connect the coefficients to the integral , or to the series , some other way. The terms of decay like . The terms of the goal series decay only like , so the goal series converges slowly.
iteratedDeriv.HasSum is unconditional (equivalently absolute) convergence. Every statement asserts convergence, so no statement can hold only because Lean assigns to a divergent tsum.The index theorem says that among several Markov reward processes, of which one may be advanced at each decision time, the right one to advance is the one of greatest Gittins index. Chapter 4 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks how far this extends when the constituents are not reward processes but decision processes, each with its own controls: a research project that can be run in several ways, a job that can be processed at different speeds, a sampling process that may be stopped and exploited. A family of such superprocesses requires two choices at every decision time, which superprocess to continue and with which control, and an index policy in the sense of Chapter 2 need not be optimal (Example 4.1). Whittle (1980) identified the condition under which it is: Condition D, that when a superprocess is played against a standard bandit process paying a constant rent, the control one should apply to it does not depend on the rent. Under that condition the index theorem survives (Theorem 4.3), the index is characterized (Note 4.2), stoppable bandit processes with improving stopping options satisfy the condition (Lemma 4.4), and the chapter adds two results about indices themselves: any index that works for all bandit processes is a strictly increasing function of the Gittins index (Theorem 4.8), and a policy that is within of the index policy loses at most (Theorem 4.18).
A decision process on a countable state space has in each state a nonempty finite set of controls; applying yields the reward and moves the state by . Adding the freeze control, which leaves the state unchanged and yields nothing, makes a superprocess . Operating under a feasible deterministic stationary Markov policy (that is, ) gives an ordinary bandit process , and the superprocess index is
with the Gittins index of the Bandit Algorithms model. A simple family of alternative superprocesses (SFAS) is superprocesses on a common ; at each decision time exactly one is continued, with a control from its control set, the others being frozen, and rewards are discounted by . A policy is a Markov kernel per decision time from the history to the pair (superprocess, control); it is optimal if it is feasible and attains the supremum of the discounted payoff over feasible policies from every initial state-vector, and it is an index policy if it always continues a superprocess and control of maximal .
Condition D. Let be a standard bandit process with parameter (one state, reward ). satisfies Condition D if there is a function such that, for every and for which it is optimal in the family to select in state , it is optimal to apply the control . A stoppable bandit process is a bandit process with a stop control that makes it behave as a standard bandit process with parameter ; its stopping option is improving if is almost surely nondecreasing in process time.
For a decision process with bounded rewards and a Condition-D control , every index policy with respect to that applies to the superprocess it continues is optimal for the family of superprocesses:
Note 4.2 (under Condition D, is selected in iff , and at a control is optimal iff ; the printed equivalence fails for ); Lemma 4.4 (Condition D for stoppable bandit processes with improving stopping options); Theorem 4.8 (an index for the bandit processes with discount factor is strictly increasing in ); Theorem 4.18 (the -index bound, for the discrete-time index).
Theorem 4.3 is the widest form in which the index theorem holds without further structure, and Condition D is exactly the right hypothesis: it says the superprocess has a canonical control, and once it does the family reduces to a family of bandit processes and the prevailing-charge argument goes through. Lemma 4.4 gives the model where the condition is known to hold, a research project that may be exploited at any time; the buyer's problem of Bergman and Bather is the case where it fails. Theorem 4.8 explains why every index theorem in the book is about the Gittins index: any function that orders bandit processes optimally must order them as does. Theorem 4.18 is the quantitative version of the index theorem that heuristics and computations rely on.
Nothing here is machine-checked. The mission builds the first controlled multi-armed model on the platform, a run law for families of decision processes with an explicit feasibility constraint, and states Whittle's condition as a property of the two-member family, which is how the literature uses it. Theorems 4.8 and 4.18 are statements about the existing Bandit Algorithms model and are usable by any later work on that model.
The obvious attack on Theorem 4.3, "replace each superprocess by the bandit process for its Condition-D policy and apply the index theorem", is the second half of the book's proof; the first half is to show that an optimal policy never gains by applying a control other than to a superprocess it continues, and that uses the prevailing-stake accounting of §4.3 with the other superprocesses treated as one bandit process, plus the observation that the class of policies deviating at most times is -exhaustive. Both halves require the whole run law of the family to be related to the run laws of its constituents, which is where a formalization spends its effort. Note 4.2 is short on the page but needs the optimal-stopping characterization of Chapter 2 for the bandit process under charge . Theorem 4.8 is elementary given the value of under a freezing rule, , but that identity is itself a computation on the run law. Theorem 4.18 has no proof in the book (Glazebrook 1982c); the natural route is the prevailing-charge upper bound with the charges perturbed by .
Decision processes carry their control sets as finsets with a nonemptiness proof and their kernels as Markov kernels; the state space is countable with measurable singletons (so stationary kernels and control-dependent maps are measurable without side conditions) and the control type is finite with measurable singletons. The family's run law is built decision time by decision time as the Bandit Algorithms model builds markovBanditMeasure, with the policy's kernel producing the pair (superprocess, control). Feasibility is an almost-sure condition on the policy kernel, and optimality is the book's: feasible, and the supremum from every initial state-vector. The superprocess index is a real supremum over feasible stationary policies with , bounded by the reward bound and nonempty for ; for an unavailable it is a default value that no index policy consults. Condition D is stated on the family on , where the standard state has every control available, all equivalent. A stoppable bandit process is the decision process with control type Bool. Theorem 4.8 quantifies over index functions defined on every measurable state space and takes as hypothesis only what its proof uses, optimality of -index policies for the families . Theorem 4.18 is on the -armed Bandit Algorithms model with and the bound : the book's is in continuous-time index units, times the discrete-time index used here, and read with the discrete index it is false for . Theorem 4.3's index policy applies the Condition-D control to the superprocess it continues, as the book's proof does; an index policy that breaks ties among controls otherwise need not be optimal.
Trivializing readings are excluded: index policies must be feasible, optimality is required from every initial state, and Condition D is a statement about optimal policies of a genuine two-member family, not about a chosen policy. Welcome contributions: the relation between the family's run law and the constituents' chain laws, the freezing-rule value identity behind Theorem 4.8, and the prevailing-stake accounting of §4.3.