Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A reproducing kernel Hilbert space (RKHS) is a Hilbert space of functions in which evaluation at each point is a continuous functional. Each such space is determined by its kernel, and in practice spaces are usually given by their kernels: Gaussian or Sobolev kernels in kernel methods and Gaussian-process regression, the Bergman and Szegő kernels in complex analysis. A recurring question is therefore how a relation between two function spaces reads on their kernels. When is one space contained in another? When do two kernels define the same space?
N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) answers both questions. §7 (pp. 354–356) compares a class with a contractively included subclass. §13 (C) (pp. 382–383) uses Banach's closed graph theorem to remove the contractivity assumption. The answer is an order relation between kernels, checkable on finite point sets. It is the standard tool for comparing RKHSs: Part II of the paper (§2, p. 387) applies §7, Theorem II to compare Bergman kernels of nested plane domains.
Let be an arbitrary set (no topology, no measure). A function is a positive matrix if
for every finite family and every . For two kernels, means that is a positive matrix.
A class with a reproducing kernel is a complex Hilbert space of functions for which there is a function with and for all and . The scalar product is linear in . Every such is a positive matrix, and by Moore's theorem (§2 (4)) every positive matrix is the kernel of exactly one such class. A linear class of functions is an (R.K.)-class if some norm makes it a Hilbert space with a reproducing kernel. Such a class carries many admissible norms, and correspondingly many kernels.
In the Lean development, is a Mathlib RKHS ℂ H X ℂ instance on a complete complex inner product space H. The class of functions is Set.range (⇑ : H → X → ℂ). The scalar kernel is kernelFn H x y = RKHS.kernel H x y 1, and is AronszajnRK.Limits.KernelLE K₁ K (the series' shared definition).
For classes with reproducing kernels :
The constant is left unspecified: it measures the norm of the inclusion operator and has no canonical value.
The result. Corollary IV₂ reduces inclusion of infinite-dimensional function spaces to positivity of finite matrices. Corollary IV₃ says when two kernels give the same space, as sets of functions with equivalent norms. Kernel-method theory uses these facts to compare hypothesis spaces of different kernels. In complex analysis they compare Bergman spaces of nested domains, since the restricted kernel of a larger domain is dominated by the kernel of a smaller one (Part II, §2, p. 387, of the paper). Theorem VI makes (R.K.)-classes a lattice under intersection and sum.
Formalizing it. All statements are classical and have been proved since 1950. To our knowledge none is machine-checked. Mathlib has RKHSs, their kernels, positive semidefiniteness of kernels and the construction of a space from a kernel. It has no comparison theorem between two RKHSs, and no characterization of an RKHS by its kernel up to inclusion or equality of function sets. This mission adds these. As a by-product it produces the closed-graph argument for RKHS inclusions in a form that other missions can reuse.
The sufficiency direction () does not follow from the definitions alone. Domination is a statement about finite quadratic forms; membership of a function of in is a statement about an infinite-dimensional space, and nothing pointwise connects the two. The paper's argument rests on the sum theorem of §6, the goal of a separate mission in this series.
The necessity direction cannot start from an assumed norm inequality, because the two norms are a priori unrelated. Producing the constant needs the closed graph theorem together with the fact that norm convergence in an RKHS implies pointwise convergence. A direct estimate of against from the inclusion alone has no route to a uniform constant.
RKHS ℂ H X ℂ instance on a complete complex inner product space H. The function of f : H is ⇑f.⟪f, g⟫_ℂ is conjugate-linear in f, so Aronszajn's is ⟪g, f⟫_ℂ, and the reproducing property is ⟪k y, f⟫_ℂ = f y.Matrix.PosSemidef over the index type X. Its quadratic form over finitely supported vectors is exactly the paper's. Over it includes Hermitian symmetry, which nonnegativity implies. is fun x y => (M : ℂ) * K x y with real .RKHS instance, since having a kernel is the conclusion. It is a complex Hilbert space with an injective linear map into the functions of .Trivializations ruled out. No statement defines a class as RKHS.OfKernel K and then asserts that its kernel is K. Classes are always compared through their sets of functions and norms. "" is never weakened to the existence of some injection .
Substrate. Mathlib's RKHS, RKHS.kernel, RKHS.kerFun, RKHS.kerFun_inner, RKHS.posSemidef_kernel, RKHS.OfKernel, Matrix.PosSemidef (with .add, .smul), Banach's LinearMap.continuous_of_isClosed_graph, and the continuous functional calculus (CFC.sqrt, for the square root in the proof of Theorem II). The sum theorem of §6, used in the proof of Theorem I, is the goal of mission I of this series. Contributions of that theorem and of reusable lemmas on RKHS inclusions are welcome.
Shadow tomography asks for predictions of many specified measurements of an unknown quantum state, while using as few prepared copies of that state as possible. The requested output is a list of acceptance probabilities, not a full description of the state. A procedure might exploit the fact that these are only numbers, even when the state has dimension . The natural question is how far this saving can go. Aaronson's paper gives upper bounds and separates two sources of difficulty: one already present for ordinary probability distributions, and one arising from noncommuting quantum measurements.
This mission concerns the first source. It formalizes Theorem 16, which says that even when the state and every requested measurement are diagonal in the same basis, the number of copies must grow with in the relevant asymptotic regime. In that special case, the unknown state is an ordinary distribution on outcomes. The theorem therefore puts a limit on any proposed improvement to shadow tomography that would promise fewer copies in all instances.
A mixed state on a -dimensional system is a positive semidefinite complex matrix with trace one. A two-outcome measurement is represented by an effect satisfying ; it accepts with probability . When is diagonal, its diagonal entries are the probabilities of the basis outcomes. When is diagonal too, it specifies a randomized yes-or-no test on those outcomes. These conventions are stated in Section 3 of the paper.
Given effects , a shadow-tomography strategy measures independent copies and outputs estimates . It succeeds on when every estimate differs from by at most . The lower bound requires success probability at least for every diagonal mixed state. The strategy may make a joint quantum measurement on all copies and may choose its estimates from its observed outcome. This is the same measurement model used in Problem 1.
The goal is the classical clause of Theorem 16. There are absolute constants and such that, for , , and , there are diagonal effects with 0/1 entries, corresponding to the known Boolean functions in Section 6.1, for which every strategy successful on all diagonal states must use
The hard measurements are chosen before the strategy is quantified. The statement therefore also rules out a strategy with a smaller copy count that works uniformly for all quantum states and measurements. Its constants and threshold express the notation in Theorem 16, rather than specifying a numerical optimum.
Four milestones come from the proof on pages 20–21: the high-probability overlap bound for independently chosen half-size subsets (Eq. (1)); the acceptance probability of a subset under its associated biased distribution; an upper bound on the mutual information between the hidden subset index and the observed samples; and the exact entropy formula with a quadratic entropy deficit. These statements expose the combinatorial and information-theoretic parts of the lower bound while leaving the goal as the paper's copy-complexity result.
Theorem 16 sets a floor for shadow tomography that survives even when all operators commute. Any uniform copy bound for the full quantum task must respect this floor. The result also distinguishes the difficulty of predicting many properties of a distribution from the extra difficulty possible for noncommuting states and measurements, which the paper treats in a separate lower bound. Section 6 presents both bounds.
A complete formalization would give machine-checked statements and proofs for the finite subset construction, the entropy calculation, the information inequality, and the reduction from a successful quantum measurement procedure on diagonal states to a lower bound on . The theorem is proved on paper; these draft statements are open Lean goals and do not claim that its proof has been machine checked. The finite-distribution and information-theory infrastructure is reusable for other lower bounds based on hidden-index families.
Counting how many possible measurements there are does not by itself show that samples reveal enough about which distribution generated them. The lower bound needs a quantitative relation between estimation accuracy and information about a hidden index, while each individual sample carries limited information. The paper's printed overlap condition (1) is too weak for the next displayed estimate: at its boundary it gives . The milestone preserves Eq. (1) as printed; closing the goal requires the correspondingly sharper overlap fact with , which follows from the same type of concentration statement after adjusting its constant. The printed assertion that learning the index requires mutual information at least is also imprecise at success probability ; a quantitative decoding inequality is needed. Neither incorrect display is a draft milestone.
Matrices are indexed by Fin D. WildeQIT.IsDensityOperator supplies the mixed-state predicate and . Diagonal states and effects use the standard matrix diagonal predicate. An effect is positive semidefinite together with its complement. The tensor power uses functions Fin k → Fin D as basis indices; at it is a one-by-one identity matrix. A strategy is a finite-outcome POVM on that tensor power, followed by a real estimate vector for each outcome. The output values are not restricted to : clipping them to this interval cannot worsen an estimate of a probability. No restriction to classical estimators is placed in the goal; that would change the allowed strategies before the theorem has been proved.
The asymptotic threshold excludes the one-dimensional and single-measurement corners where the claimed rate does not describe the problem. The bound keeps the biased distributions used on page 20 nonnegative; would permit a zero-copy constant estimate. Subset milestones require even or explicitly require a half-size subset, so has its intended meaning. The natural logarithm appears nowhere in the lower-bound rate; entropy, mutual information, and use base two. At zero probability the entropy convention is .
The finite distributions, entropy, conditional entropy, and mutual information reuse the published WildeQIT definitions. Contributions that prove the four source milestones, establish the sharper overlap fact, or supply the quantitative decoding step are welcome. The goal must retain its order of quantifiers: one hard measurement family, then every strategy, with success demanded on every diagonal state.
A stochastic approximation algorithm is a recursion with decreasing step sizes and a noise term . Recursions of this form appear in stochastic gradient methods, adaptive control, learning in games (fictitious play, reinforcement learning) and urn models. The ODE method compares the iterates with the solutions of . In Benaïm's lecture notes (Benaïm 1999), the comparison is phrased through the continuous-time interpolated process . Under standard noise conditions, is almost surely an asymptotic pseudotrajectory of the flow of , and its limit set is almost surely internally chain transitive.
That theorem constrains where the process may end up. It does not say which of several candidate sets the process actually reaches. When the ODE has several attractors, for example several stable equilibria of a learning dynamic or several stable compositions of an urn, an application needs to know that each attractor is reached with positive probability. Section 7 of the notes answers this question. The answer is a criterion of attainability: if the process can, with positive probability and at arbitrarily late times, enter the basin of an attractor, then it converges to that attractor with positive probability.
Timeline.
Let be a metric space and let be a semiflow on : a continuous map with and .
Now let be a process on a probability space with continuous paths in , adapted to a filtration . The standing assumption of Section 7 is that for all , and ,
for a function with as .
A point is attainable if for every and every open neighbourhood of . is the set of attainable points.
If is locally compact, is an attractor of , and , then
This statement contains no constants and no rates, so it does not depend on how (24) is quantified for a particular algorithm.
If is open and relatively compact with , there are , depending only on (and on , ), such that for every process satisfying the standing assumption and every
The result. Theorem 7.3 turns a question about the long-run limit of a random process into a question about where the process can go. Attainability is usually checked by a controllability argument: the noise can push the iterates in every direction. For urn processes with an urn function mapping the simplex into its interior, every point is attainable (Example 7.2 of the notes). Then every attractor of the mean ODE is reached with positive probability. Combined with nonconvergence results for unstable sets (Section 9 of the notes), this characterizes the possible limits of many learning and urn processes. Theorem 7.3 is the positive half of that picture.
Formalizing it. The theorem has a published proof (p. 32 of the notes) and no machine-checked version. A formal proof needs the following:
The obvious argument says: once enters a compact part of the basin, the flow carries it into . That fails because is not a trajectory of the flow. Each window of length adds an error, and errors over infinitely many windows can push the process out of the basin.
Two things are needed instead:
A naive union bound over all times is useless: it does not use the conditional form of (24).
Flow ℝ≥0 M on a metric space; local compactness is LocallyCompactSpace M.X : ℝ≥0 → Ω → M with continuous paths. The paper's alternative of càdlàg paths is not covered.Filtration ℝ≥0. is a probability measure.These choices rule out the trivializing formalizations: a conditional-probability hypothesis that holds vacuously, invariance read as inclusion, constants that depend on the process or on , and a probability bound without monotonicity.
A complete development needs:
The first and second are reusable well beyond this mission. Contributions toward either, and alternative proofs of Lemma 6.8, are welcome.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-90 mission already covers every , the new work is the range from 89 to 90.
The argument for was reached by tightening its estimates step by step, starting from 256. With its current choices those estimates stop working below 90, and nobody has yet found a way past that point. It is not known whether 90 is a real limit of the method or only of the choices made so far, so this mission is the smallest test of whether the cutoff can move at all. The accepted proof for and its research note are the natural starting point. The goal theorem below gives the exact statement.
This is an open entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 89 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryGradient methods are the workhorse of large-scale nonlinear optimization and of the training of statistical models. In practice the direction actually used is rarely the exact negative gradient: it may be scaled, computed incrementally one data component at a time, or perturbed by approximation error. The classical convergence theory of such methods often assumes that the iterates stay bounded, that the objective is bounded below, or that the errors vanish at a prescribed rate, and these assumptions must then be checked separately for each method.
Bertsekas and Tsitsiklis (2000) proved convergence results for gradient methods with errors that need none of these assumptions. Their deterministic result (Proposition 1) allows a general descent direction together with an error whose size is proportional to the stepsize, and concludes that either the objective values diverge to or they converge and the gradients tend to zero. It applies, among others, to the incremental gradient method for a sum of functions (Proposition 2 of the same paper), which underlies backpropagation-style training. The stochastic counterpart (Proposition 3, zero-mean errors) is the subject of a companion mission.
Throughout, is a continuously differentiable function whose gradient is Lipschitz continuous: for some constant ,
Here is the Euclidean norm and the standard inner product. The gradient method with errors generates a sequence of iterates
where is the stepsize, is a descent direction and is an error vector. Nothing is assumed about how and are produced, beyond the two conditions below, which hold for some positive scalars and every :
The stepsizes are diminishing in the standard sense:
A stationary point of is a point with ; a limit point of is the limit of some subsequence.
Under (2.1), (2.2), (2.3) and the stepsize conditions, either
or else converges to a finite value and
Furthermore, every limit point of is a stationary point of .
The milestones follow the paper's own argument, in order.
The result. Proposition 1 separates two concerns that are usually entangled: what the method guarantees, and what must be known about . It concludes stationarity of all limit points and convergence of the gradients to zero without assuming that the iterates are bounded or that is bounded below; when is bounded below the first alternative is excluded and follows outright. Because need not be the negative gradient and need not vanish faster than the stepsize, the result covers scaled gradient methods, incremental gradient methods for sums of functions, and gradient methods with deterministic approximation error. The descent inequality (2.4) and the deterministic supermartingale-type Lemma 1 are standard tools that recur throughout optimization theory.
Formalizing it. The proposition is proved in the paper; it has not been machine-checked. A formal proof would give a reusable, verified convergence theorem for a broad class of first-order methods on , together with a formal descent lemma for functions with Lipschitz gradient, which Mathlib does not currently state in this form, and a deterministic Robbins–Siegmund-type lemma for sequences.
The summability estimate (2.6) gives only . Passing to is the main step: the obvious argument (a summable series with forces the gradient norms to zero) is false in general, because a nonnegative sequence with these two properties may still have infinitely many large terms. What is missing is a bound on how far can travel while the stepsizes are small, and only (2.1) and (2.2)–(2.3) together supply it. A second difficulty is that there is no boundedness of the iterates: every estimate must hold globally, and the error is controlled only relative to , which may be unbounded along the sequence.
EuclideanSpace ℝ (Fin n), is the real inner product ⟪x, y⟫_ℝ, and is Mathlib's gradient f; the hypothesis ContDiff ℝ 1 f makes it the true gradient. The paper's statement is for and the formalization does not generalize to Hilbert spaces.LipschitzWith L (gradient f) with L : ℝ≥0; this is equivalent to (2.1) for some real constant.Contributions welcome: proofs of the descent lemma and Lemma 1 (both reusable well beyond this mission), and of the steps (2.5)–(2.6) and the excursion argument.
A stochastic approximation algorithm is a recursion
in , where is a vector field, are small step sizes and is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of .
Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (and the iterates are bounded, or is Lipschitz and bounded on a neighbourhood of them), the interpolated process is an asymptotic pseudotrajectory of the flow of . A probabilistic step then verifies A1 for concrete noise models. This mission formalizes the first such verification, Proposition 4.2: martingale difference noise with bounded -th moments and step sizes with . The result is described as a particular case of a general theorem of Métivier and Priouret (1987); the same estimates reappear later in the notes.
Let be a deterministic sequence with , and (a step sequence). Put , , and let
be the index of the step that contains time . For a sequence define the piecewise constant processes and , so that step occupies the time interval of length .
Assumption A1 asks that for every
or, in the form the notes call equivalent, for every , where
Let be a probability space with a nondecreasing sequence of sub--algebras, and continuous. A sequence given by the recursion above is a Robbins–Monro algorithm if is deterministic, is -measurable, and .
For a Robbins–Monro algorithm and some real , if
then with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all .
Proposition 4.2 is the standard sufficient condition under which the ODE method applies to stochastic gradient-type recursions with martingale noise. With it covers step sizes with (for example ) and noise with bounded variance; larger trades stronger moment assumptions for slower decay of the steps, down to . Combined with Proposition 4.1 it shows that the interpolated process of a Robbins–Monro algorithm with bounded iterates is almost surely an asymptotic pseudotrajectory of the flow of ; the limit set theorems of the notes then locate the limit points of the algorithm.
The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would supply reusable pieces that Mathlib currently lacks, most notably a Burkholder (or Burkholder–Davis–Gundy) inequality for discrete-time vector martingales in , and the continuous-time bookkeeping of the step processes , and the noise deviation , shared by the other missions of this series.
The obvious argument controls each window by Doob's maximal inequality and sums over windows. That works for only. For the second moment of the window sums is not summable under , and one needs an maximal inequality whose right-hand side is the -th moment of the square function. That inequality, Burkholder's, is not in Mathlib. Converting the square function into the moment bound requires a Hölder-type inequality with tuned exponents, and passing from the discrete sums to requires handling partial steps at both ends of . A second subtlety is that A1 quantifies over all : the almost-sure statement must hold on a single event of full probability for every , not on an event that depends on .
The space is as EuclideanSpace ℝ (Fin d); time is real; is a real number with , and all powers are real powers of nonnegative quantities. The sequences and are indexed by , and their values at are unused, as the paper indexes them from . The filtration is a Mathlib Filtration ℕ, is required to be -strongly measurable and integrable, and the martingale difference condition is almost surely. Expectations of nonnegative quantities, the suprema in A1 and , and the moment bound are taken in , so no default value of a non-integrable expectation or of an empty supremum can make a statement hold vacuously; the supremum over an empty range of is .
The following readings are excluded and are not acceptable formalizations: a moment hypothesis that holds vacuously, a conditional expectation hypothesis on non-integrable noise, the conclusion "for each , A1 holds almost surely" in place of "almost surely, A1 holds for all ", and fixed to or restricted to integers.
All hypotheses are satisfiable: , , and with satisfy every one of them.
Contributions welcome: a general Burkholder inequality for discrete-time martingales in finite-dimensional spaces (reusable well beyond this mission), lemmas on the step processes and (measurability, local integrability, additivity), and the proofs of the milestones.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Salikhov's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (7.606309 : ℝ), i.e. .
Value. The bound is quoted as (e.g. by Zeilberger–Zudilin), a truncation. This entry rounds the last digit up to .
Salikhov uses integrals of rational functions that are symmetric under a group of transformations (in the spirit of Rhin–Viola), which gives larger arithmetic savings in the common denominators than Hata's construction.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Zeilberger–Zudilin's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (7.103205334138 : ℝ), i.e. .
Value. The paper states its bound as , a truncation. This entry rounds the last digit up to so that the goal follows from the published proof.
Zeilberger and Zudilin modify Salikhov's integrals and use the Almkvist–Zeilberger algorithm (creative telescoping) to find recurrences for them, then optimise the arithmetic and analytic estimates. This is the current record.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Hata's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (8.016046 : ℝ), i.e. .
Value. The paper computes the exponent as and states the rounded bound . This entry rounds the computed value's last digit up to , which is still below the paper's and above .
Hata obtains simultaneous approximations to from complex contour integrals of Legendre type, with extra arithmetic savings from primes that divide the coefficients to a predictable extent. His linear-form measure is , giving (stated in the paper as ). It stood as the record for about fifteen years.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
A stochastic approximation algorithm is a recursion with decreasing steps and noise . Stochastic gradient descent, the Robbins–Monro procedure, reinforcement-learning updates and learning dynamics in games all have this form. The ODE method compares such a recursion with the deterministic dynamics . Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) do this in two steps. First, the limit set of the interpolated process is internally chain transitive for the semiflow of (Theorem 5.7, the subject of mission 1 of this series). Second, internally chain transitive sets are located using properties of the dynamics alone.
The most common tool in the second step is a Lyapounov function: a function that decreases strictly along every trajectory outside a set and is constant on . Proposition 6.4 of the notes states exactly when such a function forces every internally chain transitive set into . It is the step behind the convergence of stochastic gradient algorithms to critical points (Corollary 6.7) and behind convergence results for learning in potential games.
Timeline.
Let be a metric space, with no compactness or completeness assumed. A semiflow on is a continuous map , , with and .
Let be compact invariant and a Lyapounov function for , and assume that has empty interior in . Then for every internally chain transitive set ,
The result. Proposition 6.4 converts a statement about real numbers, that has empty interior, into a statement about dynamics: the chain recurrent behaviour of is confined to . With Theorem 5.7 it gives the following. If has such a Lyapounov function, then the limit set of any precompact asymptotic pseudotrajectory, in particular of a bounded stochastic approximation process, lies in , and is constant on it. When is the set of equilibria and is Lebesgue-null by Sard's theorem, this is the convergence of stochastic gradient algorithms to connected sets of critical points (Corollary 6.7). Remark 6.5 gives a flow on the circle with a strict Lyapounov function, where the circle itself is internally chain transitive. So the empty-interior hypothesis cannot be removed.
Formalizing it. The result is proved, in the notes and in the earlier literature. No machine-checked version of chain recurrence for semiflows on metric spaces, Conley's attractor lemma, or Bowen's characterization of chain transitive sets is known to us. The mission therefore adds the following:
Flow;The obvious argument does not work. It runs: decreases along trajectories, so along an orbit in the value of must settle on . But points of an internally chain transitive set are joined only by pseudo-orbits. At each of the jumps, may increase by an amount that is small but not controlled in number, so monotonicity of along true trajectories says nothing directly about . Remark 6.5 shows that the conclusion is genuinely false without a condition on . The difficulty is therefore global: pseudo-orbits that climb back up through many small jumps must be excluded using information about the restricted semiflow as a whole, not the monotonicity of along single trajectories. Milestones 1 and 2 are the general facts about chain transitive sets that this requires, and their own proofs involve compactness and uniform-continuity estimates over arbitrarily long pseudo-orbits.
MetricSpace, and the semiflow is Flow ℝ≥0 M.interior (V '' Λ) = ∅ in , not countability, finiteness or measure zero.IsGLB, not a real sInf.The following formalizations are trivializing and are excluded:
A complete development needs elementary facts about ω-limit sets of points of a compact invariant set: they are nonempty, compact and invariant. It also needs the attractor construction and the open sets used in Proposition 5.3. These are reusable for any work on Conley theory. Contributions of any of these lemmas, or of proofs of the milestones in any order, are welcome.
Reinforcement learning formulates control as maximizing reward accumulated over time. For continuing tasks, where interaction never terminates, the standard textbook objective is the discounted return with a discount rate . Chapter 10 of Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018), argues that once values are approximated by a function of features rather than stored per state, this objective is the wrong one, and it proposes the average-reward setting, long standard in dynamic programming (Puterman, Markov Decision Processes, 1994), as its replacement.
The central piece of evidence is a short calculation printed in the box The Futility of Discounting in Continuing Problems (p. 254). If one tries to rescue discounting by averaging discounted values over the states the policy actually visits, the resulting objective is a constant multiple of the average reward, so the discount rate has no effect on which policy is preferred. This mission formalizes that calculation together with the definitions of §10.3 that it rests on, and the two exercises of §10.3 that illustrate the differential value (10.13).
A finite MDP has finite state set , finite action set , finite reward set and dynamics , a probability distribution over next state and reward for each state–action pair (3.2)–(3.3). Write . A policy is a distribution over actions for each state. It turns the MDP into a Markov chain with transition matrix and expected one-step reward , so that and .
A stationary distribution of is a probability vector on with
The average reward of is
the second form holding when the steady-state distribution exists and does not depend on (an ergodic MDP).
The discounted value function is , and the objective of the box is
Finally, the differential value of a state (10.13) is .
For , every policy and every stationary distribution of ,
and therefore, for a fixed and policies with their own stationary distributions,
The book prints no answers to Exercises 10.6 and 10.7; the values above were computed for this mission.
The result itself. The identity shows that the discount rate cannot enter the ranking of policies once performance is measured over the on-policy state distribution: any objective of the form "discounted value averaged over where the policy goes" is the average reward up to a positive factor. The book draws from it the conclusion (p. 253) that changes from a problem parameter to a solution-method parameter, and that discounting algorithms with function approximation, which do not optimize this averaged objective, are not guaranteed to optimize average reward either. Milestones 1–2 connect the closed form of to its definition as a long-run rate; milestone 4 explains why differential methods determine values only up to an offset; the exercises show that (10.13) gives finite differential values in periodic chains where the differential return (10.9) has no limit.
Formalizing it. The results are classical and elementary, but the book's derivation is informal: it takes the Bellman equation for granted, sums a geometric series of equalities, and leaves implicit which distribution is meant and when (10.6) and (10.7) agree. This mission fixes each of those points: is defined from returns, the identity is proved for every stationary distribution, and the ergodicity hypothesis is made the exact limit condition the text states. No machine-checked version of these statements is known to exist; the platform's Markov-chain and average-reward libraries (Puterman's unichain optimality equation, Doeblin convergence) state different results.
The box reads as a chain of equalities, and each individual step is short. The one step that is not algebra is "(Bellman Eq.)": with defined as an expected discounted return, the Bellman equation requires exchanging an infinite sum with a finite expectation and shifting the index of a convergent series, which needs absolute convergence for and bounded rewards. The final line, which unrolls into a geometric series, is only valid because is finite. For milestone 1, the book's hypothesis is the existence of an -independent limiting distribution, not irreducibility or aperiodicity; replacing it by either would change the statement. The exercises require the iterated limit in (10.13) to be computed explicitly: the inner limit is a periodic series summed in closed form, and the outer limit is a removable singularity at .
The Lean development lives in the namespace SuttonBartoRL.AverageReward. States, actions and rewards are finite; one action set serves every state; the dynamics are the four-argument . Probabilities and are computed from the matrix powers . The discounted value is a real series ; it is not defined as the solution of the Bellman equation, since that definition would reduce the goal to three lines of algebra. The average reward and take the state distribution as an explicit argument; the goal holds for every stationary distribution of and assumes no ergodicity, which is all the box uses (under ergodicity is the unique one). is allowed. The differential value (10.13) is stated as the existence of both limits with the given value, with from below, so no default value of a nonexistent limit can make a statement true. The optimality equations use a nonempty action set. The sum of (10.6) is written with the index shifted to .
The Lean does not formalize a trajectory probability space: expectations and probabilities are the matrix expressions above, which is what they equal for a Markov chain. The Exercise 10.6 hypothesis constrains expected rewards of one policy, which is all the exercise uses.
Reusable parts: the finite-MDP layer duplicates the one drafted for the other missions of this series and is expected to be merged with it; the Cesàro and stationary-distribution lemmas of milestones 1–2 are general facts about finite Markov chains. Contributions welcome: proofs of any milestone, and a proof of the goal from milestone 3.
Many problems in signal processing, statistics and machine learning take the additively separable form
a smooth term plus a nonsmooth but "simple" term , such as an penalty or the indicator function of a convex constraint set. The forward-backward method alternates a gradient step on with a proximal step on . Beck and Teboulle's FISTA (Beck–Teboulle 2009) combined it with Nesterov's acceleration and improved the worst-case rate for function values from to . Whether the iterates of the accelerated scheme converge at all, and not just their function values, remained unsettled for a long time; in the words of Attouch and Peypouquet, it "puzzled researchers for over two decades".
Timeline.
The case , the original choice of FISTA, is not covered by this result.
Let be a real Hilbert space with scalar product and norm .
Given and , algorithm (2) generates by
The auxiliary sequence (6) is . For a point , the proof of Theorem 3 uses
A sequence converges weakly to , written , if for every .
In Lean these are theta, extrap (), IsAccelFBRun and zSeq (shared definitions in the namespace NesterovFB.Rates), and deltaSeq in the namespace NesterovFB.Weak. The predicates IsProperClosedConvex and IsProx and the predicate WeakTendsto are reused from the platform.
Under the assumptions above, with and ,
The limit is required to be a minimizer of ; weak convergence to an arbitrary point would be a weaker statement.
For every and :
The result. Theorem 3 shows that the accelerated forward-backward method with behaves like the unaccelerated method in one important respect: its iterates converge to a solution rather than just producing small function values. In infinite-dimensional settings (inverse problems, PDE-constrained optimization, signal recovery in function spaces) weak convergence is the natural notion, and strong convergence can fail. The four milestones are the steps that matter for other analyses too: a "Fejér-type" step inequality from the extrapolated point, and the convergence of the distance to every minimizer.
Formalizing it. The result is proved in the literature; no machine-checked proof of it is known. A complete formalization needs the energy estimates of the paper's §1.1–1.2 (summability of , boundedness of , and the convergence of ), which a companion mission poses separately, and Opial's lemma, which is not in Mathlib.
The unaccelerated forward-backward method is Fejér monotone: decreases for every minimizer , and Opial's lemma applies directly. The accelerated iterates are not Fejér monotone. The first milestone only compares with the extrapolated point , and can exceed by the inertial term. The quantity therefore satisfies only a second-order inequality with coefficients that grow in . The obvious attempt, to show that is eventually monotone and apply Opial's lemma as for the unaccelerated method, fails.
A second difficulty is the passage from distances to weak convergence: in a Hilbert space this needs the weak sequential compactness of bounded sets and the weak lower-semicontinuity of (to place weak cluster points in ).
InnerProductSpace ℝ H, CompleteSpace H), not ; in finite dimensions weak and strong convergence coincide and the goal would be a different, weaker theorem.EReal; is never assumed real-valued.WeakTendsto, not convergence in norm.A trivializing formalization is ruled out by the sanity check: the hypotheses are jointly satisfiable, and the goal asks for weak convergence to a minimizer, so neither a vacuous hypothesis nor an arbitrary limit point is admitted.
Infrastructure that a complete development needs, and that is reusable beyond this mission: the descent inequality (9) of the proximal-gradient operator, Opial's lemma in a real Hilbert space, the weak lower-semicontinuity of proper lower-semicontinuous convex functions, and the lemma that a bounded real sequence whose positive increments are summable converges. Contributions of any of these are welcome.
Convex duality in optimization rests on one transformation: to a convex function one associates the function , which records, for each slope , the best affine lower bound of with that slope. Lagrangian duality, the duality theory of linear and conic programming, the analysis of first-order methods through smoothness and strong convexity of conjugates, and the dual representations of risk measures and divergences all read off properties of from properties of . Each of these uses needs one fact: that the transformation loses no information, so that applying it twice returns .
That fact, for functions on , is the theorem of W. Fenchel's five-page note On conjugate convex functions (Canad. J. Math. 1 (1949) 73–77). Its timeline:
Points of are , and .
A standing pair consists of a set and a real function defined in such that
need be neither open, nor closed, nor bounded. The paper writes the lower limit as a "lim" with a bar under it; the milestone texts write it , and it always means .
The conjugate pair of is
The same construction applied to gives the pair , with . An interior point of is a point of the relative interior of , its interior within its affine hull.
In Lean: IsClosedConvexPair G f, conjDomain G f , conjFun G f , and is conjDomain (conjDomain G f) (conjFun G f), conjFun (conjDomain G f) (conjFun G f).
For every standing pair :
with equality for some at every interior point of ;
and every standing pair whose conjugate pair is equals .
The theorem identifies, among convex functions on convex subsets of , exactly the class on which conjugation is a bijection and an involution. It is the finite-dimensional base case of the Fenchel–Moreau theorem and underlies Fenchel's duality theorem for , the conjugate-based optimality conditions of convex programming, and the inversion of gradients of conjugate differentiable convex functions (the paper's §6, the Legendre transformation). The pair form is also how the result is used in practice: the conjugate of a function finite on a set comes with an explicit domain , and the theorem says that domain determines and is determined by .
The result has been proved for 75 years. What a formalization adds is the theorem in Fenchel's own form: a real-valued function on an explicit convex domain rather than an extended-real function on all of , the domain identity together with the identity of values, and the attainment of equality in (5) at relative-interior points. Machine-checked versions of biconjugation exist in other forms: for extended-real functions on Hilbert spaces, for finite convex functions on all of , and for functions on a set with a closed restricted epigraph over continuous linear functionals. None of them states the domain identity or the attained equality, and none is in the paper's pair form.
Milestones 1, 3, 4 and 5 follow from the definition of the conjugate alone. The content sits in three places.
Fin n → ℝ with its product topology, which is the Euclidean one; is Mathlib's x ⬝ᵥ ξ. The paper's in is ξ ⬝ᵥ x, equal by commutativity.(Fin n → ℝ) → ℝ, but every hypothesis and conclusion concerns its values on only: ConvexOn ℝ G f, LowerSemicontinuousOn f G, and Tendsto f (𝓝[G] x) atTop for x ∈ closure G \ G.sSup, which is on unbounded sets; it is evaluated only on .intrinsicInterior ℝ G). The paper's segment definition makes the equality clause false, and the topological interior makes it vacuous for lower-dimensional .Fin n → ℝ and the intrinsic interior), affine minorants of convex functions on lower-dimensional domains, and the boundary-limit argument of milestone 6. All of these are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome.Many problems in convex optimization, variational inequalities and equilibrium modelling reduce to finding a point with , where and are maximal monotone operators on a real Hilbert space : for example, minimizing for closed proper convex is the case , . When the resolvent of is hard to evaluate but the resolvents of and separately are easy, one uses a splitting method. Douglas–Rachford splitting, introduced for monotone operators by Lions and Mercier (1979) after an alternating-direction scheme of Douglas and Rachford (1956) for the heat equation, is the most widely used one; through its dual form it underlies the alternating direction method of multipliers (ADMM) used throughout large-scale optimization and statistics.
Eckstein and Bertsekas (MIT report LIDS-P-1919, 1989; Mathematical Programming 55, 1992) showed that Douglas–Rachford splitting is a special case of the proximal point algorithm applied to a single derived operator, the splitting operator . This identification lets the convergence theory of the proximal point algorithm transfer to splitting, and yields a generalized method with inexact resolvent evaluations and relaxation.
Timeline.
An operator on is a subset , with ; it may be multivalued and partially defined. Its domain is , its image the projection on the second coordinate, its inverse . Scaling and sum are and ; is the identity. is monotone if for all , and maximal monotone if no other monotone operator strictly contains it. The resolvent is , and . An operator is firmly nonexpansive if for all .
For the Douglas–Rachford map is , and the splitting operator is
Its zero set is .
Let , be maximal monotone, , and let , and satisfy
with , and . Then
In the paper's order: Minty's theorem (Theorem 1); properties of firmly nonexpansive operators (Lemma 1); the monotone / firmly nonexpansive correspondence (Theorem 2, Corollaries 2.1–2.3); zeros as fixed points of resolvents (Lemma 2); the generalized proximal point algorithm (Theorem 3): weak convergence to a zero of under summable errors, relaxation in and stepsizes bounded away from , unboundedness when ; (maximal) monotonicity of (Theorem 4) and firm nonexpansiveness of its resolvent (Corollary 4.1); (Theorem 5); and (Theorem 6).
Theorem 7 gives convergence of Douglas–Rachford splitting with both resolvents evaluated inexactly and with over- or under-relaxation, and it characterizes the case without a solution: the iterates are unbounded exactly when has no zero. The relaxed, inexact form is the one implementations actually run, and through Gabay's identification of ADMM with Douglas–Rachford on the dual it is the basis of the paper's Theorem 8, a convergence theorem for a generalized ADMM. Theorem 3, used to prove Theorem 7, is itself a standard reference form of the inexact relaxed proximal point algorithm.
All results here are proved in the paper (one step in the unbounded case of Theorem 3 rests on results of Rockafellar 1969 and 1970 on sums of maximal monotone operators). As of 2026, neither Douglas–Rachford splitting in this generality nor the generalized proximal point algorithm is formalized in Lean or Mathlib. Mathlib has Hilbert spaces, weak topologies and summability, but no theory of maximal monotone operators, Minty's theorem or resolvents. The mission builds that layer and machine-checks the paper's results on it.
The convergence argument cannot be strong: in infinite dimensions the proximal point algorithm need not converge in norm (Güler 1991), so the conclusion is weak convergence, and identifying the weak limit as a zero requires the weak–strong closedness of the graph of a maximal monotone operator. The maximality halves of Theorems 2 and 4 need Minty's theorem, whose proof requires a nontrivial existence argument (all known proofs use Zorn's lemma or an equivalent). The unbounded case of Theorem 3 is a contradiction argument that truncates by the subdifferential of the indicator of a ball and invokes two external facts: maximality of the sum of two maximal monotone operators under an interiority condition (Rockafellar 1970), and existence of zeros for maximal monotone operators with bounded domain (Rockafellar 1969). Neither is available in Lean. The natural first idea for Theorem 7, iterating the firm nonexpansiveness of , gives neither the error tolerance on both resolvents nor the unbounded case without the full machinery of Theorem 3.
[CompleteSpace H]). An operator is a map H → Set H. Monotonicity, maximal monotonicity, , and the function-level resolvent predicate IsResolvent are the published definitions ThreeOpSplitting_Convergence_MonotoneOperators; weak convergence is the published WeakTendsto ( for every ).opResolvent, IsFirmlyNonexpansiveOp, ...), so Theorem 2 and Corollary 2.1 can speak of resolvents that are a priori partial or multivalued. In Theorems 3, 6 and 7 the resolvents are maps with for all , unique by Corollary 2.2.IsResolvent hypothesis would make the iteration unrelated to and ; the hypothesis is always present.Summable with nonnegative terms. Sequences start at ; is unused. Unboundedness is ¬ Bornology.IsBounded (Set.range z).A manufacturer that makes one product to stock faces random demand, can produce at most units per period, and can store at most units. The classical result without the production limit is that a base-stock policy is optimal: raise inventory to a fixed level each period. With a production limit, the natural modification is to produce up to when that is possible and to produce at full capacity otherwise. Federgruen and Zipkin (1986) proved that this modified base-stock (critical-number) policy is optimal under the long-run average-cost criterion, for discrete demand with a general convex cost. Production-capacity models of this type are standard in operations management texts, and the result underlies the computational and comparative-static work that followed, starting with Part II of the same paper, which treats discounted costs.
Timeline.
Time is divided into periods . The demands are independent copies of a random variable with values in and probability mass function ; write and . At the start of period the inventory is an integer (negative values are backorders). The decision maker raises it to
pays the expected one-period cost , and demand is subtracted: . The order cost per unit is set to zero, as in the paper; this loses no generality because every policy with finite average cost has the same average order cost.
The standing assumptions are: is convex and as (Assumption 1); the characteristic function of is analytic at the origin (Assumption 2), and ; for some positive integer (Assumption 3); and (Assumption 4). The smallest global minimizer of is , and .
A Markov policy is a sequence of maps with . The critical-number policy with critical number is . A stationary policy is strongly optimal with average cost if, from every initial state , its average cost converges to , while every Markov policy has lim-inf average cost at least from every initial state.
The analysis uses the operators and , and the optimality equation
For an interval , is the largest expected sum of , over policies forced to produce at capacity below and to produce nothing above , until the inventory first returns to .
There exist , and such that solves (6), is convex with global minimizer , and
The in the optimality claim is the minimizer constructed in part (a).
The result. Theorem 1 reduces an infinite-state average-cost control problem to a one-parameter search over critical numbers. The paper then evaluates the average cost of by a renewal formula, proves it convex in (Theorem 2), and in §5 extends optimality to unlimited storage. The strong form of optimality matters: it compares with every Markov policy from every starting state, and it compares lim-infs, not only lim-sups.
Formalizing it. The theorem has a published proof, but no machine-checked one, and its proof relies on external results that are themselves unformalized: the countable-state average-cost theory of Federgruen, Schweitzer and Tijms, a fixed-point theorem on a compact convex subset of a product space, and a large-deviation estimate quoted from Feller. A formal development produces reusable infrastructure: expected first-passage sums for integer-valued random walks with a reflecting control, polynomial moment bounds for them, and the convexity-preservation argument for capacitated value iteration.
The state space is unbounded below, so the finite-state theory of average-cost Markov decision processes does not apply, and the one-period cost is unbounded. The obvious approach, letting the discount factor tend to one in the discounted problem, needs uniform bounds on relative value functions. Those bounds come from the expected cost until the inventory returns to a fixed interval, and with capacity limits that expectation must be controlled with growth uniformly over a class of policies. This is the content of Lemma 3, whose proof combines a large-deviation estimate for the demand sums with a renewal-type recursion. A second obstacle is strong optimality: comparing with policies whose lim-inf average cost is smaller requires that the relative value function grows sublinearly along every admissible trajectory (Corollary 2).
All objects are in the namespace FedergruenZipkin.AvgCost, defined in one file. States and the capacity are integers; demands are natural numbers with a real probability mass function p; is a positive natural number. Convexity on is the second-difference inequality. Expectations of a real function are series ; expected policy costs and hitting sums are -valued and need no integrability side condition. Feasibility and all properties of value functions are required only on states , which are the only states visited. Assumption 2 is stated literally, as real-analyticity of at . The order cost is zero, as in the paper. is a parameter characterised as the least minimizer of , not an infimum.
"Strongly optimal" has no displayed definition in the paper; it is read from eq. (7) in the proof of Theorem 1(b): convergence of the average cost of to from every state, together with a lim-inf lower bound for every Markov (memoryless, possibly nonstationary) policy from every state. The class is neither widened to history-dependent policies nor narrowed to stationary ones. The goal additionally records that converges, that has growth , and that ; all three follow from the paper's proof.
A trivializing reading is ruled out: the existence of , and is one existential, so cannot be decoupled from the solution of (6), and strong optimality includes the convergence of 's own average cost to , so does not satisfy it vacuously.
Not posed: Lemma 1 (quoted from Feller, and replaceable by a Chernoff bound); the renewal formulas (10)–(11) and Theorem 2; and §5 (unlimited storage). Useful contributions include a formal theory of expected hitting sums for skip-free-upward random walks, and a proof of Lemma 3 by any route.
Many problems in statistics and machine learning minimize an average of losses, one per data point, plus a regularizer: least squares, logistic regression, and their - or -penalized versions. When is large, a full gradient costs component gradients, while stochastic gradient descent, which uses one component per step, needs decreasing step sizes and converges slowly. Incremental gradient methods with variance reduction (SAG, SVRG, SDCA, Finito, MISO) use one component gradient per step but converge at the rate of a full-gradient method.
SAGA (Defazio, Bach and Lacoste-Julien, NIPS 2014, arXiv:1407.0202) is a method of this family. It handles a non-smooth regularizer through its proximal operator, and it comes with a guarantee when the losses are convex but not strongly convex. This mission covers that second guarantee, Theorem 2 of the paper. A companion mission covers the linear rate under strong convexity (Theorem 1, Corollary 1).
Timeline.
Let and . The components are convex and differentiable, and each gradient is -Lipschitz (). Write
The regularizer is convex but possibly non-differentiable. The objective is the composite function , and is any minimizer of . Minimizers need not be unique, and need not vanish.
The proximal operator with parameter is
SAGA keeps an iterate and a table of points , initialized as . At step it draws an index uniformly from , independently of the past, and sets
It then sets and leaves the other table entries unchanged. The averaged iterate is , which excludes .
With step size , for every ,
The expectation is over the indices . The constants are those printed in the paper.
In milestones 3–5, is the expectation over the single index of the next step, given the current state.
The result. Theorem 2 shows that one method, with a step size that depends only on , covers composite problems that are not strongly convex. Examples are -regularized least squares and logistic regression without a ridge term. On these problems the method converges in expected objective value at rate . SAG has no proximal analysis, and SDCA requires strong convexity. With the same step size , the paper also states adaptivity to strong convexity, so no strong convexity constant has to be known in advance. The bound is in terms of , a quantity computable from the starting point.
Formalizing it. The result is proved on paper, but the proof is not self-contained. Its central inequality (milestone 4) is quoted from the prox-SVRG analysis of Xiao and Zhang, with only the remark that their argument uses . A machine-checked proof must therefore reconstruct that argument for SAGA's estimator. To our knowledge, no machine-checked proof of SAGA, SVRG or prox-SVRG exists in Lean or Mathlib. The mission also produces reusable statements about convex functions with Lipschitz gradients (Lemmas 1 and 2) and an explicit finite model of a randomized incremental method.
The naive approach applies the non-expansiveness of the proximal operator to , as in the strongly convex proof. That bounds distances, but it produces no term in . Without strong convexity, the distance terms cannot be traded for function values, so the argument yields no rate.
The function-value term comes from the prox-SVRG inequality (milestone 4), which the paper does not prove. Its difficulty is that depends on the same random index as , so the cross term between them does not vanish in expectation even though . A second difficulty is bookkeeping: uses the old table, the table entry receives and not , and the constants must make three coefficients vanish exactly. A final step converts the bound on into a bound on , which requires Jensen's inequality for the convex .
EuclideanSpace ℝ (Fin d). Components are indexed by Fin n (0-based), with .f' with HasGradientAt (f i) (f' i x) x at every point. Smoothness is the Lipschitz bound .ConvexOn ℝ Set.univ. Lemma 1 uses StrongConvexOn Set.univ μ, whose modulus is the paper's.Two trivializations are excluded. The averaged-iterate bound carries , since at the factor collapses to . The left side is evaluated at the averaged point, not the average of , which is a weaker intermediate step.
A complete development needs the descent lemma and co-coercivity for convex functions with Lipschitz gradients, the characterization and non-expansiveness of the proximal operator, and finite-sum manipulations over index sequences. The lemmas on smooth convex functions and on proximal operators are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, a reusable proximal-operator library, and the telescoping argument for the goal.
A Markov decision process (MDP) is solved for one model of its dynamics and rewards, but in practice that model is estimated from data, and a policy that is optimal for the estimate can perform poorly on the true system (Mannor et al., 2007). Robust MDPs address this by evaluating a policy against the worst model in an uncertainty set (Iyengar, 2005; Nilim and El Ghaoui, 2005; Wiesemann, Kuhn and Rustem, 2013). Robust planning, however, solves an inner optimization over at every Bellman update, which is expensive and does not scale to learning settings.
A separate line of work regularizes the policy (entropy, KL, Tsallis penalties) and observes empirically that regularized policies are robust to perturbations (Geist, Scherrer and Pietquin, 2019). Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) make this precise: for uncertainty sets centred at a nominal model, the robust value function is the solution of a regularized problem posed on the nominal model alone, with a regularizer that is the support function of the uncertainty set. This mission formalizes that equivalence: Proposition 3.1, Theorem 3.1 and Theorem 4.1 of the paper.
Let and be finite sets of states and actions, nonempty, and . Fix a discount factor and a strictly positive initial distribution . A transition kernel assigns to every pair a probability distribution on ; a reward is . A policy assigns to every state an action distribution .
For write , , and define the evaluation Bellman operator
The inner product on is , and the support function of a set is .
Given a set of models , the robust Bellman operator is
and the robust value function is its fixed point. Around a nominal model , an s-rectangular uncertainty set is given by sets and , one per state: its models are and , with and chosen independently for each . Finally .
For and every policy , has a unique fixed point , and it is the optimal solution of
Theorem 3.1 is the special case of the goal; it is listed separately because it is the paper's statement that policy regularization is equivalent to reward uncertainty.
The goal says that a robust MDP with s-rectangular uncertainty in both reward and transitions is a regularized MDP on the nominal model, with two regularizers: a policy regularizer coming from reward uncertainty, and a regularizer coming from transition uncertainty that depends on both the policy and the value. For ball-shaped sets these support functions are explicit ( and , Corollary 4.1 of the paper), which leads to the twice regularized (R²) Bellman operators of Section 5 and to robust planning at the cost of non-robust planning. Theorem 3.1 also explains why standard policy regularizers (negative entropy, KL, Tsallis) yield robustness: each is the support function of a reward uncertainty set.
The results are proved in the paper (appendices A.1, A.2, B.1); none has a machine-checked proof. The mission produces formal statements and proofs of the equivalence, the robust Bellman operator's fixed-point theory for stochastic policies and general compact uncertainty sets, and a closed-form robust counterpart that later R² results can import. The paper's printed proof of Proposition 3.1 treats as linear in one step; a formal proof settles the statement independently of that step.
The obvious argument reads Proposition 3.1 as linear-programming duality, as for a single MDP. That fails: is a minimum of affine maps, hence concave and not affine, and the feasible set of is an intersection of infinitely many half-space systems; the argument has to go through monotonicity and contraction of , which in turn requires every model in to be a genuine transition kernel. For the goal, the paper invokes Fenchel–Rockafellar duality to evaluate the inner maximum; the work in Lean is to separate the maximum over the product set into per-state maxima, which needs the s-rectangular structure and attainment of every maximum (compactness), and to track the index order of the perturbation against the kernel .
A nonempty; values are S → ℝ ordered pointwise; a transition array is P : S → A → S → ℝ with P s a s' , and the kernel property is the published IsTransitionKernel; is the published InducedTransition. A policy has π s ∈ stdSimplex ℝ A for every s.S × A → ℝ indexed , as in the paper's ; rewards perturbations are A → ℝ.sInf/sSup. Every theorem assumes the sets nonempty and compact, so these are attained; nothing is quantified over an unbounded set.Contributions welcome: the monotone-contraction fixed-point lemma for and the per-state separation of maxima over rectangular sets are reusable for any robust MDP mission.
Many problems in machine learning and statistics are finite sums: an empirical risk over data points, often plus a regulariser such as an penalty. When is large, a full gradient of costs component gradients, while stochastic gradient descent uses one component per step but converges only sublinearly because its gradient estimate has non-vanishing variance. Incremental gradient methods with variance reduction keep the per-step cost of one component gradient and still converge linearly on strongly convex problems.
SAGA, introduced by Defazio, Bach and Lacoste-Julien at NIPS 2014 (arXiv:1407.0202), is one of the standard methods of this family, alongside SAG, SVRG, SDCA and Finito/MISO. It keeps a table of past component gradients and handles a non-smooth regulariser through its proximal operator.
Timeline. Le Roux, Schmidt and Bach (2012) gave SAG the first linear rate for strongly convex finite sums at the cost of one gradient per step. Shalev-Shwartz and Zhang (2013) proved linear rates for SDCA, a dual method. Johnson and Zhang (2013) introduced SVRG, with periodic full-gradient passes; Xiao and Zhang (2014) extended it to composite objectives (prox-SVRG). SAGA (2014) combines an unbiased SVRG-style estimator with a SAG-style table, and proves a linear rate in the composite strongly convex case with a simple Lyapunov argument.
Let carry the Euclidean inner product. There are differentiable components with gradients . Each is -strongly convex (): for , . Each gradient is -Lipschitz: . Write and . The regulariser is convex, and the goal is to minimise the composite objective ; denotes its minimiser, which is unique.
The proximal operator with step is
SAGA keeps an iterate and points at which the stored gradients were taken. It starts from with . At iteration it draws uniformly from , independently of the past, and sets
then , with every other entry unchanged.
The analysis uses the Lyapunov function
With , for every ,
where the expectation is over the indices drawn in the first iterations. The constants are the paper's.
With as above, and , for every state ,
with the expectation over the next index only.
Lemma 4 (p. 10), a lower bound combining strong convexity and smoothness; Lemma 1 (pp. 6–7), its average over the components; Lemma 2 (p. 7), which bounds the stale-gradient variance by the table part of ; and Lemma 3 (p. 7), a second-moment bound for the SAGA step.
The result. Corollary 1 gives an -accurate iterate in expectation after component-gradient evaluations. This is the complexity of full-gradient descent with the condition number decoupled from , and it holds in the composite setting, so it covers the lasso and elastic-net problems that SAG's analysis does not reach. The paper notes that the rate improves on the published rates of SAG and SVRG and is within a factor 2 of SDCA's. Theorem 1 is the template of later Lyapunov analyses of variance-reduced methods.
Formalizing it. The result has been proved since 2014, and no machine-checked proof is known to this mission. The work left is to formalize the known proof: the convexity inequalities (Lemmas 4, 1, 2), the variance computation (Lemma 3), the one-step contraction (Theorem 1), and the passage from conditional to total expectation along the random index sequence (Corollary 1). The paper's Lemma 3 has a sign misprint, which the formalization corrects; see the scope section.
The obvious argument for SGD-type methods bounds in terms of alone. That fails here: the variance of the SAGA estimator depends on the stale table points , which can be far from even when is close. One needs a potential that also measures the table. Balancing the terms of then requires the four round-bracket coefficients in the paper's display (10) to be non-positive for the specific , and an auxiliary . Checking these coefficients is routine but long algebra in , , . The composite case adds one step: since in general, the argument goes through the fixed-point identity and the non-expansiveness of the proximal operator, neither of which is a numbered result of the paper.
Space and data. The space is EuclideanSpace ℝ (Fin d). Components are indexed by Fin n (0-based), with 0 < n. The gradients are given maps with HasGradientAt (f i) (f' i x) x. Strong convexity is Mathlib's StrongConvexOn Set.univ μ, whose modulus is the paper's.
Regulariser and minimiser. is real-valued and convex; extended-valued regularisers are out of scope, as on the page. A minimiser of is a hypothesis.
Proximal operator. It is any map such that minimises for every (IsProxPoint). The minimiser is unique, so is .
State and expectation. The state is the pair . The run after steps is a deterministic function of the index sequence in Fin k → Fin n. The expectation in Corollary 1 is the average over all sequences, which is exactly the law of independent uniform indices; no measure theory is involved. Theorem 1's conditional expectation is the average over the next index.
Constants and corrections. Constants are as printed and fixed, not "for some constant" and not "for all small enough steps". Lemma 4 carries the hypothesis , which its fractions require. Lemma 3 is stated with , as in its proof and its use in Theorem 1; the printed is false whenever .
Trivializing formalizations, ruled out. Taking the proximal step as merely non-expansive, fixing an index sequence instead of averaging over all of them, measuring against instead of , or restricting Theorem 1 to reachable states changes the theorem and is excluded.
Infrastructure. A complete development needs:
These pieces are reusable well beyond SAGA, by SVRG, SAG and proximal-gradient analyses. Contributions of any of them, or of proofs of the individual milestones, are welcome.
The simplex method solves linear programs very fast in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972, for Dantzig's rule; Goldfarb, 1983, for the shadow-vertex rule). Average-case analyses (Borgwardt, 1980s; Smale, 1983) explained good behaviour on random inputs, but random inputs look nothing like real ones. Spielman and Teng introduced smoothed analysis to close this gap: the input is chosen by an adversary and then perturbed by a small Gaussian, and the running time is measured in expectation over the perturbation. They proved that the shadow-vertex simplex method has smoothed complexity polynomial in the number of constraints , the dimension and (Spielman–Teng, J. ACM 2004; this mission follows the preprint arXiv:cs/0111050v7). The work received the Gödel Prize (2008) and the Fulkerson Prize (2009).
Timeline. Borgwardt (1977–1987) bounded the expected number of shadow-vertex pivots for rotationally symmetric random data. Spielman and Teng (2001, STOC; journal 2004) proved the first smoothed bound, with a shadow bound of order — the theorem of this mission. Deshpande and Spielman (FOCS 2005) improved the shadow bound, Vershynin (2009) reduced the dependence on to polylogarithmic, and Dadush and Huiberts (STOC 2018) obtained for small .
Fix and . The data are vectors , the constraint vectors of the linear program subject to for all . Each is a Gaussian of standard deviation centered at a point with : it has density
and the are independent (joint density ).
For a direction , is the set of index sets with such that is linearly independent, the simplex is a facet of , and lies in the cone . In polar terms, is the set of tight constraints at the vertex of the feasible polyhedron that maximizes .
For linearly independent , the shadow is the set of index sets that belong to for some nonzero . Its size is the number of vertices of the projection of the feasible polyhedron onto the plane ; the shadow-vertex method walks along this polygon, one pivot per vertex. Finally
for every , , every pair of linearly independent , every and all centers of norm at most .
The milestones follow the paper's proof, leaves first.
The result. Theorem 4.0.1 is the geometric heart of the smoothed analysis of the simplex method. Section 4.3 of the paper extends it to arbitrary centers, covariances and right-hand sides, and Section 5 combines these extensions with a two-phase method to show that the simplex method has polynomial smoothed complexity. The same shadow bound underlies later analyses of the simplex method, of perturbed polytopes' diameters, and of condition numbers of random linear programs.
Formalizing it. The theorem has been proved, and improved constants are known, but none of this is machine-checked. A formal proof would verify a long and delicate argument: a change of variables of integral geometry (Blaschke's formula), several conditional-density estimates, and explicit constants in the millions. The mission also produces reusable statements about Gaussian vectors and convex hulls of random points.
The obvious approach is to count, for each candidate facet , the probability that appears in the shadow; there are candidates, so a union bound is exponential in . The paper avoids this by discretizing the angle of (Lemma 4.0.6) and bounding, for each fixed direction, the probability that the optimal facet changes within a small angular step. That needs a lower bound on the angle between and the boundary of its optimal facet, conditioned on the facet being optimal. The conditioning changes the distribution of , so the bound cannot come from the Gaussian density alone. The proof changes variables to the facet's normal , offset and in-plane coordinates (Corollary 2.5.3), whose Jacobian contributes the factors and . It then shows that both the distance of the origin to a face of the in-plane simplex and the angle of incidence are unlikely to be small. Measure-theoretic bookkeeping is as hard as the geometry: densities known only up to normalization, conditioning on events of positive measure, and the measure-zero degeneracies the paper sets aside.
Points live in EuclideanSpace ℝ (Fin d). Constraint vectors are indexed by Fin n (0-based), so the paper's is . The Gaussian of standard deviation centered at is Lebesgue measure with the density above, and the joint law is the product measure. Lemma 4.0.6 also uses Mathlib's multivariateGaussian with a positive definite covariance. Expectations of shadow sizes are lower Lebesgue integrals of -valued counts, and their measurability is part of each conclusion. "Density proportional to " and conditional probabilities are stated cross-multiplied, , so no appears.
The shadow is the set of index sets , and the direction is excluded. Including it would add every facet of to the shadow, since lies in every cone, and make the goal false. is represented exactly in , never by a real infimum. Where the paper omits a hypothesis it uses, it is added and recorded in the item: the standing assumptions , and (Lemma 4.2.3 is false without a bound on ), unit length of the reference vector , , and for strict inequalities. Lemma 2.3.7 is stated with rather than the page's , which fails in an edge case.
Infrastructure a complete development needs: Gaussian tail and chi-square estimates; faces and facets of convex hulls; the Blaschke change of variables and the latitude–longitude change of variables on the sphere (not in Mathlib); surface measure on (Mathlib's Measure.toSphere); and the disintegration of the joint law used in the combination lemma. The Gaussian estimates, the combination lemma and the Blaschke formula are useful beyond this mission. Proofs of any milestone, and of supporting lemmas such as the change-of-variables formulas, are welcome.
A perfect graph is one whose coloring problem has a particularly sharp answer on every induced subgraph: the fewest colors needed is exactly the size of its largest clique. This makes a local obstruction, a clique, certify the optimum number of colors throughout the graph. Claude Berge proposed in 1961 that perfection could be recognized by the absence of two kinds of induced odd cycles, one in the graph and one in its complement. The equivalence became known as the strong perfect graph conjecture. Chudnovsky, Robertson, Seymour, and Thomas proved it in their 2006 paper, which also proves a structural decomposition of the graphs under study. The paper connects this question to graph coloring, Shannon capacity, and linear and integer programming. Chudnovsky et al., pp. 51–54
The earlier complement theorem was proved by Lovász in 1972 and appears as Theorem 1.1 in the paper. The strong conjecture remained unresolved for roughly four decades; the authors' Theorem 1.2 settles it. Their proof places a second result, Theorem 1.3, beside the equivalence: a graph with no forbidden odd hole or antihole must either belong to a basic class or admit one of several specified decompositions. The graph classes and decompositions are therefore part of the statement of the route to the main result, not merely vocabulary for a proof. Chudnovsky et al., pp. 52–56
All graphs here are finite and simple. The complement has the same vertices as , and two distinct vertices are adjacent in exactly when they are not adjacent in . For a vertex set , the notation means the induced subgraph on . A clique is a set of pairwise adjacent vertices. Its largest possible size in a graph is , and is the minimum number of colors in a proper vertex coloring of .
A hole is an induced cycle of length at least four. An antihole of is a hole in . A graph is Berge if every hole and antihole has even length. Thus a perfect graph requires for every , while a Berge graph satisfies a restriction on induced cycles in both and . “Induced” matters: a cycle with a chord is not a hole. Chudnovsky et al., pp. 51–52
For the structural milestones, a basic graph is a bipartite graph, the complement of one, a line graph of a bipartite graph, the complement of such a line graph, or a double split graph. The latter consists of paired vertices and with the within-pair and between-pair adjacencies specified on pp. 52–53. A proper 2-join partitions the vertices into two sides with two prescribed complete cross-edge blocks, connected-component conditions on both sides, and a special odd-path condition. A proper homogeneous pair is a pair of vertex sets whose outside vertices split into four nonempty adjacency classes. A balanced skew partition has one side disconnected and the other disconnected in the complement, together with parity restrictions on induced paths and antipaths. Chudnovsky et al., pp. 52–54
The goal is the exact equivalence for every finite simple graph:
No order bound, chosen graph class, or decomposition hypothesis is attached to the goal. Chudnovsky et al., p. 52, 1.2
Theorem 1.1 says that perfect implies perfect. Theorem 1.5 says that a minimum imperfect graph, a Berge nonperfect graph with the smallest vertex count among all such graphs, cannot admit a balanced skew partition. Theorem 13.5 says that a recalcitrant graph—a Berge graph with the listed line-graph, double-split, 2-join, homogeneous-pair, and balanced-skew outcomes absent—has or bipartite. Theorem 1.3 states the decomposition conclusion:
The milestone order records the two reduction results, the later structural capstone, and the decomposition statement it yields. The paper's other section results that establish 13.5 are posed in the remaining missions of this series. Chudnovsky et al., pp. 52, 54–55, 154
Theorem 1.2 gives a forbidden-induced-subgraph characterization of perfect graphs. Its cycle condition is intrinsic to the graph and its complement; its coloring condition quantifies over every induced subgraph. Together with Theorem 1.3, it ties a numerical property of colorings to explicit graph structures and separations. The complement theorem and the exclusion of decompositions for a minimum imperfect graph explain why the structural alternatives have the strength needed for the equivalence. Chudnovsky et al., pp. 52–56
The mathematical theorem was proved in the cited paper. This mission poses its statements in Lean and seeks machine-checked proofs; the draft theorem declarations are open targets. The definition layer is useful beyond this mission: induced holes, Berge graphs, perfection, balanced skew partitions, and the decomposition predicates can support the later missions without changing what each source statement means. No machine-checked proof of these draft targets is claimed here.
The forward implication can be tested on induced odd cycles, but that observation does not settle the converse. Excluding odd holes and antiholes does not give an immediate coloring of an arbitrary induced subgraph. The paper instead establishes a detailed account of what a Berge graph can look like when it is not in a basic class. The delicate point in turning this account into Theorem 1.2 is that each decomposition outcome must be incompatible with a minimum imperfect graph. Ordinary skew partitions are too broad for that role; the balanced parity conditions are part of the statement. The structural conclusion 13.5 collects restrictions established across many later sections, so formalizing its prerequisites is a substantial graph-theoretic task. Chudnovsky et al., pp. 52–56, 154
Lean uses SimpleGraph V with finite vertices, decidable vertex equality, and the Mathlib complement, induced subgraph, chromatic number, clique number, bipartiteness, and line graph. A hole is a list in cyclic order whose adjacency relation agrees exactly with the cycle edges; a path is likewise listed in one orientation with exactly its consecutive edges. Antiholes and antipaths use the complement graph. The empty vertex set is connected, matching p. 54. The double split partition is encoded by an equivalence from the four indexed parts to the whole vertex type, making disjointness and coverage explicit. A minimum imperfect graph is globally minimal by vertex count, among all finite Berge graphs.
No hypothesis beyond the paper's finite, simple graph convention is added to the goal or numbered milestones. In particular, “Berge” includes holes in both and ; “perfect” ranges over every induced subgraph; and the complement occurs only in those decomposition outcomes where the paper places it. A non-induced cycle or a missing complement condition would make the formal target different. The definitions and Lean proofs of the graph classes, their boundary cases, and the structural milestones are welcome contributions. Later missions pose the paper's intervening numbered results rather than duplicating them here.
Policy iteration alternates two steps: evaluate the current policy, then replace it by a policy that is greedy with respect to the evaluated action values. The policy improvement theorem guarantees that each greedy step does not make the policy worse, and that the process stops only at an optimal policy. When the action values are estimated from experience rather than computed from a model, as in Monte Carlo control, a greedy policy is a problem: it never tries the actions it does not currently prefer, so their values are never re-estimated. Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., 2018), §5.4, resolve this without the unrealistic assumption of exploring starts by moving the policy only toward a greedy one, to an ε-greedy policy that keeps every action's probability at least ε/|A|.
The question this mission formalizes is whether policy iteration still works under that restriction. The book's answer (pp. 101–102) is yes, in a precise sense: an ε-greedy step never makes an ε-soft policy worse, and it fails to make it strictly better only when the policy is already the best among all ε-soft policies. This is the dynamic-programming fact that justifies on-policy first-visit Monte Carlo control for ε-soft policies, and more broadly every ε-greedy on-policy control scheme that is analysed with exact action values.
A finite Markov decision process has a finite state set S, a finite nonempty action set A used in every state, a finite reward set R ⊂ ℝ and dynamics p(s′, r | s, a) ≥ 0 with . A policy π gives, for each state s, a probability distribution π(· | s) on A. With a discount rate , the state value is the expected discounted return , and the action value is
For ε > 0, a policy is ε-soft if for all s and a. A policy π′ is ε-greedy with respect to if at each state some maximizer of receives probability and every other action receives ; ties among maximizers are broken arbitrarily. A policy π is optimal among the ε-soft policies if it is ε-soft and for every ε-soft π″ and every state s.
The book's analysis uses a new environment with the same states, actions and rewards, in which with probability 1 − ε the chosen action is executed and with probability ε a uniformly random action replaces it:
Its optimal value function is written .
For , , an ε-soft policy π and any ε-greedy policy π′ with respect to ,
The goal is stated in terms of the original MDP and ε-soft policies only; the new environment appears only in the milestones.
The result is what makes ε-greedy on-policy control a form of generalized policy iteration: monotone improvement at every step, and a characterization of where the process can stop. It also locates precisely what is lost by exploring, namely that the fixed point is optimal among ε-soft policies, not among all policies. The value of the new environment is the benchmark against which ε-greedy methods converge when action values are exact.
The book presents the argument informally and states the stochastic policy improvement theorem without proof ("we will not go through the details", p. 79). A formalization supplies the missing proof of the stochastic case, the identification of the best ε-soft policy value with the optimal value of a modified MDP, and the uniqueness of that value. As far as a search of the platform shows, no statement about ε-soft or ε-greedy policies has been formalized there; existing finite-MDP results (Bellman optimality in the Foundations of Machine Learning and Bertsekas series) use different reward models and do not cover the modified environment.
The improvement half follows from (5.2) and the policy improvement theorem, but both need work in the return-based model: the theorem requires comparing infinite discounted sums under two different Markov chains, and (5.2) uses the identity , which is a theorem about returns, not a definition. The equality half is where the obvious argument fails. The deterministic-policy argument of Chapter 4 shows that an unimproved greedy policy satisfies the ordinary Bellman optimality equation; here the unimproved policy satisfies a different equation, and nothing in the original MDP identifies its solution with the best ε-soft value. That identification needs two further facts: every policy of the new environment corresponds to an ε-soft policy of the original one with the same values, and conversely (at ε = 1 only the uniform policy is ε-soft); and the altered optimality equation has exactly one solution.
Everything is stated in the namespace SuttonBartoRL.EpsSoft on a finite MDP with four-argument dynamics, one finite nonempty action set for all states (so , the book's footnote 3, p. 48), and a finite reward set. The conventions are:
Defining as the solution of the Bellman expectation equation, or as the solution of the altered optimality equation, would make milestones 3–5 and the goal's equality half hold by definition; the formalization does neither. The goal is not the statement "" alone: the equality case is part of the book's claim and part of the goal.
The finite-MDP definitions duplicate those of other missions in this series and are expected to be merged later. Useful contributions include the Neumann-series identity , the Bellman expectation equation, the contraction property of Bellman operators, and the correspondence between policies of the new environment and ε-soft policies of the original one; these are reusable for the other finite-MDP missions of the series.
The bullwhip effect is the observation that the variability of orders increases as one moves up a supply chain, from the retailer towards the manufacturer and its suppliers. It was documented in industry and in classroom experiments such as the Beer Game (Sterman 1989), and analysed by Lee, Padmanabhan and Whang (1997), who named demand forecasting, lead times, batch ordering, rationing and price variations as its main causes. A remedy often proposed is to centralize demand information: give every stage of the chain the customer demand data, so that no stage forecasts from the distorted orders of its downstream neighbour.
Chen, Drezner, Ryan and Simchi-Levi (2000) quantified the effect for a retailer that forecasts with a moving average and orders with an order-up-to policy. They gave an explicit lower bound on the ratio of the order variance to the demand variance in terms of the lead time, the forecasting window and the demand autocorrelation. They then showed that in a multistage chain with fully centralized demand information this ratio still grows with the total lead time upstream of each stage. This mission formalizes that result, Theorem 3.1 of the paper, together with the single-stage analysis it rests on.
Time is indexed by the integers. The customer demands seen by the retailer follow the AR(1) model
where , , and the errors are independent and identically distributed from a symmetric distribution with mean and variance . The demand is in steady state, so that and for every .
The retailer does not know the demand process. With a window of past observations it forms the moving-average estimates
where is the lead-time parameter ( means an order placed at the end of period arrives at the start of period ) and is a constant the paper leaves unspecified. The order-up-to point is for a safety factor , and the order placed in period is . It may be negative: excess inventory is returned without cost.
In the multistage chain with centralized information, stages (stage is the retailer) all observe and use the same estimate . Stage has lead time and safety factor and uses the order-up-to point . Following the paper's sequence of events, stage orders , and stage , receiving , orders .
For every stage and every period ,
with equality when . The bound holds for every choice of the constants and of the safety factors.
with equality when .
Theorem 2.2 shows that forecasting with a positive lead time is enough to make orders more variable than demand, even for independent demands (). It also says how the effect depends on each parameter: the bound decreases in the window and increases in the lead time . Theorem 3.1 is the paper's answer to the centralization remedy. When every stage sees the true customer demand and uses the same forecast and the same policy, the variability of orders at stage is still bounded below by the single-stage expression with the cumulative lead time . Centralization reduces the bullwhip effect but does not remove it. The decentralized comparison (Theorem 3.2, where the bound becomes multiplicative across stages) is a separate mission in this series.
On the formalization side, the Gaussian special case of the single-stage results is on the platform. Snyder and Shen's Fundamentals of Supply Chain Theory states Theorem 2.2, Lemma 2.1, Eq. (4) and the AR(1) moments for normally distributed errors, as the items SupplyChainTheory.bullwhip_signal_processing, bullwhip_lemma_13_1, bullwhip_order_identity and ar1_moments. This mission states them under the paper's weaker hypothesis of a symmetric error distribution. The multistage Theorem 3.1 has no machine-checked counterpart. The paper proves only Theorem 2.2 in print. For the proofs of Lemma 2.1 and Theorem 3.1 it refers to Ryan (1997) and to a working paper, so a formalization supplies arguments the published article does not contain.
Most of the algebra is routine. The difficulty is Lemma 2.1 and the covariances like it. The estimate is a square root of a quadratic form in past demands, so its covariance with a demand cannot be computed from second moments. Under Gaussian errors one can appeal to properties of Gaussian vectors. With only a symmetric error law, every distributional fact has to come from the symmetry of the errors and from the representation of the steady-state demand as an infinite series in past errors.
The printed derivation also moves faster than a proof. Expanding from Eq. (4) produces the cross terms and , which lie outside the lags of Lemma 2.1. The display after Eq. (4) does not account for them. A complete proof of milestone 4 must show that these terms vanish too. For the chain, the stage orders are defined by a recursion across stages, and the variance of involves the estimates of all stages .
Random variables are real functions on a probability space , and time is , so that exists for every . Variance and covariance are Mathlib's ProbabilityTheory.variance and ProbabilityTheory.covariance. The demand structure ChenBullwhip.Centralized.AR1Demand records (1) for every outcome and the paper's error hypotheses: independence, identical distribution, symmetry, mean and variance . It adds four disclosed conditions:
The published Gaussian structure SupplyChainTheory.AR1Demand satisfies these conditions, so this mission generalizes the Snyder–Shen items rather than referencing them. The constants are free real parameters, and in the chain is for an arbitrary function . Lead times are natural numbers, included. Sums and run over and , and stages are numbered from . The order recursion is read from the paper's sequence of events, because the paper prints no formula for .
The orders are computed from the demands through the definitions above. They are never arbitrary random variables with assumed moments. "Tight" is formalized as equality, and orders are never truncated at zero. Without the steady-state condition, a process started from an arbitrary satisfies (1) but has time-dependent moments, and the results fail; with the ratio form would be false. Both cases are excluded by the structure, not by vacuous hypotheses. The structure is satisfiable: i.i.d. standard Gaussian demands on form an instance.
A complete development needs: the series representation of a stationary AR(1) process; distributional symmetry facts for i.i.d. sequences with a symmetric law; and covariance bookkeeping for finite linear combinations. The first two are reusable for any linear time-series model with symmetric innovations. Contributions to any milestone, and to general lemmas about stationary AR(1) processes, are welcome.
Combinatorial optimization problems are routinely solved by writing the convex hull of their feasible solutions as the feasible region of a linear program. When that convex hull has exponentially many facets, a classical trick is to add auxiliary variables: a polytope with many facets may be the linear projection of a higher-dimensional polyhedron with few. The spanning tree polytope, the permutahedron and the parity polytope all have compact descriptions of this kind. This raises the question of whether every polytope of an NP-hard problem might also have one, which would yield a polynomial-size linear program for that problem.
In the late 1980s several papers claimed polynomial-size linear programs for the traveling salesman problem (TSP). Yannakakis (STOC 1988; JCSS 1991) refuted all such claims at once by showing that every symmetric extended formulation of the TSP polytope has exponential size. He asked whether the symmetry assumption could be removed. Fiorini, Massar, Pokutta, Tiwary and de Wolf (STOC 2012; J. ACM 2015) answered the question: every extended formulation of the TSP polytope, symmetric or not, has inequalities.
Timeline.
Let be a finite index set. An extended formulation (EF) of a set is a linear system , in variables such that exactly when some satisfies it. Its size is the number of inequalities. The extension complexity is the least size of an EF of .
A polytope is the convex hull of finitely many points. A face of is itself or its intersection with a valid hyperplane, and a facet is a maximal proper face. A polytope is an extension of if for some linear map . Given , the slack matrix has entries . The nonnegative rank is the least with , where has columns and has rows.
For -bit strings , is the number of common ones, and is the matrix . A 1-monochromatic rectangle cover of its support is a family of products , each containing only entries with , that together contain all of them.
On the complete graph , is the characteristic vector of an edge set and is the cut of . The polytopes are
The constant is left unfixed, so the goal survives any improvement of it.
The theorem rules out every polynomial-size linear programming formulation of the TSP polytope, in any number of auxiliary variables, which settles Yannakakis's question. The cut polytope bound does the same for max-cut, and the stable set bound for the stable set problem on general graphs. The results do not depend on P vs NP: they concern one specific model of computation, linear programs whose feasible region projects onto the polytope. They started a line of work on extension complexity, including perfect matching (Rothvoss), approximate EFs and semidefinite lifts.
Formalizing the result would produce a machine-checked chain from a communication-complexity bound to a polyhedral one. The paper's results are proved; the input of Theorem 1, Razborov's bound, is only cited, and is posed here as a separate target. To our knowledge none of these statements has a formal proof in Lean or another proof assistant. The polyhedral layer (Yannakakis's theorem, faces and extensions) and the matrix layer (nonnegative rank, rectangle covers) can be reused for later extension-complexity results.
The obvious approach, bounding the number of facets of the TSP polytope, does not work: extended formulations exist precisely because a projection can have far more facets than the lifted polyhedron. Any lower bound must cover every lifting at once, which means working with the nonnegative rank of a slack matrix rather than with any concrete formulation. Ordinary rank is no help, because has rank . The step that carries the weight is Razborov's distributional bound for disjointness, a nontrivial piece of communication complexity. On the polyhedral side, Lemma 11 needs a reduction from 3SAT to a directed and then an undirected Hamiltonian cycle problem, realized as a face of with . Theorem 12 also needs a monotonicity of in that the paper only indicates.
Sym2 (Fin n)). is indexed by ordered pairs, and the Frobenius product is the dot product over ordered pairs. Bit strings are Fin n → Bool.sInf of the attainable sizes), never , so no lower bound can hold through an infinite value. The size of an EF counts inequalities only.The dynamic lot size model asks when, and how much, to order of a single item over a planning horizon of periods with known, time-varying demands, setup costs, unit order costs and holding costs. It is the textbook model of production planning and the building block of material requirements planning, multi-item scheduling and many decomposition schemes for larger supply-chain problems.
Wagner and Whitin (1958) showed that some optimal policy orders only when inventory is zero, which turns the problem into a shortest-path recursion with running time. For more than thirty years this was the standard algorithm. In 1991 three groups independently reduced the complexity: Federgruen and Tzur (Management Science 37(8), 1991), Wagelmans, van Hoesel and Kolen (Operations Research 40, 1992) and Aggarwal and Park (Operations Research 41, 1993). Each obtained in general and under special cost structures. The Federgruen–Tzur algorithm is a forward algorithm: at iteration it keeps a short list of periods that could still be the best last setup period for some future horizon, and updates it by local tests on neighbouring entries. This mission formalizes the theorem that justifies those tests.
For periods let be the demand, the setup cost, the variable per unit order cost and the cost of carrying a unit of inventory at the end of period . Write and , so . For let , let , and let
be the carrying cost of an order placed in period that covers the demands of periods .
The costs are given by the zero-inventory recursion (2): and, for ,
is the cost of the first periods when the last setup is in period .
For two periods the difference is affine in , with intercept given by (4) and slope . Its root is defined by (5): when the slopes differ, and or according to the sign of when they agree. It is extended symmetrically, .
At iteration the future demands are unknown, so a future horizon has a potential cumulative demand . The th Minimal Optimal Predecessors list is the set of periods that are the lowest-index optimal last setup period, among , for every potential cumulative demand in some open interval above .
Let and let with , ranked so that , with equal -values in ascending order of index. Put and for . Then
In attack order:
A supporting item potCost_spec certifies that the potential costs used to define agree with the paper's , up to a term that does not depend on .
Theorem 1 is what makes the forward algorithm correct. Part (a) reduces the minimality of a candidate list to a condition on consecutive pairs of a sorted list. Part (c) says which entry to delete when the condition fails. Part (b) says where to read off the optimal last setup period. With these, is maintained by deletions at the ends and in the interior of a list ordered by , and each period is inserted and deleted at most once; the bound, and the bound under the paper's special cost structures, follow from this bookkeeping. The same lower-envelope reasoning appears in the other 1991–1993 algorithms and in later extensions to backlogging and capacitated variants.
The result has a complete published proof. To our knowledge there is no machine-checked development of the Wagner–Whitin recursion or of any of the fast lot-sizing algorithms. This mission produces the model, the breakpoints and the Minimal Optimal Predecessors lists as reusable definitions, and a checked proof of the characterization. It also records two small corrections that a formal reading forces on the printed text (see Formalization scope).
Each piece in isolation is elementary algebra on affine functions. The difficulty is in the combinatorics of the lower envelope with ties. The natural argument "consecutive breakpoints increase, so each line owns an interval" must handle three things:
The "only if" direction needs every failure of (6) to be traced to an element that is never the unique lowest-index optimum on an interval. Ties are exactly where the printed definition of , read literally at a single demand value, breaks the theorem. A proof that ignores ties proves a statement that is false.
EReal, so are kept distinct from every real number. The final "" of (6) is part of the condition.List ℕ. Lean lists are 0-based, so the paper's and are entry and gval j L m.(r, Q) policies are the standard replenishment rule for a single item under continuous review: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point , an order of size is placed. They are known to be optimal in the classical models with Poisson or compound renewal demand, constant or exogenous lead times and full backlogging, and they are used widely in practice and in multi-item and multi-echelon systems where they are applied item by item.
For decades, computing an optimal pair exactly was not routine. The textbook treatment of Hadley and Whitin (1963) gives approximations; as Browne and Zipkin (1991) put it, "until recently, there was no reliable, straightforward method for computing an optimal (r, Q) policy, even in the simple case of Poisson demand processes." Many heuristics were proposed (surveyed by Lee and Nahmias, 1989); the only exact procedure in circulation was in Zipkin's classnotes, based on a result of Sahin (1982).
Federgruen and Zheng (1992) give a short exact algorithm, Algorithm OPT, whose work is linear in the optimal order quantity . It rests only on the form of the cost, not on a particular demand model.
Inventory positions are integers (demand arrives unit by unit). A fixed cost is charged per order, and is the expected holding and backlogging cost rate as a function of the inventory position . In all the models of the paper the long-run average cost of the policy, for an integer and an integer , has the form
The paper's standing assumptions on are:
The sequence . Let be an integer minimizing . Given , let and , and set
So the window grows by one point at a time towards the smaller neighbouring value, ties going left. Write for an optimal reorder point for a given , and
Algorithm OPT, Step 1. Variables start at , , , , . Each pass compares and ; on the smaller side (left on ties) it stops if is at most that value, and otherwise adds the value to and moves one step left or one step right; then and . The output is the final .
Under the standing assumptions, Step 1 of Algorithm OPT, started from any global minimizer of , stops after finitely many passes, and its output satisfies and
The goal fixes no constants and no demand model: it is a statement about every satisfying the standing assumptions.
The result turns the joint minimization of (1) over , an unbounded two-dimensional integer problem, into a single scan whose length is plus the distance to the minimizer of . Because it uses only the form (1) and the unimodality of , it applies at once to Poisson and compound Poisson demand, to stochastic lead times with an equilibrium lead-time demand, and to cost structures with stockout penalties; the paper also notes extensions to policies. Lemma 1 and Corollary 1 additionally give the structure of the optimal reorder point as a function of .
The result has been proved on paper since 1992. What this mission adds is a machine-checked proof of the algorithm's correctness for general under exactly the paper's hypotheses. The platform already has the linear-cost special case of the underlying lemmas for one discrete demand model (InventoryControl.rq_discrete_recursion, rq_discrete_joint_optimal), but with and given as hypotheses and no algorithm; nothing on the platform states the algorithm or treats general unimodal .
The obvious argument says: for fixed the sum in (1) should cover the smallest values of , and the greedy window collects exactly those. Both halves need care on the integers with flat stretches of : "the smallest values" is ambiguous under ties, and the claim that a greedy window holds them relies on being a global minimizer together with the unimodality of , not on convexity.
The stopping rule is the second point. Lemma 2 looks like a first-order condition, but need not be convex; optimality of the first stopping for all larger uses that the values are nondecreasing along the sequence, which the paper uses without stating. Termination of the algorithm is not discussed on the page; it needs , and fails for constant .
Finally, the goal is about an imperative loop. Connecting its five variables to , and is an invariant argument that has to match the tie-breaking and the non-strict stopping tests exactly.
NegUnimodal G: , antitone on and monotone on . "" is Coercive G: along atBot and atTop. Mathlib's QuasiconvexOn ℤ is not used: over -weights it holds for every function.Proofs of any milestone are welcome, as are general lemmas on windows of unimodal integer sequences, which are reusable beyond this mission.