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.
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?
Set cover is one of the basic covering problems of combinatorial optimization: given a ground set and a family of subsets with costs, choose a cheapest subfamily whose union contains every element. In many applications the elements to be covered are not known in advance but appear over time: requests for a service that must be served by opening facilities, clients that must be assigned to servers, or constraints of a covering program that are revealed one at a time. Each arriving element must be covered at once, and decisions cannot be undone. This is the online set cover problem, introduced by Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; conference version STOC 2003).
The quality of an online algorithm is measured by its competitive ratio: the worst case, over all arrival sequences, of the ratio between the algorithm's cost and the cost of an optimal offline cover of the elements that actually arrived. The paper gives a deterministic algorithm with ratio , where is the number of elements and the number of sets, and shows a nearly matching lower bound for deterministic algorithms. Its algorithm for the weighted case, analysed with a potential function, became a template for the online primal–dual method surveyed by Buchbinder and Naor (Found. Trends Theor. Comput. Sci. 3(2–3), 2009).
This mission formalizes the core of the weighted result: the algorithm that is given a value at least the optimal cost, and its guarantee (Theorem 3.4).
The ground set has elements and the family has sets; every set has a cost . Both are known to the algorithm in advance. For an element , denotes the sets containing . Elements of an unknown subset of arrive one at a time in a sequence ; on arrival each must be covered by a chosen set. The chosen family can only grow. is any family covering every arriving element, and .
The algorithm is given . It discards sets costing more than , buys sets costing at most outright, and rescales costs; on the resulting normalized instance and for every set (p. 365).
The algorithm keeps a weight for every set, initially ; the weight of an element is . With the set of covered elements and the indicator of , the potential is
with natural logarithms throughout. When arrives with nothing happens; otherwise the algorithm performs weight augmentation steps while . In a step, for each : (a) ; (b) if , add to when does not exceed its value before (a); (c) if has increased, return FAIL.
In Lean, the instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance over finite types X (elements) and T (sets), with the published elementWeight, coveredBy and potential. The run is OnlineSetCover.Weighted.Reachable inst α σ, the set of configurations reachable from initState σ under the transition relation Step.
On the normalized instance, with covering , , and , every reachable configuration is a running state (never FAIL) in which (i) every with is covered, and (ii)
The Proved platform theorem OnlinePrimalDual.OnlineSetCover.algorithm_correctness (the last paragraph of the proof of Theorem 3.4, with the invariant assumed) is included as a supporting reference.
Theorem 3.4 is the analysis of the subroutine; with the doubling over guesses of described on pp. 364–365 (which loses a factor of at most 4) it yields the paper's deterministic -competitive algorithm for weighted online set cover. The lower bound of Section 4 shows that no deterministic algorithm can do much better on general instances, so the result is close to the deterministic optimum. The technique, a potential that couples a fractional multiplicative-weights solution to a deterministic rounding, reappears in online covering and packing, online facility location and related problems.
The result is proved in the paper and restated in the Buchbinder–Naor monograph. On Prove2Me, the monograph's final step (from the invariant to the cost bound) is a Proved theorem, and its expectation form of the monotonicity lemma is Disproved because it omits the hypothesis . Neither the full statement about the algorithm's run nor Lemmas 3.1, 3.2 and the corrected Lemma 3.3 are formalized on the platform. This mission produces them, with the terms replaced by explicit expressions.
The cost bound in the last step is short once two facts about the run are available: that stays below , and that the fractional cost stays logarithmic. Neither is a local fact about one state. The first requires showing that, at every per-set step, one of the two deterministic choices (add or not) does not increase ; the paper proves this by a probabilistic argument over an auxiliary randomized choice, and the bound on the exponential term depends on the cost of the set being at most . The platform's earlier statement of this lemma, which omits that hypothesis, is Disproved. The second requires a bound on the number of augmentation steps over the whole run, which depends on the run's history and not on any single state. In Lean both are inductions over an operational semantics with real-valued exponentials and powers , where the initial bound is a genuine size condition on and .
The run is a small-step transition relation. A state records the weights, the cover, the number of augmentation steps begun, the elements not yet given, and the position inside the current step; FAIL is a separate terminal configuration. The order in which a step visits is arbitrary and may differ between steps; every statement holds for every order. "Throughout the algorithm" means every reachable configuration, including those between per-set substeps. Arrival sequences are arbitrary lists (repetitions allowed) of elements covered by .
Conventions: costs, weights and are real; and are the cardinalities of the finite types cast to ; is Real.log; and are real powers. The paper's asymptotic expressions are replaced by what its proofs establish:
The goal is a statement about the configurations the algorithm actually reaches from and the empty cover. Taking the invariant or the fractional-cost bound as a hypothesis on an arbitrary state would trivialize it, and is ruled out: those are exactly what the milestones establish. The doubling wrapper for unknown is not part of this mission.
A complete development needs an invariant for reachable states (positive weights, steps of an element processed in full), the per-set potential inequality, and the step-counting argument. The per-set inequality is reusable for the monograph's version of the algorithm. Contributions of proofs of any milestone, and of auxiliary invariants as separate lemmas, are welcome.
In the online set cover problem of Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009; preliminary version STOC 2003), a ground set and a family of subsets are known in advance, but the elements that actually need covering arrive one at a time, and each must be covered on arrival by sets chosen irrevocably. The paper's motivating example is a network of servers with activation costs: the set of potential clients is known, the clients that actually request service are not, and each request must be served on arrival.
The paper gives a deterministic online algorithm whose cost is within a factor of the offline optimum, where is the number of elements and the number of sets. Its Section 4 shows that this is close to optimal for deterministic algorithms: for all interesting values of and , every deterministic online algorithm has competitive ratio . The lower bound is the reason the product, rather than the of offline approximation (Feige 1998), is the right target online. The online primal–dual framework that grew out of this paper (Buchbinder and Naor 2009) cites it as the benchmark for online covering problems.
This mission formalizes the exact, non-asymptotic statements behind that lower bound: Propositions 4.1 and 4.2 of the paper.
A ground set and a family of distinct subsets of are fixed and known to the algorithm; . An adversary presents elements of one by one, choosing each after seeing the algorithm's previous responses. A deterministic online algorithm , on the arrival of , sees the earlier arrivals and , and adds a finite family of sets to its collection; sets are never removed. It is valid if after every arrival that lies in some member of , that element lies in a chosen set. After an arrival sequence the chosen collection is , and since every set has unit cost, the cost is . The offline optimum is the least number of members of covering the elements of . The competitive ratio of is at least when some arrival sequence has and .
Two families are used.
and the family consists of all ; it has members.
For all positive integers and all with
there is a family of exactly distinct subsets of an -element set such that for every valid deterministic online algorithm there is a nonempty arrival sequence , covered by a single member of , with
The goal leaves the instance existential, as the paper does, and keeps both bounds on and the bound on exactly as printed.
A supporting item (not a milestone) records the count of the block family.
The result. Proposition 4.2 is the exact statement behind the paper's lower bound: choosing of order and of order turns it into the asymptotic bound , which shows that the paper's algorithm is optimal among deterministic algorithms up to a factor. Without it, the gap between the achievable offline and the achieved online would be unexplained. Proposition 4.1 alone gives the matching bound when .
Formalizing it. Both propositions are proved in the paper; neither is formalized anywhere to our knowledge. The mission produces a reusable model of deterministic online algorithms against an adaptive adversary, with a validity notion and a cost, and machine-checked adversary arguments on it. The paper's proof tacitly lets the algorithm add one set per arrival; the statements here cover algorithms that add any number of sets per arrival, so a complete formalization also closes that gap.
The adversary must be adaptive, and the quantifiers are ordered instance, then algorithm, then arrival sequence. The obvious single-block argument (Proposition 4.1) forces only sets. To force sets with , the adversary must move to blocks that no chosen set has touched yet, which requires counting the blocks touched by the sets chosen so far. When an algorithm adds many sets at once, the paper's count "at most blocks after steps" no longer applies as written, and the stopping rule has to be phrased in terms of the cost already paid. The padding of Proposition 4.2 must reach exactly elements and exactly distinct sets without creating sets that help cover the adversary's elements.
The ground set is a Fin type: Fin (2^k) for Proposition 4.1, Fin (k r²) × Fin (2^k) (block, element) for the block family, Fin n for Proposition 4.2. A family is a Finset (Finset X), so its cardinality counts distinct sets. Bit (1-based) of is Nat.testBit j (i-1). An online algorithm is a function from (earlier arrivals in arrival order, current element) to the finite family of sets it adds; it may add any number of sets. Validity demands coverage only for elements that some member of the family contains. Costs are unit (the problem of Section 4 is unweighted).
The offline optimum is never encoded as an infimum: lower bounds exhibit a nonempty arrival sequence and a single covering set (), and the upper bound of Proposition 4.1 quantifies over all offline covers. This rules out the trivializing reading in which the empty arrival sequence satisfies as .
The statements contain no : every quantity is the paper's exact one. The asymptotic bound (8) under the range (7), whose final paragraph only sketches the choice of and , is excluded, as are the remarks on the trivial ratio- and algorithms.
Contributions welcome: proofs of the milestones; lemmas on the chosen collection (monotonicity, decomposition along a sequence); the count of the block family; and the padding construction of Proposition 4.2. The online-algorithm model is reusable for other deterministic online covering lower bounds.
Set cover asks for the fewest sets from a family of subsets of a ground set of elements whose union contains . It is NP-hard, and the best ratio achievable in polynomial time is (Feige 1998, doi:10.1145/285055.285059).
Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; preliminary version STOC 2003) introduced an online version. The instance is known in advance, but an adversary reveals elements one at a time, and each revealed element must be covered at once, by sets that can never be removed later. The set of elements that will actually be revealed is unknown. The paper's motivating example is a network of servers: the potential clients and the servers that can serve each client are known, but which clients will request service is not, and every activated server costs money.
The question is how much an algorithm loses against an offline adversary who knows and covers it with a family . This mission formalizes the paper's answer for unit costs (Section 2): a deterministic algorithm whose cover is within a factor of . Section 3 of the paper extends the algorithm to weighted sets and Section 4 proves a nearly matching lower bound; those are separate missions of this series.
An instance consists of a finite ground set with elements and a finite family of sets. For an element , is the collection of sets containing . Every set has cost , so the cost of a family is its number of members.
The adversary gives a sequence of elements (the given elements form ). A family covers if each element of lies in some member of it.
The algorithm keeps a weight for every set, initially , and a cover , initially empty. The weight of an element is , and is the set of elements covered by members of . The potential is
When the adversary gives an element :
Step (c) prescribes a property of the chosen sets, not the sets themselves. A run on is any sequence of iterations, one per arrival, in which every iteration makes an admissible choice.
For , every arrival sequence , and every family covering : a run of the algorithm on exists, and every run ends with a cover that covers every element of and satisfies
The paper states ; the displayed bound is the constant its proof produces. Because the bound holds for every covering family, it holds in particular for an optimal one.
Lemma 2.1. In every run, the number of iterations with a weight augmentation is at most
Lemma 2.2. In an iteration with a weight augmentation, from a state with positive weights, there is a family with such that
where is the potential before the iteration and the potential after it, computed with the augmented weights and the cover .
The theorem shows that online set cover over a known instance admits a deterministic -competitive algorithm. Section 4 of the paper shows this is nearly optimal: no deterministic algorithm achieves over a wide range of parameters. Its multiplicative weight updates were developed further into the online primal–dual framework for covering problems of Buchbinder and Naor (FnT TCS 3(2–3), 2009), whose Section 5.1 restates this algorithm.
The result is proved in the paper; it is not machine-checked. The Prove2Me platform has the weighted version's final counting step from the Buchbinder–Naor monograph, but no statement of Section 2. A complete development here gives a checked proof of the unweighted competitive ratio with an explicit constant, together with a reusable formal model of an online algorithm with a nondeterministic step, whose correctness includes the existence of an admissible choice at every step.
The central step is Lemma 2.2: a family of at most sets that keeps the potential from increasing must exist at every augmentation. The obvious rules fail. Adding every set of can exceed the cardinality bound, since may contain up to sets. Adding nothing, or a single set, can increase : every uncovered element sharing a set with has its weight raised, and its term grows by a factor up to . The paper's argument is non-constructive, and a formal proof must establish existence for a finite averaging statement over real powers of .
The second difficulty is that the algorithm is nondeterministic. A statement "every run has property P" is empty if no run exists, and the existence of a run is exactly Lemma 2.2 applied at every step under the invariants that weights stay positive and that each arriving element lies in some set. Feasibility (that every given element ends up covered) is not part of the algorithm's rule; it follows from the potential never increasing, which needs and a careful treatment of the initial potential, which is at most and equals when every element lies in every set.
The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (finite types E of elements and T of set indices, incidence elemSets), with the published elementWeight () and coveredBy (). Its positive cost field is not used: all sets have unit cost and the cover is measured by its cardinality. and . Weights are real numbers; is the real power.
The algorithm is the definition OnlineSetCover.Unweighted.Algorithm: a relation Step for one iteration (recording whether a weight augmentation occurred) and Run for a sequence of iterations from the initial state, counting augmentations. Arrival sequences are lists and may repeat elements.
Explicit forms of the paper's asymptotic and unspecified quantities:
The goal adds the hypothesis , which the paper's assumes tacitly: for no set may be added and the element is never covered.
Replacing the algorithm by the set of states whose potential is at most the initial one, or dropping the existence of a run from the goal, gives a weaker theorem; part (a) of the goal rules this out.
A complete development needs elementary real analysis (Real.rpow, Real.log, ), a finite probabilistic or averaging argument for Lemma 2.2, and induction over runs. Contributions are welcome on any milestone; a derandomized averaging lemma for Lemma 2.2 would be reusable in the weighted mission of this series.
The conditional logit model is the workhorse of discrete choice analysis: it is used to forecast travel mode shares, to estimate demand for differentiated products, and, in operations research, as the multinomial logit (MNL) choice model behind assortment optimization and revenue management. Its selection probabilities have the form . Daniel McFadden's 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior gave the model two behavioural foundations, one of which is the subject of this mission: the logit form is a consequence of a single axiom on how choice probabilities change when the set of available alternatives changes.
That axiom is Luce's choice axiom, which McFadden calls Independence of Irrelevant Alternatives (IIA): the relative odds of choosing one alternative over another do not depend on which other alternatives are present. Luce (1959) introduced it; McFadden (1974, §I) showed how, together with positivity and a mild condition on which alternative sets can occur, it yields the conditional logit form with a "utility indicator" shared by all alternative sets.
Timeline. Luce, Individual Choice Behavior (1959): the choice axiom and its ratio-scale representation. McFadden (1974, pp. 109–110): the derivation in the econometric setting with measured attributes , the binary-odds identities (5)–(10), and footnote 3, which removes an extra axiom (Axiom 3) by a universal benchmark alternative. McFadden (1974, pp. 111–112): the companion random-utility characterization by extreme-value shocks, treated in mission 2 of this series.
Let be the universe of objects of choice and the universe of vectors of measured attributes of decision-makers. An alternative set is a finite set ; a designated family of finite sets is the family of possible alternative sets. The selection probability is the probability that an individual drawn at random from the population, with attributes and facing , chooses . For every and possible , is a probability vector on . Whenever belong to a possible set, the pair is possible too, so binary choices are defined.
In Lean these are IsSelectionProb, PairsPossible, Axiom1, Axiom2, binProb, altSetV and IsUniversalBenchmark in the namespace McFadden1974.IIA.
Under Axioms 1 and 2 and a universal benchmark , with , for every , every possible (containing or not) and every :
The function is the same for all alternative sets; this is what distinguishes the goal from Equation (10).
The result. The goal identifies a testable axiom on choice probabilities, IIA, with a parametric functional form, the conditional logit model. It is what licenses the econometric specification estimated in the rest of McFadden's chapter, and it is the reason the MNL model is the default in assortment and pricing problems in operations research. It also makes the model's limitations precise: any population whose choices violate IIA (the auto/red-bus/blue-bus example on p. 113 of the chapter) cannot be logit.
Formalizing it. The result is classical and proved on paper. No machine-checked statement of it exists on the platform, which has the logit form only as a definition (soft-max, MNL revenue) and IIA only in Arrow's social-choice sense, a different axiom about preference aggregation. This mission produces a formal statement of the derivation with every standing assumption explicit, including two the paper leaves implicit: that selection probabilities are normalized on binary sets, and that binary subsets of possible sets are possible.
The algebra is elementary; the difficulty is bookkeeping of where each axiom may be applied. Axioms 1 and 2 are assumed only on possible alternative sets. Equation (10) needs the benchmark to lie in the alternative set, and the naive argument "pick as benchmark" produces a function that depends on the set through the choice of . The goal requires a single for all sets, including sets that do not contain , where neither Equation (10) nor the axioms on alone say anything about . A second subtlety is the diagonal: , so is set to by definition rather than read off a singleton choice.
Alternatives form a type X with decidable equality, alternative sets are Finset X, possible sets are a Set (Finset X), and selection probabilities are a real-valued function P : S → Finset X → X → ℝ. Only values P s B x with x ∈ B and B possible are constrained; no statement depends on the others. binProb sets the diagonal to 1/2. altSetV uses Real.log, which is 0 on non-positive arguments; under Axiom 2 on the binary sets its argument is always positive where it is used.
The probability-vector hypothesis on every possible set, binary sets included, is part of every statement: without it the zero function satisfies Axiom 1 vacuously and Equations (7)–(8) fail. The goal is stated with the explicit , never as "for each there is a ", which would only restate (10).
Nothing beyond Mathlib's finite sums, Real.exp and Real.log is needed. Proofs of the milestones and of the goal are welcome, as is a formal statement of the auto/bus example or of the converse (logit selection probabilities satisfy Axioms 1 and 2).
A set function on a finite ground set is submodular if it has diminishing returns, equivalently if for all . Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular through a value oracle, for a set of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.
Timeline:
Let be a finite ground set and a nonnegative submodular function. Write , and let denote a set attaining it.
Algorithm 1 (DeterministicUSM) fixes an arbitrary order of and maintains two solutions, starting from and . In iteration it computes
If it sets , ; otherwise , . A tie adds . After iterations , which is the output.
The analysis uses the hybrid sets , which agree with and on and with on . In Lean, the run is state f l i, the state after the first entries of the order l, and is optI O (state f l i).
For every nonnegative submodular and every order of ,
The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees of the optimum for every order, without the polynomial-but-large running time and the loss of local search. Its analysis, which charges the decrease of to the increases of and , is the template the paper then refines into the randomized -approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that is the exact ratio of this algorithm, so the improvement to requires randomization (or a different deterministic rule) rather than a sharper analysis.
Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.
The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants and , which follow from the order being an enumeration (no repetitions, every element present), and the identification of from in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing with directly, without the hybrid sets, gives no bound: the greedy choices are made against and , not against . For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.
X with decidable equality; subsets are Finset X; is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every and ") would force monotonicity when and is read as the footnote. is the published NonmonotoneSubmod.Shared.OPT f, the maximum of over all subsets.l with l.Nodup and ∀ x, x ∈ l; is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of is assumed: for an empty ground set the goal reads .O with ∀ S, f S ≤ f O.List.foldl over List.take, on membership in the states of the run, and on telescoping sums over . A reusable lemma "the run keeps and decides exactly " would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It uses the same density estimate as the companion entry, for with (explicit Selberg sieve, weighted first moment, eighth moment of the singular-series factor, Hölder). It then replaces Schnirelmann's sumset inequality by Mann's theorem, for sets containing :
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the entry, and improves only the density estimate:
Only Chebyshev-type prime bounds, the Selberg upper-bound sieve, Hölder's inequality and Schnirelmann's inequality are used.
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the entry, and improves the density estimate:
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Most physical supply chains hold stock at several levels: a factory warehouse feeds a regional depot, which feeds a retail outlet. Each level orders from the one above it, and a shortage upstream delays replenishment downstream. Optimizing such a multi-echelon system by dynamic programming looks hopeless, because the state is a vector of stock levels and stock in transit at every installation, and the value function of a two-installation system with a two-period shipping lag already depends on three continuous variables.
Andrew J. Clark and Herbert Scarf (Management Science 6(4):475–490, 1960) showed that for a serial system this curse of dimensionality disappears. Working with echelon stock (the stock at a level plus everything below it or in transit to a lower level), the optimal system cost separates into the cost of the lowest installation, optimized as if it stood alone, plus a function of echelon stock only. The result is the foundation of multi-echelon inventory theory: the echelon base-stock policies used in practice, the stationary analyses of Federgruen and Zipkin (1984) and Chen and Zheng (1994), and textbook treatments (Zipkin, Foundations of Inventory Management, 2000; Snyder and Shen, Fundamentals of Supply Chain Theory) all descend from it.
Timeline. Arrow, Harris and Marschak (1951) and Arrow, Karlin and Scarf (1958) set up periodic-review inventory models with discounted costs. Karlin and Scarf (1958) treated a single installation with a delivery lag, reducing it to a problem without lag (the paper's facts 1–3). Clark and Scarf (1960) proved the decomposition for serial systems with linear shipping costs and a setup cost permitted only at the top. Federgruen and Zipkin (1984) extended it to infinite horizons and Chen and Zheng (1994) gave a lower-bound proof that reaches more general structures.
Two installations are in series. Customer demand occurs only at installation 1; its demand in each period is non-negative with density on , independent across periods, and excess demand is backlogged. Installation 2 ships to installation 1 with a two-period lead time at unit cost . The system orders units from outside at cost for and (eq. (5)); these arrive at installation 2 one period later. Costs periods ahead are discounted by , .
The state at the start of a period is : is the stock on hand at installation 1, the stock that reaches installation 1 next period, and the echelon-2 stock (on hand at both installations plus in transit), so . Installation 1 pays the expected holding and shortage cost (1),
and echelon 2 pays a natural one-period cost (Assumption 3).
With periods remaining, the optimal system cost satisfies, with ,
where is installation 1's target (stock on hand plus in transit after shipping). Installation 1 in isolation, buying at unit cost with a two-period lag, has optimal cost , :
In Lean these are ClarkScarf.Serial.Model.sysCost and isoCost; the expressions in braces are sysObj and isoObj, indexed by for the problem with periods remaining.
There are functions with such that, for all and ,
and installation 1 acts optimally by aiming at an isolated-optimal target and taking , as much as installation 2 can supply. The goal fixes no form for and needs no critical numbers.
The result. Theorem 1 replaces one three-dimensional dynamic program by two one-dimensional ones. Installation 1 solves its own problem (15), whose solution is a critical-number policy, and echelon 2 solves a single-installation problem in with one-period cost . When is convex the augmented cost is convex (the paper remarks this for Expression (10)), so the echelon-2 policy is of type by Scarf's theorem, and the whole system runs on echelon base-stock rules. Every later serial-system result, finite or infinite horizon, uses this decomposition or its proof idea, and the "induced penalty" is the prototype of the penalty functions used in the multi-echelon literature.
Formalizing it. The theorem is classical and proved, but no machine-checked version exists. The published platform items on Clark–Scarf are a stationary single-period decomposition with normal demand and a disproved infinite-horizon base-stock recursion, neither of which is this finite-horizon dynamic program. A formal development produces the value functions (14)–(15) with real infima and set integrals, the measurability and integrability of value functions defined by infima, the convexity propagation through the recursion (7), and the decomposition itself, which are reusable for any finite-horizon inventory recursion with lead times.
The obvious induction on substitutes (16) into (14) and separates the minimizations over and . The separation is immediate; the hard step is that the constrained minimum over differs from the unconstrained one by an amount that a priori depends on . Showing that it depends on alone is the content of Theorem 1; nothing in the separation step itself rules out a dependence on . On the measure-theoretic side, every value function is defined by an infimum over an uncountable set and then integrated against . Its measurability and integrability are not automatic, and they must be established before any identity between integrals can be manipulated.
Everything lives in ClarkScarf.Serial, one definition file Def_ClarkScarf_Serial_Model and seven theorem files. Conventions committed to:
structure Model whose fields carry the data and the standing hypotheses: ; with ; and two additions the page leaves implicit, disclosed in each statement: a finite demand mean (otherwise (1) is infinite for ) and non-negative, continuous and of at most linear growth (Assumption 3 leaves unspecified; these make every expectation in (14) finite and measurable). No discount bound , no convexity of , no and no sign condition on is assumed.A formalization in which the feasible set of (14) is empty, in which the expectations are junk zeros of non-integrable integrands, or in which may depend on would make (16) trivial; the domain restriction, the integrability conditions and the order rule these out. A sorry-free check (not part of the mission) verifies and and exhibits a model with exponential demand satisfying all hypotheses.
Needed infrastructure: Fubini-type rearrangement of iterated set integrals against a density, integrability of functions of linear growth against a finite-mean density, convexity preserved under infimal projection and under convolution with a density, and measurability of infimum-defined functions. Contributions of these general lemmas, of the base cases , and of any milestone are welcome.
Routing and network optimization often require the length of the best route between every ordered pair of points. Robert W. Floyd's Algorithm 97 gives a compact procedure for this task: it receives a matrix of direct-link lengths and changes the matrix in place until each entry is meant to represent a shortest-path length. The procedure is a small historical source for an algorithm now used as a standard all-pairs shortest-path routine. Its published text consists of the ALGOL code and a short explanatory comment, without a correctness proof.
The same page contains Floyd's Algorithm 96, a Boolean procedure for ancestor relations. Its output records whether a chain of parent links connects two individuals. Floyd cites Warshall's theorem on Boolean matrices in both comments. The Boolean procedure and the length procedure use the same order of three loops; together they expose the distinction between discovering that a route exists and determining its best length. This mission formalizes both claims from Floyd's published page, with the shortest-path statement as its goal.
A directed network has numbered points. Its length matrix assigns a real number to a direct link from to . The value means that the direct link is absent. Links may have negative lengths, and the initial diagonal entries are unrestricted. The paper's matrix index range is ; the Lean development uses in the same order.
A path from to is a sequence with links. The points are distinct, as are . Thus a path between different points has no repeated point, while a path from a point to itself is a simple closed path with at least one link. Its length is ; a missing link gives length . Write for the minimum length among these paths, taking when there is no finite-length path. Since , this is a minimum over a finite family.
The no-negative-cycle condition says that every closed path has nonnegative length. Individual links can still be negative. This condition matters because, in a network with a negative cycle, repeated travel around that cycle can keep reducing a walk's length. Floyd's comment does not state the condition, although the claimed output needs it.
Algorithm 97 scans a pivot , then row , then column , each in increasing order. It enters the column scan when the current is finite; if the current is also finite, it computes and replaces when . Every replacement affects subsequent reads of the same matrix. Algorithm 96 makes the corresponding Boolean update: when and are true, it sets to true.
For Algorithm 96, let be the transitive closure of the initial parent relation , using chains of one or more links. Its comment asserts
For Algorithm 97, the separate unreachable-pair sentence asserts that, whenever no finite-length path runs from to ,
This second target needs no condition on cycle lengths. Both statements are milestones because they are claims printed in the two algorithm comments, rather than lemmas invented for the formalization.
The goal is the whole output claim of Algorithm 97. For every , every matrix with no negative cycle, and all points ,
The equality includes paths with negative individual links, diagonal entries, and unreachable pairs. It fixes the entire final matrix, rather than only an upper or lower bound.
The goal connects an explicit in-place matrix program with a route-based definition of shortest length. Once established, it permits later formal developments to use the procedure as a justified all-pairs distance computation, including networks whose individual links have negative lengths. The Boolean milestone similarly identifies the final state of an ancestor procedure with the transitive closure of the initial relation. Neither assertion requires treating an implementation's output as the definition of the mathematical answer.
Floyd's 1962 paper states these outcomes but supplies no proof. This mission supplies precise Lean statements and definitions for a proof to target. A completed machine-checked development would establish the published procedure's correctness under the missing necessary premise. The statements in this proposal are currently open theorem targets; compiling their declarations checks syntax and types, not their proofs. Supporting work on finite paths, cycle decompositions, and matrix updates can be reused in other finite directed-network arguments.
The array is changed in place. During a pivot's sweep, an entry used in a later update may already differ from its value at the start of that pivot. The test on is evaluated before the column loop, but the same entry is read again within every column iteration. A proof based only on a simultaneous, out-of-place matrix recurrence does not directly describe these reads. Negative individual links also prevent arguments that rely on every update decreasing only through a nonnegative segment. The no-negative-cycle condition must control what happens when a proposed route returns to a point already visited.
Points are Fin n, including the empty network at and the single-point network at . Lengths are WithTop ℝ, where ⊤ represents the paper's ₁₀10 sentinel as mathematical infinity. The paper's literal sentinel is ; a finite bound cannot represent arbitrarily long paths, so this mission uses infinity in its goal. The ALGOL real operations are represented by exact real arithmetic. The printed procedure's loop order, strict comparison, two finiteness guards, and immediate assignments are part of the Lean definition.
The initial diagonal is not normalized. Therefore a path from to itself has at least one link, and the final diagonal denotes a shortest closed-path length when one exists. The Boolean comment's “is true if” is read as an equivalence, supported by its following explanation of the final matrix; chains have one or more links, matching Lean's Relation.TransGen.
The sole added hypothesis in the main goal is absence of negative cycles. It is necessary: with one point and self-link length , the procedure changes that entry to , although the shortest simple closed path has length . No nonnegative-link or zero-diagonal premise is imposed. The unreachable-pair milestone omits the cycle hypothesis because its claim holds without it. The benchmark is a finite minimum of summed link lengths, defined independently of Algorithm 97; defining it from the procedure or its recurrence would empty the goal of its intended content. Contributions proving the printed algorithms' statements, or establishing reusable finite-path and update results needed for them, fit this scope.
The dynamic lot size model asks when, and how much, to order of a single item over a planning horizon of periods with known, time-varying demands, setup costs, unit order costs and holding costs. It is the textbook model of production planning and the building block of material requirements planning, multi-item scheduling and many decomposition schemes for larger supply-chain problems.
Wagner and Whitin (1958) showed that some optimal policy orders only when inventory is zero, which turns the problem into a shortest-path recursion with running time. For more than thirty years this was the standard algorithm. In 1991 three groups independently reduced the complexity: Federgruen and Tzur (Management Science 37(8), 1991), Wagelmans, van Hoesel and Kolen (Operations Research 40, 1992) and Aggarwal and Park (Operations Research 41, 1993). Each obtained in general and under special cost structures. The Federgruen–Tzur algorithm is a forward algorithm: at iteration it keeps a short list of periods that could still be the best last setup period for some future horizon, and updates it by local tests on neighbouring entries. This mission formalizes the theorem that justifies those tests.
For periods let be the demand, the setup cost, the variable per unit order cost and the cost of carrying a unit of inventory at the end of period . Write and , so . For let , let , and let
be the carrying cost of an order placed in period that covers the demands of periods .
The costs are given by the zero-inventory recursion (2): and, for ,
is the cost of the first periods when the last setup is in period .
For two periods the difference is affine in , with intercept given by (4) and slope . Its root is defined by (5): when the slopes differ, and or according to the sign of when they agree. It is extended symmetrically, .
At iteration the future demands are unknown, so a future horizon has a potential cumulative demand . The th Minimal Optimal Predecessors list is the set of periods that are the lowest-index optimal last setup period, among , for every potential cumulative demand in some open interval above .
Let and let with , ranked so that , with equal -values in ascending order of index. Put and for . Then
In attack order:
A supporting item potCost_spec certifies that the potential costs used to define agree with the paper's , up to a term that does not depend on .
Theorem 1 is what makes the forward algorithm correct. Part (a) reduces the minimality of a candidate list to a condition on consecutive pairs of a sorted list. Part (c) says which entry to delete when the condition fails. Part (b) says where to read off the optimal last setup period. With these, is maintained by deletions at the ends and in the interior of a list ordered by , and each period is inserted and deleted at most once; the bound, and the bound under the paper's special cost structures, follow from this bookkeeping. The same lower-envelope reasoning appears in the other 1991–1993 algorithms and in later extensions to backlogging and capacitated variants.
The result has a complete published proof. To our knowledge there is no machine-checked development of the Wagner–Whitin recursion or of any of the fast lot-sizing algorithms. This mission produces the model, the breakpoints and the Minimal Optimal Predecessors lists as reusable definitions, and a checked proof of the characterization. It also records two small corrections that a formal reading forces on the printed text (see Formalization scope).
Each piece in isolation is elementary algebra on affine functions. The difficulty is in the combinatorics of the lower envelope with ties. The natural argument "consecutive breakpoints increase, so each line owns an interval" must handle three things:
The "only if" direction needs every failure of (6) to be traced to an element that is never the unique lowest-index optimum on an interval. Ties are exactly where the printed definition of , read literally at a single demand value, breaks the theorem. A proof that ignores ties proves a statement that is false.
EReal, so are kept distinct from every real number. The final "" of (6) is part of the condition.List ℕ. Lean lists are 0-based, so the paper's and are entry and gval j L m.(r, Q) policies are the standard replenishment rule for a single item under continuous review: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point , an order of size is placed. They are known to be optimal in the classical models with Poisson or compound renewal demand, constant or exogenous lead times and full backlogging, and they are used widely in practice and in multi-item and multi-echelon systems where they are applied item by item.
For decades, computing an optimal pair exactly was not routine. The textbook treatment of Hadley and Whitin (1963) gives approximations; as Browne and Zipkin (1991) put it, "until recently, there was no reliable, straightforward method for computing an optimal (r, Q) policy, even in the simple case of Poisson demand processes." Many heuristics were proposed (surveyed by Lee and Nahmias, 1989); the only exact procedure in circulation was in Zipkin's classnotes, based on a result of Sahin (1982).
Federgruen and Zheng (1992) give a short exact algorithm, Algorithm OPT, whose work is linear in the optimal order quantity . It rests only on the form of the cost, not on a particular demand model.
Inventory positions are integers (demand arrives unit by unit). A fixed cost is charged per order, and is the expected holding and backlogging cost rate as a function of the inventory position . In all the models of the paper the long-run average cost of the policy, for an integer and an integer , has the form
The paper's standing assumptions on are:
The sequence . Let be an integer minimizing . Given , let and , and set
So the window grows by one point at a time towards the smaller neighbouring value, ties going left. Write for an optimal reorder point for a given , and
Algorithm OPT, Step 1. Variables start at , , , , . Each pass compares and ; on the smaller side (left on ties) it stops if is at most that value, and otherwise adds the value to and moves one step left or one step right; then and . The output is the final .
Under the standing assumptions, Step 1 of Algorithm OPT, started from any global minimizer of , stops after finitely many passes, and its output satisfies and
The goal fixes no constants and no demand model: it is a statement about every satisfying the standing assumptions.
The result turns the joint minimization of (1) over , an unbounded two-dimensional integer problem, into a single scan whose length is plus the distance to the minimizer of . Because it uses only the form (1) and the unimodality of , it applies at once to Poisson and compound Poisson demand, to stochastic lead times with an equilibrium lead-time demand, and to cost structures with stockout penalties; the paper also notes extensions to policies. Lemma 1 and Corollary 1 additionally give the structure of the optimal reorder point as a function of .
The result has been proved on paper since 1992. What this mission adds is a machine-checked proof of the algorithm's correctness for general under exactly the paper's hypotheses. The platform already has the linear-cost special case of the underlying lemmas for one discrete demand model (InventoryControl.rq_discrete_recursion, rq_discrete_joint_optimal), but with and given as hypotheses and no algorithm; nothing on the platform states the algorithm or treats general unimodal .
The obvious argument says: for fixed the sum in (1) should cover the smallest values of , and the greedy window collects exactly those. Both halves need care on the integers with flat stretches of : "the smallest values" is ambiguous under ties, and the claim that a greedy window holds them relies on being a global minimizer together with the unimodality of , not on convexity.
The stopping rule is the second point. Lemma 2 looks like a first-order condition, but need not be convex; optimality of the first stopping for all larger uses that the values are nondecreasing along the sequence, which the paper uses without stating. Termination of the algorithm is not discussed on the page; it needs , and fails for constant .
Finally, the goal is about an imperative loop. Connecting its five variables to , and is an invariant argument that has to match the tie-breaking and the non-strict stopping tests exactly.
NegUnimodal G: , antitone on and monotone on . "" is Coercive G: along atBot and atTop. Mathlib's QuasiconvexOn ℤ is not used: over -weights it holds for every function.Proofs of any milestone are welcome, as are general lemmas on windows of unimodal integer sequences, which are reusable beyond this mission.
Many controlled systems are judged by a ratio of two long-run quantities rather than by a single one: cost per unit of output, cost per unit of time when the time spent in a state depends on the decision, cost per customer served, or expected cost per cycle of a renewal process. In a finite Markov decision model each of these is a quotient of two average costs per unit time. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (DOI 10.1287/mnsc.9.1.16) introduced this ratio-of-costs criterion in its §4, prompted by the fractional linear program that its §3 uses to solve the total-cost problem as a linear program, and pointed to Klein's work on maintenance policies as an example of the problem.
The paper's §4 first observes that, restricted to stationary randomized procedures, the ratio criterion is a ratio of two linear functions of the stationary state-decision frequencies, so it can be minimized by the fractional linear programming lemma of §3. The question it then raises is the one this mission formalizes: is the procedure optimal over stationary procedures also optimal over all procedures, including history-dependent and randomized ones? Derman's Theorem 3 answers yes under an irreducibility assumption, by reducing the ratio problem to a family of ordinary average-cost problems with costs of either sign.
Timeline, as far as it bears on this mission:
A system is observed at times in one of finitely many states . After each observation one of the decisions is made, all of them available in every state. If the system is in state and decision is made, the next state is with probability , where .
A procedure chooses the decision at time at random, with probabilities that may depend on the whole past; the class of all procedures is . The class consists of the stationary randomized procedures, for which the probability of in state is a fixed number , whatever the past and the time. The class consists of the deterministic stationary procedures, those of with every ; it is finite. A procedure of turns the states into a Markov chain with transition probabilities .
Let and be two sets of costs incurred when decision is made in state . For a fixed procedure started at , let and be the expected costs at time . The ratio criterion is
For a single cost set with expected costs , the average cost per unit time is .
Assumption A says that for every procedure of all states belong to the same class of the induced Markov chain.
Under Assumption A, for every initial state there is a deterministic stationary procedure with
that is, for every procedure .
Theorem 3 justifies solving ratio problems over stationary procedures only. Combined with the display of milestone 4 it shows that the fractional linear program over stationary state-decision frequencies yields a procedure optimal against every procedure, including those that remember the past or randomize. The same reduction, minimizing and adjusting , underlies later parametric methods for fractional Markov decision problems and the analysis of semi-Markov decision processes, where the denominator is the expected sojourn time.
All four steps and the theorem are classical and proved on paper. None of them is formalized on Prove2Me: the platform has average-cost optimality statements with nonnegative costs (Sennott's Proposition 6.2.3) and Jewell's gain-rate results restricted to stationary policies, but no statement of a ratio criterion over history-dependent procedures. This mission produces the statement of Theorem 3, the signed-cost version of Theorem 1 that it uses, and the two translation steps between the ratio criterion and the average-cost criterion.
The obvious argument restricts to stationary procedures, where all Cesàro limits exist and the ratio criterion is a ratio of two linear functionals of a stationary distribution. It says nothing about a history-dependent procedure, whose averages and need not converge, and for which the limit superior of the ratio is not the ratio of the limits superior. The translation from the ratio to an average cost therefore works in one direction for every procedure (milestone 2) and in the other direction only for stationary ones (milestone 3). The other ingredient, optimality of a deterministic stationary procedure for the average-cost criterion against all procedures with costs of either sign (milestone 1), is the substance of Derman's Theorem 1 and requires a vanishing-discount or equivalent argument over history-dependent procedures.
The dynamics and the procedures come from the published definitions SennottDP_AvgFinite_Model: the system is an MDC S Act with [Fintype S] [Fintype Act] and the hypothesis ∀ s, M.A s = Finset.univ (all decisions available); the class is Policy M, history-dependent and randomized; is StationaryPolicy M through .toPolicy; the law of the history is histProb. The cost field M.C of that structure plays no role: the costs , and the signed cost of milestone 1 are explicit real arguments S → Act → ℝ.
The local definitions are: the expected cost at time for a real cost, as a finite sum over histories of length ; with Derman's normalization ( terms divided by ); as the limit superior of the ratio of partial sums; the induced matrix ; Assumption A as Matrix.IsIrreducible of for every row-stochastic ; and membership of a procedure in with probabilities . All limits superior are real, of bounded sequences; positivity of and is a hypothesis of every statement involving , which keeps the denominators positive.
The goal quantifies "for every initial state there is ", following the proof. The competitors in the goal and in milestone 1 range over all of Policy M; a version comparing only with stationary procedures is a different and easier theorem and does not close this mission. Assumption A is kept in the goal although the proof does not visibly use it, because the theorem states it.
Contributions welcome: proofs of the milestones, in particular the signed-cost Theorem 1 (which may reduce to Sennott's Proposition 6.2.3 by shifting costs by a constant), Cesàro limits for stationary procedures on finite chains (reusable for milestones 3 and 4), and the final compactness argument over the finite class .
Learning from a finite sample is useful only if changing the sample has a controlled effect on the learned predictor. Uniform stability asks for a bound on the change in loss at every test point when one training example is removed. Bousquet and Elisseeff use this property to obtain generalization bounds for learning algorithms, and identify regularization as a source of stability in methods built from reproducing kernels. The present mission isolates their result for a squared norm penalty in a reproducing kernel Hilbert space (RKHS). It concerns the sensitivity of the optimizer itself, before any probability bound on a random training sample is applied. The result is Theorem 22 of Bousquet and Elisseeff (2002).
Let be an input space, a label space, and a real reproducing kernel Hilbert space of real-valued predictors on . A kernel and a feature representative express the reproducing identity and . Thus . The source assumes that all diagonal kernel values satisfy .
A labeled example is . Its loss under is , where is a real-valued cost. Let be the set of predictions that some element of can produce at some input. The loss is -admissible when is convex for every label and for all and . Here is a nonnegative Lipschitz constant. The definition compares any two attainable predictions, even when they arise at different inputs.
Fix a sample , a deleted index , and a regularization weight . The paper's full and truncated objectives, with squared RKHS norm regularization, are
The factor in both objectives is . Let and be minimizers of these respective objectives over all of . The statements allow any minimizer satisfying the relevant global optimality condition; they do not choose one by an arbitrary fallback rule.
The central target is the explicit deletion stability estimate of Theorem 22. For every test point ,
Its four milestones follow the paper's route through Lemma 20, the point-evaluation inequality (25), and the two quantitative inequalities displayed in the proof of Theorem 22. In particular, the intermediate RKHS distance bound is when . The main theorem uses , so it does not need a choice of sign for . These numerical constants are part of the target, rather than placeholders for unspecified bounds.
The theorem supplies a deterministic, uniform sensitivity estimate for kernel methods trained by squared norm regularization. The bound applies simultaneously to every test example and decreases as either the sample size or the regularization weight increases. It is one of the ingredients that lets the paper apply its earlier stability-to-generalization results to concrete learning procedures. The loss need not be bounded for this theorem; bounding it is a separate question addressed later in the paper.
The result is proved in the source article. This mission asks for a machine-checked version of its exact pairwise claim and the reusable infrastructure around it: the paper's admissibility condition, the two objectives, the general regularizer inequality, and the RKHS evaluation bound. The existing Prove2Me library already has definitions for loss, empirical error, and the RKHS reproducing identity, so the new definitions concentrate on what is specific to these pages. The related replace-one estimate in Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning uses a different perturbation and constant; it is not interchangeable with this result.
The two minimizers solve different objectives, and the deleted example appears in only one of them. A comparison of their objective values alone does not directly give a bound on their distance in the Hilbert norm. The source also distinguishes an abstract convex class of functions in Lemma 20 from the full RKHS used in Theorem 22. A proof must keep those domains straight while preserving the precise normalization of the truncated objective. Another delicate point is that the kernel bound controls evaluations through the reproducing identity; a bound on is not by itself a bound on loss unless the admissibility condition is also used.
The Lean model uses an abstract complete real inner product space , an evaluation map , a feature map , and the published IsRKHSOf predicate tying these to . The completeness instance matches the source's Hilbert-space assumption. Samples have type Fin m → X × Y, so an index i : Fin m already forces . Minimization ranges over the entire for Theorem 22 and over the declared convex class for Lemma 20. The objective definitions use the published Loss and EmpiricalError objects. No probability measure or measurability assumption is needed for these deterministic assertions.
There is a printed mismatch that affects what “deletion” means. Theorem 22 names an algorithm defined by equation (26), which, run afresh on points, would normalize its data term by . Lemma 20 and the proof of Theorem 22 instead compare the full objective with equation (20), whose data term uses . The formalized goal states that comparison, with its explicit constant, and records the discrepancy for audit. This excludes the tempting shortcut of treating the two normalizations as identical. The regularizer is the genuine squared norm and the second minimizer is required to minimize the genuine truncated objective; neither a restricted hypothesis ball nor an artificially assumed distance bound enters the goal. Contributions that establish minimizer existence or connect the pairwise bound to an algorithmic selection would extend this core without changing its statement.
An airline sells the seats of one flight leg in several fare classes at different prices. Low-fare passengers usually book first, so the airline must decide how many seats to keep back, or protect, for later high-fare passengers. Peter Belobaba's 1987 MIT dissertation introduced the expected marginal seat revenue (EMSR) rule for this decision, and EMSR-type rules became a standard of airline revenue management practice (Talluri and van Ryzin 2004). A protection level is computed from a demand forecast, and forecasts are uncertain. Section 6.2 of the dissertation asks how the protection level moves when its inputs move: the mean of forecast demand, its standard deviation, and the ratio of the two fares. That question decides where forecasting effort pays off, and this mission formalizes the answers the dissertation gives for Gaussian demand.
This is the third mission in a series on the dissertation. The first treats marginal allocation among distinct fare classes, and the second the two-class nested protection level in the discrete model, including its revenue optimality. This mission takes the continuous Gaussian model of Chapter 6 on its own terms.
Let be the number of requests for a fare class, a real random variable with law . For a seat level the tail probability is
and for the fare of the class the expected marginal seat revenue is (Eqs. (6.1)–(6.2)).
There are two classes: class 1 with fare and class 2 with fare , where . Requests for class 1 are Gaussian with estimated mean and estimated standard deviation , written . A real number is an EMSR protection level for class 1 against class 2 when
The standardized level is the value "which has a probability of of being exceeded" by a standard normal variable:
In the Lean development these are tailProb, emsr, gaussianLaw rbar σ, stdNormal, IsProtectionLevel rbar σ f₁ f₂ S and IsStdNormalLevel f₁ f₂ Z, all in the namespace SeatInventory.Gaussian.
For and :
The goal states no numerical constant and no particular fare ratio; it fixes only the shape of the dependence.
The dissertation's constant-coefficient-of-variation form, Eq. (6.13), with , follows from (6.12) by substitution and is not stated separately.
The result gives every Gaussian protection level as a closed form in one standard normal quantile. From it come the three sensitivities that Sect. 6.2 uses to argue for better forecasts. The protection level moves one-for-one with mean demand. The standard deviation moves it in a direction fixed only by whether the discount fare is above or below half the full fare. A higher fare ratio always lowers it. The dissertation uses these facts, and its Figures 6.1 and 6.2, to argue that reducing the estimated standard deviation of demand narrows the range of protection levels a forecast can produce. The same quantile structure is behind Littlewood's rule and the newsvendor critical fractile, so the statements here are the Gaussian specialization of a pattern that recurs throughout revenue management and inventory theory.
All the statements are classical and easy to believe. None of them, to our knowledge, has a machine-checked proof. Mathlib provides the Gaussian law and its affine images, but no standard normal quantile and no statement that a Gaussian tail is a strictly decreasing bijection onto . Formalizing this mission produces both, in a form that can be used again wherever a normal critical fractile appears.
Most of the work is in the existence and uniqueness of the two tail solutions. The tail must be shown continuous, strictly decreasing, and to take every value in . Strictness needs the Gaussian density to be positive everywhere, and existence needs a limit argument at both ends. Monotonicity alone, which holds for every law (Eqs. (6.1)–(6.2)), gives neither, because a general law can have flat stretches and jumps in its tail. The relation then requires transporting the tail of to that of through the affine map , and the sign of requires the symmetry of , namely . Once uniqueness is available, each sensitivity statement follows from these facts. The tempting shortcut of reading as a definition is ruled out below.
gaussianReal rbar (σ^2), parameterised by the variance. Every theorem assumes ; at the law is a Dirac mass and (6.10) has no solution.Useful infrastructure, all reusable: the strict monotonicity, continuity and range of Gaussian tails; the standard normal quantile; and tail transport under affine maps. Contributions of these as separate lemmas are welcome.
Earliness/tardiness (E/T) scheduling penalizes a job both for finishing late and for finishing early. It models just-in-time production, where an early job ties up inventory and a late one delays a customer. Baker and Scudder's review (Oper. Res. 38 (1990) 22–36) organized the single-machine E/T literature around a short list of structural properties of optimal schedules for a common due date shared by all jobs. For the problem without tolerances these properties go back to work the review surveys, beginning with Kanet (1981) for equal penalties.
The review then turns to due-date tolerances: a job pays nothing if it completes within a window around the due date, as in contracts that accept delivery within a few days of a target. Cheng (1988) studied a version in which the penalty is discontinuous at the window ends. Baker and Scudder state the continuous version and prove two generalized properties, III(G) and IV(G), in the paper's Appendix (pp. 34–35). They are the paper's own results; the rest of the review cites results proved elsewhere.
Fix jobs, processed on one machine in a fixed order, one after another, starting at time with no idle time between them. The job in position has a processing time , so it completes at . All jobs share a common due date , which is a decision variable. Job has tolerances and is free of penalty when . Outside its window it pays a unit earliness penalty or a unit tardiness penalty :
The tolerances are small compared with the processing times: for distinct jobs . Under this condition at most one job can avoid penalty costs. A due date is optimal if it minimizes over , and the least optimal due date is the smallest optimal one. The paper minimizes as a secondary criterion when there are alternative optima.
In Lean the model is BakerScudder1990.Tolerance.Instance n, with fields p u v α β : Fin n → ℝ, completion times I.C, earliness I.earliness d, tardiness I.tardiness d, total penalty I.cost d, and the predicates I.IsOptimalDueDate and I.IsLeastOptimalDueDate.
Let be the least optimal due date and let be the number of jobs with . Then a least optimal due date exists, and exactly one of the following holds:
The case labels follow the paper's proof. The printed statement swaps them (see Formalization scope).
III(G) reduces the choice of an optimal common due date for a given sequence to candidates. IV(G) goes further and names the candidate directly from prefix and suffix sums of the penalties. Baker and Scudder use this to say which V-shaped sequences remain candidates for optimality, so that an enumeration over sequences can discard the others. With the two properties reduce to the classical common-due-date conditions: some job completes exactly at , and which one is fixed by a weighted-median condition.
The results are proved in the paper, so the formalization does not settle an open question. It produces a machine-checked version of the Appendix, with two printed errors corrected, and a reusable model of single-machine E/T costs with tolerance windows. No earliness/tardiness model or result was formalized on Prove2Me as of October 2026.
Each linear piece of is elementary. The work lies in showing that the pieces are the claimed ones: the tolerance condition must imply that a job before position is early, and a job after it tardy, throughout each gap and window. That needs the ordering for every , not only for consecutive jobs. The second point is the least optimal due date. Optimality alone does not determine on a flat stretch of , where every point is optimal and only the left end satisfies the strict inequalities. Existence of a least minimizer also has to be shown, from the two outer slopes and finitely many breakpoints. Finally, the count of jobs without tardiness must be matched to the position of the critical job at both kinds of breakpoint.
Fin n, so the paper's job is position and the goal states the count of untardy jobs as . Data are real numbers. is max 0 x.max 0 terms with a sign determined on each piece), a general lemma that a convex piecewise-linear coercive function on attains its least minimizer at a breakpoint, and the special cases as corollaries.In the classical secretary problem a decision maker sees candidates in a uniformly random order and must accept or reject each one on arrival, irrevocably, aiming to accept a valuable one. Its online, random-order structure models hiring, selling an item to sequentially arriving buyers, and posting prices in online markets. Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study the discounted secretary problem, where the reward of a selection depends on when it is made: a candidate accepted late is worth less (or more) by a time-dependent factor, as with a seller whose revenue decays with time, or a firm that loses value the longer a position stays empty.
Timeline of the setting:
There are elements, indexed by . Element has a value , and each time has a discount . The elements arrive in a uniformly random order , a bijection from times to elements: element arrives at time . Selecting the element that arrives at time earns , and an algorithm selects at most one element.
The offline optimum on the order is . It is a random variable, and the benchmark is its expectation
For a real parameter , algorithm selects the first time at which and earns that product; if no time qualifies, it selects nothing and earns . It knows and , sees the values one at a time, and never sees the future of . Its expected value is .
The proof uses three derived objects:
For every , all discounts , all values and every real ,
Taking gives , a -competitive algorithm when the expected optimum is known.
The result. The discounted problem separates sharply by information: a logarithmic gap is unavoidable without prior knowledge, while knowledge of the single number , or of any lower estimate of it, closes the gap to a constant. The algorithm is a fixed posted threshold, so read as a mechanism it is a posted price, which is truthful for single-parameter agents (§1). The paper also notes that when all values are known, can be estimated by sampling (its Lemma A.1), which yields a constant-competitive algorithm in that setting. The companion lower bound (Theorem 4.6) shows that even complete knowledge of the values does not give a ratio better than .
Formalizing it. The result is proved on paper; no machine-checked proof is known. The formalization yields a checked version of the paper's counting argument on permutations (Claim 4.8) and of the tie-breaking step behind Eq. (4.3), and reusable finite random-order bookkeeping: expectations over as averages, threshold stopping rules, and the decomposition of an online algorithm's value by the time and element it selects.
The obvious argument fails when rarely selects. earns at least whenever it selects anything, so . That settles the case and nothing else: the probability of selecting can be tiny while is still large, because the optimum may be concentrated on a few orders with a large product. In that case the bound must come from comparing the algorithm with the optimum pair by pair: every time–element pair with must be realized by on a positive fraction of the orders.
Two points need care in a formal proof:
Neither (4.2) nor the map appears in the statements, so solvers may replace either with any argument they like.
Fin n; the paper's time is the index . An order is π : Equiv.Perm (Fin n), read as time ↦ element, as on p. 3. The instance [NeZero n] encodes , so the maximum over times is a genuine maximum (Finset.sup').Equiv.Perm (Fin n) and on first-hitting times are reusable beyond this mission.In the classical secretary problem a decision maker sees candidates in uniformly random order, learns each candidate's value on arrival, and must accept or reject it on the spot; the goal is to pick a valuable one. A simple sample-then-select rule picks the best candidate with probability at least , so the problem is constant-competitive. The secretary problem is also a model of online mechanism design: a rule that accepts the first agent above a threshold computed from earlier agents is a truthful posted-price mechanism (as the paper notes in §1).
Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009; authors' version) study the discounted secretary problem, where accepting at time is worth for a known discount function . Discounts model settings where a sale is worth more at some times than at others. The case had been studied before (Rasmussen and Pliska 1976); the paper asks what happens for arbitrary . Its answer has two sides: an -competitive algorithm, and the result of this mission, a lower bound showing that no online algorithm is better than -competitive. So, unlike the classical problem, the discounted problem with a general discount is not constant-competitive.
There are elements with values , and a discount function on the times. The elements arrive in a uniformly random order : element arrives at time . A randomized online stopping rule specifies, for each time and each sequence of values seen so far , a probability of stopping at if it has not stopped yet. Stopping at selects and earns ; the rule selects at most one element and may select none. The rule knows and , but it sees only values, only as they arrive, and it is not told which instance it is facing.
The expected value of is
and the benchmark is the expected offline optimum
which is itself a random variable averaged over the order. is -competitive on an instance when .
The hard family (§4.1.1 of the paper): fix an integer and put , , for , and . The step discount is on the times and on . The instance has elements of value and the rest ; is obtained from by raising of its values to , so has elements of value .
For every integer and every randomized online stopping rule for horizon and the step discount,
That is, no online rule is -competitive on all of .
The result separates the discounted secretary problem from its classical and weighted relatives, which admit constant-competitive algorithms (the paper's Theorem 3.4 and the -competitive classical rule). Together with the paper's upper bound (Theorem 4.4) it pins the competitive ratio for general discounts between and up to constants, and it motivates the paper's known- model (§4.2), where an estimate of restores a constant ratio. The construction is a template for lower bounds against randomized online algorithms in random-order models: geometrically nested instances that a rule cannot tell apart early, played against a discount that punishes waiting.
The theorem is proved in the paper, in about a page. To our knowledge no part of it has a machine-checked proof. This mission produces the formal model of randomized online stopping rules in the random-order discounted setting, a reusable object for the paper's other discounted results (the upper bound, and the lower bound with known values of Theorem 4.6), and a checked version of the lower bound with explicit constants.
The obvious attempt is to fix one instance and show that every rule loses on it. That fails: for any single instance there is a rule tuned to it (a rule that waits exactly as long as that instance warrants). The lower bound has to play the instances against each other. A rule that does well on must commit early, within the first steps, yet the rule cannot distinguish from during those steps except with probability . Making "cannot distinguish" precise is the central step: it needs a coupling of the two runs over the same random order and the same internal randomness, which works only because the rule's decision at time depends on the values observed so far and nothing else. The accounting then has to show that the rule's early earnings on and its late earnings are both small compared with , which uses and that dwarfs .
Fin n, 0-based: index is the paper's time , so the paper's block is the index range . The random order is π : Equiv.Perm (Fin n) read as time element, and every expectation over it is the finite average . Values and discounts are real.StoppingRule n: stopping probabilities indexed by time and the arrival-ordered value sequence, with the non-anticipation condition that depends only on . The theorem quantifies over all such rules, so it covers deterministic and randomized online algorithms that observe values only. A rule may depend on and but not on the instance index.Fin n), and competitiveness is multiplicative, , never a quotient.Fin n (the probability that a set of elements misses the first positions), the coupling of two value sequences that agree on a prefix, and elementary estimates on geometric sums. The rule model and the permutation-counting lemmas are reusable for the paper's other discounted results. Contributions of these supporting lemmas, as well as proofs of the milestones, are welcome.A correlated equilibrium is the equilibrium notion that arises when the players of a game take their actions on the advice of a common randomizing device, each player seeing only his own recommendation. It was introduced by Aumann in 1974 (Aumann 1974). Aumann's 1987 paper (Aumann 1987) gives the simple, finite form of the definition used today (Definition 2.1) and shows that the notion is what Bayesian rationality with a common prior predicts. On the way it records, as Proposition 2.3, the fact that makes correlated equilibrium tractable in practice: for a finite two-person game, the distributions over action pairs that come from correlated equilibria are exactly the solutions of an explicit finite system of linear inequalities.
That characterization is the starting point of the computational theory of correlated equilibria. Because the set is a polyhedron, an optimal correlated equilibrium can be found by linear programming, and no-swap-regret learning dynamics converge to this set (Foster and Vohra 1997; Hart and Mas-Colell 2000). In each of these works the linear-inequality description is taken as the definition; the paper's Proposition 2.3 is the bridge back to the strategic definition.
Player 1 has a finite set of actions and player 2 a finite set . For and , and are the two players' payoffs at the action pair .
A correlated strategy pair is a pair of functions , on a finite probability space : a finite set with nonnegative weights summing to . Chance draws and suggests the action to player . The pair is a correlated equilibrium (Definition 2.1, condition (2.2)) if no player gains by a deviation that depends only on his own suggestion: for every ,
and the analogous inequality holds for player 2 and every .
A distribution is a family with and . The distribution of a correlated strategy pair assigns to the probability . A correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium on some finite probability space.
In the Lean development these are IsDistribution p, IsProbVec μ, IsCE h₁ h₂ μ f₁ f₂, distr μ f₁ f₂ and IsCED h₁ h₂ p, with h₁ j k and p j k .
For every distribution : is a correlated equilibrium distribution if and only if
A further statement, not a milestone, records the paper's example on p. 5: in the game of chicken (Figure 4) the distribution of Figure 5 is a c.e.d. with expected payoff .
The result. Proposition 2.3 turns an existential statement — there is some probability space and some correlated strategy pair that is an equilibrium and has distribution — into finitely many linear inequalities on alone. Consequently the set of c.e.d.'s is a compact convex polyhedron, membership is decidable by evaluating linear forms, and optimizing a linear objective over it is a linear program. The paper states the two-person case and remarks that "the principle, however, is no different in the general case".
Formalizing it. The proposition is classical and its proof is short; to our knowledge it has no machine-checked proof. The platform already has the linear-inequality (swap) form of correlated equilibrium for two-player games on Fin m × Fin n (Foster–Vohra 1997 missions) and Aumann's 1974 randomizing-structure model, but no statement that connects the strategic definition over arbitrary finite probability spaces with the linear system. This mission supplies that connection, so that results proved about the polyhedron apply to equilibria in Aumann's sense and conversely.
The mathematics is elementary; the care is in the statement. Two points need attention. First, the direction from the inequalities to a c.e.d. requires constructing a probability space and a correlated strategy pair whose distribution is the given ; the c.e.d. notion quantifies over probability spaces, not over distributions. Second, the paper's argument divides by the probability of a suggestion, which may be zero; the conditional formulation (milestone 2) holds only over possible suggestions, while (2.4) and (2.5) quantify over all actions and hold trivially at impossible ones. Deviations must be functions of the player's own suggestion: restricting to constant deviations gives coarse correlated equilibrium, which (2.4)–(2.5) do not characterize, and allowing arbitrary functions of gives a stronger notion.
Two players with finite action types S₁ S₂ : Type* (Fintype, DecidableEq); payoffs h₁ h₂ : S₁ → S₂ → ℝ; distributions p : S₁ → S₂ → ℝ with the sign and sum conditions as an explicit hypothesis of every statement about distributions. Finite probability spaces are finite types Γ : Type with a probability vector μ : Γ → ℝ; deviations are compositions φ ∘ f₁ with φ : S₁ → S₁. The conditional payoffs , use Lean's x / 0 = 0 and are only ever used at possible suggestions. Empty action sets admit no distribution, so the statements are then vacuous, exactly as in the paper.
A trivializing formalization is ruled out: "c.e.d." is the existential notion over finite probability spaces with a genuine probability vector and an equilibrium in the sense of Definition 2.1, not the inequalities themselves or the swap form on .
No infrastructure beyond finite sums and Finset.filter is needed. Contributions welcome: proofs of the milestones, and the -player generalization the paper alludes to.
An orthogonal projection onto a closed subspace is straightforward to describe when that subspace is given directly. It is less straightforward when the subspace is specified as the closed sum of two others: a vector can have contributions from both, and the two component projections generally do not commute. In §12 of Aronszajn's 1950 paper, this problem arises while expressing the reproducing kernel of a sum of two closed subspaces of a reproducing-kernel Hilbert space through their individual kernels. The projection formula is the analytic heart of that calculation. It also gives a series whose finite partial sums can be applied without first describing a basis for the closed sum.
Aronszajn states the result for closed subspaces of a complex Hilbert space of functions. The projection identity itself uses only Hilbert-space geometry; evaluation at a point and the reproducing property enter when the operator formula is translated into a kernel formula later in the section. This mission isolates the projection theorem so that the same formal result can be used both in that kernel calculation and in other settings with two closed subspaces.
Let be a complex Hilbert space and let be closed linear subspaces. The algebraic sum is the set of all with . It need not be closed. Write for its closure and for the intersection. All four subspaces are closed except possibly the algebraic sum itself. Let be the orthogonal projections onto , respectively. Operator products denote composition, with the rightmost factor applied first; is the identity.
The paper writes for , even when is nonzero, and uses a distinct dotted plus for the algebraic sum. These symbols can look like a direct sum in newer notation. Here the definitions of and remove that ambiguity. Aronszajn assumes complex scalars throughout Part I after §1, p. 343; the statements below keep that convention. Neither a topology on an underlying set of functions nor a measure is part of these operator assertions.
The goal is the strong projection series, §12, Eq. (7). For each ,
The sum means that its finite partial sums converge in the norm of for each fixed . No operator-norm limit is claimed. The first term of the sum, at , includes because both zero powers are identity operators.
Three source statements are milestones. Equation (1) is a finite identity that expresses a power of through a partial sum and a power of . The paragraph following Eq. (4) identifies the strong limit of as . The paragraph before Eq. (7) asserts that tends strongly to zero. Together these statements specify the finite and limiting parts of the displayed target. They require no assumption that is zero.
The formula describes the orthogonal projection onto a closed sum in terms of projections onto its two constituents. In Aronszajn's application, an orthogonal projection on a closed subspace determines that subspace's reproducing kernel; therefore the operator expansion supplies a kernel expansion without constructing a basis of the sum. It also makes explicit why an intersection term survives when the subspaces overlap. The result is proved in the 1950 paper; this mission asks for a Lean proof of that known result, with its convergence mode and closure convention made explicit.
A machine-checked development would provide a reusable complex-Hilbert-space statement for alternating projections and closed sums. Mathlib already provides closed submodules and their orthogonal projections, so the new contribution is the finite identity and the strong-limit claims connecting them. The resulting theorem can support the paper's later kernel expression, §12, Eq. (18), once the correspondence between bounded operators and kernels from §11 is available. Equation (18) is outside this mission's target list.
The algebraic sum of two closed subspaces can fail to be closed, so projecting onto it directly would leave the target undefined as a Hilbert-space orthogonal projection. Passing to its closure gives the correct target but does not imply the two projections commute or that their product has a uniform contraction factor. In particular, strong convergence of the powers and of the final series does not generally improve to convergence in operator norm. The later special case in §12, where the intersection is zero and the minimal angle is positive, has a stronger uniform-convergence conclusion; that extra angle condition is absent from Eq. (7).
The finite formula also has four terms per summand whose order matters. Reversing and , beginning the power at rather than , or omitting changes the statement. Even a proof of pointwise convergence of each selected term would not by itself establish the convergence of the bracketed partial sums in the target.
The Lean representation is an arbitrary complex Hilbert space E with two ClosedSubmodule ℂ E objects. Mathlib's Submodule.starProjection supplies and . Two small definitions name as projection onto the join of the closed submodules and as projection onto their meet. The closed-submodule join is the closure of the algebraic sum; the meet is the intersection. These definitions are computed from , not independently quantified projections. The theorem quantifies over every vector and uses Filter.Tendsto along natural-number partial sums, giving norm convergence of the resulting vectors.
The source's ambient class has a reproducing kernel, but no step in Eqs. (1)–(7) uses point evaluations. The formal statements therefore apply to any complex Hilbert space, including the paper's RKHS. The stronger scope is explicit here and does not assert a new kernel identity. The -th Lean partial sum uses indices for the paper's ; it has the same terms and is defined at as . The finite identity is stated only for , as its version is false in general.
Eq. (1) on p. 375 is printed without the opening bracket of the summand (only the closing bracket appears); the formalization reads it as in Eq. (4) on p. 376, where both brackets are printed. There are two printing slips on p. 377: a running sentence drops brackets from the power of , and it prints while discussing the projection . The formalization follows the bracketed expression in Eqs. (1) and (4), using ordinary operator subtraction. The corresponding milestone preserves the printed wording. No assumption from the later angle analysis, especially , is imported into these results. The series is stated through actual partial sums; it is not defined by an arbitrary RKHS chosen to have a desired kernel.
In make-to-order production, chemical process industries and other manufacturing settings modelled as projects, activities do not only occupy machines for a while: they also consume intermediate products at their start and deposit products into storage facilities at their completion. Storage is bounded above by a tank or warehouse capacity and below by a safety stock. Resources of this kind are called cumulative resources (or inventory resources, reservoirs in the constraint-programming literature). They were introduced into resource-constrained project scheduling by Neumann and Schwindt (2002), and Chapter 2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), develops their theory in §2.12.
A scheduler handling cumulative resources needs a finite combinatorial description of which schedules respect the inventory bounds at every instant, because the time axis is continuous and cannot be checked point by point in a search procedure. Theorem 2.12.4 of the book gives such a description, and it is the basis of the branch-and-bound procedure of Neumann and Schwindt for the problem .
A project consists of activities with , where is the project beginning and the project completion. Activity has an integer duration , with and for the real activities.
For each cumulative resource in a set , every activity has an integer demand . If , activity withdraws units of at its start; if , it deposits units at its completion; means is not used. The demand of the project beginning is the initial stock. Write and . Each resource has a safety stock and a storage capacity .
A schedule is a vector of real start times with and . The active set and the inventory of at time are
The schedule is inventory-feasible if for all and all .
Two standing assumptions of the section are used throughout: (2.12.1) , so the final inventory is admissible; and Remark 2.12.2, .
A nonempty is a -surplus set if , and a -shortage set if . A -surplus set is minimal if no -surplus set arises from by removing a nonempty set of replenishing activities, and none arises by adding a nonempty set of depleting activities. Minimal -shortage sets are defined with the roles of replenishing and depleting activities exchanged. and denote the minimal -surplus and -shortage sets.
A schedule is inventory-feasible if and only if
The theorem turns a constraint over a continuum of time points into finitely many disjunctions, each a choice among precedence relations. An inventory excess caused by a minimal surplus set is removed by a start-to-completion relation (a replenishment is postponed until after a withdrawal starts, equivalently a maximum time lag), and a shortage by a completion-to-start relation . Consequences stated in the book: the feasible region of is a finite union of polyhedra; branching on these relations, organized as pairs of strict orders and reflexive relations, is a complete search scheme; and minimal delaying alternatives for surplus and shortage sets can be enumerated. Because every problem with renewable resources can be rewritten as one with cumulative resources (p. 130), the book also concludes that this union of polyhedra is in general disconnected.
The result is proved in the book (and in Neumann and Schwindt, 2002). To our knowledge it has no machine-checked proof. This mission produces a Lean formalization of the model, of the one-sided minimality notion, and of the two-sided characterization with its supporting lemma.
The combinatorial core is simple to state but easy to state wrongly. The natural first idea, to use inclusion-minimal surplus sets as for renewable resources, gives a different family and a false theorem: the book's minimality allows removing only replenishing activities and adding only depleting ones. The existence lemma needs Remark 2.12.2 to keep at least one replenishing activity in the minimal set, and the sufficiency direction needs (2.12.1) to guarantee a depleting activity outside the minimal set. Both membership conditions of the active set are closed at , so activities that deplete or replenish exactly at the critical instant must be counted on the correct side; a half-open reading changes which schedules are feasible. The initial stock is handled by the same active-set rule as any other demand, which matters for the invariance claim.
Fin (n + 2), activity is Fin.last (n + 1); resources are an arbitrary type K. Demands, safety stocks and capacities are integers (ℤ); start times are reals (ℝ); durations are natural numbers cast to ℝ.TotalDemandWithinBounds, BoundsStraddleZero) wherever the book's proofs use them. Surplus and shortage sets are nonempty by definition, and minimality uses proper inclusions.Reusable parts: the cumulative-resource model and inventory profile, which later missions on continuous cumulative resources (§2.12.2) or on the NP-completeness of (Theorem 2.12.1) can build on. Contributions welcome: proofs of the lemmas, of either half of the theorem, and finite-sum lemmas about Finset.filter that the proofs need.
The smallest enclosing ball problem asks, for finitely many points , for a ball of the smallest radius that contains all of them. It appears in clustering, in collision detection and bounding-volume hierarchies, in facility location (placing one service point so that the farthest client is as close as possible), and in the analysis of geometric algorithms. Sylvester posed the planar version in 1857; Megiddo (1983) gave a linear-time algorithm in fixed dimension, and Welzl (1991) a simple randomized one.
This mission formalizes Section 8.7 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer, 2007), which uses the problem to introduce convex programming. Unlike the geometric problems of the book's Chapter 2, the smallest ball cannot be written as a linear program. The section shows instead that it is a convex quadratic program, derives the Karush–Kuhn–Tucker (KKT) conditions for convex programs in equational form from the duality theorem of linear programming, and uses them to prove that the smallest enclosing ball exists and is unique. It is the book's bridge from linear to convex optimization.
A function is convex if for all and . A convex program in equational form is
with a real matrix with columns , and convex. A vector is feasible if and componentwise, and optimal if it is feasible and for every feasible . For differentiable , is the row vector of partial derivatives, so is a scalar.
For points , write and let be the matrix whose th column is . The program studied is
A ball is a closed Euclidean ball . The ball is the unique smallest enclosing ball of a set if , , every ball containing has radius at least , and every ball containing of radius at most has center .
For points , the objective of (8.15) is convex, and
The result. Theorem 8.7.4 gives existence and uniqueness of the smallest enclosing ball together with an explicit certificate: the center is a convex combination of the input points, the squared radius is the negated optimum value, and the points with lie on the boundary. It reduces the geometric problem to a convex quadratic program, for which interior-point and simplex-type solvers exist, and it is the basis of the combinatorial characterization "the center lies in the convex hull of the boundary points" used by Welzl-type algorithms. Proposition 8.7.2 is the KKT theorem for equational-form convex programs; it holds without any constraint qualification because the constraints are linear.
Formalizing it. All results here are classical and proved in the book; none is open. The mission produces machine-checked statements and, when solved, proofs of: the first-order optimality criterion for convex functions on convex sets in ; the equational-form KKT theorem derived from LP duality; the boundary characterization of unique smallest enclosing balls; and existence and uniqueness of the smallest enclosing ball in every dimension. Mathlib has first-order necessary conditions at local minima and general convexity theory, but no KKT theorem for linearly constrained convex programs in this form and no smallest-enclosing-ball theory.
Existence of an optimum and convexity of are routine. For the KKT conditions, the necessary direction needs multipliers, which do not come from calculus alone: the obvious Lagrange-multiplier argument handles only equality constraints and says nothing about the sign pattern forced by . For the goal, a solver must connect three layers — the gradient of a quadratic form in matrix notation, the multiplier conditions, and the Euclidean geometry of distances to — and uniqueness of the ball does not follow from uniqueness of the optimizer , which in general is not unique (repeated or cospherical points). The statement quantifies over all optimal and asserts that they all yield the same center.
Fin n → ℝ, so the book's indices become . Points of are EuclideanSpace ℝ (Fin d), so and are Euclidean. The matrix is Matrix (Fin d) (Fin n) ℝ.ContDiff ℝ 1 f. Convexity is ConvexOn ℝ Set.univ f.Fin n → ℝ, LP duality for the pair (maximize , , ) / (minimize , ), compactness of the standard simplex, and elementary Euclidean geometry. The first-order criterion and the KKT theorem are reusable beyond this mission; proofs through any route are welcome.The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Chudnovsky's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (19.8899945 : ℝ), i.e. .
Value. The bound is quoted in the literature as (e.g. Hata 1993), a truncation. This entry rounds the last digit up to so that the goal follows from the published constant.
Chudnovsky determined the exact asymptotic behaviour of the Hermite-type contour integrals behind Mahler's approximations, which sharpens the resulting exponent.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Mignotte's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (20.6 : ℝ), i.e. .
Value. The paper's abstract states for all , which gives exactly as stated. The paper also proves for (explicit), so follows from the same source; this entry uses the table value .
Mignotte refined Mahler's method of explicit rational approximations to (Hermite's approximation formulae for the exponential and logarithm) and sharpened the estimates that turn their size and denominators into an irrationality measure.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
This mission formalizes Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016) 177–200 (doi:10.4171/GGD/347; arXiv:1308.4250v3, whose page numbers are used): the group generated by three explicit piecewise projective homeomorphisms of the line is nonamenable and finitely presented, the first torsion-free finitely presented counterexample to the von Neumann–Day problem.
A discrete group is amenable when it has a finitely additive invariant probability measure on all its subsets. A group containing a nonabelian free subgroup is not amenable, and von Neumann and Day asked whether the converse holds. The counterexamples found before Monod's work are built from torsion groups by elaborate inductive constructions. Monod (2013) found nonamenable groups without free subgroups among piecewise projective homeomorphisms of the line. Lodha and Moore isolate in Monod's group a subgroup with three explicit generators and nine explicit relations.
Timeline.
The generators act on the real line: , and , are the piecewise projective maps of p. 2 (aFun, bFun, cFun). As homeomorphisms of the projective line (a, b, c) they generate (G0), inside the group where the published Monod bundle defines (Monod.Hpp).
Lodha and Moore move to infinite binary sequences through the continued-fraction map (Phi), under which , , become functions , , of sequences (Proposition 3.1). There and are and acting on the sequences that extend . is the group generated by all and , the group generated by the and the with not constant, and the five families of relations (1)–(5) among them. Products are taken left to right, as in the paper.
Section 5 rewrites words in the generators by explicit substitutions into standard forms and sufficiently expanded standard forms, and tracks them through strings in , , , ; these notions form the second definitions bundle.
ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel) as two milestones; Theorems 2.1 (Zimmer) and 2.2 (Carrière and Ghys) as printed; the group ; and the identities and orbit comparison of p. 4.The result. settles the finitely presented von Neumann–Day problem with a group that is torsion-free, has explicit generators and relations, and acts by piecewise projective maps, so its elements can be described by labeled tree diagrams much as those of Thompson's group . It shows that shares the combinatorics of without its unresolved amenability question.
Formalizing it. Before this mission none of the paper was formalized. The Monod mission's milestones supply the setting, and the case of Carrière and Ghys that Monod uses is already proved there by an elementary argument (Monod.not_isAmenableRel_mob).
Nonamenability is a short reduction to Theorem 2.2, which in general is deep. Finite presentation is the bulk: one must show that every word that evaluates to the identity can be reduced to an -word by the substitutions of §5, through a well-founded ordering on standard forms (Lemma 5.6) and an analysis of how acts on binary expansions (Lemmas 5.9–5.11).
Lean representation and conventions.
List Bool (finite) and Stream' Bool (infinite). is explicit; and are defined by the recursion of p. 5, digit by digit.Stream' Bool, so that products are left to right as in the paper. Statements about , , take products in the opposite of the homeomorphism group for the same reason.a, b, c are the homeomorphisms that agree with the formulas on , and toSeqGroup turns a bijection of sequences into a group element. Both fall back to the identity for a function that is not a homeomorphism or a bijection. Every generator is in fact one, so the fallback is never reached, and a trivial group would make the goal false.Matrix.ProjectiveSpecialLinearGroup, with the quotient topology), as on p. 4; a class acts on the projective line by the Möbius map of either of its matrices, through the published Monod bundle.What is left out, and deviations.
CountableOrbit.exists_perm_rel_iff_exists_zpow_eq is the underlying fact).LodhaMoorePrinted.printed_relations_four_and_nine_ne); the milestone uses the translations of the relations in , that they come from.LodhaMoorePrinted.eq_of_step_singleton_y_neg_one), and allow commuting and for any exponents, as the proof of Lemma 5.6 does (with commuting only for positive exponents, Lemma 5.6 fails: LodhaMoorePosCommute.not_forall_exists_derives_sufficientlyExpanded).What a development needs. Monod's mission supplies , its lack of free subgroups, the elementary non-amenability argument for with dense, and the passage from an amenable group to an amenable orbit relation. The theorem of Connes, Feldman and Weiss is published and proved (ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel); it gives the hard direction of the equivalence. The presentation of Thompson's group is published by the Cannon–Floyd–Parry mission on the two presentations of Thompson's group . Proofs of any milestone are welcome.