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?
Many queueing systems evolve in continuous time: customers arrive according to a Poisson process, services take exponentially distributed times, and a controller may change the service rate, admit or reject customers, or route them whenever the state changes. Minimizing the long-run average cost of such a system is a standard problem in the control of queues (Lippman 1975; Puterman 1994, Ch. 11; Sennott 1999, Ch. 10). The continuous time model does not fit directly into the discrete time theory of Markov decision chains developed in the earlier chapters of Sennott's book, because time spent in a state now matters and the natural average cost is a ratio of expected cost to expected elapsed time.
This mission formalizes Sections 10.1–10.4 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999): the elementary properties of the exponential distribution, the continuous time Markov decision chain and its average cost, a reduction of the continuous time problem to an auxiliary discrete time Markov decision chain, and the theorem stating that finite state approximating sequences of the auxiliary chain compute optimal average costs and optimal stationary policies of the continuous time chain. The chapter closes with an explicit average cost computation for the M/M/1 queue with service rate control.
A random variable has the exponential distribution with rate if for . A function is if as .
A continuous time Markov decision chain (CTMDC) has a countable state space and, for each , a finite nonempty action set . Choosing in state incurs an instantaneous cost and a cost rate in effect until the next transition. The time until the next transition is exponential with rate , so its mean is ; the next state is with probability , where . A policy chooses, at each transition, an action (possibly at random) from the history of past states, actions and sojourn times; a stationary policy chooses in state . With the cost and the time of the first transition periods, the average cost and the minimum average cost are
Assumption (CTB) requires constants and with . The auxiliary MDC has the same states and actions, costs , and transition probabilities for , . Its average cost and minimum average cost are those of Chapter 2. Assumption (CTAC) is .
An approximating sequence for uses finite state spaces increasing to and transition probabilities on converging to . The (AC) assumptions ask for constants and functions on solving
with , for a constant , and , .
Under (CTB), (CTAC) and the (AC) assumptions for an approximating sequence of :
and every limit point of a sequence of stationary policies realizing the minimum in (10.21) satisfies and . The goal leaves the chain, the approximating sequence and the constants of (CTB) arbitrary.
The goal theorem turns the average cost control of a continuous time chain on an infinite state space into a finite computation: solve the optimality equation (10.21) of a finite truncation of the auxiliary chain, let the truncation grow, and read off the optimal average cost and an optimal stationary policy of the original continuous time chain. The auxiliary chain is the book's form of uniformization, and the result is what licenses the numerical study of the M/M/1 service rate control problem in Section 10.4 and of the M/M/K and polling models in Sections 10.5–10.6. Proposition 10.4.1 gives the closed-form benchmark against which the computed optimal policy is compared.
The results are proved in the book, some with details left to the reader (Lemma 10.3.2(ii), Problem 10.10), and the goal rests on Theorem 8.1.1 and Lemma 7.2.1 of the same book. None of them has, as far as a search of Mathlib and the Prove2Me catalogue shows, a machine-checked proof: Mathlib provides the exponential law (ProbabilityTheory.expMeasure) and its distribution function, but not memorylessness or the minimum of independent exponentials, and no continuous time Markov decision model. A formalization would supply these, together with a checked average cost comparison between a continuous time chain and its discrete time auxiliary chain.
The obvious argument compares the two chains policy by policy, but the policy classes differ: a policy for may change action in every time slot, including slots where the state does not change, while a policy for acts only at transitions and may use the observed sojourn times. Only the stationary policies coincide. The lower bound therefore cannot be obtained by transferring policies, and it is exactly what Assumption (CTAC) supplies. The upper bound requires passing from the discrete time inequality (10.20) for the limit point to a bound on a ratio of expected cost to expected time in continuous time, where the denominator depends on the policy; the uniform bounds of (CTB) on the mean sojourn times are what control it. Inside Lemma 10.3.1 the function is only bounded below, so the telescoping of expectations must be justified without integrability of from above.
The state space is a countable type S, actions a type Act, and action sets A i : Finset Act; the CTMDC and MDC structures hold data, and their axioms (nonempty action sets, nonnegative costs, positive rates, stochastic transition rows with ) are separate predicates. Transition probabilities are ℝ≥0∞-valued; costs, rates and the functions are real. Expected costs, expected times and all average costs are ℝ≥0∞-valued, so is a legitimate value, and they are compared with real constants in EReal; the limits superior and inferior of (AC) are taken in EReal. The expected cost of transition periods under a general policy is a recursion over the periods in which the sojourn time is integrated against expMeasure ν(i,a) and the next state is drawn independently from ; policies are measurable in the past sojourn times. In (10.15) and (10.20) the convergence of the series is part of the inequality. The strict inequality of (CTB) is kept strict (as a positive margin); weakening it to would make vanish or turn negative.
The average cost is a ratio of expectations, not the expectation of a ratio, and the infimum ranges over history dependent randomized policies that may use sojourn times; replacing either by a stationary-only class, or dropping (CTAC), gives a different theorem.
A complete development needs: expected rewards of a chain with exponential holding times, the average cost theory of Chapter 8 for the auxiliary chain (Theorem 8.1.1 and Lemma 7.2.1, restated here as needed), and renewal-reward reasoning for Proposition 10.4.1. The exponential-distribution lemmas are reusable beyond this mission and are welcome as independent contributions.
In a discrete-time queue the service of a customer lasts a random number of slots. When such a system is modelled as a Markov decision chain (Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, DOI 10.1002/9780470317037, Chapter 9), the state must record how much service is still owed, and the controller only observes that a service has lasted slots and is not yet finished. The relevant random quantity is then the residual life : the remaining service time given that slots have elapsed without completion. Verifying the book's average cost assumptions for such a model requires bounds on expected first passage times and costs, and these reduce to moment bounds on and on the residual lives .
Section 9.2 isolates a single condition that makes those bounds available: the expected remaining service time is bounded uniformly in the elapsed time. The concept of mean residual life comes from reliability theory, where is the lifetime of a component and is its expected remaining lifetime at age . This mission formalizes Section 9.2 of the book, together with the moment computation for batch arrivals (Lemma 9.5.2) that the same verification uses.
Let be a random variable with values in and distribution , . Write and for , so and . The -th moment is
For with , the residual life has distribution
with ; its tail is , and is the mean residual lifetime.
The distribution of has bounded mean residual lifetimes (BMRL-, Definition 9.2.4) if there is a finite constant with
and it is BMRL if it is BMRL- for some .
Three families appear by name: the geometric distribution of the number of Bernoulli() trials to the first success, ; the negative binomial of the number of trials to the -th success, for ; and the truncated Poisson , for .
For Lemma 9.5.2, batches of customers arrive in each slot; the batch sizes are independent with common distribution , mean and second moment , and is the number of arrivals in slots.
If the distribution of is BMRL, then
The goal fixes no constant: it asserts only that a uniform first-moment bound on the residual lives forces every moment of to be finite.
The result itself. Proposition 9.2.5 turns a condition that is easy to check for concrete service distributions, and natural for services (a service whose expected remaining duration grows without bound as it goes on is undesirable), into the moment bounds that the average cost analysis consumes. With Proposition 9.2.6 it shows that the most common unbounded service distributions on have finite moments of all orders; with Lemma 9.5.2 it supplies the linear and quadratic growth of expected arrivals and their second moments that the verification of the (WAC) assumptions for the batch-arrival queue of Example 9.3.1 needs (Section 9.5). Every bounded distribution is BMRL as well (the book's Problem 9.3).
Formalizing it. All results here are proved in the book; none has a machine-checked proof on the platform or in Mathlib, which has geometric and Poisson distributions but no residual lives, negative binomial or truncated Poisson laws. A complete development gives a reusable tail-sum calculus for moments of -valued random variables in , a residual-life construction for discrete distributions, and the BMRL property of three standard families. The platform's mean residual life order (the "Stochastic Orders II" mission, Shaked–Shanthikumar) compares two variables; BMRL is a uniform bound on one variable's residual lives and is not an order, so none of that material states these results.
BMRL controls only first moments, of the conditional laws ; the goal asks for moments of every order of itself. Bounding by expanding for each fixed gives nothing, because each single bound is compatible with a heavy tail: the uniformity in is essential. The residual lives are also only defined where , so every argument must handle distributions with bounded support separately. Proposition 9.2.6 requires explicit control of ratios of tail sums for three families; for the negative binomial and truncated Poisson the tails have no closed form.
IsDistOnPos). , moments and residual-life moments are ℝ≥0∞-valued series; an infinite moment is and "finite" means . No Bochner integral is used, so a finite-moment conclusion cannot hold vacuously through an integrability default.geometricPMF does.iIndepFun) batch sizes of common law , expectations as lower Lebesgue integrals, and only assumption (BA1), , which is the part of the book's (BA) that concerns arrivals.Control problems for queueing systems (admission control, service rate control, routing to parallel servers) are naturally modelled as Markov decision chains whose state is a vector of queue lengths. The state space is therefore denumerably infinite, and the performance measure of interest is usually the long-run average cost per slot. For such models the existence theory of average cost optimal stationary policies is well developed (Chapter 7 of Sennott's book), but existence gives no algorithm: an optimal policy is a function on an infinite set, and value iteration cannot be run on an infinite state space.
The approximating sequence method answers this by replacing the infinite model with a sequence of finite models on truncated state spaces , solving the average cost optimality equation in each, and passing to the limit. Chapter 8 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) gives a set of conditions, the (AC) assumptions, under which this limit procedure provably produces the minimum average cost and an average cost optimal policy of .
Timeline. The approximating sequence method for the average cost criterion and the (AC) assumptions were introduced in Sennott (1997a), with further results in Sennott (1997b) (bibliographic notes, p. 194). The book collects these results, adds the four step verification template (Proposition 8.2.1), the finite-set augmentation route based on the (BOR) assumptions (Proposition 8.2.3), and the weakening (WAC) of Section 8.7, which Chapter 9 uses.
An MDC has a countable state space , a finite nonempty action set in each state , a finite cost , and transition probabilities . A general policy chooses actions at random using the whole past history. Its average cost is
and the minimum average cost is . A policy is average cost optimal if .
An approximating sequence consists of finite sets increasing to and MDCs on with the same actions and costs and with transition probabilities on converging to . Write and for the -horizon and discounted value functions of .
The (AC) assumptions are:
The (WAC) assumptions of Section 8.7 allow to depend on the state, at the price of integrability conditions along every stationary policy.
Under (AC), the limit exists and
and every limit point of stationary policies realizing the minimum in (8.1) is average cost optimal for . The statement fixes no constants; it asserts the shape of the conclusion for any model satisfying (AC).
exist and satisfy (AC).
The result itself. Theorem 8.1.1 is what turns the existence theory of Chapter 7 into a computation. It certifies that the minimum average costs of the truncations converge to the minimum average cost of the infinite model, that this cost is constant, and that the policies produced by value iteration on converge, along subsequences, to an optimal policy for . Propositions 8.2.1–8.2.3 reduce (AC) to properties that can be checked model by model; Section 8.3 checks them for queues with reject option, service rate control, and routing to parallel queues. Proposition 8.7.1 is the version used in Chapter 9 for models whose relative values are not uniformly bounded below. Proposition 8.5.1 gives the closed-form open-loop benchmark used in the numerical study of Section 8.5.
Formalizing it. All results are proved in the book; none has a machine-checked proof. A formalization would give the first verified convergence theorem for truncations of denumerable-state average cost MDPs, and would make the approximating sequence method usable as a certified reduction from infinite to finite models. The template results (8.2.1–8.2.3) additionally require a formal treatment of conformity of approximating Markov chains (Appendix C.4–C.5), which is of independent use.
The naive argument takes limits in (8.1) along : the minimum over and the finite sums pass to the limit only in the inequality direction, and only after a Fatou-type lemma for sums against the converging distributions with integrands that are neither bounded nor monotone. The lower bound in (AC3) is exactly what makes this possible; without it the limit inequality can fail. The limit inequality then produces only an average cost optimality inequality, and turning it into optimality of the limit policy requires a separate argument that a function bounded below and satisfying the inequality yields an upper bound on the average cost. Existence of is not given: (AC4) controls only the limit superior, and the limit must be identified through every subsequence. For the template results, the difficulty is in the Markov chain side: the convergence of first passage times and costs of the truncated chains, which fails for general approximating sequences (Examples C.4.4, C.4.7).
The Lean development is in the namespace SennottDP.AvgASM. The state space is any countable type; action sets are Finsets, assumed nonempty; costs are finite and nonnegative (ℝ≥0); transition probabilities are ℝ≥0∞-valued, with each row a probability distribution for admissible actions. All value functions and average costs take values in (ℝ≥0∞), and every infimum over policies ranges over the full class of history-dependent randomized policies. The and of (AC1) are real; the limits superior and inferior over in (AC2)–(AC4) and (WAC) are taken in EReal, so an unbounded sequence cannot produce a junk finite value. The equality is stated in EReal, which also asserts that is finite. Quantities of at states outside are junk values that affect only finitely many for each state.
A trivializing formalization is ruled out: and are the witnesses of (AC1), not free variables, the policies must realize the minimum in (8.1) for those witnesses, and the minimum average cost is an infimum over all policies, so the goal cannot be satisfied by choosing or the limit policy.
A complete development needs: the induced process law of a general policy; the average cost optimality inequality argument (Lemma 7.2.1); the finite-state average cost results of Chapter 6 (Propositions 6.4.1, 6.5.1, 6.6.3); a Fatou lemma for converging distributions (Proposition A.2.5); limit points of policy sequences (Proposition B.5); and, for the template results, the theory of standard chains and conformity (Appendix C.2–C.5). The Markov chain layer and the approximating sequence definitions are reusable beyond this mission. Contributions of any of these intermediate results as separate theorems are welcome.
Controlled queues, inventories and communication links are run for a long time, and the quantity an operator usually cares about is the long-run average cost per period rather than a discounted total. The average cost criterion is harder to work with than the discounted one: its value is a of Cesàro means, it is not given by a contraction, and for general (history dependent, randomized) policies the limit need not exist. Chapter 6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) treats the case of a finite state space, where the strongest results hold: an average cost optimal policy exists, can be taken stationary, and can be obtained as a limit of discount optimal policies as the discount factor tends to one.
The results go back to D. Blackwell, "Discrete dynamic programming", Ann. Math. Statist. 33 (1962), who showed that for finite states and actions some stationary policy is discount optimal for all discount factors close to one. Such a policy is now called Blackwell optimal. Sennott's Chapter 6 derives average cost optimality of this policy and the multichain average cost optimality equation from it, in the notation used throughout the book.
A Markov decision chain (MDC) has a countable state space , a finite nonempty action set in each state , nonnegative finite costs , and transition probabilities with . A policy chooses the action at time from a distribution on that may depend on the whole history . A stationary policy always chooses a fixed action in state .
With the state and action at time and , define
All infima range over all general policies, and every quantity may equal . A policy is discount optimal if , and average cost optimal if .
For a stationary policy on a finite state space, the induced Markov chain splits into positive recurrent classes and transient states. With the probability of reaching from , distinguished states , and , the relative value function is .
For an MDC with a finite state space there are and one stationary policy such that is discount optimal for every , is average cost optimal, and
with three equivalent conditions for equality. 3. Proposition 6.2.2. For finite and stationary , . 4. Proposition 4.5.1, Proposition 4.5.4, Corollary 4.5.5. The power series structure of in ; monotonicity and left continuity of ; continuity under bounded costs. 5. Theorem 6.3.1. For the policy of the goal, exists, and
together with the limit identities (i)–(iii) and the optimality criterion (v). 6. Proposition 6.3.3. with as .
The goal says that on a finite state space nothing is gained by randomizing or by remembering the past when minimizing average cost, and that the minimum average cost is the vanishing-discount limit of the discounted value function. This justifies computing average cost optimal policies through discounted problems and value iteration, the route taken in the rest of Chapter 6 and, via approximating sequences, for countable state spaces in Chapters 7 and 8. Theorem 6.3.1 supplies an optimality equation without any unichain or communication assumption. The book's Example 6.3.2 shows that the inequality in that equation can be strict, and that a stationary policy attaining the minimum need not be optimal.
The results are classical and proved in the book. No machine-checked version of them is known to exist. The platform has average-reward results for unichain finite MDPs with Markov policies (the Puterman series) and an average-cost optimality equation under recurrence assumptions (the Bertsekas series). Neither covers existence of a Blackwell optimal policy against the class of all history dependent randomized policies, or the multichain equation. A formal development also yields reusable infrastructure: the law of a controlled process under a general policy, first passage quantities of finite chains, and the Abelian inequality between Abel and Cesàro means of a nonnegative sequence.
The obvious argument picks, for each , a stationary discount optimal policy and lets . Finiteness of the set of stationary policies gives one policy that is optimal along some sequence , but not on an interval. Excluding infinite switching between two policies requires the analytic structure of (Proposition 4.5.3), which in turn rests on matrix inversion of . Passing from the discounted criterion to the average one requires an Abelian inequality for nonnegative series whose terms may be infinite (Proposition 6.1.1), and comparison against general policies rules out any argument that works only within stationary or Markov policies. For Theorem 6.3.1 the difficulty is the multichain structure: the relative value function has to be assembled class by class from first passage times and costs, and its limit must be identified.
S; [Countable S] for Section 4.5 and Proposition 6.1.1, [Fintype S] from Section 6.2 on, as in the book. Actions form a type Act with A i : Finset Act nonempty. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞.A i. Stationary policies embed as degenerate policies. The law of the process is built from this data, and every infimum ranges over all general policies.ℝ≥0∞, so is represented. is the filter 𝓝[<] 1. On a finite state space these quantities are finite. The real valued objects of Section 6.3 (, , , equation (6.6)) are therefore formed with toReal, and this switch from ℝ≥0∞ to ℝ happens only in Theorem 6.3.1 and Proposition 6.3.3.p/q without requiring . Each is excluded here: and are infima over all general policies, one pair is quantified before all , and the denominator is required to be nonzero on .Useful infrastructure includes rational functions of one real variable and their finitely many sign changes, the resolvent of a stochastic matrix, the Abelian inequality for -valued sequences, and renewal-reward identities for finite chains. Contributions of general lemmas on these topics are welcome, as are proofs of individual milestones.
Control problems for queueing systems (admission control, routing, service rate selection, inventory replenishment) are naturally modelled as Markov decision chains with a countable state space, such as the number of customers in a buffer, and with costs that grow without bound in the state, such as holding costs proportional to queue length. The expected discounted cost criterion is the first infinite horizon criterion applied to such models, and it is also the tool through which the average cost criterion is treated later in the same book (Chapters 6–8 of Sennott's text reach average cost optimal policies through limits of discounted problems as the discount factor tends to one).
Classical treatments of discounted dynamic programming assume bounded costs, under which the dynamic programming operator is a contraction and has a unique bounded fixed point. That assumption fails for queueing models. This mission formalizes Chapter 4, Sections 4.1–4.4, of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), which develops the discounted theory for nonnegative, possibly unbounded costs, where value functions may be infinite.
Timeline of the underlying theory:
A Markov decision chain has a countable state space ; for each state a finite nonempty action set ; for each a nonnegative finite cost and a probability distribution of the next state. A policy chooses the action at time at random from a distribution on that may depend on the entire history . A stationary policy always chooses in state ; for it one writes and .
Fix a discount factor . For an initial state and a policy , the -horizon cost with terminal cost zero and the infinite horizon discounted cost are
and the value functions are and , infima over all policies. All of these lie in . A policy is discount optimal if . The discount optimality equation is
With , denotes the set of actions attaining the minimum at .
solves (4.9); every solving (4.9) satisfies ; and every stationary policy with
is discount optimal. No boundedness of costs and no finiteness of is assumed.
In attack order: Lemma 4.1.1 (); Proposition 4.1.2 (a supersolution of the one-policy equation dominates and ); Corollary 4.1.3 (a supersolution of the optimality inequality dominates ); then, beyond the goal, Corollary 4.1.5 ( where ), Proposition 4.2.2 and Corollary 4.2.4 (conditions under which a solution of (4.9) equals ), Proposition 4.3.1 (, and limit points of finite horizon optimal stationary policies are discount optimal) and Proposition 4.4.1 (optimal policies are exactly those concentrated on the sets along histories of positive probability).
Theorem 4.1.4 is the foundation for everything in the book that concerns discounted costs: it produces an optimal stationary deterministic policy, identifies among the many solutions of (4.9) (Example 4.2.1 of the book gives a one-parameter family of finite solutions), and underlies value iteration (Proposition 4.3.1) and the approximating-sequence method of Sections 4.6–4.7. The average cost results of Chapters 6–8 are proved from it by letting . Proposition 4.4.1 describes the full set of optimal policies, including randomized and history-dependent ones.
These are known results with published proofs. The contribution of this mission is a machine-checked development of the discounted theory for countable state spaces with unbounded costs and infinite values, over the general policy class. Related statements on the platform (the monotone-mapping propositions of Bertsekas 1977 in the MonotoneDP missions, and bounded-cost or finite-state discounted results) use different models and are open; no machine-checked proof of the present statements is known to this mission.
The contraction argument that settles the bounded case is unavailable: with unbounded costs the operator in (4.9) has many fixed points, and can equal at some states, so neither uniqueness of fixed points nor subtraction of values is available. The optimality equation compares the infimum over all history-dependent randomized policies with a one-step minimum, so the general policy class and the law of the process under it must be handled directly; restricting attention to Markov or stationary policies begs the question. Every limit exchange (monotone limits of finite horizon costs, the passage to limit points of policies in Proposition 4.3.1) takes place in , where finite-valued arguments do not transfer verbatim.
The Lean development lives in the namespace SennottDP.Discounted. Conventions:
S with [Countable S]; actions form a type Act and A i : Finset Act is nonempty. Costs are ℝ≥0; transition probabilities are ℝ≥0∞ with ∑' j, P i a j = 1 for a ∈ A i.Fin (n+1) → S, Fin n → Act; a policy assigns to every history a distribution on the action set of its last state. The probability of a history is the product of the policy and transition probabilities; expectations are ℝ≥0∞ sums over histories, so no integrability conditions arise.ℝ≥0∞-valued; . The discount factor is α : ℝ≥0 with 0 < α and α < 1. Terminal costs are zero.Useful infrastructure, reusable by the later missions of this series (approximating sequences, average cost): the shift of a general policy after its first step, the Chapman–Kolmogorov identity for the history law, and the computation for stationary policies. Contributions of such lemmas, and proofs of any milestone, are welcome.
Controlled queueing systems (admission control, routing, service-rate selection) are naturally modelled as Markov decision chains whose state is a buffer content and therefore ranges over a countably infinite set. Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, DOI 10.1002/9780470317037) develops the dynamic programming theory for exactly this setting: countable state space, finite action sets, nonnegative and possibly unbounded costs, and value functions that are allowed to be infinite. The book's computational method, the approximating sequence method (ASM), replaces the infinite chain by a sequence of finite truncations and asks when optimal values and policies of the truncations converge to those of the original chain.
This mission is the first of a series on the book. It covers Chapter 3, finite horizon optimization, together with the model of Chapter 2 and three results from Appendices A and B that the chapter uses. The finite horizon theory is the entry point: it is where the book's general policy class, its extended-valued cost criteria and its approximating sequences are first used together.
A Markov decision chain has a countable state space ; for each a finite nonempty action set ; a finite cost ; and for each a transition distribution . A history at time is , and a general policy chooses the action at time from a distribution on : it may use the whole history and may randomize. Stationary policies () and deterministic Markov policies (a stationary policy for each time) are special cases.
Fix a finite terminal cost and a discount factor ( is the undiscounted case). The horizon expected discounted cost of from initial state is
and the value function is over all general policies. Both may be . A policy is optimal for the horizon if it attains at every . For put and let be the set of minimizing it.
An approximating sequence has finite nonempty state spaces increasing to , the same actions and costs, and transition distributions on converging to as . Its value functions are . In an augmentation type approximating sequence, the probability of leaving to is redistributed over by an augmentation distribution . Assumption FH(, ) requires to be finite and at most for every . A stationary policy is a limit point of stationary policies if, along a subsequence, eventually for each .
For fixed ,
and under either condition every limit point of stationary policies with satisfies for all .
Theorem 3.1.2 is the finite horizon dynamic programming equation in the generality the rest of the book needs: the value function is an infimum over history-dependent randomized policies, and the equation holds with infinite values allowed. Its characterization of optimal policies is Bellman's principle of optimality in necessary-and-sufficient form. Corollary 3.1.4 shows that deterministic Markov policies suffice. The discounted chapter builds on these results, since its value function is the limit of finite horizon ones, and so does the value iteration algorithm of the average cost chapters.
Theorem 3.2.3 is the finite horizon case of the approximating sequence method. It says exactly when finite truncations give the right answer, and it reduces the question to Assumption FH, for which Section 3.3 gives checkable conditions. The same structure (a lim inf inequality, a lim sup assumption, a limit point of optimal truncated policies) recurs for the discounted and the average cost criteria in later chapters.
The results are proved in the book. None of them is formalized: the platform has finite horizon dynamic programming only for Markov policies, abstract monotone mappings or finite reward-maximizing MDPs, and nothing on approximating sequences. A formalization contributes a Lean model of Markov decision chains with general policies and extended-valued criteria, which the later missions of the series restate and can merge with this one.
The obvious proof of the optimality equation conditions on the first action and state and then applies the induction hypothesis to the rest of the trajectory. With general policies the rest of the trajectory is governed by a continuation policy that depends on the first state and action, and the decomposition of the path law into a first step and a continuation must be proved from the definition of the process, not assumed. Infinite values also make the "only if" direction delicate: a strict inequality between expected costs becomes an equality once both sides are infinite.
For approximating sequences, the natural idea is to pass to the limit in the optimality equation of . This fails in general. Example 3.2.1 of the book has , because truncation moves probability onto states of high cost and dominated convergence is not available. Only the lim inf inequality holds for free, through a generalized Fatou lemma for approximating distributions. The lim sup side is exactly what Assumption FH supplies. The limit point argument then needs the compactness statement of Appendix B and the fact that a lim inf can be passed through a minimum over a finite set.
The state space is a type S with [Countable S], the actions a type Act, and A i : Finset Act is nonempty. Costs are ℝ≥0, transition probabilities ℝ≥0∞ summing to 1 over S, and all values and expectations are in ℝ≥0∞, so infima over policies are lattice infima and +∞ is a genuine value. A history is the list of past state–action pairs, most recent first, with the current state, and a policy gives a distribution on A i for every history. Expectations are sums over histories of the path probabilities , which is the book's (2.6) and (2.9), not the dynamic programming recursion. The discount factor satisfies in every statement. An approximating sequence is indexed by with a start level ; its value functions are set to for the finitely many at which a given state is not yet in , which does not affect limits.
The optimality equation must not be made definitional by defining or through the recursion (3.2). The policy class must not be restricted to deterministic Markov policies either, since that would make the characterization in Theorem 3.1.2 a different statement. Theorem 3.1.2(ii)(2) is stated with the guard ; the book omits it, and without it the "only if" direction is false (see the item's note).
A complete development needs the first-step decomposition of the path law under a general policy, the generalized Fatou lemma for approximating distributions (Proposition A.2.5, a milestone of the Appendix A mission of this series), and lim inf / lim sup manipulations in ℝ≥0∞. The model definitions are reusable by every later mission of the series. Contributions are welcome at every milestone, including proofs of the definitional sanity facts (for instance ).
The irrationality of rules out an exact representation as a rational number. A quantitative question asks how closely rational numbers can approximate it as their denominators grow. The irrationality measure records the threshold exponent for exceptionally accurate rational approximations. This mission formalizes the historical upper-bound milestone listed as in the optimization constants project.
Mahler's 1953 paper establishes a stronger, explicit inequality in Theorem 1. The mission extracts its consequence for the irrationality measure and states that consequence through a shared Lean predicate. The number 42 is the chosen historical milestone; it is neither a claim about the exact value of the measure nor a claim to the strongest bound mentioned anywhere in Mahler's paper. Mahler, original p. 33.
Write for a numerator and for a positive denominator. The approximation error is the real number . The exponent describes an upper bound on the irrationality measure through an eventual lower bound on this error.
The shared predicate PiIrrationality.UpperBound B means that for every real , some natural-number threshold satisfies
for every integer and every natural number with . The threshold can depend on and on the chosen bound ; it cannot depend on the later choices of or . Numerators may be negative, zero, or positive. Fractions need not be in lowest terms. This is the epsilon characterization used in the definition of .
The goal is
represented by PiIrrationality.UpperBound (42 : ℝ). Expanded, the target is
The mission contains one shared definition and one goal theorem. The definition introduces the proposition without asserting any bound. The theorem has no additional hypotheses, and its proof is intentionally left open. Future historical-bound missions can import the same definition and state a different numeric bound without changing the quantity being tracked.
A finite upper bound restricts the quality of rational approximations to and excludes approximation at arbitrarily large exponents. The formal result would supply a reusable quantitative fact beyond the assertion that is irrational. The published mathematical result is known; the work requested here is a machine-checked proof of the stated consequence.
The shared definition also fixes the meaning of all entries in the accompanying campaign. A smaller bound makes a stronger claim. A proof of a stronger entry may establish this historical goal as a consequence, provided it uses the same definition and no extra hypotheses. The mission remains mathematically valid after further improvements to the numerical bound.
A proof that is irrational only establishes nonzero approximation errors. The target requires a uniform lower estimate over every numerator once the denominator passes a threshold. Checking finitely many rational approximations cannot establish the quantified conclusion. A formal development must control the dependence of its estimates and thresholds, and justify every passage between an analytic estimate and the final rational-approximation inequality.
The exact theorem from Mahler should be distinguished from this goal: his explicit uniform inequality is stronger than the eventual epsilon statement recorded here. A proof may pass through that uniform result, but the goal does not require a particular proof method, a particular threshold, or a separate treatment of every auxiliary theorem in the original paper.
The circle constant is Mathlib's Real.pi. Absolute value, division, and exponentiation in the displayed inequality are operations on the real numbers; in particular, is a real power. The denominator is explicitly positive, so division by zero cannot satisfy the premises. Allowing does not remove the positivity requirement on .
The definition is stored in Definitions.Def_PiIrrationality_UpperBound. The goal imports this definition instead of introducing another version of it. The conclusion is not placed among the theorem's assumptions. The definition contains no proof placeholder; the sole sorry is the open proof of the goal theorem. Contributions may establish supporting estimates or a complete proof while preserving these conventions.
Chess, checkers, Go and Backgammon share a feature that card games such as Poker lack: whenever a player moves, the player knows everything that has happened so far. von Neumann and Morgenstern call this perfect information and devote §15 of Theory of Games and Economic Behavior (1944; 3rd ed. 1953) to it. Their result is that such a game, viewed as a zero-sum two-person game, is strictly determined: it has a value that each player can secure with a pure strategy, without any randomization. For Chess this means that exactly one of three statements is true: White can force a win, Black can force a win, or both can force at least a draw ((15:D:a)–(15:D:c)).
Timeline. Zermelo (1913, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels) showed for Chess that either one side can force a win or both can avoid losing; his argument is not phrased in terms of strategies and a value, and was later corrected and completed by König (1927) and Kalmár (1928/29). von Neumann and Morgenstern (1944, §15) proved strict determinateness for every finite zero-sum two-person game with perfect information, including chance moves (15.7.1), and gave the explicit formula (15:12) for the value. Kuhn (1953, Extensive games and the problem of information, Annals of Mathematics Studies 28) recast games in tree form and extended the pure-strategy existence result to general-sum games with perfect information (subgame-perfect equilibria by backward induction).
A game tree is a finite rooted tree. Each leaf is a finished play and carries the payoff to player 1; player 2 receives . Each internal node is a move of one of three kinds , with alternatives leading to subtrees :
A pure strategy of player 1 is a complete plan choosing an alternative at every node of kind 1; does the same at every node of kind 2. The normalized form is the expected payoff to player 1, the expectation being over the chance moves. With the maxima and minima taken over the finitely many pure strategies,
Always ; the game is strictly determined when (14.4.2).
For a function of the alternatives of the first move , of kind , the operation of (15:8) is , or for . Applying these operations from the leaves back to the root gives the backward-induction value .
For every finite game tree ,
Both the equality and the value formula are part of the goal.
The theorem is the first existence result for the value of a class of games in pure strategies. It shows that the whole difficulty of the general zero-sum two-person game, the need for mixed strategies (§17), comes from imperfect information. It gives a construction as well as an existence proof: the value and optimal strategies are computed by backward induction, the procedure behind retrograde analysis of endgames, minimax search in game-playing programs, and the dynamic programming recursions of sequential decision problems with an adversary. The Chess trichotomy (15:D) is its best-known consequence.
Formalizing it adds a checked account of the passage from the extensive to the normalized form for a whole class of games, which the book carries out informally (15.4.2, 15.5.1: "the reader may verify it from the formalistic point of view"). The result is classical and fully proved in the book; the work is to formalize that proof on a tree model. Mathlib has saddle points (Order/SaddlePoint) and the minimax theorem for continuous functions (Topology/Sion), but no game trees, strategies of extensive games, or backward induction. No machine-checked version of this theorem with chance moves and the normalized form over complete plans is known to the mission.
The recursions (15:2)–(15:7) are not formal consequences of the definitions: and are extrema over whole plans of , while the right-hand sides are extrema over plans of the separate games . At a personal move of player 1, requires interchanging a Min over player 2's plans, which are functions of player 1's first choice, with a Max over that choice: this is exactly (13:E), a max-min equality that fails for general functions of two variables and holds here because the minimizing variable is a function of the maximizing one. A proof that treats the Max over and the Min over as interchangeable without this step is circular.
A second difficulty is the strategy spaces themselves. A complete plan chooses at nodes the plan itself excludes, so the pure strategies of are not simply pairs of a first choice and one strategy of the chosen subgame; the identification the book uses in 15.5.1 has to be justified by showing that the extra coordinates do not change .
A game is an inductive type GameTree with constructors leaf w, chance α p next hp hsum, move1 α hα next, move2 α hα next; alternatives are Fin α (numbered from ). The conditions , and at personal moves are constructor fields, so every tree is a legitimate game. Pure strategies are dependent types Strategy1 t, Strategy2 t defined by recursion on the tree (complete plans), with Fintype and Nonempty instances; is payoff t τ₁ τ₂, the expected leaf payoff; v1, v2 are Finset.sup'/Finset.inf' over all strategies, so every Max and Min is attained.
Standing hypotheses and conventions taken from the book:
The book's formal model is the set-theoretic one of §§9–10, with partitions of the set of plays; the tree restates it for the perfect-information case and does not formalize §§9–10. The book fixes one length for all plays; trees with plays of different lengths contain the book's games as a special case, so the goal is at least as strong as the book's theorem.
Strategies are plans, never responses: a strategy of player 1 is fixed before play and cannot depend on player 2's strategy, which would make trivial. Chance moves are part of the goal; a version without them proves only the Chess case and is weaker than the book.
Reusable beyond this mission: the tree model, its strategy types and the normalized form, which later chapters on extensive games can import. Welcome contributions: proofs of the milestones, and a lemma identifying the strategies of with the book's recursive description (15.4.2, 15.5.1).
Military and commercial service parts systems keep repairable parts at a central depot warehouse and at a set of operating bases. Chapter 10 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) turns from the planning models of the earlier chapters to execution. Each period, the stock that is at the depot or arriving there must be divided among the bases. The planner knows what is already in the pipeline and faces random demand at each base. The chapter's models are solved in a rolling-horizon manner. Each period's decisions are the first step of an optimal plan over a short horizon. That plan has to be computable at scale, for thousands of items and dozens of bases.
What makes this possible is a structural fact. In an optimal allocation, the cumulative stock sent to a base never exceeds what a single-period newsvendor problem at that base would ask for. This bound shrinks the allocation integer programs to linear programs of manageable size. This mission formalizes that bound and the facts it rests on.
Fix one item. Time is counted in whole periods , and is the finite set of bases. For each base :
If units have arrived at base by period , the expected cost of that period is
and stock left at the end of the horizon costs
The stock allocation model chooses nonnegative integer regular shipments , , with cumulative shipments never exceeding cumulative depot supply. The cumulative stock at base is , and the model minimizes . The extended model adds expedited shipments , which arrive after periods at an extra cost per unit.
The constrained newsvendor problem minimizes over integers . Its largest optimal solution is written .
In every optimal solution of , for every base and every ,
The bound is uniform over optimal solutions and uses nothing but the single-period problems.
Two supporting items state that and have optimal solutions. A third, theorem16_counterexample, exhibits an instance in which Theorem 16's upper bound, as printed, fails.
Theorem 15 is what allows the book (pp. 238–239) to rewrite with 0–1 variables indicating . Only between and is needed, so the number of variables is governed by the newsvendor quantities rather than by the total depot supply. Theorem 16 plays the same role for the model with expediting. Both bounds also justify the greedy heuristics of Sections 10.4.3 and 10.5.3. Those heuristics never raise a base's stock above its newsvendor level.
The book proves both theorems in half a page each by an exchange argument. This mission produces machine-checked versions and, in doing so, settles the exact scope of Theorem 16. As printed it is false. With , an expedited shipment in the last decision period can be the only way to cover a later period's demand, and the optimal plan then overstocks an earlier period. The mission states the corrected theorem and the counterexample; the counterexample was checked in Lean during drafting. None of the chapter's results has been formalized before, as far as the platform's catalogue shows.
The central step is the exchange. Take the first period in which an optimal plan overshoots its bound, and delay by one period one unit that arrives at . This must be shown feasible, to change only , and to lower the objective strictly. That in turn needs strict decrease of a convex function to the right of its largest minimizer, and an argument for the last period, where there is no later period to delay into. The indexing is heavy: two lead times, truncated sums , and cumulative constraints across bases.
The first idea, that a plan above the newsvendor level can always be improved by shipping less, fails. Shipping less changes the stock in every later period too, and later periods may need the unit. The bound follows only from a delay that affects exactly one period. For even such a delay is sometimes unavailable, which is where the book's Theorem 16 breaks.
ItemModel J Ω P bundles the data of one item with the cumulative demands on a probability space , [IsProbabilityMeasure P]. Bases form a Fintype. Periods are ℕ. Stock levels and supplies are ℤ, since net inventory may be negative. Shipments are functions J → ℕ → ℕ, so nonnegativity and integrality are built in. Costs are in ℝ.tsum for . The item model requires finite means and convergence of the series for at every stock level, so that no integral or sum takes Lean's junk value .IsLargestCNSolution (feasible, minimizing, and above every feasible minimizer). Theorems take as a function satisfying it. Milestone (10.19) shows it exists.Some elementary functions, such as , and , have antiderivatives that cannot be written as elementary functions. Liouville's theorem, formulated by Joseph Liouville between 1833 and 1841, is the algebraic statement that explains when an elementary antiderivative can exist: if a function has an elementary antiderivative at all, then that antiderivative lies in the differential field of the function, plus finitely many logarithms. The theorem underlies the Risch algorithm for symbolic integration, which relies on it to find any elementary antiderivative.
A differential field is a field together with a derivation , i.e. an additive map satisfying . Its constants form the subfield
Let be a differential field extension (the derivation of restricts to that of ).
The running example is , the field of rational functions in one variable with the standard derivative .
Let be differential fields of characteristic zero with , and let be an elementary differential extension of . If and satisfy , then there are , constants and nonzero , and with
The theorem reduces the question of whether an integral is elementary to a question about the base differential field. That reduction is what makes decision procedures for integration in finite terms (the Risch algorithm) possible, and it is the standard route to proving that , or have no elementary antiderivative.
The result is classical and proved (Liouville; modern algebraic proof by Rosenlicht; textbook proof in Geddes–Czapor–Labahn, §12.4). Mathlib contains a formalization of the algebraic-extension part of the argument (IsLiouville, isLiouville_of_finiteDimensional in Mathlib/FieldTheory/Differential/Liouville.lean); the logarithmic and exponential steps and the full theorem for elementary extensions are the remaining work.
The algebraic steps can be handled by taking traces. The central difficulty is the transcendental steps: for a logarithmic or exponential generator one must show, by comparing partial-fraction expansions in and degrees in , that an expression of the Liouville form over can be pushed down to one over . This needs the hypothesis that no new constants appear. The induction must also track how constants and logarithmic derivatives behave along the whole chain.
A differential field is a Mathlib Field with a Differential instance (a derivation over , written ); the extension is an Algebra F G with DifferentialAlgebra F G, i.e. commutes with the embedding. The chain of the elementary extension is a sequence of IntermediateField F G, starting at and ending at . Each step adjoins a single element, which is algebraic, logarithmic, or exponential over the previous field, and every derivative is computed in . Characteristic zero is assumed (CharZero F). The article does not state it, but it is the standing convention of the theorem in its standard sources. is stated as the equality of the image of with . In the conclusion, the are required to be nonzero, so the quotients carry no division-by-zero junk.
For the examples, is Mathlib's RatFunc ℂ. Mathlib does not provide its derivative, so the examples take an arbitrary derivation satisfying IsStandardDerivation (it agrees with the formal derivative on polynomials). Milestone 2 asserts that exactly one such derivation exists, so the examples are not vacuous.
Given a monic polynomial with integer coefficients, one can reduce it modulo each prime and factor it over the finite field . The way factors changes with , and the question of how often each factorization pattern occurs has a precise answer: Chebotarëv's density theorem (1922). It is the common generalization of Dirichlet's theorem on primes in arithmetic progressions (1837) and a theorem of Frobenius (1880, published 1896), and it underlies a large part of algebraic number theory, for example the fact that a Galois extension of a number field is determined by the set of primes that split completely in it. This mission follows the elementary exposition of P. Stevenhagen and H. W. Lenstra, Jr. (Math. Intelligencer 18 (1996)), which states all three theorems over with a minimum of terminology.
Timeline.
Let be monic of degree with nonzero discriminant , so that has distinct complex zeros . Let be its splitting field and its Galois group. Every permutes the zeros; the lengths of the cycles (including cycles of length 1) form the cycle pattern of , a partition of .
For a prime , the degrees of the irreducible factors of over form the decomposition type of modulo , again a partition of .
A Frobenius substitution of is an element such that, for some prime ideal of the ring of integers lying over ,
For these elements form a single conjugacy class of , written .
A set of primes has (analytic, or Dirichlet) density if
and natural density if as .
For every conjugacy class of ,
Chebotarëv's theorem shows that every conjugacy class of the Galois group occurs as a Frobenius class for infinitely many primes, with a predictable frequency. Its standard consequences include: the Frobenius elements are equidistributed; a Galois extension is determined by its completely split primes; if has a zero modulo almost every prime then is linear or reducible; prime ideals are equidistributed over ideal classes. The theorem is the first step in many arguments in arithmetic geometry (e.g. Serre's work on -adic representations).
The theorem is classical and proved; this mission is about formalizing it. Mathlib contains Frobenius elements in Galois extensions of Dedekind domains and Dirichlet's theorem in the form "infinitely many primes in each coprime residue class", but, to our knowledge, neither the density form of Dirichlet's theorem nor Frobenius's or Chebotarëv's density theorem.
The Galois-theoretic parts (milestones 3–6) are standard but require connecting Frobenius elements in with factorization of modulo , including the fact that forces to be unramified in . The analytic core is harder: one needs Dedekind zeta functions and -functions of number fields and their behaviour at . The reduction of the general case to the cyclotomic case (Chebotarëv's "crossing" with cyclotomic extensions) needs the density statement over an arbitrary number field as base, not only over ; in particular, the statement over alone cannot be proved by induction on itself.
All declarations live in the namespace ChebotarevDensity and share one definition file.
SplittingField of viewed in ; is Polynomial.Gal; is Mathlib's Polynomial.discr.IsArithFrobAt at some prime ideal of containing ; "" means that some Frobenius substitution of lies in (for this is equivalent to all of them lying in , by milestone 4).Equiv.Perm.partition of the permutation induced on the complex zeros of ; it includes fixed points.Welcome contributions: Dedekind zeta functions and Hecke -functions at , the density form of Dirichlet's theorem, unramifiedness of primes not dividing the discriminant, and the general number-field version of the theorem.
In 1998 Smale listed eighteen problems for the twenty-first century; the eighteenth asks: What are the limits of intelligence, both artificial and human? (Smale 1998). The paper of Acharjee and Gogoi (arXiv:2310.10792) proposes a mathematical model of a mind, the cognitive-consequence space, built from a Tarski consequence operator, and claims that two theorems about this model (its Theorems 3.3 and 3.4) show that "human intelligence is limitless" (Discussion, p. 22; Conclusion, p. 23).
This mission records that model and its results in Lean 4 exactly as stated, so that each claim becomes a checkable statement: proved, or refuted, by the verifier rather than by argument.
A cognitive-consequence space is a set of mental representations (thoughts) with a consequence operator and an implication connective satisfying Tarski's axioms as listed in the paper (p. 5):
together with the paper's standing assumption (p. 5, after Definition 3.2).
A set is deductive if . The cognitive-consequence topology is
and members of are consequence-wise open (CWO). The cognitive closure is the intersection of all deductive sets containing .
Separately, a cognitive similarity distance is a function together with a relation (" and cognitively coincide") such that , is symmetric, , and the triangle inequality holds. A sequence of thoughts converges to if for every we have for all large .
For every cognitive-consequence space,
Theorems 3.1, 3.2, 3.3, 3.5, 3.6, 3.7 and Corollary 3.5 (the topology and the cognitive closure), Theorems 3.8 and 3.12 (cognitive limits), Theorem 4.3 (the filter ) and Theorem 5.1 (Gödel's incompleteness black hole).
The paper presents the goal as its answer to the human-intelligence half of Smale's eighteenth problem. A machine-checked verdict on the goal settles whether that conclusion follows from the paper's own axioms. The milestones are the paper's structural results about , cognitive closure and cognitive limits.
Status: to the best of current knowledge none of these results has a published machine-checked proof. The first conjunct of the goal (Theorem 3.3) follows from the standing assumption . The second conjunct (Theorem 3.4) is not implied by the listed axioms as formalized: the consequence operator with for every , on a one-point language, satisfies all of them and has . The goal is therefore expected to be resolved by a disproof.
The content of the goal is the existence of a nonempty CWO set, equivalently of a deductive set different from (a consistent theory). The paper's argument for Theorem 3.4 derives and calls this a contradiction; nothing in the axioms forbids it.
CogCons.CognitiveConsequenceSpace C bundles , the connective imp, axioms (i)–(vi) and . The syntax and interpretation of the paper are not modelled beyond imp.CogCons.CognitiveSimilarityDistance C is independent of ; sequences are indexed by starting at ; is an arbitrary relation constrained only by the listed axioms.Linear programming is usually described as "solvable in polynomial time", but that statement is about rational inputs given exactly. In Smale's list of problems for the 21st century (Smale 1998), Problem 9 asks for a polynomial-time algorithm over the reals deciding the feasibility of , and Smale explicitly calls for "models which process approximate inputs and which permit round-off computations". Real data such as , entries of a discrete cosine transform, or even in floating point can only be accessed approximately.
Bastounis, Hansen and Vlačić pose the extended Smale's 9th problem: in a model where the algorithm can only query approximations of the input to any requested accuracy, can one compute minimisers of linear programming, basis pursuit and Lasso to correct digits? Their Main Theorem I (Theorem 3.4) shows that the answer depends on in a sharp way: for a suitable class of well-conditioned, bounded inputs, no algorithm at all (not only no efficient one) produces correct digits, while digits are computable (but not in bounded time) and digits are computable in polynomial time.
This mission targets the first, impossibility, half of Theorem 3.4(i) for linear programming.
Linear program. For , and , the solution set is
It is a subset of with the norm, . An input is a pair , and the evaluations of are its coordinates and entries .
Extended model (-information). Let . An oracle representation of is a family , indexed by evaluations and accuracies , with and . An algorithm must succeed on every oracle representation of every input.
General algorithm. To make impossibility results independent of the machine model, the paper uses general algorithms (Definition 9.3): a map from inputs to ( = no output) together with a nonempty set of evaluations read on . This set is finite whenever halts. The output is determined by the values read, and any input that agrees on those values reads the same set. Turing machines and BSS machines with an oracle are special cases; general algorithms can even solve the halting problem.
Error and breakdown epsilon. The error is , with distance from . The strong breakdown epsilon is the supremum of all such that every general algorithm has error on some input (Definition 9.17).
For every integer , all dimensions and every there is a nonempty class of inputs with nonempty solution sets, and , such that
The theorem shows that for LP with inexact input, being non-computable in Turing's sense does not rule out a finer complexity theory. The paper builds a " / / digits" classification on this. It also explains why established solvers can return wrong answers with a success flag on small, well-conditioned LPs (§4 of the paper), and it bears on computer-assisted proofs that rely on inexact LP, such as the Flyspeck proof of the Kepler conjecture.
The result is proved on paper. As far as the proposer knows, it has not been machine-checked. This mission formalizes the deterministic impossibility part for LP and puts in place reusable infrastructure: general algorithms, breakdown epsilons and -information. That infrastructure is the base for later missions on the randomised parts of Theorem 3.4(i)–(ii), the weak breakdown epsilon (iii), the exit-flag theorem (Theorem 5.1), and basis pursuit and Lasso.
The obvious objection is that LP is in P for rational inputs, so some rounding scheme ought to work. It fails because an algorithm must halt after reading finitely many approximations. Two inputs that agree to that accuracy but have minimisers far apart then receive the same output. Setting this up needs a notion of algorithm strong enough to cover every computational model, a precise -information model in which the adversary controls the approximations, and explicit LP geometry in which an arbitrarily small perturbation of moves the minimiser by a fixed amount.
PiLp p (Fin N → ℝ).run : Ω → Option M (none = NH) and a read set queried, satisfying the axioms (i)–(iii) of Definition 9.3.ℝ≥0∞), and the error of NH is . The infimum over an empty solution set is . The goal also requires nonempty solution sets, so no junk value enters.ℕ+). An oracle input is stored as a pair (input, oracle family), and algorithms can read only the oracle family.Optimal transport asks for the cheapest way to move one distribution of mass onto another. Monge posed the problem in 1781 for maps; Kantorovich (1942) relaxed it to transference plans (couplings), turning it into an infinite-dimensional linear program with a dual: maximize the total revenue of pickup and delivery prices that never exceed the cost, . The equality of the two values — Monge–Kantorovich duality — underlies much of modern optimal transport, with uses in economics (matching markets, principal–agent problems), probability, and PDE.
This mission formalizes the duality theorem and its proof as presented in Colin Yao, Monge–Kantorovich and Transportation Theory (paper dated September 10, 2023), whose proof follows Villani's Optimal Transport: Old and New and, for the weak inequality, Galichon's Optimal Transport Methods in Economics.
and are Polish spaces (separable, completely metrizable) with their Borel σ-algebras; and are Borel probability measures on and ; is a continuous cost function.
including existence of a minimizing plan; the common value may be .
Duality converts a minimization over measures into a maximization over functions; it characterizes optimal plans by the complementary-slackness condition that they are concentrated on , and it is the entry point to Brenier's theorem, the Kantorovich–Rubinstein formula for the Wasserstein-1 distance, and the economic applications discussed in Section 5 of the source. The result is classical and proved in the literature; the work here is to formalize the known proof and to supply reusable infrastructure (couplings, -cyclical monotonicity, -transforms) on top of Mathlib's measure theory.
The weak inequality is a short integration argument; the reverse inequality is where the work lies. Finite-dimensional linear-programming duality does not pass to general measures directly: one must produce a cyclically monotone plan as a limit of discrete approximations (tightness and Prokhorov's theorem, closedness of the cyclic-monotonicity condition under weak convergence), build a potential from chains of cost differences, and control measurability and integrability of and . Passing from bounded to unbounded nonnegative costs requires an additional approximation argument, which the source only sketches (Section 4.5).
Lean namespace MongeKantorovichYao; one definition file provides transference plans, -cyclical monotonicity, -conjugates, -concavity and -subdifferentials. Conventions: marginals are pushforwards along the projections; -conjugates are extended-real infima (no default values); the transport cost in the goal is the -valued integral of the nonnegative cost, and both sides of the goal are compared in the extended reals, so the infinite-cost case is included and no integrability hypothesis is added. The dual side ranges over bounded continuous functions with the constraint imposed at every point. Proposition 4.22 is stated for bounded (as used in Proposition 4.31), since with unbounded costs a real-valued potential need not exist. Infrastructure that may be missing from Mathlib: Prokhorov-type compactness of tight families of probability measures, weak convergence of empirical measures, and lower semicontinuity of .
Service parts supply chains are often limited by a capacitated resource, such as a production line or a repair shop, instead of by lead times alone. Once capacity binds, the classical tools for setting stock levels (Palm's theorem and the Poisson distribution of units in resupply) no longer apply, and the quantity that determines how much stock is needed is the shortfall: the amount by which the end-of-period inventory falls below its target because capacity was insufficient. Chapter 8 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) builds its tactical planning models for capacity-limited systems on the distribution of this random variable, and on a continuous-time repair queue in which item counts are geometric.
The shortfall recursion is the Lindley recursion of queueing theory (Lindley 1952), so its stationary law is the law of the maximum of a random walk with negative drift. The exponential tail of that maximum goes back to Cramér's work on ruin probabilities; for capacitated production–inventory systems it was stated by Glasserman (1997), whose theorem the book quotes as Theorem 11. Glasserman and Tayur (1995) used the shortfall to optimize base-stock levels in multi-echelon capacitated systems, and Roundy and Muckstadt (2000) studied the mass-exponential approximation that the theorem motivates.
A single item is produced in periods of an infinite horizon; at most units can be produced per period. The demand of period is ; the demands are nonnegative, independent and identically distributed, with generic demand and (the standing assumption of Section 8.1.1).
Under the modified policy with target level , the facility observes and produces units, where is the end-of-period net inventory and . The shortfall satisfies and
With the random walk (), the stationary shortfall is
A law on is lattice if it is concentrated on a progression with .
In the discrete case ( and integer valued) is a Markov chain on with transition probabilities (p. 185). In the repair model of Section 8.3.1, reparable units of item arrive at rate , , a single exponential server repairs at rate , is the number of units in repair and the number of item- units, and .
Assume for all , with ; ; the law of is non-lattice; and has a root in . Then there are and with
The constant is left unspecified, as in the book.
The exponential tail is the justification the book gives for approximating the shortfall by a mass-exponential law (an atom at zero plus an exponential tail), from which target stock levels and fill rates are computed in closed form. The decay rate depends only on the demand law and the capacity, so the theorem also says how the stock needed for a given service level grows as utilization approaches one. The discrete-chain milestones justify the exact computation of the shortfall distribution behind the book's Table 8.1 and Figures 8.3–8.8. The geometric law of reduces the multi-item repair problem to independent newsvendor problems with an explicit solution.
The asymptotics of the random-walk maximum are proved in the literature (Cramér–Lundberg theory, Feller Vol. II, XII.5; Asmussen, Applied Probability and Queues, XIII.5); no machine-checked proof is known to exist. Mathlib has neither the Lindley recursion, nor ladder-height decompositions, nor the key renewal theorem for non-lattice laws. The printed Theorem 11 is not correct as stated (see Formalization scope), so the mission also records a corrected statement.
The central step of the goal is the passage from the random walk to an exact asymptotic. An exponential change of measure (Esscher tilt) with the root turns into an expectation under a law with positive drift, but it only yields the upper bound (Lundberg's inequality); it does not show that converges, nor that the limit is positive. Convergence needs a renewal theorem for the overshoot of the tilted walk, which fails for lattice laws. That is why the non-lattice hypothesis cannot be dropped. For the milestones, the existence of the stationary law needs the reversal argument that identifies the law of with that of , plus the strong law of large numbers to show from .
iIndepFun plus IdentDistrib with ), integrable, with ; these are fields of ShortfallModel. Periods are numbered from as in the book (demand 0 is an unused i.i.d. copy). The discrete case is a separate structure with -valued demand and capacity.Service parts networks (spare parts for aircraft, military systems, industrial equipment) hold stock at several echelons: a depot, intermediate stocking facilities, and bases or warehouses that face demand. Two questions recur in their planning. First, how should a given amount of stock be split among locations whose expected costs are convex in the stock they hold? Second, does adding an echelon, a depot that pools the demand of several warehouses, raise or lower the stock the system needs?
Chapter 7 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879), treats both. For the second it follows Eppen and Schrage (1981, reference [78] of the book): with normal demands, a depot that places orders every period and allocates stock so that all warehouses face the same stockout probability reduces the choice of system stock to a single critical-fractile equation. For the first, the chapter's multi-echelon pooling model (Section 7.3) evaluates nested cost functions of the form "holding and shortage cost plus the minimum over allocations of a sum of convex costs", and its appendix (Section 7.4) gives the marginal allocation algorithm AllocOpt that computes these minima exactly for every stock level at once.
Marginal analysis for separable convex resource allocation is classical (Fox, Management Science, 1966); the monograph of Ibaraki and Katoh (MIT Press, 1988) surveys it.
Allocation data (Section 7.4). There is a set of locations and an augmented set . Each location has integer gridpoints . For , the value of a convex function is given at each gridpoint. The slopes (7.19) are for , and repeats the last one. The piecewise linear approximation of (7.20)–(7.21) interpolates the values at the gridpoints and continues with slope beyond the last one. A convex function on is also given.
The allocation optimization (7.22) asks, for each , for
Algorithm AllocOpt (Definition 4) keeps a current gridpoint index and allocation per location. For each increment of the target, it repeatedly gives units to a location whose current slope is minimal, up to that location's next gridpoint, and records the accumulated cost.
Pooling system (Section 7.2.1). One depot supplies warehouses. The demand at warehouse in period is normal with mean and variance , independent across periods and warehouses. The supplier-to-depot lead time is periods, the depot-to-warehouse lead time periods, and holding and backorder costs are equal at all warehouses. Positions are in balance when is the same for all . For system inventory position , with the system demand over periods and the demand at over the next periods, the balanced allocation gives each warehouse a share proportional to , and is its end-of-period net inventory.
For every tie-breaking rule in its arg min steps, AllocOpt returns values that satisfy (7.22) for every : some feasible integer allocation attains , and no feasible integer allocation does better.
then a nonnegative allocation of the arriving units restores balance. 5. Net inventory law (pp. 156–157): is normal with mean and variance . 6. Critical fractile (pp. 157–158): minimizes if and only if , where
The goal certifies an algorithm that the chapter uses as a subroutine three times: in the pool cost (7.14), the subsystem cost (7.15) and the system cost (7.17), and hence in the claim of Section 7.3 that the system-wide cost function can be computed in time in the number of locations. Because AllocOpt produces the whole vector in one pass, its correctness gives the nested value functions at every gridpoint of the next echelon, which is what allows the recursion up the echelons. The Eppen–Schrage milestones give the classical quantitative form of risk pooling: the system stock is set by one critical fractile, and the standard deviation term is what the book compares with the single-warehouse and the decentralized systems.
On formalization: the book states Proposition 2 with a two-sentence argument and Remark 2 without proof. The Eppen–Schrage computations are displayed derivations. None of these results has a machine-checked proof on the platform. A verified AllocOpt, stated for an explicit algorithm rather than for an abstract greedy procedure, is reusable for any separable convex integer allocation with a sum constraint.
The usual greedy exchange argument assumes that units are allocated one at a time. AllocOpt allocates in blocks, up to the next gridpoint of the chosen location, and it carries its state across successive targets without restarting. The proof must therefore show that the state after each outer step is itself an optimal allocation for the current target, and that block moves never step past a breakpoint where the arg min would change. The slopes can be negative, and the equality constraint forces allocation even when every marginal cost is positive. Remark 2 needs an additional argument: under the inequality constraint the loop may stop before reaches zero, and that point is optimal only because the slopes are nondecreasing.
For the pooling results, the balanced allocation mixes the depot-lead-time demand of all warehouses with the local demand , and the Gaussian law of rests on the independence of disjoint blocks of periods. The fractile statement requires strict monotonicity of each warehouse's expected cost derivative in , not only a first-order condition.
Fin Mbar; gridpoints are integers, values and slopes real numbers; allocations are functions Fin Mbar → ℕ. The standing assumptions of Section 7.4 form the predicate WellFormed: , for (a slope (7.19) needs two gridpoints), gridpoints starting at and strictly increasing at every location of , each the value of a function convex on , and convex on .Service parts (spare engines, avionics modules, repairable components) are usually managed one unit at a time: whenever a customer order removes a unit from stock, a replacement is ordered at once, from a repair shop or an outside supplier. This is the (s–1, s) policy, under which the inventory position (on hand plus on order minus backorders) stays constant at the stock level . Every performance measure of such a system (fill rate, expected backorders, availability) is a function of one random variable: the number of units in resupply, i.e. ordered but not yet returned. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005) computes its distribution, and the rest of the book (the METRIC-type multi-echelon models of Chapters 4 and 5, the stock-level optimization of Section 3.4) is built on that computation.
Timeline. C. Palm (1938) showed, in the setting of telephone traffic, that in an infinite-server system with Poisson arrivals the number of busy servers has, in steady state, a Poisson law whose mean is the arrival rate times the mean service time, whatever the service-time distribution. Feeney and Sherbrooke (1966) carried the result to (s–1, s) inventory systems with compound Poisson demand, and treated the lost-sales case. Sherbrooke's METRIC model (1968) made the Poisson law of units in resupply the basis of multi-echelon spare-parts planning.
A single item is stocked at one location. Customer orders arrive at epochs of a Poisson process with rate , started empty at time : the interarrival times are independent and exponential with rate , and . The -th order triggers a resupply order with resupply time . The resupply times are independent and identically distributed, independent of the arrival process, with a density , distribution function and finite mean
With backorders allowed, the number of units in resupply at time is
and counts the orders placed in . On-hand stock and backorders at time are and .
In the compound Poisson version the -th order asks for units, the sizes are i.i.d. with , independent of arrivals and resupply times, and all units of one order share its resupply time . The units in resupply are . Writing for the probability that orders ask for units in total, the compound Poisson probabilities with parameter are
In the lost-sales version an order that finds no stock on hand is lost, so at most units are ever in resupply.
For every ,
The resupply-time law enters only through its mean. This is the statement the book's proof establishes and every later chapter uses.
The result. Palm's theorem turns an infinite-dimensional object (the whole resupply-time distribution) into one number, . This insensitivity is what makes spare-parts planning computable: the expected backorders at stock level are , the fill rate is , and both can be optimized over with only the demand rate and mean repair time as data. Theorem 7 extends this to batch demand, Theorem 9 to systems allowed a response time, and Theorem 8 gives the exact law when shortages are lost instead of backordered.
Formalizing it. All of these results are classical and proved. None of them is formalized on the platform, and Mathlib has Poisson and exponential distributions but no Poisson process, no thinning theorem and no infinite-server queue. The mission produces a Poisson arrival stream built from i.i.d. exponential gaps, the conditional-uniformity property of its epochs, independent thinning, and the M/G/∞ transient law, all reusable in queueing and inventory missions.
The algebra of the proof (summing the binomial against the Poisson law of ) is short. The work is in the probabilistic step the book treats in a sentence: that, given , the orders behave like independent uniform epochs, each of which independently is still in resupply at time with the same probability . This needs the joint law of the partial sums of exponential variables (Eq. (3.3)), and then a symmetrization argument, since the epochs are ordered while the resupply times are attached to order indices. The naive route of computing by conditioning on individual epochs does not go through without that exchangeability step. The limit is then elementary; stating a stationary version directly is not a substitute, since the book's "steady state" is exactly this limit.
The model is a structure on a probability space : exponential interarrival times with rate , nonnegative resupply times with a density and an integrable first coordinate, and mutual independence of the whole family. Orders are indexed from , so the book's are . Counts are cardinalities of sets of order indices, with value on the probability-zero event where infinitely many orders fall in a bounded interval.
Commitments and pinnings:
A model in which is postulated through its law, or in which resupply times may depend on the arrival epochs, makes the goal empty or false; here is computed from the primitive arrival and resupply times, whose joint law is fully specified.
Welcome contributions: a general Poisson-process library (construction from exponential gaps, Poisson marginals, order-statistics property), independent thinning, and proofs of the milestones in the listed order.
A stocking point that reviews its inventory once per period and must decide how much to order is the basic unit of every service parts supply chain: each warehouse, each repair depot and each forward location in the networks studied later in Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) faces this decision for thousands of items. The practical rule used everywhere is the order-up-to (base-stock) rule: bring the inventory position up to a fixed target level whenever it falls below it, and order nothing otherwise. Chapter 2 of the book justifies this rule for a single item with linear costs, following the dynamic-programming argument of Karlin and Scarf, and the rest of the book takes the rule as given.
Timeline. Arrow, Harris and Marschak posed the periodic-review inventory problem as a dynamic program in 1951 (Econometrica). Bellman, Glicksberg and Gross showed in 1955 that with linear ordering cost and convex expected holding and shortage costs the optimal policy has a critical-number form (Management Science). Karlin and Scarf (1958) extended the analysis to a positive lead time, the setting of the book's Theorems 1–3. Veinott (1965) gave conditions under which a base-stock policy is optimal in multi-product, nonstationary models (Management Science).
One item is stocked at one location. At the start of each period the inventory position is observed and a quantity is ordered; with lead time one period it arrives at the start of the next period. Demand in each period is independent of other periods and has a density on that is positive and continuous. Unmet demand is backordered. Costs are linear: per unit ordered, per unit on hand at the end of a period, per unit backordered at the end of a period, and future costs are discounted by . The one-period cost is
The book assumes throughout that : the backorder cost outweighs the saving from deferring a purchase.
The -period value functions are and, for ,
An order is optimal at if it attains this minimum over all . The order-up-to rule with level orders . The marginal function of eq. (2.8) is . In Lean these are Model, Model.L, Model.f, Model.IsOptimalOrder, Model.IsOrderUpToOptimal and Model.F in the namespace ServiceParts.BaseStock.
For every horizon , either there is a real level with
or ordering nothing is optimal for every (level ); and there is such that the level is real for all . No value of is fixed: the goal asserts the shape of the optimal policy only.
The theorem reduces an infinite-dimensional control problem, a choice of order quantity for every possible inventory position, to one number per period. Every later chapter of the book (Palm's theorem for policies, METRIC-type stock level optimization, allocation in multi-echelon systems) parameterizes policies by such stock levels; this is where the book justifies that parameterization.
The result is classical and proved in many texts. On Prove2Me the mission produces a machine-checked finite-horizon version with a continuous demand density, including the calculus the proof needs: convexity of an expected cost defined by integrals against a density, differentiation under the integral sign in the recursion, and the one-sided behaviour of the value function at the order-up-to level. Existing platform results on base-stock optimality (Veinott's multi-product model, advance demand information) use different models and different arguments; none covers this recursion.
The argument is an induction on whose hypothesis carries convexity, the derivative formula (b), and bounds on . The delicate step is the existence of a finite root of : its limit at depends on whether the previous level was finite. For nothing is ordered and the limit is , which the assumption does not make negative. The book's base case ("left to the reader") therefore fails when : with , , the two-period problem never orders. The goal is corrected accordingly.
Two properties the book's induction also carries are not usable as printed. Property (d), , is false: for large , approaches , which increases with . The second-derivative clause of property (c) fails at whenever . A solver cannot follow the printed induction step for step; property (a), which the book derives from (d), is true and is a milestone in its own right.
Model, together with positivity and continuity of on , , and .Differentiable, HasDerivAt) and do not read deriv as evidence of it.A recursion in which ordering is restricted to order-up-to rules, or in which is defined through , would make the goal a tautology; here is defined by minimization over all and optimality is checked against all orders.
Needed infrastructure: convexity and differentiation of parametric integrals against a density on , and minimization of a differentiable convex function over a half-line. Both are reusable for the other stochastic inventory missions on the platform. Proofs of individual milestones are welcome independently of the goal.
Many optimization problems in operations research have an objective that is an expectation, , over a random parameter whose distribution is known only through samples or is too complex to integrate. Two-stage stochastic programs, inventory and reliability models, and simulation-based design all have this form. Neither nor its subgradients can be evaluated exactly, but a random vector whose conditional mean is close to a subgradient is often cheap to compute: a sample subgradient of , or a finite-difference quotient of two sampled values.
Stochastic quasigradient (SQG) methods, developed by Ermoliev and co-workers in Kiev from the late 1960s, use such vectors in place of subgradients. They extend the stochastic approximation procedures of Robbins–Monro (1951) and Kiefer–Wolfowitz (1952) to nonsmooth convex objectives, general convex constraints, and directions whose conditional mean is biased by a vanishing amount. This mission formalizes the basic convergence theory of the simplest SQG method, the projection method, as presented by Yu. Ermoliev in Chapter 6 of the IIASA volume Numerical Techniques for Stochastic Optimization (Springer 1988).
Timeline (as cited in the chapter's bibliography).
Let be a nonempty convex compact set and convex and continuous on . The optimal set is . The projection onto is .
On a probability space, the stochastic quasigradient projection method produces random vectors by
where is a step size and a random direction. Write for conditional expectation given the history . The direction is a stochastic quasigradient if, for every ,
where the error is a function of the history. If the conditional mean of is a subgradient plus a bias , then (6.12) holds with (6.13).
A sequence of random vectors is a stochastic quasi-Féjer sequence for if and there are random with such that for all
If, with probability 1, and , and
then with probability 1 the iterates converge and .
Theorem 6.2 is the prototype convergence theorem for SQG methods. Its hypotheses allow random step sizes chosen from the history, nonsmooth objectives, and directions with a bias that vanishes fast enough; its conclusion is convergence of the iterates themselves to a single optimal point, not only convergence of function values or of . The later chapters of the same volume (adaptive step sizes, Chapters 17–18; nonstationary problems, §6.4) reuse the same framework. Theorem 6.1 isolates the probabilistic content in a form that applies to any algorithm with a quasi-Féjer inequality. The efficiency estimate gives a non-asymptotic accuracy bound for the averaged iterate.
The results are classical and proved in the literature: Theorem 6.1 in Ermoliev (1976, p. 98), Theorem 6.2 in this chapter (pp. 145–146). To our knowledge none of them has a machine-checked proof. Mathlib has conditional expectations and the a.s. martingale convergence theorem, but no Robbins–Siegmund-type almost-supermartingale lemma and no stochastic subgradient method. A formal proof of this mission would supply both.
The deterministic argument for projected subgradient methods compares with for a fixed . In the stochastic setting this comparison holds only in conditional mean, with a perturbation that is random, and the distances converge only almost surely, with an exceptional null set that depends on . Since is typically uncountable, "for every , almost surely" does not immediately give "almost surely, for every ", and it is the second form that identifies a single limit. A second difficulty is that only yields a subsequence along which approaches its minimum; passing from there to convergence of the whole sequence is exactly what part (c) of Theorem 6.1 is for.
EuclideanSpace ℝ (Fin n). The probability space is an arbitrary measurable space with a probability measure. is a chosen minimizer of over (unique for nonempty closed convex ). The history is the -algebra generated by ; and are measurable with respect to it.condExp. The quasi-Féjer definition requires square integrability of every (implied by the book's definition when ), so no conditional expectation is taken of a non-integrable function.The scenario approach replaces an optimization problem with uncertain constraints , , by the program that enforces only constraints drawn at random from the distribution of the uncertainty. Its solution is then judged by its violation, the probability that a new instance is not satisfied. For convex programs in the violation is controlled by the dimension alone (Calafiore and Campi 2006; Campi and Garatti 2008), because a convex program has at most support constraints. Many problems where the scenario approach is used in practice are not convex: control with quantized inputs, mixed-integer design, classification with nonconvex losses, and decisions over infinite-dimensional or unstructured sets. For those programs no a priori bound on the number of constraints that determine the solution exists.
Timeline, as recorded in Chapter 8 of Campi and Garatti's textbook:
Let be a generic set; it may be an infinite-dimensional space or a set with no algebraic structure. Let be a cost and constraint sets indexed by , where carries a probability . Neither nor the is required to be convex. With a sample drawn independently from , the scenario program is
and denotes its solution, assumed to exist and be unique for every sample.
The violation of a decision is (Definition 3.1).
A support set (Definition 8.8) is a subset of the constraints such that the program with only these constraints in place has the same solution as the program with all constraints. The full set of constraints is always a support set; a support set need not be minimal (of smallest cardinality) or irreducible (with no removable element). Let be the cardinality of the support set returned, for every sample, by some fixed algorithm.
For every function with ,
The level function is free: the statement is one inequality per admissible , and it holds for any algorithm producing support sets. This is the weakest form that carries the whole result.
For let
The arithmetic half states that maps into , , and the right-hand side of (8.15) equals (for ). The probabilistic half states .
The result turns the size of a support set, a quantity observed after the program is solved, into a certificate on the violation of the solution, for any optimization or decision problem whose solution is determined by a subset of the data. With the choice (8.16), a user who finds a support set of size can assert with confidence . The book's Figure 8.12 shows that for remains well below for up to a sizeable fraction of . Because the algorithm that finds the support set is arbitrary, cheap heuristics that return non-minimal support sets still give valid, if weaker, guarantees. The result does not recover the tight convex bound (3.4); for convex programs the Chapter 3 theory remains sharper.
The statement is proved in [31] and is the probabilistic core of the sample-compression arguments of learning theory (Floyd and Warmuth 1995) in the form used by the scenario approach. To the best of available knowledge it has no machine-checked proof. The platform's UnderstandingML.compression_bound proves a sample-compression bound for a fixed compression size with a different constant; it does not cover a data-dependent size or an arbitrary level function. A formal proof here provides a reusable bound for data-dependent support sets over arbitrary decision sets.
The natural first step is: condition on the support set being a particular index set with , and argue that the solution is then a function of the sampled constraints in alone, while the other samples are independent of it and must all be satisfied. The difficulty is that the event "the algorithm returns " depends on all samples, and the solution of the reduced program on is defined only where that program has a unique solution; the decomposition of the probability therefore has to be carried out on sections of the product space, with a measurability argument for each piece. A second point is that is random and data-dependent: a bound for each fixed does not directly give a bound at the random level , and the role of the condition must be accounted for at .
Lean representation and committed conventions:
ω : Fin N → Δ with law Measure.pi (fun _ : Fin N => P); indices run over .Finset (Fin N); the reduced program with index set has feasible set (all of for ).alg : (Fin N → Δ) → Finset (Fin N) returning a support set for every sample; is the cardinality of its output. The goal is universal over such maps.ENNReal.ofReal of the real right-hand side.Implicit hypotheses of the page, made explicit (the book states on p. 33 that measurability issues are glossed over): the constraint relation is measurable in ; the solution map is measurable; each event is measurable; exists and is unique for every sample; in the arithmetic half of (8.16).
A trivializing formalization is ruled out: the algorithm is not existentially quantified and is not the minimal support set, the reduced programs are not all assumed solvable (which would be unsatisfiable when has no unconstrained minimizer), and the support-set property requires uniqueness of the reduced solution, without which the bound is false.
Needed infrastructure: product measures on Fin N → Δ, splitting of such products along a subset of coordinates, and Fubini/Tonelli for sections. These pieces are reusable for other compression-type bounds. Contributions welcome: proofs of the two milestones and of the goal, and lemmas on splitting Measure.pi over a Finset of coordinates.
Search engines sell advertisement slots next to their results through ad-auctions. Advertisers bid on keywords, and each advertiser also sets a daily budget: the most it is willing to pay in a day. Queries arrive one at a time and each must be assigned to an advertiser at once, with no knowledge of the queries still to come. The seller's revenue from an advertiser is capped by its budget, so an allocation rule that ignores budgets can exhaust a high bidder early and forgo revenue that a more even allocation would have collected. The question is how much of the offline optimum an online rule can guarantee against every arrival sequence.
Mehta, Saberi, Vazirani and Vazirani (FOCS 2005 / J. ACM 2007) gave a deterministic algorithm whose competitive ratio tends to when bids are small compared with budgets, and showed that no deterministic algorithm does better. Their algorithm builds on online bipartite matching (Karp, Vazirani and Vazirani, STOC 1990) and online -matching (Kalyanasundaram and Pruhs, 2000). Buchbinder, Jain and Naor (ESA 2007) rederived the bound with an online primal-dual algorithm, which gives the ratio in closed form for every value of the bid-to-budget ratio and extends to multiple slots, stochastic information, bounded degree and budget flexibility. This mission formalizes the basic algorithm of that paper and its Theorem 1.
There is a finite nonempty set of buyers. Buyer has a known budget . Products arrive one by one; when product arrives, every buyer's bid on it is revealed. The bid-to-budget ratio is
A fractional allocation assigns fractions of products to buyers; the revenue from buyer is the minimum of and .
The offline fractional problem is the packing LP, which the paper calls the dual:
Its LP dual, the paper's primal, is the covering LP:
The Allocation Algorithm has a parameter and starts from . When product arrives it takes a buyer maximizing . If , the product is not sold. Otherwise it charges the minimum of and 's remaining budget, sets and , and updates
Its revenue is the total amount charged.
For every instance and every bound with for all , the Allocation Algorithm run with , under any tie-breaking of the maximum, satisfies for every feasible of the packing LP
With this is the paper's statement that the algorithm is -competitive; the fractional optimum bounds every integral offline allocation.
The proof of Theorem 1 rests on three claims and three auxiliary facts, each a milestone:
and, separately, the second sentence of Theorem 1,
Theorem 1 gives an explicit ratio for every value of , not only in the limit. It tends to the optimal deterministic ratio as bids become small, and it quantifies how the guarantee degrades as single bids become a larger share of a budget. The primal-dual analysis is the template for the paper's later sections and for a line of work on online packing and covering problems, surveyed in Buchbinder and Naor's monograph The Design of Competitive Online Algorithms via a Primal-Dual Approach (Foundations and Trends in TCS, 2009).
The result is proved in the paper, and the proof is short. What this mission adds is a machine-checked proof about an algorithm that is defined, not described: the run is computed by recursion from the instance, and the guarantee is proved for that run and every tie-breaking. A related private mission on the platform, The Design of Competitive Online Algorithms via a Primal-Dual Approach VI: Maximizing Ad-Auctions Revenue, states the monograph's Theorem 10.1, which is this theorem, in a form that takes the analysis's intermediate inequalities as hypotheses over arbitrary lists of won bids; the present mission states it for the algorithm itself. No machine-checked proof of Theorem 1 is known to this mission.
Each step of the proof is elementary; the difficulty is the bookkeeping of an online process. Claims (1) and (2) are statements about a single iteration that must be lifted to the whole run: Claim (1) uses that only increases, and Claim (2) that each product is processed once. Inequality (1) is an induction over the iterations that allocate to one buyer, interleaved with iterations that allocate to others and is the only place where the value of matters. Claim (3) needs a further invariant: the amount charged equals the minimum of the allocated bids and the budget.
A tempting shortcut is to take Inequality (1) and the "at most one undercharge" fact as hypotheses about some list of bids. That does not describe the algorithm and is not the theorem; here the only hypotheses are on the instance and on the tie-breaking rule.
Buyers are a type I with [Fintype I] and [Nonempty I]; products are Fin m, whose order is the arrival order. Bids and budgets are real, with and . The state of the algorithm records , the amounts charged, and ; one iteration is step, the run after products is runPrefix, and revenue sums the charges of the final state. The tie-breaking rule is a function sel of the current and the product, required to return a maximizer of ; the theorem holds for every such rule. The constant is a real power and requires . The theorem is stated for any bound on the ratios, of which the exact maximum is one instance. Claims (1) and (2) are stated for every , which covers the paper's choice. The paper's inequality for allows , read as a limit; the Lean statement requires .
A statement over an unconstrained allocation, or one conditioned on the proof's own intermediate inequalities, would be trivially true or false; the targets here concern only the run the definitions compute.
The development needs finite sums, real powers and logarithms from Mathlib and an induction principle for the run. The LP pair and weak duality are reusable for the paper's extensions, and the run invariants for any primal-dual online algorithm with multiplicative updates. Proofs of any milestone are welcome, as are sharper variants, such as the exact- form or the bound against integral allocations.
Traffic information systems (TIS) such as navigation apps send drivers noisy signals about the state of a road network: incidents, weather, closures. When several such systems coexist, each with its own subscriber base and its own information, a natural question for operators and regulators is whether subscribing to one system rather than another actually lowers a driver's expected travel cost in equilibrium, and how this advantage depends on how many drivers use each system. More information for one population also changes the congestion everybody else faces, so the answer is not simply "more information is better".
Wu, Amin and Ozdaglar (Operations Research 69(1), 2021) answer this question for nonatomic routing games with heterogeneous, possibly correlated information. Their model builds on the weighted potential game framework of Sandholm (2001) and on sensitivity analysis of convex programs. This mission formalizes their Section 5 result: for any two populations the sign of the relative value of information is determined by which of three explicitly computable size regimes the population sizes lie in, and the relative value decreases as one population grows at the expense of the other.
A Bayesian routing game has a finite set of populations , one per TIS, a finite set of network states , and for each population a finite nonempty type space of signals. A common prior is a probability distribution on , . A network with a single origin–destination pair has edges and a finite nonempty set of routes ; each edge has a state-dependent cost that is positive, strictly increasing and differentiable. The total demand is , and population carries the fraction of it, with and .
A strategy profile assigns to each population and type a split of its demand over routes. It induces the route flow and the edge load . With the belief , type evaluates route by its expected cost . A Bayesian Wardrop equilibrium (BWE) is a feasible in which every type uses only routes of minimal expected cost. The equilibrium population cost is at a BWE .
The game has a weighted potential ; its minimum over feasible profiles is the equilibrium potential value . For two populations , the direction moves demand share from to , and is the total share of the other populations. The impact of information measures how much of population 's demand is moved by its signal. Two thresholds are computed from the optimal set of an auxiliary convex program over route flows in which the separate information constraints of and are merged. They define three regimes: (), () and (). The relative value of information is .
For and admissible (in the simplex with ), and every BWE of ,
and is nonincreasing along : for with both endpoints admissible.
The route to the goal follows the paper: Lemma 1 (weighted potential), Lemma 2 (strict convexity of the edge-load potential), Theorem 1 (equilibria are the minimizers of ; unique edge load), Lemma 3 (unique Lagrange multipliers), Proposition 1 (the feasible route flows form a polytope ), Proposition 2 (equilibrium route flows minimize over ), Lemma 4 (), Theorem 2 (equilibrium flows in each regime), Proposition 3 ( decreases, stays constant, increases along in the three regimes) and Lemma 5 ( is convex and directionally differentiable, and ).
Theorem 3 says that a population has an advantage over another exactly when it is the minor population of the pair, relative to thresholds that depend only on the other populations' sizes. Both populations face the same equilibrium cost in the middle regime. It gives a procedure for comparing two information systems without computing equilibria for each size vector: solve one convex program, read off two thresholds, and locate . The paper's Section 6 uses the same machinery, through Lemma 5, to characterize the equilibrium adoption rates of information systems.
The paper proves these results with the main proofs in the article and the sensitivity-analysis lemmas (Lemmas EC.1–EC.4) in its e-companion. None of them has a machine-checked proof. The formalization requires a Lean account of Bayesian Wardrop equilibria, of the equivalence between equilibria and a convex program, and of directional derivatives of the optimal value of a parametric convex program. Parts of this are reusable for any nonatomic routing or congestion game.
The equilibrium strategy profile is not unique and changes discontinuously with . Differentiating equilibrium costs in directly therefore fails. The paper instead works with the optimal value , whose one-sided directional derivative is expressed through Lagrange multipliers. That requires a sensitivity theorem for convex programs whose constraints depend affinely on the parameter, together with uniqueness of multipliers, which fails for populations of size zero. The regime analysis also needs a characterization of the route flows that are induced by feasible strategy profiles. That set is described by the nonlinear-looking constraint , a minimum over types inside a sum over routes. Strict monotonicity of in the side regimes needs the tightness of an information constraint at every equilibrium, not only at one.
The model is a Lean structure BayesRouting.VOI.Game over finite types of populations, type spaces, states, edges and routes. Routes are given by their edge sets, and the directed-graph structure is not used. Type spaces and the route set are nonempty. The prior is a probability distribution, , and costs are positive on nonnegative loads, strictly increasing and differentiable on . One assumption is added: every type profile has positive probability. It makes beliefs well defined and the equilibrium edge load unique, and it excludes perfectly correlated signals.
Conventions: is the last form of eq. (7), which does not divide by . is the maximum of eq. (16) over the reference profile, so that is exactly (14d). and the thresholds are sInf/sSup over sets that are nonempty and compact for size vectors in the simplex, and every statement keeps size vectors there. Statements about "the" equilibrium are stated for every BWE, and existence of a BWE is a separate item, so they are not vacuous. The thresholds are defined from the optimal set of the auxiliary program, not assumed as parameters. Taking them as parameters constrained only by Lemma 4 would give a different theorem.
Disclosed deviations: Lemma 2's clause assumes costs; Lemma 3 is stated for populations of positive size; Lemma 5 assumes ; Proposition 3 is stated with strict monotonicity in the side regimes, as used in the proof of Theorem 3. Contributions of reusable infrastructure are welcome: interval-integral potentials of monotone costs, KKT theory for polyhedral constraints, and directional derivatives of parametric optimal values.
Extremal graph theory asks how many edges a graph on vertices can have without containing a fixed graph . The answer, the Turán number , and the graphs attaining it, the set of extremal graphs, are known precisely only for special ; the Erdős–Stone–Simonovits theorem gives , where is the chromatic number.
Spectral extremal graph theory asks the same question with the number of edges replaced by the spectral radius , the largest eigenvalue of the adjacency matrix. Since , a spectral bound implies an edge bound, and spectral extremal results are usually stronger than their edge versions. Nikiforov (Linear Algebra Appl. 427, 2007) showed that the Turán graph maximises among -free graphs, so for the spectral and the edge extremal graphs coincide. Whether this happens for other is the subject of the paper.
Timeline:
All graphs are finite and simple. For a graph on vertices, is its adjacency matrix and is the largest eigenvalue of . A graph is -free if no subgraph of is isomorphic to . The Turán number is the maximum number of edges over -free graphs on vertices, and is the set of -free -vertex graphs with edges. The Turán graph is the complete -partite graph on vertices with parts of sizes or .
The hypothesis on is: for fixed integers and and all large , and every graph in contains a spanning copy of , i.e. is plus edges. The paper states "adding edges" and fixes the constant at the start of Section 3 (p. 4): "We may assume that the graphs in are obtained from by adding edges." The mission follows that reading. Examples: with , the friendship graphs, and the intersecting cliques .
A graph is spectral extremal for if it is -free and for every -free on the same vertices.
For , and satisfying the hypothesis, there is such that for all every spectral extremal graph for on vertices satisfies
The statement contains no numerical constant, and depends only on , , .
The milestones follow the proof, in order: strict monotonicity of under proper subgraphs of a connected graph (Lemma 2.3); connectivity of (Lemma 3.1); the bound (Lemma 3.2); spectral stability for (Corollary 2.6); for every maximum -cut , and (Lemma 3.3); a counting inequality for intersections (Lemma 2.8); and minimum degree above (Lemma 3.6); at most vertices of each part have a neighbour in that part, and all others see every other part completely (Lemma 3.7); Perron entries for (Lemma 3.8); (Lemma 3.9); balancing two parts of a complete multipartite graph increases (Lemma 2.7); and the maximum partition is balanced, (Lemma 3.10).
The theorem settles the Cioabă–Desai–Tait conjecture: for every whose extremal graphs are Turán graphs plus a bounded number of edges, the spectral extremal problem reduces to the edge extremal problem for large . This recovers the earlier cases (friendship graphs, the graphs , intersecting cliques) at once, and it turns any future determination of of this type into a spectral result with no further work.
The result is proved on paper; it has no machine-checked proof. Mathlib has Turán's theorem (extremalNumber_top, uniqueness of turanGraph) and the definition of extremalNumber, but no spectral extremal graph theory: no Perron–Frobenius theorem for graphs, no spectral Turán theorem, no stability theorem. The formalization would supply these, and the milestone statements are independently reusable: strict monotonicity of (Lemma 2.3), the spectral comparison of complete multipartite graphs (Lemma 2.7) and spectral stability (Corollary 2.6) are standard tools of the area.
The natural first idea, comparing with an extremal graph by Rayleigh quotients, fails at the start: gives only , far from . Closing an additive gap of edges requires control of the Perron vector to within at every vertex and exact control of the part sizes. The second is the delicate step: an imbalance of one vertex between two parts costs in , while the extra edges contribute only beyond the Turán graph, so the two effects must be compared at different scales. Further, the proof needs the deep spectral stability theorem of Nikiforov (Lemma 2.5), whose own proof is long.
Graphs on vertices are SimpleGraph (Fin n), matching Mathlib's extremalNumber n F; is a graph on any finite type. is the largest eigenvalue of G.adjMatrix ℝ (index of Mathlib's decreasingly sorted eigenvalues₀), not an absolute value and not a norm. "-free" is F.Free G (no copy of , not necessarily induced). "Sufficiently large " is ∃ N, ∀ n ≥ N with chosen after and before ; "sufficiently small " is ∃ ε₀ > 0, ∀ ε ∈ (0, ε₀). Partitions are labellings Fin n → Fin r whose parts may be empty; the Section 3 lemmas hold for every partition maximising the number of crossing edges. Lemma 3.8 carries the extra hypothesis , because as printed it is false for (for and the Perron vector of has entries below ); the goal does not assume it.
Trivializing formalizations are ruled out: is not defined from the edge count (which would make spectral and edge extremality the same), the hypothesis on does not contain the conclusion and is satisfiable (a sorry-free check for , was compiled), the conclusion is and not a weaker bound, and the threshold is not chosen after .
A complete development needs the Perron–Frobenius theorem for irreducible nonnegative symmetric matrices, the Rayleigh quotient characterisation of , the spectrum of complete multipartite graphs, Nikiforov's spectral stability lemma, and max-cut partition arguments. All of these are reusable beyond this mission, and proofs of any milestone, of the cited Lemmas 2.1, 2.2 and 2.5, or of Nikiforov's spectral Turán theorem are welcome.
The periodic-review inventory model with a fixed ordering cost is one of the basic models of operations research. When every order incurs a set-up cost in addition to holding and shortage costs, the optimal replenishment rule over an infinite horizon is, under standard convexity assumptions, a stationary policy: whenever the stock falls below the reorder point , order up to the level . Existence of such an optimal policy goes back to Scarf (1960) and Iglehart (1963). Knowing that an optimal policy exists does not say how to find one, and the average cost of an policy is neither convex nor unimodal in .
Veinott and Wagner (Management Science 11 (1965) 525–552) gave an exact algorithm. It proceeds in three steps: (i) compute integers bounding an optimal policy; (ii) find the set of all policies within those bounds that minimize the cost for starting stocks below ; (iii) choose from a policy that is optimal for every starting stock. This mission formalizes the theory behind Step iii. It is the third mission of a series on the paper: mission I treats the renewal closed form of the discounted cost, mission II the bounds of Step i.
Demands are independent non-negative integer random variables with common distribution and finite mean. Following the paper's Eq. (2), the unit purchase cost and the holding and penalty costs are combined into a single function , assumed convex with as ; the set-up cost is and is the discount factor.
A stationary policy, with integers , sets the stock after ordering to
and the stock evolves as from . Its discounted cost is
where for and , and its equivalent average cost is .
A policy is optimal for a set of integers if, for each , it minimizes over all policies; it is optimal if it is optimal for every integer . Under a fixed policy, is accessible from if for some .
Below the reorder point the cost does not depend on the starting stock; its value is written with . The bounds are: the smallest minimizer of ; the smallest integer with (21); the smallest integer with (22); the smallest integer with (23). The candidate set consists of the policies with , that minimize among such policies.
For and : if is optimal and every with
is accessible from under , then is optimal.
Theorem 2 turns the final selection step of the algorithm into a reachability check on the demand distribution: a policy of is certified optimal without comparing average costs at every starting stock. Its corollaries give checkable sufficient conditions; for example (Corollary 2.2) if for , the policy of with the largest reorder point is optimal, which covers Poisson and negative binomial demand. Theorem 1 separately reduces the comparison of two policies to finitely many starting stocks.
The results are proved in the paper (Section 4 and Appendix §3). No machine-checked version is known: the platform has no discrete inventory chain, no discounted cost of a stationary policy on , and no accessibility notion for such a chain. The mission produces these objects together with the paper's selection theory on top of them.
Theorem 1 needs a renewal decomposition at the first passage of the stock below , carried out for expectations over an unbounded integer state space with a discounted infinite sum. Lemma 1 is the delicate step. The paper's argument compares the policy with a hybrid policy that follows until the stock first reaches and then switches to an optimal policy; the inequality "the hybrid cannot be better than the optimal policy" requires that some stationary policy is optimal among all ordering policies, including non-stationary ones. That existence result is cited by the paper (Section 2), not proved there. A proof of Lemma 1 within the class of policies alone does not go through, because the hybrid policy is not an policy.
All objects live in the namespace VeinottWagnerSS.Selection. The model is the structure Model: the demand distribution φ : PMF ℕ with finite mean, K ≥ 0, and G : ℤ → ℝ convex (non-decreasing forward differences) and tending to at both ends. The unit cost , the function and the lead time do not appear (the paper's own reduction, Eq. (2), p. 529). Stock levels are integers. stateLaw is the law of , obtained by iterated PMF.bind; fCost is the expected discounted cost of that chain as a real series, which converges absolutely for because every lies in . aCost is times fCost. Accessible uses the law of with strictly. Optimality is among policies (p. 536); the class of general ordering policies is not formalized.
The bounds are infima of sets of integers; under the standing assumptions and these sets are nonempty and bounded below, so each bound is the least integer the paper describes. is defined as , the cost at the starting stock just below ; that this is the common value for every is milestone 1.
The standing assumptions are kept in every statement, including Theorem 1 and milestone 1, which do not need them; Lemma 1 and Theorem 2 are true only because of them. No printed slip was found in the three results.
Trivializing formalizations are excluded: is the expected cost of the stock process, not a closed formula or a fixed point of a recursion, so milestone 1 is not definitional; the bounds are the least integers of (21)–(23), not arbitrary integers, so is determined by the data; the goal does not assume that is optimal below , and Lemma 1 assumes optimality only at the single starting stock .
Useful contributions beyond the milestones: summability lemmas for fCost, the Markov (one-step) equation for fCost, the first-passage decomposition, and, for Lemma 1, a formalization of general ordering policies with the existence of an optimal stationary policy. The chain and cost definitions are reusable for other results of the paper (Theorem 3, Corollaries 2.1 and 2.2).
The policy is the standard ordering rule for a single stocked item with a fixed charge per order: when the stock position falls below a reorder point , order up to a level ; otherwise order nothing. Scarf (1960) proved that when the expected one-period cost is convex, some policy is optimal in every period of a finite-horizon model with set-up cost. Iglehart (1963) extended this to the infinite horizon. These results establish existence only. They give no procedure for finding the optimal pair.
Veinott and Wagner (1965) gave such a procedure. Its first step is to bound the optimal and by four integers computed from the one-period cost alone. This reduces the search for an optimal policy to a finite box. Their Theorem 4(a) proves that the bounds hold for the first-period parameters of an optimal policy in every -period model. This mission formalizes that theorem and the four comparison lemmas (Lemmas 2–5 of the paper's Appendix §2) from which the paper derives it.
Demands in periods are independent, non-negative integer random variables with common distribution and finite mean. Unfilled demand is backlogged, so stock levels are arbitrary integers. In period , is the stock on hand plus on order before ordering and the level after ordering. Then and .
A policy chooses as any integer function of the information available at the start of period . Given , that information is determined by and . Policies may therefore depend on the whole history; they are not required to be Markov.
Costs are summarized by a set-up cost , a discount factor and a one-period cost . The paper reduces the model with purchase cost , lead time and holding–penalty cost to these data by its Eq. (2), with . The -period cost of a policy from is
where and for . A policy is optimal if it minimizes for every simultaneously. The standing assumptions are that is convex on the integers (non-decreasing forward differences) and as .
The bounds (p. 537) are defined as follows. is the smallest minimizer of . is the smallest integer with (21). is the smallest integer with (22). is the smallest integer with (23).
For every there is an optimal policy for the -period model whose first-period rule satisfies
Optimality is against all history-dependent policies and for every starting level. The existence of an optimal policy is part of the conclusion.
The theorem turns the optimization over policies into a search over a finite box that depends only on , and . The paper's Section 4 procedure for the infinite-horizon problem (Theorem 4(b), Step i) is built on this box, and the bounds also give an interpretation of and : is the single-period optimum, and , , mark where the one-period cost exceeds that optimum by the fractions , and of the set-up cost.
The results are proved in the paper. None of them has a machine-checked proof as far as is known; no discrete-state finite-horizon inventory model with set-up cost is on the platform. A formal proof would provide a reusable finite-horizon dynamic-programming model with history-dependent policies and extended-real expected costs, and a machine-checked version of the existence of optimal policies in the discrete setting, which Theorem 4(a) contains.
The four lemmas compare an optimal policy with an explicit modification of it. The modification in Lemmas 2 and 5 raises the stock in period 1 and then orders , where is the original policy's decision along the original demand path. This comparison policy is history-dependent even when the original policy is not, so the argument cannot be carried out inside the class of Markov or policies. Expectations must be handled over finite demand histories, and costs can be infinite for general policies.
The goal also contains the existence of an optimal policy for the -period model. The paper cites this from Scarf and Zabel rather than proving it. Applying Lemma 3 or 4 yields an optimal policy whose later periods are no longer of form. Restoring the form requires the dynamic-programming principle of optimality together with the -convexity argument.
The Lean model (VeinottWagnerSS.Bounds.Model) uses the reduced model of Eq. (2): G : ℤ → ℝ is a primitive, and , and do not appear. Stock levels are integers and demands are natural numbers; the demand law is a PMF ℕ with finite mean. A policy is Y : (t : ℕ) → ℤ → (Fin t → ℕ) → ℤ: period 's level as a function of and the first demands, so it cannot see current or future demand. Periods are numbered from in Lean. Expectations are sums over demand histories weighted by . is the difference of the expectations of the positive and negative parts, and is valued in EReal. Under the standing assumptions is bounded below, so the negative part is finite and no arises. Both and are allowed.
The bounds SLow, SHigh, sLow, sHigh are infima of the sets in (21)–(23); a milestone proves they are the least elements. A trivializing formalization is ruled out as follows. Optimality is over all admissible policies and for every . The bounds are the least integers of (21)–(23). The goal requires an optimal policy, not only a bounded pair. Existence of an optimal policy is proved, not assumed.
Printed statements corrected. Lemma 4 as printed has no hypothesis on . Its proof begins "By lemma 3 we may assume that ", and without that assumption need not be an rule. The Lean statement adds . The last display of the proof of Lemma 5 reads where is meant; this affects only the proof. The milestone texts are verbatim.
Useful contributions include lemmas on convex functions on (monotonicity on either side of a minimizer), expectation lemmas for sums over Fin t → ℕ, and the finite-horizon principle of optimality for this model.