Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Hadwiger's conjecture (1943) asserts that for every integer , every graph with no minor is -colourable. It is a far-reaching strengthening of the four-colour theorem, and it is widely described as one of the central open problems of graph theory (Bollobás, Catlin and Erdős called it "one of the deepest unsolved problems in graph theory"). The interest is structural: the four-colour theorem concerns planar graphs, and Hadwiger's conjecture proposes that the only obstruction to -colourability that matters is the presence of a complete graph as a minor.
Timeline.
The case (graphs with no minor are -colourable) is the first open case.
All graphs are finite and simple. A minor of a graph is any graph obtained from a subgraph of by contracting edges. Equivalently, a graph on vertex set is a minor of if there are branch sets , , which are pairwise disjoint, each inducing a connected (nonempty) subgraph of , and such that for every edge of some vertex of is adjacent to some vertex of . has a minor if the complete graph is a minor of , i.e. contains pairwise disjoint connected vertex sets, every two joined by an edge.
A graph is -colourable if its vertices can be coloured with colours so that adjacent vertices receive different colours; is the least such . Write for the statement "every graph with no minor is -colourable". A graph is -degenerate if every nonempty set of vertices contains a vertex with at most neighbours inside the set. The stability number is the largest size of a set of pairwise non-adjacent vertices.
A proof of the conjecture would give a structural explanation of the four-colour theorem that does not depend on planarity, and would settle the chromatic number of every minor-closed class defined by excluding a single complete graph. Partial results already drive the theory of graph minors: bounds on the average degree of -minor-free graphs are the standard input to colouring, and linear Hadwiger-type bounds are used in structural and algorithmic graph theory.
On the formal side, only the smallest cases have Lean proofs: the platform already contains proofs of the cases under a different encoding of minors (namespace Hadwiger), which may be reused after bridging the definitions. The cases , Wagner's bound, the degeneracy lemma, the small extremal bounds and the Duchet–Meyniel theorem have elementary proofs and are realistic targets. The cases depend on the four-colour theorem, whose formal proof exists in Coq but not in Lean; formalizing them here requires either porting that proof or proving the reduction to it. The general conjecture is open.
The natural approach — contracting the colour classes of an optimal colouring — does not produce a minor, because colour classes are independent sets and contraction is only allowed along edges. Degeneracy arguments only give bounds of order , since dense random graphs with no large clique minor have average degree of that order; closing the gap to requires using large chromatic number itself, not just density. Already for the statement is equivalent to the four-colour theorem, so no short proof is expected for any .
Graphs are SimpleGraph V on a finite vertex type V : Type. Minors are encoded by branch sets (IsMinor), complete minors by HasCompleteMinor G t (the complete graph on Fin t is a minor of G), colourability by Mathlib's SimpleGraph.Colorable, and edge counts by the cardinality of the edge set. is the definition HC t. Logarithms are natural logarithms; asymptotic bounds are stated with an explicit existential constant and a ceiling. The case is included; HasCompleteMinor G 0 holds for every graph, so no statement becomes vacuous through a degenerate minor definition.
Useful reusable infrastructure: minor models and their composition, contraction of connected sets, greedy colouring of degenerate graphs, and edge-counting for minor-free graphs. Contributions of intermediate lemmas along the milestones are welcome.
Chess, checkers, Go and Backgammon share a feature that card games such as Poker lack: whenever a player moves, the player knows everything that has happened so far. von Neumann and Morgenstern call this perfect information and devote §15 of Theory of Games and Economic Behavior (1944; 3rd ed. 1953) to it. Their result is that such a game, viewed as a zero-sum two-person game, is strictly determined: it has a value that each player can secure with a pure strategy, without any randomization. For Chess this means that exactly one of three statements is true: White can force a win, Black can force a win, or both can force at least a draw ((15:D:a)–(15:D:c)).
Timeline. Zermelo (1913, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels) showed for Chess that either one side can force a win or both can avoid losing; his argument is not phrased in terms of strategies and a value, and was later corrected and completed by König (1927) and Kalmár (1928/29). von Neumann and Morgenstern (1944, §15) proved strict determinateness for every finite zero-sum two-person game with perfect information, including chance moves (15.7.1), and gave the explicit formula (15:12) for the value. Kuhn (1953, Extensive games and the problem of information, Annals of Mathematics Studies 28) recast games in tree form and extended the pure-strategy existence result to general-sum games with perfect information (subgame-perfect equilibria by backward induction).
A game tree is a finite rooted tree. Each leaf is a finished play and carries the payoff to player 1; player 2 receives . Each internal node is a move of one of three kinds , with alternatives leading to subtrees :
A pure strategy of player 1 is a complete plan choosing an alternative at every node of kind 1; does the same at every node of kind 2. The normalized form is the expected payoff to player 1, the expectation being over the chance moves. With the maxima and minima taken over the finitely many pure strategies,
Always ; the game is strictly determined when (14.4.2).
For a function of the alternatives of the first move , of kind , the operation of (15:8) is , or for . Applying these operations from the leaves back to the root gives the backward-induction value .
For every finite game tree ,
Both the equality and the value formula are part of the goal.
The theorem is the first existence result for the value of a class of games in pure strategies. It shows that the whole difficulty of the general zero-sum two-person game, the need for mixed strategies (§17), comes from imperfect information. It gives a construction as well as an existence proof: the value and optimal strategies are computed by backward induction, the procedure behind retrograde analysis of endgames, minimax search in game-playing programs, and the dynamic programming recursions of sequential decision problems with an adversary. The Chess trichotomy (15:D) is its best-known consequence.
Formalizing it adds a checked account of the passage from the extensive to the normalized form for a whole class of games, which the book carries out informally (15.4.2, 15.5.1: "the reader may verify it from the formalistic point of view"). The result is classical and fully proved in the book; the work is to formalize that proof on a tree model. Mathlib has saddle points (Order/SaddlePoint) and the minimax theorem for continuous functions (Topology/Sion), but no game trees, strategies of extensive games, or backward induction. No machine-checked version of this theorem with chance moves and the normalized form over complete plans is known to the mission.
The recursions (15:2)–(15:7) are not formal consequences of the definitions: and are extrema over whole plans of , while the right-hand sides are extrema over plans of the separate games . At a personal move of player 1, requires interchanging a Min over player 2's plans, which are functions of player 1's first choice, with a Max over that choice: this is exactly (13:E), a max-min equality that fails for general functions of two variables and holds here because the minimizing variable is a function of the maximizing one. A proof that treats the Max over and the Min over as interchangeable without this step is circular.
A second difficulty is the strategy spaces themselves. A complete plan chooses at nodes the plan itself excludes, so the pure strategies of are not simply pairs of a first choice and one strategy of the chosen subgame; the identification the book uses in 15.5.1 has to be justified by showing that the extra coordinates do not change .
A game is an inductive type GameTree with constructors leaf w, chance α p next hp hsum, move1 α hα next, move2 α hα next; alternatives are Fin α (numbered from ). The conditions , and at personal moves are constructor fields, so every tree is a legitimate game. Pure strategies are dependent types Strategy1 t, Strategy2 t defined by recursion on the tree (complete plans), with Fintype and Nonempty instances; is payoff t τ₁ τ₂, the expected leaf payoff; v1, v2 are Finset.sup'/Finset.inf' over all strategies, so every Max and Min is attained.
Standing hypotheses and conventions taken from the book:
The book's formal model is the set-theoretic one of §§9–10, with partitions of the set of plays; the tree restates it for the perfect-information case and does not formalize §§9–10. The book fixes one length for all plays; trees with plays of different lengths contain the book's games as a special case, so the goal is at least as strong as the book's theorem.
Strategies are plans, never responses: a strategy of player 1 is fixed before play and cannot depend on player 2's strategy, which would make trivial. Chance moves are part of the goal; a version without them proves only the Chess case and is weaker than the book.
Reusable beyond this mission: the tree model, its strategy types and the normalized form, which later chapters on extensive games can import. Welcome contributions: proofs of the milestones, and a lemma identifying the strategies of with the book's recursive description (15.4.2, 15.5.1).
Military and commercial service parts systems keep repairable parts at a central depot warehouse and at a set of operating bases. Chapter 10 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) turns from the planning models of the earlier chapters to execution. Each period, the stock that is at the depot or arriving there must be divided among the bases. The planner knows what is already in the pipeline and faces random demand at each base. The chapter's models are solved in a rolling-horizon manner. Each period's decisions are the first step of an optimal plan over a short horizon. That plan has to be computable at scale, for thousands of items and dozens of bases.
What makes this possible is a structural fact. In an optimal allocation, the cumulative stock sent to a base never exceeds what a single-period newsvendor problem at that base would ask for. This bound shrinks the allocation integer programs to linear programs of manageable size. This mission formalizes that bound and the facts it rests on.
Fix one item. Time is counted in whole periods , and is the finite set of bases. For each base :
If units have arrived at base by period , the expected cost of that period is
and stock left at the end of the horizon costs
The stock allocation model chooses nonnegative integer regular shipments , , with cumulative shipments never exceeding cumulative depot supply. The cumulative stock at base is , and the model minimizes . The extended model adds expedited shipments , which arrive after periods at an extra cost per unit.
The constrained newsvendor problem minimizes over integers . Its largest optimal solution is written .
In every optimal solution of , for every base and every ,
The bound is uniform over optimal solutions and uses nothing but the single-period problems.
Two supporting items state that and have optimal solutions. A third, theorem16_counterexample, exhibits an instance in which Theorem 16's upper bound, as printed, fails.
Theorem 15 is what allows the book (pp. 238–239) to rewrite with 0–1 variables indicating . Only between and is needed, so the number of variables is governed by the newsvendor quantities rather than by the total depot supply. Theorem 16 plays the same role for the model with expediting. Both bounds also justify the greedy heuristics of Sections 10.4.3 and 10.5.3. Those heuristics never raise a base's stock above its newsvendor level.
The book proves both theorems in half a page each by an exchange argument. This mission produces machine-checked versions and, in doing so, settles the exact scope of Theorem 16. As printed it is false. With , an expedited shipment in the last decision period can be the only way to cover a later period's demand, and the optimal plan then overstocks an earlier period. The mission states the corrected theorem and the counterexample; the counterexample was checked in Lean during drafting. None of the chapter's results has been formalized before, as far as the platform's catalogue shows.
The central step is the exchange. Take the first period in which an optimal plan overshoots its bound, and delay by one period one unit that arrives at . This must be shown feasible, to change only , and to lower the objective strictly. That in turn needs strict decrease of a convex function to the right of its largest minimizer, and an argument for the last period, where there is no later period to delay into. The indexing is heavy: two lead times, truncated sums , and cumulative constraints across bases.
The first idea, that a plan above the newsvendor level can always be improved by shipping less, fails. Shipping less changes the stock in every later period too, and later periods may need the unit. The bound follows only from a delay that affects exactly one period. For even such a delay is sometimes unavailable, which is where the book's Theorem 16 breaks.
ItemModel J Ω P bundles the data of one item with the cumulative demands on a probability space , [IsProbabilityMeasure P]. Bases form a Fintype. Periods are ℕ. Stock levels and supplies are ℤ, since net inventory may be negative. Shipments are functions J → ℕ → ℕ, so nonnegativity and integrality are built in. Costs are in ℝ.tsum for . The item model requires finite means and convergence of the series for at every stock level, so that no integral or sum takes Lean's junk value .IsLargestCNSolution (feasible, minimizing, and above every feasible minimizer). Theorems take as a function satisfying it. Milestone (10.19) shows it exists.Some elementary functions, such as , and , have antiderivatives that cannot be written as elementary functions. Liouville's theorem, formulated by Joseph Liouville between 1833 and 1841, is the algebraic statement that explains when an elementary antiderivative can exist: if a function has an elementary antiderivative at all, then that antiderivative lies in the differential field of the function, plus finitely many logarithms. The theorem underlies the Risch algorithm for symbolic integration, which relies on it to find any elementary antiderivative.
A differential field is a field together with a derivation , i.e. an additive map satisfying . Its constants form the subfield
Let be a differential field extension (the derivation of restricts to that of ).
The running example is , the field of rational functions in one variable with the standard derivative .
Let be differential fields of characteristic zero with , and let be an elementary differential extension of . If and satisfy , then there are , constants and nonzero , and with
The theorem reduces the question of whether an integral is elementary to a question about the base differential field. That reduction is what makes decision procedures for integration in finite terms (the Risch algorithm) possible, and it is the standard route to proving that , or have no elementary antiderivative.
The result is classical and proved (Liouville; modern algebraic proof by Rosenlicht; textbook proof in Geddes–Czapor–Labahn, §12.4). Mathlib contains a formalization of the algebraic-extension part of the argument (IsLiouville, isLiouville_of_finiteDimensional in Mathlib/FieldTheory/Differential/Liouville.lean); the logarithmic and exponential steps and the full theorem for elementary extensions are the remaining work.
The algebraic steps can be handled by taking traces. The central difficulty is the transcendental steps: for a logarithmic or exponential generator one must show, by comparing partial-fraction expansions in and degrees in , that an expression of the Liouville form over can be pushed down to one over . This needs the hypothesis that no new constants appear. The induction must also track how constants and logarithmic derivatives behave along the whole chain.
A differential field is a Mathlib Field with a Differential instance (a derivation over , written ); the extension is an Algebra F G with DifferentialAlgebra F G, i.e. commutes with the embedding. The chain of the elementary extension is a sequence of IntermediateField F G, starting at and ending at . Each step adjoins a single element, which is algebraic, logarithmic, or exponential over the previous field, and every derivative is computed in . Characteristic zero is assumed (CharZero F). The article does not state it, but it is the standing convention of the theorem in its standard sources. is stated as the equality of the image of with . In the conclusion, the are required to be nonzero, so the quotients carry no division-by-zero junk.
For the examples, is Mathlib's RatFunc ℂ. Mathlib does not provide its derivative, so the examples take an arbitrary derivation satisfying IsStandardDerivation (it agrees with the formal derivative on polynomials). Milestone 2 asserts that exactly one such derivation exists, so the examples are not vacuous.
Given a monic polynomial with integer coefficients, one can reduce it modulo each prime and factor it over the finite field . The way factors changes with , and the question of how often each factorization pattern occurs has a precise answer: Chebotarëv's density theorem (1922). It is the common generalization of Dirichlet's theorem on primes in arithmetic progressions (1837) and a theorem of Frobenius (1880, published 1896), and it underlies a large part of algebraic number theory, for example the fact that a Galois extension of a number field is determined by the set of primes that split completely in it. This mission follows the elementary exposition of P. Stevenhagen and H. W. Lenstra, Jr. (Math. Intelligencer 18 (1996)), which states all three theorems over with a minimum of terminology.
Timeline.
Let be monic of degree with nonzero discriminant , so that has distinct complex zeros . Let be its splitting field and its Galois group. Every permutes the zeros; the lengths of the cycles (including cycles of length 1) form the cycle pattern of , a partition of .
For a prime , the degrees of the irreducible factors of over form the decomposition type of modulo , again a partition of .
A Frobenius substitution of is an element such that, for some prime ideal of the ring of integers lying over ,
For these elements form a single conjugacy class of , written .
A set of primes has (analytic, or Dirichlet) density if
and natural density if as .
For every conjugacy class of ,
Chebotarëv's theorem shows that every conjugacy class of the Galois group occurs as a Frobenius class for infinitely many primes, with a predictable frequency. Its standard consequences include: the Frobenius elements are equidistributed; a Galois extension is determined by its completely split primes; if has a zero modulo almost every prime then is linear or reducible; prime ideals are equidistributed over ideal classes. The theorem is the first step in many arguments in arithmetic geometry (e.g. Serre's work on -adic representations).
The theorem is classical and proved; this mission is about formalizing it. Mathlib contains Frobenius elements in Galois extensions of Dedekind domains and Dirichlet's theorem in the form "infinitely many primes in each coprime residue class", but, to our knowledge, neither the density form of Dirichlet's theorem nor Frobenius's or Chebotarëv's density theorem.
The Galois-theoretic parts (milestones 3–6) are standard but require connecting Frobenius elements in with factorization of modulo , including the fact that forces to be unramified in . The analytic core is harder: one needs Dedekind zeta functions and -functions of number fields and their behaviour at . The reduction of the general case to the cyclotomic case (Chebotarëv's "crossing" with cyclotomic extensions) needs the density statement over an arbitrary number field as base, not only over ; in particular, the statement over alone cannot be proved by induction on itself.
All declarations live in the namespace ChebotarevDensity and share one definition file.
SplittingField of viewed in ; is Polynomial.Gal; is Mathlib's Polynomial.discr.IsArithFrobAt at some prime ideal of containing ; "" means that some Frobenius substitution of lies in (for this is equivalent to all of them lying in , by milestone 4).Equiv.Perm.partition of the permutation induced on the complex zeros of ; it includes fixed points.Welcome contributions: Dedekind zeta functions and Hecke -functions at , the density form of Dirichlet's theorem, unramifiedness of primes not dividing the discriminant, and the general number-field version of the theorem.
A classical way to recognize an algebraic function is through the arithmetic of its Taylor coefficients. Eisenstein's theorem (1852) says that if a power series is algebraic over , only finitely many primes occur in the denominators of its coefficients. The converse fails in general: many transcendental power series have integer coefficients. Lam and Litt (arXiv:2501.13175) conjecture that the converse does hold for power series that solve an algebraic differential equation at a non-singular point, and that even a weak control on denominators — primes may appear, but only after roughly coefficients — already forces algebraicity.
For linear differential equations, the conjecture is a strengthening of the Grothendieck–Katz -curvature conjecture, one of the central open problems about algebraic solutions of linear differential equations (arXiv:2501.13175). The bounded-denominator form is Problem 1 on Litt's list of open problems (problemsilike.com/1).
Timeline.
Let be a formal power series with rational coefficients and write for its -th formal derivative. Let be a rational function in variables. The series solves the algebraic ODE defined by if
and is defined at . Concretely, for polynomials with and .
For , is the subring generated by . For a function from the primes to , the coefficients of are -integral if for every prime the numbers lie in (denominators prime to ); is superlinear if .
For solving an algebraic ODE as above, the following are equivalent:
Together the four milestones imply the goal; the last two are the open content of the conjecture.
A proof would give an arithmetic criterion for algebraicity of solutions of arbitrary algebraic differential equations, and, for linear equations, would imply the Grothendieck–Katz -curvature conjecture (arXiv:2501.13175). Lam and Litt draw algebro-geometric consequences from the cases they prove.
For formalization: the conjecture is open, so the goal and the two open milestones are research targets. Eisenstein's theorem is a classical result; formalizing it is concrete, self-contained work. The implication (2)⇒(3) is elementary. The cases proved by Lam and Litt are candidates for further milestones.
Integrality of coefficients alone does not detect algebraicity: there are transcendental power series with integer coefficients that satisfy linear differential equations, such as . Its equation is singular at , which the non-singularity hypothesis on excludes; the conjecture asserts that at non-singular points such examples cannot occur. Even for linear equations the statement contains the Grothendieck–Katz conjecture, which is open in general.
PowerSeries ℚ with the formal derivative; rational functions are the fraction field of MvPolynomial (Fin (n + 1)) ℚ, where variable 0 is and variable i + 1 is .IsAlgebraic (Polynomial ℚ) f, i.e. over (equivalently over ).List.TFAE of the three conditions.Useful infrastructure: formal derivatives and substitution for power series, algebraic power series and their coefficient arithmetic (Eisenstein), and -adic valuations of coefficients. Formalizations of Eisenstein's theorem and of the special cases proved by Lam and Litt are welcome.
FormalConjectures/LittProblems/1.lean. https://github.com/google-deepmind/formal-conjecturesIn 1998 Smale listed eighteen problems for the twenty-first century; the eighteenth asks: What are the limits of intelligence, both artificial and human? (Smale 1998). The paper of Acharjee and Gogoi (arXiv:2310.10792) proposes a mathematical model of a mind, the cognitive-consequence space, built from a Tarski consequence operator, and claims that two theorems about this model (its Theorems 3.3 and 3.4) show that "human intelligence is limitless" (Discussion, p. 22; Conclusion, p. 23).
This mission records that model and its results in Lean 4 exactly as stated, so that each claim becomes a checkable statement: proved, or refuted, by the verifier rather than by argument.
A cognitive-consequence space is a set of mental representations (thoughts) with a consequence operator and an implication connective satisfying Tarski's axioms as listed in the paper (p. 5):
together with the paper's standing assumption (p. 5, after Definition 3.2).
A set is deductive if . The cognitive-consequence topology is
and members of are consequence-wise open (CWO). The cognitive closure is the intersection of all deductive sets containing .
Separately, a cognitive similarity distance is a function together with a relation (" and cognitively coincide") such that , is symmetric, , and the triangle inequality holds. A sequence of thoughts converges to if for every we have for all large .
For every cognitive-consequence space,
Theorems 3.1, 3.2, 3.3, 3.5, 3.6, 3.7 and Corollary 3.5 (the topology and the cognitive closure), Theorems 3.8 and 3.12 (cognitive limits), Theorem 4.3 (the filter ) and Theorem 5.1 (Gödel's incompleteness black hole).
The paper presents the goal as its answer to the human-intelligence half of Smale's eighteenth problem. A machine-checked verdict on the goal settles whether that conclusion follows from the paper's own axioms. The milestones are the paper's structural results about , cognitive closure and cognitive limits.
Status: to the best of current knowledge none of these results has a published machine-checked proof. The first conjunct of the goal (Theorem 3.3) follows from the standing assumption . The second conjunct (Theorem 3.4) is not implied by the listed axioms as formalized: the consequence operator with for every , on a one-point language, satisfies all of them and has . The goal is therefore expected to be resolved by a disproof.
The content of the goal is the existence of a nonempty CWO set, equivalently of a deductive set different from (a consistent theory). The paper's argument for Theorem 3.4 derives and calls this a contradiction; nothing in the axioms forbids it.
CogCons.CognitiveConsequenceSpace C bundles , the connective imp, axioms (i)–(vi) and . The syntax and interpretation of the paper are not modelled beyond imp.CogCons.CognitiveSimilarityDistance C is independent of ; sequences are indexed by starting at ; is an arbitrary relation constrained only by the listed axioms.Brocard's problem asks for all natural numbers such that is a perfect square. Henri Brocard raised the question in 1876 and again in 1885, and Srinivasa Ramanujan independently posed it in 1913 in the Journal of the Indian Mathematical Society. Only three solutions are known, and the problem is listed as Erdős problem #398 (erdosproblems.com/398). It is one of the simplest-looking Diophantine equations mixing a multiplicative object (the factorial) with an additive shift, and it is a standard test case for conjectures such as the abc conjecture.
No unconditional proof of finiteness is known.
For a natural number , the factorial is , with . A Brown number pair is a pair of natural numbers with
The three known pairs are , and , since , and .
For the conditional milestone, the radical of a natural number is the product of the distinct primes dividing . The abc conjecture asserts: for every there is such that for all positive integers with and ,
This says both that the three known pairs are solutions and that there are no others.
A resolution would settle a question open since 1876 and would be one of the rare complete solutions of a factorial Diophantine equation of this kind. The conditional finiteness result is a standard illustration of how the abc conjecture controls equations of the form .
For the formalization, the known-solutions milestone is a finite computation. The search-bound milestone is a large verified computation; a machine-checked certificate for it would be a reusable artifact. The conditional finiteness milestone formalizes a published argument that assumes the abc conjecture as a hypothesis. The goal itself is an open problem; none of these statements is known to have a machine-checked proof on this platform at the time of drafting.
Congruence obstructions cannot rule out large solutions: for every modulus and every one has , so is a square modulo . Local arguments alone therefore cannot close the problem. The known finiteness argument depends on the abc conjecture, which is itself unproved in the standard form used here. Computer searches only give lower bounds on any further solution.
ℕ); ranges over , so the sign of is not an issue. The factorial is Mathlib's Nat.factorial, with .Prop-valued definition used as a hypothesis in the conditional milestone; it is not asserted anywhere. The exponent is a real power.Brocard.Linear programming is usually described as "solvable in polynomial time", but that statement is about rational inputs given exactly. In Smale's list of problems for the 21st century (Smale 1998), Problem 9 asks for a polynomial-time algorithm over the reals deciding the feasibility of , and Smale explicitly calls for "models which process approximate inputs and which permit round-off computations". Real data such as , entries of a discrete cosine transform, or even in floating point can only be accessed approximately.
Bastounis, Hansen and Vlačić pose the extended Smale's 9th problem: in a model where the algorithm can only query approximations of the input to any requested accuracy, can one compute minimisers of linear programming, basis pursuit and Lasso to correct digits? Their Main Theorem I (Theorem 3.4) shows that the answer depends on in a sharp way: for a suitable class of well-conditioned, bounded inputs, no algorithm at all (not only no efficient one) produces correct digits, while digits are computable (but not in bounded time) and digits are computable in polynomial time.
This mission targets the first, impossibility, half of Theorem 3.4(i) for linear programming.
Linear program. For , and , the solution set is
It is a subset of with the norm, . An input is a pair , and the evaluations of are its coordinates and entries .
Extended model (-information). Let . An oracle representation of is a family , indexed by evaluations and accuracies , with and . An algorithm must succeed on every oracle representation of every input.
General algorithm. To make impossibility results independent of the machine model, the paper uses general algorithms (Definition 9.3): a map from inputs to ( = no output) together with a nonempty set of evaluations read on . This set is finite whenever halts. The output is determined by the values read, and any input that agrees on those values reads the same set. Turing machines and BSS machines with an oracle are special cases; general algorithms can even solve the halting problem.
Error and breakdown epsilon. The error is , with distance from . The strong breakdown epsilon is the supremum of all such that every general algorithm has error on some input (Definition 9.17).
For every integer , all dimensions and every there is a nonempty class of inputs with nonempty solution sets, and , such that
The theorem shows that for LP with inexact input, being non-computable in Turing's sense does not rule out a finer complexity theory. The paper builds a " / / digits" classification on this. It also explains why established solvers can return wrong answers with a success flag on small, well-conditioned LPs (§4 of the paper), and it bears on computer-assisted proofs that rely on inexact LP, such as the Flyspeck proof of the Kepler conjecture.
The result is proved on paper. As far as the proposer knows, it has not been machine-checked. This mission formalizes the deterministic impossibility part for LP and puts in place reusable infrastructure: general algorithms, breakdown epsilons and -information. That infrastructure is the base for later missions on the randomised parts of Theorem 3.4(i)–(ii), the weak breakdown epsilon (iii), the exit-flag theorem (Theorem 5.1), and basis pursuit and Lasso.
The obvious objection is that LP is in P for rational inputs, so some rounding scheme ought to work. It fails because an algorithm must halt after reading finitely many approximations. Two inputs that agree to that accuracy but have minimisers far apart then receive the same output. Setting this up needs a notion of algorithm strong enough to cover every computational model, a precise -information model in which the adversary controls the approximations, and explicit LP geometry in which an arbitrarily small perturbation of moves the minimiser by a fixed amount.
PiLp p (Fin N → ℝ).run : Ω → Option M (none = NH) and a read set queried, satisfying the axioms (i)–(iii) of Definition 9.3.ℝ≥0∞), and the error of NH is . The infimum over an empty solution set is . The goal also requires nonempty solution sets, so no junk value enters.ℕ+). An oracle input is stored as a pair (input, oracle family), and algorithms can read only the oracle family.Optimal transport asks for the cheapest way to move one distribution of mass onto another. Monge posed the problem in 1781 for maps; Kantorovich (1942) relaxed it to transference plans (couplings), turning it into an infinite-dimensional linear program with a dual: maximize the total revenue of pickup and delivery prices that never exceed the cost, . The equality of the two values — Monge–Kantorovich duality — underlies much of modern optimal transport, with uses in economics (matching markets, principal–agent problems), probability, and PDE.
This mission formalizes the duality theorem and its proof as presented in Colin Yao, Monge–Kantorovich and Transportation Theory (paper dated September 10, 2023), whose proof follows Villani's Optimal Transport: Old and New and, for the weak inequality, Galichon's Optimal Transport Methods in Economics.
and are Polish spaces (separable, completely metrizable) with their Borel σ-algebras; and are Borel probability measures on and ; is a continuous cost function.
including existence of a minimizing plan; the common value may be .
Duality converts a minimization over measures into a maximization over functions; it characterizes optimal plans by the complementary-slackness condition that they are concentrated on , and it is the entry point to Brenier's theorem, the Kantorovich–Rubinstein formula for the Wasserstein-1 distance, and the economic applications discussed in Section 5 of the source. The result is classical and proved in the literature; the work here is to formalize the known proof and to supply reusable infrastructure (couplings, -cyclical monotonicity, -transforms) on top of Mathlib's measure theory.
The weak inequality is a short integration argument; the reverse inequality is where the work lies. Finite-dimensional linear-programming duality does not pass to general measures directly: one must produce a cyclically monotone plan as a limit of discrete approximations (tightness and Prokhorov's theorem, closedness of the cyclic-monotonicity condition under weak convergence), build a potential from chains of cost differences, and control measurability and integrability of and . Passing from bounded to unbounded nonnegative costs requires an additional approximation argument, which the source only sketches (Section 4.5).
Lean namespace MongeKantorovichYao; one definition file provides transference plans, -cyclical monotonicity, -conjugates, -concavity and -subdifferentials. Conventions: marginals are pushforwards along the projections; -conjugates are extended-real infima (no default values); the transport cost in the goal is the -valued integral of the nonnegative cost, and both sides of the goal are compared in the extended reals, so the infinite-cost case is included and no integrability hypothesis is added. The dual side ranges over bounded continuous functions with the constraint imposed at every point. Proposition 4.22 is stated for bounded (as used in Proposition 4.31), since with unbounded costs a real-valued potential need not exist. Infrastructure that may be missing from Mathlib: Prokhorov-type compactness of tight families of probability measures, weak convergence of empirical measures, and lower semicontinuity of .
Service parts supply chains are often limited by a capacitated resource, such as a production line or a repair shop, instead of by lead times alone. Once capacity binds, the classical tools for setting stock levels (Palm's theorem and the Poisson distribution of units in resupply) no longer apply, and the quantity that determines how much stock is needed is the shortfall: the amount by which the end-of-period inventory falls below its target because capacity was insufficient. Chapter 8 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) builds its tactical planning models for capacity-limited systems on the distribution of this random variable, and on a continuous-time repair queue in which item counts are geometric.
The shortfall recursion is the Lindley recursion of queueing theory (Lindley 1952), so its stationary law is the law of the maximum of a random walk with negative drift. The exponential tail of that maximum goes back to Cramér's work on ruin probabilities; for capacitated production–inventory systems it was stated by Glasserman (1997), whose theorem the book quotes as Theorem 11. Glasserman and Tayur (1995) used the shortfall to optimize base-stock levels in multi-echelon capacitated systems, and Roundy and Muckstadt (2000) studied the mass-exponential approximation that the theorem motivates.
A single item is produced in periods of an infinite horizon; at most units can be produced per period. The demand of period is ; the demands are nonnegative, independent and identically distributed, with generic demand and (the standing assumption of Section 8.1.1).
Under the modified policy with target level , the facility observes and produces units, where is the end-of-period net inventory and . The shortfall satisfies and
With the random walk (), the stationary shortfall is
A law on is lattice if it is concentrated on a progression with .
In the discrete case ( and integer valued) is a Markov chain on with transition probabilities (p. 185). In the repair model of Section 8.3.1, reparable units of item arrive at rate , , a single exponential server repairs at rate , is the number of units in repair and the number of item- units, and .
Assume for all , with ; ; the law of is non-lattice; and has a root in . Then there are and with
The constant is left unspecified, as in the book.
The exponential tail is the justification the book gives for approximating the shortfall by a mass-exponential law (an atom at zero plus an exponential tail), from which target stock levels and fill rates are computed in closed form. The decay rate depends only on the demand law and the capacity, so the theorem also says how the stock needed for a given service level grows as utilization approaches one. The discrete-chain milestones justify the exact computation of the shortfall distribution behind the book's Table 8.1 and Figures 8.3–8.8. The geometric law of reduces the multi-item repair problem to independent newsvendor problems with an explicit solution.
The asymptotics of the random-walk maximum are proved in the literature (Cramér–Lundberg theory, Feller Vol. II, XII.5; Asmussen, Applied Probability and Queues, XIII.5); no machine-checked proof is known to exist. Mathlib has neither the Lindley recursion, nor ladder-height decompositions, nor the key renewal theorem for non-lattice laws. The printed Theorem 11 is not correct as stated (see Formalization scope), so the mission also records a corrected statement.
The central step of the goal is the passage from the random walk to an exact asymptotic. An exponential change of measure (Esscher tilt) with the root turns into an expectation under a law with positive drift, but it only yields the upper bound (Lundberg's inequality); it does not show that converges, nor that the limit is positive. Convergence needs a renewal theorem for the overshoot of the tilted walk, which fails for lattice laws. That is why the non-lattice hypothesis cannot be dropped. For the milestones, the existence of the stationary law needs the reversal argument that identifies the law of with that of , plus the strong law of large numbers to show from .
iIndepFun plus IdentDistrib with ), integrable, with ; these are fields of ShortfallModel. Periods are numbered from as in the book (demand 0 is an unused i.i.d. copy). The discrete case is a separate structure with -valued demand and capacity.Service parts networks (spare parts for aircraft, military systems, industrial equipment) hold stock at several echelons: a depot, intermediate stocking facilities, and bases or warehouses that face demand. Two questions recur in their planning. First, how should a given amount of stock be split among locations whose expected costs are convex in the stock they hold? Second, does adding an echelon, a depot that pools the demand of several warehouses, raise or lower the stock the system needs?
Chapter 7 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879), treats both. For the second it follows Eppen and Schrage (1981, reference [78] of the book): with normal demands, a depot that places orders every period and allocates stock so that all warehouses face the same stockout probability reduces the choice of system stock to a single critical-fractile equation. For the first, the chapter's multi-echelon pooling model (Section 7.3) evaluates nested cost functions of the form "holding and shortage cost plus the minimum over allocations of a sum of convex costs", and its appendix (Section 7.4) gives the marginal allocation algorithm AllocOpt that computes these minima exactly for every stock level at once.
Marginal analysis for separable convex resource allocation is classical (Fox, Management Science, 1966); the monograph of Ibaraki and Katoh (MIT Press, 1988) surveys it.
Allocation data (Section 7.4). There is a set of locations and an augmented set . Each location has integer gridpoints . For , the value of a convex function is given at each gridpoint. The slopes (7.19) are for , and repeats the last one. The piecewise linear approximation of (7.20)–(7.21) interpolates the values at the gridpoints and continues with slope beyond the last one. A convex function on is also given.
The allocation optimization (7.22) asks, for each , for
Algorithm AllocOpt (Definition 4) keeps a current gridpoint index and allocation per location. For each increment of the target, it repeatedly gives units to a location whose current slope is minimal, up to that location's next gridpoint, and records the accumulated cost.
Pooling system (Section 7.2.1). One depot supplies warehouses. The demand at warehouse in period is normal with mean and variance , independent across periods and warehouses. The supplier-to-depot lead time is periods, the depot-to-warehouse lead time periods, and holding and backorder costs are equal at all warehouses. Positions are in balance when is the same for all . For system inventory position , with the system demand over periods and the demand at over the next periods, the balanced allocation gives each warehouse a share proportional to , and is its end-of-period net inventory.
For every tie-breaking rule in its arg min steps, AllocOpt returns values that satisfy (7.22) for every : some feasible integer allocation attains , and no feasible integer allocation does better.
then a nonnegative allocation of the arriving units restores balance. 5. Net inventory law (pp. 156–157): is normal with mean and variance . 6. Critical fractile (pp. 157–158): minimizes if and only if , where
The goal certifies an algorithm that the chapter uses as a subroutine three times: in the pool cost (7.14), the subsystem cost (7.15) and the system cost (7.17), and hence in the claim of Section 7.3 that the system-wide cost function can be computed in time in the number of locations. Because AllocOpt produces the whole vector in one pass, its correctness gives the nested value functions at every gridpoint of the next echelon, which is what allows the recursion up the echelons. The Eppen–Schrage milestones give the classical quantitative form of risk pooling: the system stock is set by one critical fractile, and the standard deviation term is what the book compares with the single-warehouse and the decentralized systems.
On formalization: the book states Proposition 2 with a two-sentence argument and Remark 2 without proof. The Eppen–Schrage computations are displayed derivations. None of these results has a machine-checked proof on the platform. A verified AllocOpt, stated for an explicit algorithm rather than for an abstract greedy procedure, is reusable for any separable convex integer allocation with a sum constraint.
The usual greedy exchange argument assumes that units are allocated one at a time. AllocOpt allocates in blocks, up to the next gridpoint of the chosen location, and it carries its state across successive targets without restarting. The proof must therefore show that the state after each outer step is itself an optimal allocation for the current target, and that block moves never step past a breakpoint where the arg min would change. The slopes can be negative, and the equality constraint forces allocation even when every marginal cost is positive. Remark 2 needs an additional argument: under the inequality constraint the loop may stop before reaches zero, and that point is optimal only because the slopes are nondecreasing.
For the pooling results, the balanced allocation mixes the depot-lead-time demand of all warehouses with the local demand , and the Gaussian law of rests on the independence of disjoint blocks of periods. The fractile statement requires strict monotonicity of each warehouse's expected cost derivative in , not only a first-order condition.
Fin Mbar; gridpoints are integers, values and slopes real numbers; allocations are functions Fin Mbar → ℕ. The standing assumptions of Section 7.4 form the predicate WellFormed: , for (a slope (7.19) needs two gridpoints), gridpoints starting at and strictly increasing at every location of , each the value of a function convex on , and convex on .Service parts (spare engines, avionics modules, repairable components) are usually managed one unit at a time: whenever a customer order removes a unit from stock, a replacement is ordered at once, from a repair shop or an outside supplier. This is the (s–1, s) policy, under which the inventory position (on hand plus on order minus backorders) stays constant at the stock level . Every performance measure of such a system (fill rate, expected backorders, availability) is a function of one random variable: the number of units in resupply, i.e. ordered but not yet returned. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005) computes its distribution, and the rest of the book (the METRIC-type multi-echelon models of Chapters 4 and 5, the stock-level optimization of Section 3.4) is built on that computation.
Timeline. C. Palm (1938) showed, in the setting of telephone traffic, that in an infinite-server system with Poisson arrivals the number of busy servers has, in steady state, a Poisson law whose mean is the arrival rate times the mean service time, whatever the service-time distribution. Feeney and Sherbrooke (1966) carried the result to (s–1, s) inventory systems with compound Poisson demand, and treated the lost-sales case. Sherbrooke's METRIC model (1968) made the Poisson law of units in resupply the basis of multi-echelon spare-parts planning.
A single item is stocked at one location. Customer orders arrive at epochs of a Poisson process with rate , started empty at time : the interarrival times are independent and exponential with rate , and . The -th order triggers a resupply order with resupply time . The resupply times are independent and identically distributed, independent of the arrival process, with a density , distribution function and finite mean
With backorders allowed, the number of units in resupply at time is
and counts the orders placed in . On-hand stock and backorders at time are and .
In the compound Poisson version the -th order asks for units, the sizes are i.i.d. with , independent of arrivals and resupply times, and all units of one order share its resupply time . The units in resupply are . Writing for the probability that orders ask for units in total, the compound Poisson probabilities with parameter are
In the lost-sales version an order that finds no stock on hand is lost, so at most units are ever in resupply.
For every ,
The resupply-time law enters only through its mean. This is the statement the book's proof establishes and every later chapter uses.
The result. Palm's theorem turns an infinite-dimensional object (the whole resupply-time distribution) into one number, . This insensitivity is what makes spare-parts planning computable: the expected backorders at stock level are , the fill rate is , and both can be optimized over with only the demand rate and mean repair time as data. Theorem 7 extends this to batch demand, Theorem 9 to systems allowed a response time, and Theorem 8 gives the exact law when shortages are lost instead of backordered.
Formalizing it. All of these results are classical and proved. None of them is formalized on the platform, and Mathlib has Poisson and exponential distributions but no Poisson process, no thinning theorem and no infinite-server queue. The mission produces a Poisson arrival stream built from i.i.d. exponential gaps, the conditional-uniformity property of its epochs, independent thinning, and the M/G/∞ transient law, all reusable in queueing and inventory missions.
The algebra of the proof (summing the binomial against the Poisson law of ) is short. The work is in the probabilistic step the book treats in a sentence: that, given , the orders behave like independent uniform epochs, each of which independently is still in resupply at time with the same probability . This needs the joint law of the partial sums of exponential variables (Eq. (3.3)), and then a symmetrization argument, since the epochs are ordered while the resupply times are attached to order indices. The naive route of computing by conditioning on individual epochs does not go through without that exchangeability step. The limit is then elementary; stating a stationary version directly is not a substitute, since the book's "steady state" is exactly this limit.
The model is a structure on a probability space : exponential interarrival times with rate , nonnegative resupply times with a density and an integrable first coordinate, and mutual independence of the whole family. Orders are indexed from , so the book's are . Counts are cardinalities of sets of order indices, with value on the probability-zero event where infinitely many orders fall in a bounded interval.
Commitments and pinnings:
A model in which is postulated through its law, or in which resupply times may depend on the arrival epochs, makes the goal empty or false; here is computed from the primitive arrival and resupply times, whose joint law is fully specified.
Welcome contributions: a general Poisson-process library (construction from exponential gaps, Poisson marginals, order-statistics property), independent thinning, and proofs of the milestones in the listed order.
The second part of Hilbert's 16th problem (Paris, 1900) asks for the maximal number and the relative position of the limit cycles of a planar polynomial differential system
where are real polynomials of degree at most . Smale listed it in 1998 among the mathematical problems for the next century and remarked that, apart from the Riemann hypothesis, it seems the hardest of Hilbert's problems (Smale 1998). Even for it is not known whether the number of limit cycles is uniformly bounded.
J. Llibre's survey Sobre el problema 16 de Hilbert (La Gaceta de la RSME 18 (2015), 543–554) organises the question into seven problems and concentrates on a more tractable restriction: algebraic limit cycles, i.e. limit cycles contained in a real algebraic curve. For this restriction there is an explicit conjecture for the maximal number (Conjecture 1 of the survey, first stated in Llibre–Ramírez–Sadovskaia 2010). This mission formalizes that conjecture as its goal, together with the results of the survey on which it rests.
Timeline (as reported in the survey):
A polynomial vector field is a pair of real polynomials in ; its degree is . A solution is a differentiable curve with for all . A periodic orbit is the image of a non-constant periodic solution. A limit cycle is a periodic orbit that is isolated among periodic orbits: some open set contains no periodic orbit other than .
A limit cycle is algebraic if it is contained in the zero set of a non-zero real polynomial . The algebraic Hilbert number is the supremum, over all polynomial vector fields of degree at most , of the number of algebraic limit cycles (a value in ).
A curve is invariant with cofactor if . A family of irreducible curves is generic if (i) no curve is singular, (ii) the top-degree homogeneous part of each curve is square-free, (iii) distinct curves meet transversally, (iv) no three distinct curves share a point, and (v) the top-degree homogeneous parts of distinct curves are coprime.
The equality asserts both that the number of algebraic limit cycles is bounded by the right-hand side for every field of degree at most , and that the bound is attained.
A proof of the goal would settle Problems 6 and 7 of the survey: it would give a uniform bound, depending only on the degree, for the number of algebraic limit cycles, and identify the sharp value. The conjecture is consistent with every example known to the survey: the generic bound of Theorem 4 is sharp for even , and the known non-generic examples exceed the generic bound only in odd degree and by one. Conjecture 2 () is its first open case.
On the formal side, the milestones require a reusable library of planar dynamics that is currently absent from Mathlib: periodic orbits and limit cycles of planar vector fields, hyperbolicity via the divergence integral, inverse integrating factors, invariant algebraic curves and Darboux-type arguments, and topological configurations of Jordan curves. Theorems 1, 2, 4 and 5, Proposition 3 and the cubic example are proved in the literature but, as far as the proposal author knows, not formalized; the goal and Conjecture 2 are open.
The obvious route bounds the number of ovals of the invariant curve (Harnack's theorem) and relates the degree of the curve to the degree of the field. This fails because a field of degree can have invariant curves of arbitrarily high degree, so no a-priori degree bound on the curve is available; Theorem 4 obtains one only under the genericity conditions (i)–(v), and the degree-3 example shows that non-generic curves behave differently. On the formal side, the dynamical milestones (Theorems 2 and 5, the cubic example) need Poincaré–Bendixson-type planar topology and uniqueness of solutions, which Mathlib does not yet provide.
MvPolynomial (Fin 2) ℝ with variable 0 as and 1 as ; points are ℝ × ℝ. The degree of a field is the maximum of the total degrees of and , and ranges over fields of degree at most , matching equation (1) of the survey.Set.encard values in ℕ∞, so an infinite family is , never silently ; is an iSup in ℕ∞, so the goal also asserts finiteness.HasDerivAt at every real time). A limit cycle is isolated among periodic orbits contained in a neighbourhood. An algebraic limit cycle lies in the zero set of some non-zero polynomial, with no degree restriction on the curve.ℕ∞, not an inequality over a possibly empty family.Contributions welcome: a planar ODE library (uniqueness, flows, Poincaré–Bendixson), Darboux theory of integrability, and proofs of the classical milestones.
A stocking point that reviews its inventory once per period and must decide how much to order is the basic unit of every service parts supply chain: each warehouse, each repair depot and each forward location in the networks studied later in Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) faces this decision for thousands of items. The practical rule used everywhere is the order-up-to (base-stock) rule: bring the inventory position up to a fixed target level whenever it falls below it, and order nothing otherwise. Chapter 2 of the book justifies this rule for a single item with linear costs, following the dynamic-programming argument of Karlin and Scarf, and the rest of the book takes the rule as given.
Timeline. Arrow, Harris and Marschak posed the periodic-review inventory problem as a dynamic program in 1951 (Econometrica). Bellman, Glicksberg and Gross showed in 1955 that with linear ordering cost and convex expected holding and shortage costs the optimal policy has a critical-number form (Management Science). Karlin and Scarf (1958) extended the analysis to a positive lead time, the setting of the book's Theorems 1–3. Veinott (1965) gave conditions under which a base-stock policy is optimal in multi-product, nonstationary models (Management Science).
One item is stocked at one location. At the start of each period the inventory position is observed and a quantity is ordered; with lead time one period it arrives at the start of the next period. Demand in each period is independent of other periods and has a density on that is positive and continuous. Unmet demand is backordered. Costs are linear: per unit ordered, per unit on hand at the end of a period, per unit backordered at the end of a period, and future costs are discounted by . The one-period cost is
The book assumes throughout that : the backorder cost outweighs the saving from deferring a purchase.
The -period value functions are and, for ,
An order is optimal at if it attains this minimum over all . The order-up-to rule with level orders . The marginal function of eq. (2.8) is . In Lean these are Model, Model.L, Model.f, Model.IsOptimalOrder, Model.IsOrderUpToOptimal and Model.F in the namespace ServiceParts.BaseStock.
For every horizon , either there is a real level with
or ordering nothing is optimal for every (level ); and there is such that the level is real for all . No value of is fixed: the goal asserts the shape of the optimal policy only.
The theorem reduces an infinite-dimensional control problem, a choice of order quantity for every possible inventory position, to one number per period. Every later chapter of the book (Palm's theorem for policies, METRIC-type stock level optimization, allocation in multi-echelon systems) parameterizes policies by such stock levels; this is where the book justifies that parameterization.
The result is classical and proved in many texts. On Prove2Me the mission produces a machine-checked finite-horizon version with a continuous demand density, including the calculus the proof needs: convexity of an expected cost defined by integrals against a density, differentiation under the integral sign in the recursion, and the one-sided behaviour of the value function at the order-up-to level. Existing platform results on base-stock optimality (Veinott's multi-product model, advance demand information) use different models and different arguments; none covers this recursion.
The argument is an induction on whose hypothesis carries convexity, the derivative formula (b), and bounds on . The delicate step is the existence of a finite root of : its limit at depends on whether the previous level was finite. For nothing is ordered and the limit is , which the assumption does not make negative. The book's base case ("left to the reader") therefore fails when : with , , the two-period problem never orders. The goal is corrected accordingly.
Two properties the book's induction also carries are not usable as printed. Property (d), , is false: for large , approaches , which increases with . The second-derivative clause of property (c) fails at whenever . A solver cannot follow the printed induction step for step; property (a), which the book derives from (d), is true and is a milestone in its own right.
Model, together with positivity and continuity of on , , and .Differentiable, HasDerivAt) and do not read deriv as evidence of it.A recursion in which ordering is restricted to order-up-to rules, or in which is defined through , would make the goal a tautology; here is defined by minimization over all and optimality is checked against all orders.
Needed infrastructure: convexity and differentiation of parametric integrals against a density on , and minimization of a differentiable convex function over a half-line. Both are reusable for the other stochastic inventory missions on the platform. Proofs of individual milestones are welcome independently of the goal.
Many optimization problems in operations research have an objective that is an expectation, , over a random parameter whose distribution is known only through samples or is too complex to integrate. Two-stage stochastic programs, inventory and reliability models, and simulation-based design all have this form. Neither nor its subgradients can be evaluated exactly, but a random vector whose conditional mean is close to a subgradient is often cheap to compute: a sample subgradient of , or a finite-difference quotient of two sampled values.
Stochastic quasigradient (SQG) methods, developed by Ermoliev and co-workers in Kiev from the late 1960s, use such vectors in place of subgradients. They extend the stochastic approximation procedures of Robbins–Monro (1951) and Kiefer–Wolfowitz (1952) to nonsmooth convex objectives, general convex constraints, and directions whose conditional mean is biased by a vanishing amount. This mission formalizes the basic convergence theory of the simplest SQG method, the projection method, as presented by Yu. Ermoliev in Chapter 6 of the IIASA volume Numerical Techniques for Stochastic Optimization (Springer 1988).
Timeline (as cited in the chapter's bibliography).
Let be a nonempty convex compact set and convex and continuous on . The optimal set is . The projection onto is .
On a probability space, the stochastic quasigradient projection method produces random vectors by
where is a step size and a random direction. Write for conditional expectation given the history . The direction is a stochastic quasigradient if, for every ,
where the error is a function of the history. If the conditional mean of is a subgradient plus a bias , then (6.12) holds with (6.13).
A sequence of random vectors is a stochastic quasi-Féjer sequence for if and there are random with such that for all
If, with probability 1, and , and
then with probability 1 the iterates converge and .
Theorem 6.2 is the prototype convergence theorem for SQG methods. Its hypotheses allow random step sizes chosen from the history, nonsmooth objectives, and directions with a bias that vanishes fast enough; its conclusion is convergence of the iterates themselves to a single optimal point, not only convergence of function values or of . The later chapters of the same volume (adaptive step sizes, Chapters 17–18; nonstationary problems, §6.4) reuse the same framework. Theorem 6.1 isolates the probabilistic content in a form that applies to any algorithm with a quasi-Féjer inequality. The efficiency estimate gives a non-asymptotic accuracy bound for the averaged iterate.
The results are classical and proved in the literature: Theorem 6.1 in Ermoliev (1976, p. 98), Theorem 6.2 in this chapter (pp. 145–146). To our knowledge none of them has a machine-checked proof. Mathlib has conditional expectations and the a.s. martingale convergence theorem, but no Robbins–Siegmund-type almost-supermartingale lemma and no stochastic subgradient method. A formal proof of this mission would supply both.
The deterministic argument for projected subgradient methods compares with for a fixed . In the stochastic setting this comparison holds only in conditional mean, with a perturbation that is random, and the distances converge only almost surely, with an exceptional null set that depends on . Since is typically uncountable, "for every , almost surely" does not immediately give "almost surely, for every ", and it is the second form that identifies a single limit. A second difficulty is that only yields a subsequence along which approaches its minimum; passing from there to convergence of the whole sequence is exactly what part (c) of Theorem 6.1 is for.
EuclideanSpace ℝ (Fin n). The probability space is an arbitrary measurable space with a probability measure. is a chosen minimizer of over (unique for nonempty closed convex ). The history is the -algebra generated by ; and are measurable with respect to it.condExp. The quasi-Féjer definition requires square integrability of every (implied by the book's definition when ), so no conditional expectation is taken of a non-integrable function.The scenario approach replaces an optimization problem with uncertain constraints , , by the program that enforces only constraints drawn at random from the distribution of the uncertainty. Its solution is then judged by its violation, the probability that a new instance is not satisfied. For convex programs in the violation is controlled by the dimension alone (Calafiore and Campi 2006; Campi and Garatti 2008), because a convex program has at most support constraints. Many problems where the scenario approach is used in practice are not convex: control with quantized inputs, mixed-integer design, classification with nonconvex losses, and decisions over infinite-dimensional or unstructured sets. For those programs no a priori bound on the number of constraints that determine the solution exists.
Timeline, as recorded in Chapter 8 of Campi and Garatti's textbook:
Let be a generic set; it may be an infinite-dimensional space or a set with no algebraic structure. Let be a cost and constraint sets indexed by , where carries a probability . Neither nor the is required to be convex. With a sample drawn independently from , the scenario program is
and denotes its solution, assumed to exist and be unique for every sample.
The violation of a decision is (Definition 3.1).
A support set (Definition 8.8) is a subset of the constraints such that the program with only these constraints in place has the same solution as the program with all constraints. The full set of constraints is always a support set; a support set need not be minimal (of smallest cardinality) or irreducible (with no removable element). Let be the cardinality of the support set returned, for every sample, by some fixed algorithm.
For every function with ,
The level function is free: the statement is one inequality per admissible , and it holds for any algorithm producing support sets. This is the weakest form that carries the whole result.
For let
The arithmetic half states that maps into , , and the right-hand side of (8.15) equals (for ). The probabilistic half states .
The result turns the size of a support set, a quantity observed after the program is solved, into a certificate on the violation of the solution, for any optimization or decision problem whose solution is determined by a subset of the data. With the choice (8.16), a user who finds a support set of size can assert with confidence . The book's Figure 8.12 shows that for remains well below for up to a sizeable fraction of . Because the algorithm that finds the support set is arbitrary, cheap heuristics that return non-minimal support sets still give valid, if weaker, guarantees. The result does not recover the tight convex bound (3.4); for convex programs the Chapter 3 theory remains sharper.
The statement is proved in [31] and is the probabilistic core of the sample-compression arguments of learning theory (Floyd and Warmuth 1995) in the form used by the scenario approach. To the best of available knowledge it has no machine-checked proof. The platform's UnderstandingML.compression_bound proves a sample-compression bound for a fixed compression size with a different constant; it does not cover a data-dependent size or an arbitrary level function. A formal proof here provides a reusable bound for data-dependent support sets over arbitrary decision sets.
The natural first step is: condition on the support set being a particular index set with , and argue that the solution is then a function of the sampled constraints in alone, while the other samples are independent of it and must all be satisfied. The difficulty is that the event "the algorithm returns " depends on all samples, and the solution of the reduced program on is defined only where that program has a unique solution; the decomposition of the probability therefore has to be carried out on sections of the product space, with a measurability argument for each piece. A second point is that is random and data-dependent: a bound for each fixed does not directly give a bound at the random level , and the role of the condition must be accounted for at .
Lean representation and committed conventions:
ω : Fin N → Δ with law Measure.pi (fun _ : Fin N => P); indices run over .Finset (Fin N); the reduced program with index set has feasible set (all of for ).alg : (Fin N → Δ) → Finset (Fin N) returning a support set for every sample; is the cardinality of its output. The goal is universal over such maps.ENNReal.ofReal of the real right-hand side.Implicit hypotheses of the page, made explicit (the book states on p. 33 that measurability issues are glossed over): the constraint relation is measurable in ; the solution map is measurable; each event is measurable; exists and is unique for every sample; in the arithmetic half of (8.16).
A trivializing formalization is ruled out: the algorithm is not existentially quantified and is not the minimal support set, the reduced programs are not all assumed solvable (which would be unsatisfiable when has no unconstrained minimizer), and the support-set property requires uniqueness of the reduced solution, without which the bound is false.
Needed infrastructure: product measures on Fin N → Δ, splitting of such products along a subset of coordinates, and Fubini/Tonelli for sections. These pieces are reusable for other compression-type bounds. Contributions welcome: proofs of the two milestones and of the goal, and lemmas on splitting Measure.pi over a Finset of coordinates.
Search engines sell advertisement slots next to their results through ad-auctions. Advertisers bid on keywords, and each advertiser also sets a daily budget: the most it is willing to pay in a day. Queries arrive one at a time and each must be assigned to an advertiser at once, with no knowledge of the queries still to come. The seller's revenue from an advertiser is capped by its budget, so an allocation rule that ignores budgets can exhaust a high bidder early and forgo revenue that a more even allocation would have collected. The question is how much of the offline optimum an online rule can guarantee against every arrival sequence.
Mehta, Saberi, Vazirani and Vazirani (FOCS 2005 / J. ACM 2007) gave a deterministic algorithm whose competitive ratio tends to when bids are small compared with budgets, and showed that no deterministic algorithm does better. Their algorithm builds on online bipartite matching (Karp, Vazirani and Vazirani, STOC 1990) and online -matching (Kalyanasundaram and Pruhs, 2000). Buchbinder, Jain and Naor (ESA 2007) rederived the bound with an online primal-dual algorithm, which gives the ratio in closed form for every value of the bid-to-budget ratio and extends to multiple slots, stochastic information, bounded degree and budget flexibility. This mission formalizes the basic algorithm of that paper and its Theorem 1.
There is a finite nonempty set of buyers. Buyer has a known budget . Products arrive one by one; when product arrives, every buyer's bid on it is revealed. The bid-to-budget ratio is
A fractional allocation assigns fractions of products to buyers; the revenue from buyer is the minimum of and .
The offline fractional problem is the packing LP, which the paper calls the dual:
Its LP dual, the paper's primal, is the covering LP:
The Allocation Algorithm has a parameter and starts from . When product arrives it takes a buyer maximizing . If , the product is not sold. Otherwise it charges the minimum of and 's remaining budget, sets and , and updates
Its revenue is the total amount charged.
For every instance and every bound with for all , the Allocation Algorithm run with , under any tie-breaking of the maximum, satisfies for every feasible of the packing LP
With this is the paper's statement that the algorithm is -competitive; the fractional optimum bounds every integral offline allocation.
The proof of Theorem 1 rests on three claims and three auxiliary facts, each a milestone:
and, separately, the second sentence of Theorem 1,
Theorem 1 gives an explicit ratio for every value of , not only in the limit. It tends to the optimal deterministic ratio as bids become small, and it quantifies how the guarantee degrades as single bids become a larger share of a budget. The primal-dual analysis is the template for the paper's later sections and for a line of work on online packing and covering problems, surveyed in Buchbinder and Naor's monograph The Design of Competitive Online Algorithms via a Primal-Dual Approach (Foundations and Trends in TCS, 2009).
The result is proved in the paper, and the proof is short. What this mission adds is a machine-checked proof about an algorithm that is defined, not described: the run is computed by recursion from the instance, and the guarantee is proved for that run and every tie-breaking. A related private mission on the platform, The Design of Competitive Online Algorithms via a Primal-Dual Approach VI: Maximizing Ad-Auctions Revenue, states the monograph's Theorem 10.1, which is this theorem, in a form that takes the analysis's intermediate inequalities as hypotheses over arbitrary lists of won bids; the present mission states it for the algorithm itself. No machine-checked proof of Theorem 1 is known to this mission.
Each step of the proof is elementary; the difficulty is the bookkeeping of an online process. Claims (1) and (2) are statements about a single iteration that must be lifted to the whole run: Claim (1) uses that only increases, and Claim (2) that each product is processed once. Inequality (1) is an induction over the iterations that allocate to one buyer, interleaved with iterations that allocate to others and is the only place where the value of matters. Claim (3) needs a further invariant: the amount charged equals the minimum of the allocated bids and the budget.
A tempting shortcut is to take Inequality (1) and the "at most one undercharge" fact as hypotheses about some list of bids. That does not describe the algorithm and is not the theorem; here the only hypotheses are on the instance and on the tie-breaking rule.
Buyers are a type I with [Fintype I] and [Nonempty I]; products are Fin m, whose order is the arrival order. Bids and budgets are real, with and . The state of the algorithm records , the amounts charged, and ; one iteration is step, the run after products is runPrefix, and revenue sums the charges of the final state. The tie-breaking rule is a function sel of the current and the product, required to return a maximizer of ; the theorem holds for every such rule. The constant is a real power and requires . The theorem is stated for any bound on the ratios, of which the exact maximum is one instance. Claims (1) and (2) are stated for every , which covers the paper's choice. The paper's inequality for allows , read as a limit; the Lean statement requires .
A statement over an unconstrained allocation, or one conditioned on the proof's own intermediate inequalities, would be trivially true or false; the targets here concern only the run the definitions compute.
The development needs finite sums, real powers and logarithms from Mathlib and an induction principle for the run. The LP pair and weak duality are reusable for the paper's extensions, and the run invariants for any primal-dual online algorithm with multiplicative updates. Proofs of any milestone are welcome, as are sharper variants, such as the exact- form or the bound against integral allocations.
Large retailers hold point-of-sale and loyalty-card data that their suppliers cannot observe, and many of them sell access to it through data-sharing programs; others share the same data for free, or with only some suppliers (Shang, Ha & Tong 2016, §1). When two competing manufacturers sell through one common retailer, sharing a demand signal with a manufacturer changes how he sets his wholesale price, which in turn changes the retailer's margins and the rival's demand. Whether the retailer wants to share, with how many manufacturers, and at what price, is therefore a question about a multistage game with incomplete information.
Shang, Ha and Tong answer it for linear demand, a linear-expectation signal and quadratic production costs, under two contracting protocols. This mission covers the production economy case (marginal cost decreasing in volume, §6 of the paper), in which the retailer may have an incentive to share information even without payment. A companion mission covers production diseconomy (§5).
Two manufacturers sell substitutable products through a common retailer. Demand for product is
where is the retail price, measures competition intensity and is a demand shock with mean and variance . The retailer observes a demand signal with and a linear-expectation structure , where is the signal weight. Producing units costs with ; the paper writes and assumes (the Assumption, p. 251). Retailing is costless.
The game has three stages.
The ex ante profits of the pricing equilibrium are denoted , , , for a manufacturer and for the retailer, the number of informed manufacturers. , , denote the equilibrium number of informed manufacturers without contracting, under concurrent and under sequential contracting.
For every and , pricing equilibria exist, concurrent outcomes and sequential SPEs exist, and for every concurrent outcome and every SPE (either first mover)
where is the retailer's profit after side payments and the manufacturers' total profit net of them. The second inequality is asserted for all except at most two values depending only on . The comparisons about every pricing equilibrium family exclude the single value (see Formalization scope). The paper says "higher"; the inequalities are weak because both sides coincide on intervals of positive length.
Proposition 8(d) says that a common retailer who sells information prefers to sell it sequentially, and that the manufacturers bear the cost: sequential offers let her extract a larger payment from the first manufacturer, because his outside option depends on what she will do with the second. Together with Propositions 6 and 7 it explains why retailers under production economy share with only a subset of suppliers once economies of scale or competition are strong, and why a retailer may share data for free, a practice the diseconomy model cannot produce.
The results are proved in the paper, partly by "it is straightforward" arguments (the proofs of Lemmas 2–5 are omitted). No part of the paper is formalized. A formalization adds a machine-checked account of the equilibrium selection at the boundary payments, where the paper's case analysis is informal, and of the points at which the retailer is indifferent between outcomes.
The pricing stage is a Bayesian game with a continuum of strategies: an informed manufacturer's strategy is an arbitrary square-integrable function of the signal. Lemma 1's uniqueness needs the Assumption (without it the manufacturer's problem is not concave) and a conditional-expectation argument, not a finite-dimensional computation. The comparisons of Lemma 5 are sign conditions on rational functions of whose thresholds , are implicit roots. The contracting stage is where the naive argument fails: at the boundary payments several equilibria give the retailer the same payoff but the manufacturers different payoffs, so "the" outcome is not well defined there, and a direct comparison of closed-form profits at the paper's selected equilibria does not cover every equilibrium.
Lean represents manufacturers by Fin 2, statuses by an inductive type with informed and uninformed, and a pricing strategy by a function of the signal value. The committed conventions are these.
The ex ante profits in every statement are those of an equilibrium of the pricing game on the signal model, not the §4.2 closed forms; a formalization that defined them by the closed forms would reduce the goal to algebra and a game, and is ruled out. The model layer (signal model, pricing equilibrium, payoff table, both contracting games) is shared, name for name, with the production diseconomy mission. Contributions are welcome on each milestone, and on reusable pieces: linear-expectation signals, and pointwise optimization under conditional expectation.
Traffic information systems (TIS) such as navigation apps send drivers noisy signals about the state of a road network: incidents, weather, closures. When several such systems coexist, each with its own subscriber base and its own information, a natural question for operators and regulators is whether subscribing to one system rather than another actually lowers a driver's expected travel cost in equilibrium, and how this advantage depends on how many drivers use each system. More information for one population also changes the congestion everybody else faces, so the answer is not simply "more information is better".
Wu, Amin and Ozdaglar (Operations Research 69(1), 2021) answer this question for nonatomic routing games with heterogeneous, possibly correlated information. Their model builds on the weighted potential game framework of Sandholm (2001) and on sensitivity analysis of convex programs. This mission formalizes their Section 5 result: for any two populations the sign of the relative value of information is determined by which of three explicitly computable size regimes the population sizes lie in, and the relative value decreases as one population grows at the expense of the other.
A Bayesian routing game has a finite set of populations , one per TIS, a finite set of network states , and for each population a finite nonempty type space of signals. A common prior is a probability distribution on , . A network with a single origin–destination pair has edges and a finite nonempty set of routes ; each edge has a state-dependent cost that is positive, strictly increasing and differentiable. The total demand is , and population carries the fraction of it, with and .
A strategy profile assigns to each population and type a split of its demand over routes. It induces the route flow and the edge load . With the belief , type evaluates route by its expected cost . A Bayesian Wardrop equilibrium (BWE) is a feasible in which every type uses only routes of minimal expected cost. The equilibrium population cost is at a BWE .
The game has a weighted potential ; its minimum over feasible profiles is the equilibrium potential value . For two populations , the direction moves demand share from to , and is the total share of the other populations. The impact of information measures how much of population 's demand is moved by its signal. Two thresholds are computed from the optimal set of an auxiliary convex program over route flows in which the separate information constraints of and are merged. They define three regimes: (), () and (). The relative value of information is .
For and admissible (in the simplex with ), and every BWE of ,
and is nonincreasing along : for with both endpoints admissible.
The route to the goal follows the paper: Lemma 1 (weighted potential), Lemma 2 (strict convexity of the edge-load potential), Theorem 1 (equilibria are the minimizers of ; unique edge load), Lemma 3 (unique Lagrange multipliers), Proposition 1 (the feasible route flows form a polytope ), Proposition 2 (equilibrium route flows minimize over ), Lemma 4 (), Theorem 2 (equilibrium flows in each regime), Proposition 3 ( decreases, stays constant, increases along in the three regimes) and Lemma 5 ( is convex and directionally differentiable, and ).
Theorem 3 says that a population has an advantage over another exactly when it is the minor population of the pair, relative to thresholds that depend only on the other populations' sizes. Both populations face the same equilibrium cost in the middle regime. It gives a procedure for comparing two information systems without computing equilibria for each size vector: solve one convex program, read off two thresholds, and locate . The paper's Section 6 uses the same machinery, through Lemma 5, to characterize the equilibrium adoption rates of information systems.
The paper proves these results with the main proofs in the article and the sensitivity-analysis lemmas (Lemmas EC.1–EC.4) in its e-companion. None of them has a machine-checked proof. The formalization requires a Lean account of Bayesian Wardrop equilibria, of the equivalence between equilibria and a convex program, and of directional derivatives of the optimal value of a parametric convex program. Parts of this are reusable for any nonatomic routing or congestion game.
The equilibrium strategy profile is not unique and changes discontinuously with . Differentiating equilibrium costs in directly therefore fails. The paper instead works with the optimal value , whose one-sided directional derivative is expressed through Lagrange multipliers. That requires a sensitivity theorem for convex programs whose constraints depend affinely on the parameter, together with uniqueness of multipliers, which fails for populations of size zero. The regime analysis also needs a characterization of the route flows that are induced by feasible strategy profiles. That set is described by the nonlinear-looking constraint , a minimum over types inside a sum over routes. Strict monotonicity of in the side regimes needs the tightness of an information constraint at every equilibrium, not only at one.
The model is a Lean structure BayesRouting.VOI.Game over finite types of populations, type spaces, states, edges and routes. Routes are given by their edge sets, and the directed-graph structure is not used. Type spaces and the route set are nonempty. The prior is a probability distribution, , and costs are positive on nonnegative loads, strictly increasing and differentiable on . One assumption is added: every type profile has positive probability. It makes beliefs well defined and the equilibrium edge load unique, and it excludes perfectly correlated signals.
Conventions: is the last form of eq. (7), which does not divide by . is the maximum of eq. (16) over the reference profile, so that is exactly (14d). and the thresholds are sInf/sSup over sets that are nonempty and compact for size vectors in the simplex, and every statement keeps size vectors there. Statements about "the" equilibrium are stated for every BWE, and existence of a BWE is a separate item, so they are not vacuous. The thresholds are defined from the optimal set of the auxiliary program, not assumed as parameters. Taking them as parameters constrained only by Lemma 4 would give a different theorem.
Disclosed deviations: Lemma 2's clause assumes costs; Lemma 3 is stated for populations of positive size; Lemma 5 assumes ; Proposition 3 is stated with strict monotonicity in the side regimes, as used in the proof of Theorem 3. Contributions of reusable infrastructure are welcome: interval-integral potentials of monotone costs, KKT theory for polyhedral constraints, and directional derivatives of parametric optimal values.
Extremal graph theory asks how many edges a graph on vertices can have without containing a fixed graph . The answer, the Turán number , and the graphs attaining it, the set of extremal graphs, are known precisely only for special ; the Erdős–Stone–Simonovits theorem gives , where is the chromatic number.
Spectral extremal graph theory asks the same question with the number of edges replaced by the spectral radius , the largest eigenvalue of the adjacency matrix. Since , a spectral bound implies an edge bound, and spectral extremal results are usually stronger than their edge versions. Nikiforov (Linear Algebra Appl. 427, 2007) showed that the Turán graph maximises among -free graphs, so for the spectral and the edge extremal graphs coincide. Whether this happens for other is the subject of the paper.
Timeline:
All graphs are finite and simple. For a graph on vertices, is its adjacency matrix and is the largest eigenvalue of . A graph is -free if no subgraph of is isomorphic to . The Turán number is the maximum number of edges over -free graphs on vertices, and is the set of -free -vertex graphs with edges. The Turán graph is the complete -partite graph on vertices with parts of sizes or .
The hypothesis on is: for fixed integers and and all large , and every graph in contains a spanning copy of , i.e. is plus edges. The paper states "adding edges" and fixes the constant at the start of Section 3 (p. 4): "We may assume that the graphs in are obtained from by adding edges." The mission follows that reading. Examples: with , the friendship graphs, and the intersecting cliques .
A graph is spectral extremal for if it is -free and for every -free on the same vertices.
For , and satisfying the hypothesis, there is such that for all every spectral extremal graph for on vertices satisfies
The statement contains no numerical constant, and depends only on , , .
The milestones follow the proof, in order: strict monotonicity of under proper subgraphs of a connected graph (Lemma 2.3); connectivity of (Lemma 3.1); the bound (Lemma 3.2); spectral stability for (Corollary 2.6); for every maximum -cut , and (Lemma 3.3); a counting inequality for intersections (Lemma 2.8); and minimum degree above (Lemma 3.6); at most vertices of each part have a neighbour in that part, and all others see every other part completely (Lemma 3.7); Perron entries for (Lemma 3.8); (Lemma 3.9); balancing two parts of a complete multipartite graph increases (Lemma 2.7); and the maximum partition is balanced, (Lemma 3.10).
The theorem settles the Cioabă–Desai–Tait conjecture: for every whose extremal graphs are Turán graphs plus a bounded number of edges, the spectral extremal problem reduces to the edge extremal problem for large . This recovers the earlier cases (friendship graphs, the graphs , intersecting cliques) at once, and it turns any future determination of of this type into a spectral result with no further work.
The result is proved on paper; it has no machine-checked proof. Mathlib has Turán's theorem (extremalNumber_top, uniqueness of turanGraph) and the definition of extremalNumber, but no spectral extremal graph theory: no Perron–Frobenius theorem for graphs, no spectral Turán theorem, no stability theorem. The formalization would supply these, and the milestone statements are independently reusable: strict monotonicity of (Lemma 2.3), the spectral comparison of complete multipartite graphs (Lemma 2.7) and spectral stability (Corollary 2.6) are standard tools of the area.
The natural first idea, comparing with an extremal graph by Rayleigh quotients, fails at the start: gives only , far from . Closing an additive gap of edges requires control of the Perron vector to within at every vertex and exact control of the part sizes. The second is the delicate step: an imbalance of one vertex between two parts costs in , while the extra edges contribute only beyond the Turán graph, so the two effects must be compared at different scales. Further, the proof needs the deep spectral stability theorem of Nikiforov (Lemma 2.5), whose own proof is long.
Graphs on vertices are SimpleGraph (Fin n), matching Mathlib's extremalNumber n F; is a graph on any finite type. is the largest eigenvalue of G.adjMatrix ℝ (index of Mathlib's decreasingly sorted eigenvalues₀), not an absolute value and not a norm. "-free" is F.Free G (no copy of , not necessarily induced). "Sufficiently large " is ∃ N, ∀ n ≥ N with chosen after and before ; "sufficiently small " is ∃ ε₀ > 0, ∀ ε ∈ (0, ε₀). Partitions are labellings Fin n → Fin r whose parts may be empty; the Section 3 lemmas hold for every partition maximising the number of crossing edges. Lemma 3.8 carries the extra hypothesis , because as printed it is false for (for and the Perron vector of has entries below ); the goal does not assume it.
Trivializing formalizations are ruled out: is not defined from the edge count (which would make spectral and edge extremality the same), the hypothesis on does not contain the conclusion and is satisfiable (a sorry-free check for , was compiled), the conclusion is and not a weaker bound, and the threshold is not chosen after .
A complete development needs the Perron–Frobenius theorem for irreducible nonnegative symmetric matrices, the Rayleigh quotient characterisation of , the spectrum of complete multipartite graphs, Nikiforov's spectral stability lemma, and max-cut partition arguments. All of these are reusable beyond this mission, and proofs of any milestone, of the cited Lemmas 2.1, 2.2 and 2.5, or of Nikiforov's spectral Turán theorem are welcome.
The periodic-review inventory model with a fixed ordering cost is one of the basic models of operations research. When every order incurs a set-up cost in addition to holding and shortage costs, the optimal replenishment rule over an infinite horizon is, under standard convexity assumptions, a stationary policy: whenever the stock falls below the reorder point , order up to the level . Existence of such an optimal policy goes back to Scarf (1960) and Iglehart (1963). Knowing that an optimal policy exists does not say how to find one, and the average cost of an policy is neither convex nor unimodal in .
Veinott and Wagner (Management Science 11 (1965) 525–552) gave an exact algorithm. It proceeds in three steps: (i) compute integers bounding an optimal policy; (ii) find the set of all policies within those bounds that minimize the cost for starting stocks below ; (iii) choose from a policy that is optimal for every starting stock. This mission formalizes the theory behind Step iii. It is the third mission of a series on the paper: mission I treats the renewal closed form of the discounted cost, mission II the bounds of Step i.
Demands are independent non-negative integer random variables with common distribution and finite mean. Following the paper's Eq. (2), the unit purchase cost and the holding and penalty costs are combined into a single function , assumed convex with as ; the set-up cost is and is the discount factor.
A stationary policy, with integers , sets the stock after ordering to
and the stock evolves as from . Its discounted cost is
where for and , and its equivalent average cost is .
A policy is optimal for a set of integers if, for each , it minimizes over all policies; it is optimal if it is optimal for every integer . Under a fixed policy, is accessible from if for some .
Below the reorder point the cost does not depend on the starting stock; its value is written with . The bounds are: the smallest minimizer of ; the smallest integer with (21); the smallest integer with (22); the smallest integer with (23). The candidate set consists of the policies with , that minimize among such policies.
For and : if is optimal and every with
is accessible from under , then is optimal.
Theorem 2 turns the final selection step of the algorithm into a reachability check on the demand distribution: a policy of is certified optimal without comparing average costs at every starting stock. Its corollaries give checkable sufficient conditions; for example (Corollary 2.2) if for , the policy of with the largest reorder point is optimal, which covers Poisson and negative binomial demand. Theorem 1 separately reduces the comparison of two policies to finitely many starting stocks.
The results are proved in the paper (Section 4 and Appendix §3). No machine-checked version is known: the platform has no discrete inventory chain, no discounted cost of a stationary policy on , and no accessibility notion for such a chain. The mission produces these objects together with the paper's selection theory on top of them.
Theorem 1 needs a renewal decomposition at the first passage of the stock below , carried out for expectations over an unbounded integer state space with a discounted infinite sum. Lemma 1 is the delicate step. The paper's argument compares the policy with a hybrid policy that follows until the stock first reaches and then switches to an optimal policy; the inequality "the hybrid cannot be better than the optimal policy" requires that some stationary policy is optimal among all ordering policies, including non-stationary ones. That existence result is cited by the paper (Section 2), not proved there. A proof of Lemma 1 within the class of policies alone does not go through, because the hybrid policy is not an policy.
All objects live in the namespace VeinottWagnerSS.Selection. The model is the structure Model: the demand distribution φ : PMF ℕ with finite mean, K ≥ 0, and G : ℤ → ℝ convex (non-decreasing forward differences) and tending to at both ends. The unit cost , the function and the lead time do not appear (the paper's own reduction, Eq. (2), p. 529). Stock levels are integers. stateLaw is the law of , obtained by iterated PMF.bind; fCost is the expected discounted cost of that chain as a real series, which converges absolutely for because every lies in . aCost is times fCost. Accessible uses the law of with strictly. Optimality is among policies (p. 536); the class of general ordering policies is not formalized.
The bounds are infima of sets of integers; under the standing assumptions and these sets are nonempty and bounded below, so each bound is the least integer the paper describes. is defined as , the cost at the starting stock just below ; that this is the common value for every is milestone 1.
The standing assumptions are kept in every statement, including Theorem 1 and milestone 1, which do not need them; Lemma 1 and Theorem 2 are true only because of them. No printed slip was found in the three results.
Trivializing formalizations are excluded: is the expected cost of the stock process, not a closed formula or a fixed point of a recursion, so milestone 1 is not definitional; the bounds are the least integers of (21)–(23), not arbitrary integers, so is determined by the data; the goal does not assume that is optimal below , and Lemma 1 assumes optimality only at the single starting stock .
Useful contributions beyond the milestones: summability lemmas for fCost, the Markov (one-step) equation for fCost, the first-passage decomposition, and, for Lemma 1, a formalization of general ordering policies with the existence of an optimal stationary policy. The chain and cost definitions are reusable for other results of the paper (Theorem 3, Corollaries 2.1 and 2.2).
The policy is the standard ordering rule for a single stocked item with a fixed charge per order: when the stock position falls below a reorder point , order up to a level ; otherwise order nothing. Scarf (1960) proved that when the expected one-period cost is convex, some policy is optimal in every period of a finite-horizon model with set-up cost. Iglehart (1963) extended this to the infinite horizon. These results establish existence only. They give no procedure for finding the optimal pair.
Veinott and Wagner (1965) gave such a procedure. Its first step is to bound the optimal and by four integers computed from the one-period cost alone. This reduces the search for an optimal policy to a finite box. Their Theorem 4(a) proves that the bounds hold for the first-period parameters of an optimal policy in every -period model. This mission formalizes that theorem and the four comparison lemmas (Lemmas 2–5 of the paper's Appendix §2) from which the paper derives it.
Demands in periods are independent, non-negative integer random variables with common distribution and finite mean. Unfilled demand is backlogged, so stock levels are arbitrary integers. In period , is the stock on hand plus on order before ordering and the level after ordering. Then and .
A policy chooses as any integer function of the information available at the start of period . Given , that information is determined by and . Policies may therefore depend on the whole history; they are not required to be Markov.
Costs are summarized by a set-up cost , a discount factor and a one-period cost . The paper reduces the model with purchase cost , lead time and holding–penalty cost to these data by its Eq. (2), with . The -period cost of a policy from is
where and for . A policy is optimal if it minimizes for every simultaneously. The standing assumptions are that is convex on the integers (non-decreasing forward differences) and as .
The bounds (p. 537) are defined as follows. is the smallest minimizer of . is the smallest integer with (21). is the smallest integer with (22). is the smallest integer with (23).
For every there is an optimal policy for the -period model whose first-period rule satisfies
Optimality is against all history-dependent policies and for every starting level. The existence of an optimal policy is part of the conclusion.
The theorem turns the optimization over policies into a search over a finite box that depends only on , and . The paper's Section 4 procedure for the infinite-horizon problem (Theorem 4(b), Step i) is built on this box, and the bounds also give an interpretation of and : is the single-period optimum, and , , mark where the one-period cost exceeds that optimum by the fractions , and of the set-up cost.
The results are proved in the paper. None of them has a machine-checked proof as far as is known; no discrete-state finite-horizon inventory model with set-up cost is on the platform. A formal proof would provide a reusable finite-horizon dynamic-programming model with history-dependent policies and extended-real expected costs, and a machine-checked version of the existence of optimal policies in the discrete setting, which Theorem 4(a) contains.
The four lemmas compare an optimal policy with an explicit modification of it. The modification in Lemmas 2 and 5 raises the stock in period 1 and then orders , where is the original policy's decision along the original demand path. This comparison policy is history-dependent even when the original policy is not, so the argument cannot be carried out inside the class of Markov or policies. Expectations must be handled over finite demand histories, and costs can be infinite for general policies.
The goal also contains the existence of an optimal policy for the -period model. The paper cites this from Scarf and Zabel rather than proving it. Applying Lemma 3 or 4 yields an optimal policy whose later periods are no longer of form. Restoring the form requires the dynamic-programming principle of optimality together with the -convexity argument.
The Lean model (VeinottWagnerSS.Bounds.Model) uses the reduced model of Eq. (2): G : ℤ → ℝ is a primitive, and , and do not appear. Stock levels are integers and demands are natural numbers; the demand law is a PMF ℕ with finite mean. A policy is Y : (t : ℕ) → ℤ → (Fin t → ℕ) → ℤ: period 's level as a function of and the first demands, so it cannot see current or future demand. Periods are numbered from in Lean. Expectations are sums over demand histories weighted by . is the difference of the expectations of the positive and negative parts, and is valued in EReal. Under the standing assumptions is bounded below, so the negative part is finite and no arises. Both and are allowed.
The bounds SLow, SHigh, sLow, sHigh are infima of the sets in (21)–(23); a milestone proves they are the least elements. A trivializing formalization is ruled out as follows. Optimality is over all admissible policies and for every . The bounds are the least integers of (21)–(23). The goal requires an optimal policy, not only a bounded pair. Existence of an optimal policy is proved, not assumed.
Printed statements corrected. Lemma 4 as printed has no hypothesis on . Its proof begins "By lemma 3 we may assume that ", and without that assumption need not be an rule. The Lean statement adds . The last display of the proof of Lemma 5 reads where is meant; this affects only the proof. The milestone texts are verbatim.
Useful contributions include lemmas on convex functions on (monotonicity on either side of a minimizer), expectation lemmas for sums over Fin t → ℕ, and the finite-horizon principle of optimality for this model.
How many times can points and lines in the plane meet? The question is the prototype of incidence geometry, and the answer controls a long list of problems in discrete and computational geometry: the number of lines rich in points, the number of distinct distances or unit distances among points, the complexity of arrangements, and sum–product estimates in additive combinatorics. Erdős asked for the order of magnitude when and conjectured that the answer is ; Erdős and Purdy asked for the matching bound on the number of lines containing at least of the points.
Szemerédi and Trotter settled both questions in Extremal Problems in Discrete Geometry (Combinatorica 3 (1983) 381–392, doi:10.1007/BF02579194). Their principal theorem bounds the number of point–line incidences by over the whole range , and the same paper derives from it the Erdős–Purdy bound on -rich lines, a version of Dirac's conjecture (proved independently by Beck, Combinatorica 3 (1983)), and a bound on the number of sequences of line densities.
Timeline.
Work in the Euclidean plane , written Plane in the Lean development. A line is an affine subspace whose direction space has dimension one (IsLine l). Let be a finite set of points and a finite family of distinct lines. The number of incidences is
written incidences P L. The degree of a point is the number of lines of through it (degree L p), and the density of a line is the number of points of on it (density P l); so .
For the covering lemma, coordinate axes are fixed and a square is a closed axis-parallel square with side (closedSquare (a, b, s)); its interior is the open square (openSquare). A square contains the points of in the closed square, and a family of squares covers the points lying in at least one of them.
There is an absolute constant such that for every finite point set with and every finite family of distinct lines,
The goal leaves unspecified. The paper's proof gives , and later proofs give much smaller values; any improvement of the constant still proves this statement.
The result. The bound is sharp up to the constant throughout the range , as integer-grid configurations show. Outside that range the trivial bounds and take over. Theorem 1 is the source of the bound on -rich lines (the paper's Theorem 2), of Beck's theorem (Theorem 3), and, through them, of the unit-distance bound , of the Elekes sum–product estimate and of many algorithmic bounds on arrangements. It is the first nontrivial case of the polynomial-partitioning incidence theory developed since 2010.
Formalizing it. The theorem has been proved, and reproved in several ways, for four decades. To the best of the mission's knowledge Mathlib has no statement of it, of the crossing lemma, or of any point–line incidence bound in the Euclidean plane. This mission produces a checked statement of the theorem with lines as genuine one-dimensional affine subspaces and an absolute constant. It also produces checked statements of the auxiliary facts the 1983 proof uses. A complete proof may follow the original argument, the cutting argument or Székely's crossing-lemma argument; any of them closes the goal.
Counting pairs of lines through common points (milestone 1) gives only , and its dual gives . These Cauchy–Schwarz bounds use only the fact that two lines meet at most once, a property shared by lines in finite projective planes, where the incidence count genuinely reaches order . Any proof of the bound must therefore use a property of the real plane that the finite geometries lack: order, continuity, or the planarity of drawings. Szemerédi and Trotter use it through a covering lemma for axis-parallel squares, whose proof is only cited in the paper ([7]). The remaining difficulty is keeping the constants of a multi-stage minimal-counterexample argument under control.
The plane is EuclideanSpace ℝ (Fin 2). A line is an AffineSubspace ℝ Plane whose direction has Module.finrank equal to . Every statement requires IsLine of each member of , so neither the whole plane nor a single point counts as a line. The points form a Finset Plane and the lines a Finset (AffineSubspace ℝ Plane), which makes the lines distinct. Incidences, degrees and densities are Finset.filter cardinalities under classical decidability. Powers , are Real.rpow of the counts cast to , and is Nat.choose.
In the goal, the constant is quantified before the points and the lines. The form "for every configuration there is a " is trivially true (take ) and is not this theorem. Both ends of the range are kept exactly: without the lower end, a single line through collinear points has incidences, more than for large .
The goal follows the wording of p. 381 ("at most"). The restatement on p. 383 says "less than", which fails at and is equivalent for after doubling . The covering lemma is stated with the added non-degeneracy hypotheses . As printed it fails when (no square can hold points), and when with .
A full development needs a real-plane incidence toolkit: a crossing lemma or a cutting lemma, or the covering lemma with its quadtree proof. That toolkit is reusable for -rich lines, Beck's theorem, unit distances and sum–product bounds, and contributions of such infrastructure as separate theorems are welcome. The three numerical milestones are self-contained real-analysis exercises.
The security of the RSA cryptosystem rests on the assumed difficulty of factoring large integers, and the best known classical algorithms for factoring run in super-polynomial time. In 1994 Peter Shor showed that a quantum computer can factor an -digit integer in time polynomial in (Shor, SIAM J. Comput. 1997; conference version FOCS 1994). The algorithm has two parts. A classical reduction, due to Miller (1976), turns factoring into order finding: given coprime to , find the least with . The quantum part solves order finding.
This mission formalizes the quantum part as Shor analyzes it in §5 of the journal paper: the construction of the quantum state, the probability of each measurement outcome, and the classical post-processing that reads off the measured value. The paper's claim is that one run of this procedure returns with probability at least .
Timeline:
Fix an integer and an integer coprime to . Its order is the least with ; since is a unit, . Let be the power of with .
A quantum state on two registers, the first holding and the second a residue , is a complex vector indexed by the basis states . Measuring it returns with probability .
The Fourier matrix is the matrix with entries , with rows indexing inputs and columns outputs. The algorithm
The observed gives us if some fraction with lowest-terms denominator below is within of , and every such fraction has lowest-terms denominator exactly . In the Lean development these objects are preFourierState, finalState, outcomeProb and yieldsOrder, in the namespace ShorAlgorithms.OrderFinding, and the shared definition ShorAlgorithms.Shared.fourierMatrix.
For all sufficiently large , with , and as above,
where is the state (5.4). The threshold on is uniform in and ; it is the paper's "for sufficiently large " from the per-state bound.
The goal is the quantitative statement behind "order finding is in bounded-error quantum polynomial time": since for a constant (Hardy and Wright, Thm. 328), repetitions find with high probability, and Miller's reduction then factors . Without the bound, the algorithm is a procedure with no guarantee.
The result is proved, in the paper and in textbooks (Nielsen and Chuang, 2000, §5.3), usually with a phase-estimation analysis rather than Shor's direct count. What this mission adds is a machine-checked proof of Shor's own argument, with his choice of and his constants, starting from the state built by applying to (5.2). Formal proofs of idealized versions exist elsewhere, for instance in the exact-period model where divides and the output is uniform on peaks, but that model removes the approximation that the bound is about. Legendre's theorem on continued fractions is already on the platform (FamousTheorems.legendre_continued_fraction_theorem) and is included as a reference item.
The obvious route is to compute the output distribution in closed form. That works only when divides ; here is a power of and is arbitrary, so the amplitudes are geometric sums of terms whose phases do not cancel exactly. The per-state bound requires a lower bound on such a sum that is uniform in , and , with error terms of order controlled against a main term of order . The constant leaves only a small margin below the limiting value , so the errors must be bounded explicitly, not merely shown to vanish.
The second difficulty is the counting: distinct coprime numerators must give distinct outcomes in , and each good must determine uniquely, which uses and .
Conventions the statements commit to:
Fin q × ZMod n → ℂ; the matrix convention is row = input, so applying to the first register gives the amplitude at .orderOf (x : ZMod n). enters through the three hypotheses , , , not through a function of .Rat.den.Typing the closed form (5.4)–(5.6) in as the definition of the final state would make milestone 1 trivial and hide whether the probability model is the paper's; the definitions exclude this by construction.
Not stated: the polynomial running time of any step, the repetition count (no explicit constant), the reversible modular exponentiation of §3, and the post-processing heuristics on p. 1501. Needed infrastructure: bounds on geometric exponential sums, Euler's totient, Diophantine approximation by fractions with bounded denominator, and Mathlib's continued fractions. Lemmas on geometric sums of roots of unity and on the order of units mod are reusable in the companion discrete logarithm mission.