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.
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?
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).
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.
In 1998 Smale listed eighteen problems for the twenty-first century; the eighteenth asks: What are the limits of intelligence, both artificial and human? (Smale 1998). The paper of Acharjee and Gogoi (arXiv:2310.10792) proposes a mathematical model of a mind, the cognitive-consequence space, built from a Tarski consequence operator, and claims that two theorems about this model (its Theorems 3.3 and 3.4) show that "human intelligence is limitless" (Discussion, p. 22; Conclusion, p. 23).
This mission records that model and its results in Lean 4 exactly as stated, so that each claim becomes a checkable statement: proved, or refuted, by the verifier rather than by argument.
A cognitive-consequence space is a set of mental representations (thoughts) with a consequence operator and an implication connective satisfying Tarski's axioms as listed in the paper (p. 5):
together with the paper's standing assumption (p. 5, after Definition 3.2).
A set is deductive if . The cognitive-consequence topology is
and members of are consequence-wise open (CWO). The cognitive closure is the intersection of all deductive sets containing .
Separately, a cognitive similarity distance is a function together with a relation (" and cognitively coincide") such that , is symmetric, , and the triangle inequality holds. A sequence of thoughts converges to if for every we have for all large .
For every cognitive-consequence space,
Theorems 3.1, 3.2, 3.3, 3.5, 3.6, 3.7 and Corollary 3.5 (the topology and the cognitive closure), Theorems 3.8 and 3.12 (cognitive limits), Theorem 4.3 (the filter ) and Theorem 5.1 (Gödel's incompleteness black hole).
The paper presents the goal as its answer to the human-intelligence half of Smale's eighteenth problem. A machine-checked verdict on the goal settles whether that conclusion follows from the paper's own axioms. The milestones are the paper's structural results about , cognitive closure and cognitive limits.
Status: to the best of current knowledge none of these results has a published machine-checked proof. The first conjunct of the goal (Theorem 3.3) follows from the standing assumption . The second conjunct (Theorem 3.4) is not implied by the listed axioms as formalized: the consequence operator with for every , on a one-point language, satisfies all of them and has . The goal is therefore expected to be resolved by a disproof.
The content of the goal is the existence of a nonempty CWO set, equivalently of a deductive set different from (a consistent theory). The paper's argument for Theorem 3.4 derives and calls this a contradiction; nothing in the axioms forbids it.
CogCons.CognitiveConsequenceSpace C bundles , the connective imp, axioms (i)–(vi) and . The syntax and interpretation of the paper are not modelled beyond imp.CogCons.CognitiveSimilarityDistance C is independent of ; sequences are indexed by starting at ; is an arbitrary relation constrained only by the listed axioms.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 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 .Two-stage stochastic integer programs combine the two hardest features of mathematical programming: uncertainty in the data and integrality of the decisions. Even evaluating the objective of such a program at a single first-stage decision requires the expected optimal value of an NP-hard combinatorial problem. Chapter 8 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by A. H. G. Rinnooy Kan and L. Stougie, argues that for many such problems the way forward is probabilistic analysis: the random optimal value of the second-stage problem often converges, after normalization, to a simple function of the problem parameters, and that function can replace the intractable expectation.
The chapter illustrates this on the machine investment problem: first buy identical machines at cost each, knowing only the distribution of the processing times of jobs, then schedule the jobs once their processing times are revealed so as to minimize the makespan. This mission formalizes the chapter's analysis of that example: the almost sure asymptotics of the optimal makespan (8.13), its expectation version, and the asymptotic clairvoyance of the resulting two-stage heuristic.
Let be processing times: independent, identically distributed, nonnegative random variables on a probability space with mean and finite second moment . The instance with jobs uses the first of them.
An assignment of the jobs to identical machines is a map . The load of machine is and the makespan of is its largest load. The minimum makespan is
and the machine investment problem is to minimize over integers (8.9).
List scheduling takes the jobs in the order and assigns each to the first available machine, a machine of least current load (lowest index on ties). Its makespan is . Write and .
For §8.3, the estimate is minimized over integers by the heuristic first-stage decision , the better of and . A clairvoyant decision maker who sees the processing times first chooses minimizing .
For machine counts with ,
The machine count is allowed to grow with ; this is the regime the first-stage heuristic lives in, since is of exact order .
where is the list-scheduling makespan.
Result (8.13) says that the optimal value of an NP-hard problem, rescaled, is almost surely asymptotic to the elementary function of the data and the first-stage decision. Its expectation version replaces the intractable term in (8.9) by , and the clairvoyance statement shows that the heuristic built on that replacement loses asymptotically nothing, not even against a decision maker with full information. The chapter presents the example as the template for vehicle routing and location problems preceded by an investment decision.
All results here are classical and proved in the literature cited by the chapter (Lemma 8.1 is quoted from Feller without proof; the chapter refers to Dempster et al. for the asymptotic optimality of the two-stage heuristic and to Lenstra et al. for the notion of asymptotic clairvoyance). None of them has, to our knowledge, a machine-checked proof. The mission produces a formal model of identical-machine makespan scheduling and of list scheduling, the extreme-value estimates of Lemma 8.1 for square-integrable i.i.d. sequences, and the full chain from the strong law to (8.13).
The deterministic part is elementary on paper, but list scheduling is a recursively defined procedure, and its makespan bound has to be established for that recursion rather than for a picture like the chapter's Figure 8.3. The probabilistic core is Lemma 8.1: the strong law controls , but the error term is of order once grows like , and the strong law says nothing about maxima. With a fixed number of machines the whole statement would reduce to the strong law; the growth is exactly where the second moment is needed. For the clairvoyance statement, the clairvoyant choice is a random, unstructured minimizer, so its value must be bounded below without knowing where the minimum is attained.
Processing times are one sequence p : ℕ → Ω → ℝ, 0-based (the book's is p (j-1)), with each p j measurable, the family mutually independent (iIndepFun), identically distributed with p 0, pointwise nonnegative, p 0 ^ 2 integrable and ∫ p 0 = μ with μ > 0. Nonnegativity and are not printed in the book; they are implicit in "processing times" and in the division by . Machines are Fin m; a schedule is an assignment Fin n → Fin m, which is faithful because jobs are non-preemptive, machines identical and there are no precedence constraints.
The book writes ""; this is read as a function of with and (fun n => (m n : ℝ)) =O[atTop] (fun n => √n). Stating (8.13) for a fixed would trivialize it into the strong law and is ruled out. "" means that almost surely the limit exists and equals . Expectations are Bochner integrals of functions that are measurable and bounded by , hence integrable. List scheduling uses the index order and breaks ties towards the lowest machine index; both are admissible instances of the book's "arbitrary fixed order" and "first available machine". In the clairvoyance statement the minimum is over (the book writes ; no machine cannot process any job, and the Lean value is an empty-infimum convention). No explicit constants replace an O(·): the statements are limits and the O-hypothesis is carried as stated.
Out of scope: (8.14) and the p. 210 expectation statement, which need a positive density at and whose proof the book calls "far from easy", and the dynamic programming recursion of §8.3.
Needed infrastructure: finite maxima and minima of measurable functions, extreme-value estimates for square-integrable i.i.d. sequences (Lemma 8.1), and Mathlib's strong law. The makespan and list-scheduling definitions are reusable for other identical-machine scheduling results; alternative proofs of Lemma 8.1 and sharper forms of the clairvoyance statement are welcome.
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.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.
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.
The Smale horseshoe is the standard example of a smooth invertible map of the plane with chaotic dynamics. Smale introduced it in the 1960s as the mechanism behind the complicated orbits near a transverse homoclinic point, and it became the basic model of hyperbolic invariant sets (Smale 1967). Its importance for differential equations is the Smale–Birkhoff theorem: whenever the stable and unstable manifolds of a hyperbolic fixed point intersect transversally, some iterate of the map contains a horseshoe. Melnikov's method then turns this into a checkable criterion for chaos in periodically forced planar systems such as Duffing's equation.
This mission formalizes the horseshoe as it is treated in Chapter 13 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012). It takes along the one-dimensional results from §§11.4–11.5 that the chapter's argument reuses: the tent map's Cantor set, the one-sided shift, and the metric on two-sided sequences.
Fix parameters and and let . The two horizontal strips
are mapped by
Each strip is contracted horizontally by and stretched vertically by into a vertical strip crossing . The book specifies only on and leaves the fold between them to a picture. A horseshoe map here is any given by these formulas on . On and the inverse is given by explicit formulas.
The tent map on has the invariant set
The second coordinate of is and the first coordinate of is . The horseshoe's invariant set is
The two-sided shift space is . It carries the metric
and the shift . The itinerary of a point of records, for , which strip contains . For it records which strip contains .
A system is chaotic in the book's sense (p. 296) under four conditions: is continuous, is infinite, is topologically transitive (for nonempty open some meets ), and the periodic points are dense. A Cantor set is a compact, perfect, totally disconnected set.
For , and every horseshoe map :
The book's sentence is: "The Smale horseshoe map has an invariant Cantor set on which the dynamics is equivalent to the double sided shift on two symbols. In particular it is chaotic."
Theorem 13.1 exhibits a two-dimensional invertible system with an explicit invariant set on which the dynamics is exactly the two-sided shift. Every property of the shift is then inherited:
Theorem 13.1 is the model to which the Smale–Birkhoff theorem (13.2) reduces the dynamics near a transverse homoclinic point. It is therefore the terminal object of the book's route from Melnikov integrals to chaos in forced oscillators.
The results are classical and fully proved in the literature. Their proofs have not been formalized. Mathlib has Cantor-type sets (the middle-thirds set), totally disconnected and perfect sets, and product topologies. It has no tent-map invariant set, no two-sided symbolic dynamics with the book's metric, and no conjugacy theorem of this kind. A formal proof would supply a machine-checked conjugacy between a concrete planar map and a full shift, together with the symbolic-dynamics layer it rests on.
The book's own argument for Theorem 13.1 has two gaps that a formal proof must fill. First, it asserts that a product of two Cantor sets is again a Cantor set and leaves this as an exercise. Second, it treats continuity of the itinerary map and of its inverse as an exercise. It also leans on "all other results hold with no further modifications" to transfer the one-sided lemmas (11.7–11.9) to the two-sided shift.
The two-sided transfer is not literally a restatement. The metric (11.35) weights each off-centre index by , and so the one-sided closeness estimate does not carry over verbatim; see the correction to Lemma 11.15 below.
The inverse must also be tracked alongside . The negative half of the itinerary is defined through rather than through , so the conjugacy at index couples the two halves.
Finally, the parameter endpoints need care. The book allows and . At the defining formulas are inconsistent on , and at either endpoint one factor of is the whole interval .
IsHorseshoeMap λ μ F is a predicate fixing only on , and the goal quantifies over all such . Its conclusion therefore cannot depend on how the fold is drawn. The inverse horseshoeInv is the explicit formula (13.5)–(13.6).ℝ × ℝ; its max-distance has the Euclidean topology. Sequence spaces are ℕ → Fin N and ℤ → Fin N. The metrics (11.28) and (11.35) are functions symDist and symDistZ, not type-class instances. Density and continuity are stated in – form against them, so no unmentioned product topology enters.Preperfect and IsTotallySeparated, the last being the book's definition of total disconnectedness on p. 302. is constructed as in (13.8) and as in (13.9), not quantified over. The goal asserts the full conjunction, so it cannot be discharged by exhibiting some other invariant set or some other conjugacy. For maps satisfying IsHorseshoeMap exist, so the hypothesis is not vacuous.
A complete development needs:
The tent-map and one-sided shift lemmas duplicate those of the interval-maps mission of this series and are reusable there. Contributions proving the two-sided analogues of Lemmas 11.7–11.9 as auxiliary lemmas are welcome.
Scheduling tasks on machines owned by self-interested parties is the running example of Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001), the paper that introduced the study of mechanisms whose allocation rule is an algorithm with a computational objective. Each machine (agent) privately knows how long it needs for each task; the designer wants to minimize the make-span, the completion time of the last machine, and can only influence the agents through payments.
Without further information the designer is in a weak position: the paper shows that no mechanism approximates the optimal make-span within a factor below 2 (Theorem 4.6), and that the natural truthful mechanism, MinWork, only achieves a factor . Section 5 of the paper observes that in many applications the designer learns more than the agents' reports: it can pay after the work is done and observe how long each task actually took. It introduces mechanisms with verification and shows that, with this extra information, the make-span can be minimized exactly by a strongly truthful mechanism. This mission formalizes that result, Theorem 5.1, together with the steps of its proof and the participation variant, Theorem 5.4.
There are tasks and agents. The type of agent is the vector of positive numbers, being the least time in which agent can perform task . An allocation gives each task to one agent; is the set of tasks of agent . For a type vector and for a vector of actual execution times the make-spans are
A mechanism with verification is a pair . The allocation is computed from the agents' declarations only. Each agent then performs its tasks, in any times it chooses, and the mechanism pays agent the amount , which may depend on the declarations and on the observed actual times. Agent 's utility is . A strategy of agent therefore has two parts: a declaration and an execution plan that says, for every allocation, how long the agent takes on each of its tasks.
A strategy is dominant if it maximizes the agent's utility against all declarations and all execution plans of the other agents. The mechanism is truthful if, for every agent and type, declaring the true type (with a suitable execution plan) is dominant, and strongly truthful if the only dominant strategy is to declare the true type and to execute every task in minimal time.
The Compensation-and-Bonus mechanism uses an optimal allocation algorithm and pays
where the corrected time vector lists agent 's own tasks at their actual times and every other task at the time declared by the agent it was given to.
For agents and every optimal allocation algorithm (ties broken arbitrarily), the Compensation-and-Bonus mechanism is a strongly truthful implementation of task scheduling:
For there is a strongly truthful mechanism with an optimal allocation algorithm that satisfies participation constraints: an agent that performs its tasks in its declared times never ends with negative utility.
The result. Theorem 5.1 shows that the lower bound of 2 for task scheduling (Theorem 4.6) is an artefact of the information structure, not of incentives as such: once execution times are observable, the exact optimum is achievable in dominant strategies, and the agents have a unique rational behaviour. The construction also isolates a general principle, used again in §5.6 of the paper: an agent paid by the global objective value, computed with the others' declarations, has the designer's incentives. Theorem 5.4 shows that the bonus can be shifted to make participation individually rational, which the plain mechanism violates (its bonus is negative).
Formalizing it. The theorem is proved in the paper, in a few lines, and has no machine-checked version. A formalization has to settle what the paper leaves informal: what a strategy with an execution part is, over which strategies of the others dominance is quantified, what "the only dominant strategy" demands of the execution plan on allocations that seem never to arise, and which hypotheses on the number of agents the uniqueness needs. The model built here is also the base of two companion missions of the same series (Compensation-and-Bonus with a non-optimal allocation algorithm, and the rounding mechanism with verification).
Truthfulness (milestones 1–4) is short once the model is right. The difficulty is uniqueness. For a misreport or a slow execution to be excluded, one must exhibit, for every alternative strategy, declarations of the other agents under which that strategy is strictly worse. The declarations must be positive, the optimal allocation algorithm breaks ties arbitrarily, and agent 's slower execution only hurts it when agent is the bottleneck. The paper's proof dismisses this step with "clearly, … there are circumstances"; the naive reading ("the others declare elsewhere") is not available in a model with finite positive times, and the uniqueness clause must also cover the execution plan on every allocation, not only on the allocation produced by truthful play.
Fin n, tasks Fin k, allocations functions Fin k → Fin n; both make-spans are Finset.sup' over the nonempty set of agents ([NeZero n]).>=; Theorem 5.4 prints "strongly truthfulmechanism"; Definition 28 writes for .Welcome contributions: proofs of the milestones, the uniqueness witnesses as reusable lemmas, and the contribution-based mechanism behind Theorem 5.4. Theorem 5.3 (generalized Compensation-and-Bonus) is not stated in this mission.
Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) asks how well a computational task can be carried out when its inputs are held by self-interested agents who may lie about them. Their test case is scheduling on unrelated machines: tasks must be assigned to agents (machines), each agent privately knows how long it needs for each task, and the planner wants to minimize the time at which the last agent finishes. The paper shows that the mechanism MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is truthful and loses a factor of at most against the optimum, and that no truthful mechanism can do better than a factor . It then conjectures (Conjecture 4.9) that the factor cannot be improved by any truthful mechanism.
That conjecture became the Nisan–Ronen conjecture, one of the central questions of algorithmic mechanism design. A sequence of papers raised the general lower bound from to (Christodoulou, Koutsoupias and Vidali), to (Koutsoupias and Vidali) and to larger constants, and Christodoulou, Koutsoupias and Kovács (STOC 2023) finally proved the conjecture for all deterministic truthful mechanisms. In the original paper, Nisan and Ronen confirm the conjecture for two restricted classes of mechanisms, with short direct arguments. This mission concerns the second class, local mechanisms (Theorem 4.12).
There are tasks and agents . A type vector records, for every agent and task , the positive time agent needs for task . An allocation assigns every task to one agent; is the set of tasks of agent . For a set of tasks write . The make-span of is .
A direct mechanism asks every agent for its type, computes an allocation from the declarations, and hands agent the payment . Agent 's utility is measured with its true times. The mechanism is truthful if declaring the true type maximizes each agent's utility whatever the other agents declare. The allocation rule is a -approximation if for every type vector and every allocation .
For a truthful mechanism the payment to agent depends only on the set it receives and on the declarations of the others (Proposition 4.4). This gives the price offered to agent for a set (Definition 12):
A mechanism is local (Definition 14) if depends only on the other agents' times on the tasks of . MinWork is local: its price for is .
For every , every and every real , no truthful local mechanism is a -approximation:
The bound holds for every , so together with MinWork it shows that is the exact best ratio for local truthful mechanisms.
The result. Theorem 4.12 settles the Nisan–Ronen conjecture for a natural class of mechanisms. Locality captures the mechanisms in which the price for a bundle of tasks is set only by the competition for those tasks. It includes MinWork and, more generally, every mechanism that prices tasks separately using the other agents' bids on them. The theorem says that for this class the trivial per-task auction is already optimal, so any improvement over the ratio must use prices that depend on the other agents' times on tasks outside the bundle.
Formalizing it. The statement is not open: it follows from the 2023 proof of the Nisan–Ronen conjecture, and Nisan and Ronen's own argument is much shorter. That argument is a sketch, though. Lemma 4.13 rests on an informal measure-theoretic appeal, and the core claim relies on a maximization property stated over all sets of tasks. A machine-checked proof pins down exactly which properties of truthful mechanisms the short argument needs. None of these results is known to have been formalized. The definitions (type vectors, truthful mechanisms, prices, locality) are shared with the other missions of this series.
An argument that looks at one agent at a time does not go through. Changing one agent's declaration changes the prices offered to every other agent, so an allocation that is stable for one agent can shift for another. The argument needs a type vector at which every agent's choice is strict, and only then can it lower times agent by agent and follow the allocation. Producing such a type vector is Lemma 4.13. The printed argument for it applies a "for almost every type vector" statement to sets defined by the price functions of an arbitrary mechanism, which need not be measurable. A proof must therefore work without any regularity of the mechanism. A second difficulty is Definition 12's convention that a set the agent cannot obtain has price . Locality constrains these zero prices too, and the argument has to account for sets that are obtainable at one type vector and not at a nearby one.
Agents are Fin n, tasks Fin k. An allocation is a function Fin k → Fin n, a type vector is Fin n → Fin k → ℝ, and a mechanism is a pair of functions alloc (declarations to allocation) and pay (declarations to the payment handed to each agent). Utilities are quasi-linear. All types, declarations and misreports are positive, and every truthfulness, locality and approximation quantifier ranges over positive type vectors. The make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]).
Conventions and explicit thresholds:
Fin n → Fin k → ℝ, the sup norm. No measurability of the mechanism is assumed.Ruled-out trivializations: locality is not restricted to single tasks; the goal does not assume that maximizers are unique at every type vector (that is Lemma 4.13's conclusion at one point, not a hypothesis); and the bound holds for every , not for some.
Needed infrastructure: finite sums over allocation fibres, sup norms on function spaces, and a genericity argument for finitely many affine functions (Lemma 4.13). The model file and the price and locality definitions are reusable in the other missions of the series. Proofs of individual milestones are welcome independently.
Algorithms deployed on the Internet often take their inputs from parties who own them and who may lie when lying pays. Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) proposed studying optimization problems in this setting: the algorithm designer may hand out payments, and must guarantee that the intended output is produced when every participant acts in its own interest. The paper's central test case is scheduling on unrelated machines, a standard problem of combinatorial optimization, in which the machines are the selfish participants and only they know how long each job takes them.
For this problem the paper shows that incentives cost a factor of two at least: with two or more machines, no mechanism can guarantee a make-span below twice the optimum. This was the first lower bound separating what incentive-compatible mechanisms can achieve from what ordinary approximation algorithms can achieve, and it started a line of work on the "Nisan–Ronen conjecture" (that the right factor for machines is ), with improved lower bounds by Christodoulou, Koutsoupias and Vidali (Algorithmica, 2009) and by Koutsoupias and Vidali (Algorithmica, 2013), and a resolution announced by Christodoulou, Koutsoupias and Kovács (STOC 2023).
There are agents (machines) and tasks . Agent 's private type is the vector of positive real numbers, being the time agent needs for task ; a type vector is . An allocation assigns every task to one agent; is the set of tasks given to agent . For a set of tasks write . The objective is the make-span
and an allocation rule is a -approximation if its make-span is at most times that of every allocation, on every type vector.
A mechanism gives each agent a set of strategies. On a strategy profile it outputs an allocation and hands agent a payment . An agent of type has utility . A strategy is dominant if it maximizes the agent's utility whatever the others play. The mechanism implements a -approximation if every agent of every type has a dominant strategy and every profile of dominant strategies yields a -approximate allocation.
A direct mechanism has equal to the set of types, and is truthful if reporting the true type is dominant. For a truthful mechanism, the price is the payment agent receives when, against the others' reports , some report of its own makes it receive exactly (and if none does); the price difference is .
For every , and , no mechanism with any strategy sets implements a -approximation:
The result. Theorem 4.6 shows that the requirement of dominant-strategy incentive compatibility, by itself, rules out approximation ratios below for scheduling on unrelated machines, a problem for which polynomial-time -approximation algorithms that ignore incentives exist (Lenstra, Shmoys, Tardos 1990) and for which the exact optimum is computable in exponential time. Combined with the MinWork mechanism of the same paper (an -approximation), it determines the optimal ratio for two machines. It is the base case of the Nisan–Ronen conjecture and the prototype of the "characterize truthful mechanisms by prices" technique used throughout later work on the conjecture.
Formalizing it. The theorem has been proved since 1999, but no machine-checked version is known to exist. The mission produces a formal account of general mechanisms with arbitrary strategy sets, dominant-strategy implementation, the revelation principle in that generality, and the price characterization of truthful mechanisms (independence and maximization). These are reusable for every other lower bound in this paper and for the later literature on the conjecture.
The statement quantifies over all mechanisms, with arbitrary strategy sets and arbitrary payment functions, so no finite search settles it. The revelation principle reduces to truthful direct mechanisms, but even these are an infinite-dimensional family: the allocation rule may break ties in any way, and prices may be any functions of the other agents' reports.
The printed argument also has two places that need care. Proposition 4.5 and Lemma 4.7, as printed, range over all sets of tasks, while Definition 12 gives unattainable sets price ; the statements hold only over attainable sets, and are formalized that way. And the case where agent 2's bundle has odd size is dispatched in one sentence ("which still yields the same allocation"), which the preceding lemma does not justify when agent 2's best bundle at the perturbed prices is not unique. A complete formal proof of the goal must supply an argument for that case.
Fin n, tasks Fin k; an allocation is a function Fin k → Fin n; bundles may be empty. The make-span is a finite maximum and assumes (NeZero n).A : Fin n → Type u (any universe), output and payments on dependent strategy profiles. Implements requires both that every agent of every positive type has a dominant strategy and that every profile of dominant strategies yields a -approximate allocation. Dominance is against every profile of the others, not only dominant ones. Without the existence clause, a mechanism with no dominant strategies would implement vacuously; the definition excludes that.Contributions of any of the milestones are welcome, as are alternative proofs of the goal that avoid the terse odd case.
Most differential equations that model physical, biological or engineered systems cannot be solved in closed form, yet the question asked about them is usually qualitative: does the system settle down to an equilibrium, and does it stay near the equilibrium when perturbed? Liapunov's direct method answers that question without solving the equation, by exhibiting a function that does not increase along solutions. It is the standard tool of nonlinear stability analysis and of control design, where a controller is typically certified by a Liapunov function for the closed-loop system (Khalil, Nonlinear Systems).
A Liapunov function whose values strictly decrease along every non-constant solution gives asymptotic stability directly. In practice the natural candidate, often the total energy of a damped mechanical system, only satisfies a non-strict inequality. The Krasovskii–LaSalle invariance principle closes that gap: if the function is not constant along any complete orbit other than the equilibrium, the equilibrium is still asymptotically stable. It was established by Barbashin and Krasovskii (1952) and by LaSalle (1960, IRE Trans. Circuit Theory 7).
This mission formalizes Chapter 6 of Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version), from the local flow of an autonomous equation, through limit sets, to the principle itself.
Fix , an open set (the phase space) and a vector field of class . The autonomous system is . An integral curve is a differentiable map from an open interval into with for all .
For each there is a maximal interval and a unique maximal integral curve on with : every integral curve through at time is a restriction of it. The map on is the flow. It is a local flow: may be bounded, because solutions can leave or blow up in finite time.
The orbit of is and the forward orbit is ( with ). The -limit set is the set of with for some times in ; uses .
A point with is a fixed point. It is stable if every neighborhood of contains a neighborhood of such that solutions starting in exist and stay in for all . It is asymptotically stable if moreover as for all in some neighborhood of .
A Liapunov function at is a continuous on an open neighborhood of with , on , and for every integral curve and all with . It is strict if the inequality is always strict. denotes the connected component of containing .
Let be a fixed point and a Liapunov function at on . Write for: is not constant on any orbit lying entirely in , i.e. every with has points with . Then
and, under , every whose forward orbit lies in a compact subset of satisfies as .
In attack order: Theorem 6.1 (the maximal flow exists, is open, is on , and ); Lemma 6.3 (a forward orbit in a compact subset of forces ); Lemma 6.6 ( is then nonempty, compact and connected); Lemma 6.7 (); Theorem 6.15 (a function non-increasing along is constant on ); Lemma 6.11 (a closed is positively invariant); Lemma 6.12 ( and ); Theorem 6.13 (Liapunov: a Liapunov function makes stable).
The result itself. The invariance principle is the form of Liapunov's method used in applications. It gives asymptotic stability of damped mechanical systems from their energy, of gradient systems from their potential, and of adaptive and passivity-based controllers, where the natural Liapunov function is only non-increasing. Its limit-set formulation (Theorem 6.15) is also the entry point to the Poincaré–Bendixson theory of the next chapter, which uses the same -limit sets.
Formalizing it. Mathlib has local existence and uniqueness for ODEs and a theory of -limit sets for global flows (omegaLimit, Flow). It has no maximal solution of an ODE, no local flow with its maximal intervals, and no Liapunov stability theory. The results are classical and proved in the book; none has a machine-checked proof on this platform. This mission builds the local-flow and limit-set layer and the Liapunov layer on top of it.
The central difficulty is that the flow is local. The book's arguments pass freely between "the solution stays in a compact set" and "the solution exists for all positive time" (Lemma 6.3). In a formal setting every statement about must first establish , and the maximal interval must be constructed from local solutions. Theorem 6.1 on its own requires gluing local solutions into a maximal one and proving that the domain is open with dependence on initial conditions.
A common first idea is to assume the vector field is complete, so that Mathlib's global Flow and omegaLimit apply directly. That assumption is not available: the goal concerns orbits that stay in the neighborhood , and completeness of such orbits is a consequence of the argument, not a hypothesis. Similarly, is only continuous, so a derivative-based criterion cannot replace condition (6.36).
The state space is EuclideanSpace ℝ (Fin n), so is the Euclidean norm, and is the open ball Metric.ball. The standing assumption , , open, is a binder of every theorem (as ContDiffOn ℝ 1 f M, the weakest case, and for general in Theorem 6.1). The flow enters as a pair (I, Φ) satisfying IsMaximalFlow f M I Φ, which characterizes the maximal integral curves uniquely. Theorem 6.1 proves that such a pair exists, so no completeness or extra regularity is assumed. The two time directions of Lemmas 6.3–6.7 are one statement with a real parameter σ = 1 ∨ σ = -1. The -limit set contains only points of , as in the book.
Stability conclusions include existence of the solution for all . The Liapunov condition quantifies over every integral curve and constrains only the two endpoint values, exactly as (6.36). is a total function whose values off are never read.
Correction to the printed statement. The book's final sentence of Theorem 6.14, "every orbit lying entirely in converges to ", is false as printed. With and a strict Liapunov function, some orbits escape to infinity (Khalil, §4.1). The goal therefore asks for convergence of every forward orbit contained in a compact subset of , which is what the book's argument uses. The other two parts are as printed.
A trivializing formalization is ruled out: stability and asymptotic stability are stated for the maximal flow, with existence for all required, and not for an arbitrary map Φ or a flow assumed global. Asymptotic stability keeps both conjuncts, stability and attraction.
Needed infrastructure: maximal solutions of autonomous ODEs and their continuation (reusable across Chapters 6–13), openness of and smooth dependence on initial data, compactness arguments for limit sets, and connected components of sublevel sets. Contributions of the local-flow layer as standalone lemmas are especially welcome, since later missions of this series rely on the same objects.
Almost every quantitative statement about an ordinary differential equation, from the stability of an equilibrium to the existence of a periodic orbit, presupposes that the equation has a solution through each initial point and, usually, that this solution is unique and depends continuously on the data. Chapter 2 of Gerald Teschl's graduate textbook Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012) establishes these facts for first-order systems in . It is the foundation for the rest of the series: the flows, limit sets, Poincaré maps and invariant manifolds of later chapters are all built on the existence, uniqueness and extension results proved here.
A short history. Local existence was first proved in the nineteenth century by polygonal approximation (Cauchy) under differentiability-type hypotheses. Lipschitz isolated the condition that bears his name. Picard and Lindelöf established existence and uniqueness by successive approximation, and Banach (1922) abstracted the argument into the contraction principle. Peano (1890) showed that continuity of the right-hand side alone suffices for existence, without uniqueness. Gronwall's inequality and its integral generalisations give the continuous dependence estimates. Teschl's chapter presents all of these in a uniform notation.
An initial value problem (IVP) is
where is a continuous map from an open set to and . Here is the Euclidean norm on . A solution on an interval is a function whose graph lies in and which is differentiable on (one-sidedly at an endpoint that belongs to ) with . Such a solution is automatically continuously differentiable.
The function is locally Lipschitz in the second argument, uniformly with respect to the first, if for every compact there is a constant with whenever (the book's (2.18)).
For let , where , let , and define the existence time
The chapter also works in a real Banach space , a complete normed real vector space, where a contraction of a closed set is a map with for some .
If is continuous on and , then there is a function with solving
and the analogous statement holds on with . No Lipschitz condition is assumed and the solution need not be unique.
Peano's theorem is the existence statement with the weakest regularity hypothesis on in the classical theory. It is what lets one speak of solutions of equations with non-Lipschitz right-hand sides, such as , and it is the starting point for the theory of non-unique solutions and differential inclusions. The explicit existence time is the quantitative form used whenever one needs a uniform lower bound on the lifetime of solutions starting in a compact set. Picard–Lindelöf, Gronwall and continuous dependence together make the IVP well posed. The global existence theorem under linear growth is used throughout the later chapters to define global flows.
Mathlib already contains a Picard–Lindelöf theorem (IsPicardLindelof), Gronwall's inequality in differential form, the Banach fixed point theorem for complete (extended) metric spaces, and an Arzelà–Ascoli theorem for bounded continuous functions. It does not contain Peano's theorem, the integral form of the generalised Gronwall inequality with variable , Weissinger's theorem, or global existence under linear growth. The statements here are phrased in the book's setting: one-sided intervals, the convention for , local Lipschitz conditions on an open set, -valued functions. Connecting them to the existing Mathlib results is part of the work.
For Peano's theorem the obvious approach, Picard iteration, does not apply. Without a Lipschitz condition the integral operator need not be a contraction on any ball, its fixed points need not be unique, and a sequence of approximate solutions need not converge. Any argument has to produce a solution without a uniqueness mechanism and still reach the full interval that the theorem specifies, not merely some shorter one. On the formal side, derivatives relative to closed intervals, the corner of , and passing between the differential and the integral form of the IVP all need care.
For Theorem 2.17 the difficulty is that "every solution is defined on all of " is a statement about maximal solutions, and the book defines these only through a gluing construction. Without a Lipschitz condition that construction is no longer unique. An a-priori bound on alone does not give extension beyond a finite endpoint.
EuclideanSpace ℝ (Fin n), so is the Euclidean norm. The right-hand side is a total function ; hypotheses restrict attention to or . Banach spaces are real normed spaces with CompleteSpace.IsSolutionOn U f I x: for every , and has derivative at relative to . Initial conditions are separate hypotheses.IsGreatest {|f(p)| : p ∈ V} M. is if M = 0 then T else min T (δ / M). "Some interval around " in Theorem 2.2 is with , and "unique" means uniqueness on every interval containing . In Theorem 2.8 the suprema , of (2.41) become arbitrary constants , bounding the same quantities, which is equivalent because the bound is monotone in both; the case uses the limit . In Theorem 2.17 the constants are existential inside , so they may depend on but not on . "All solutions are defined for all " means that every solution on an open interval extends to a solution on .A complete development needs derivatives within intervals, interval integrals, uniform convergence and compactness in . The definitions IsSolutionOn and LocallyLipschitzSecond are reused throughout the Teschl series. Contributions that connect these statements to Mathlib's IsPicardLindelof, ContractingWith and BoundedContinuousFunction.arzela_ascoli are welcome.
This mission continues chapter 10's algorithmic account across its remaining two sections:
finishing the Iwata-Fleischer-Fujishige fixing algorithm for submodular minimization (§10.2.3's
tail), the steepest descent algorithm for L-convex function minimization (§10.3), and — the
capstone of chapter 10's account of the M-convex submodular flow problem (§10.4) — conjugate
scaling, the operation that finally makes the primal-dual algorithm run in polynomial time. As in
mission 34-ch10b-algorithms, most of this block's numbered results are asymptotic complexity
bounds; this mission places the results that are ordinary mathematical propositions.
The IFF fixing algorithm (mission 34-ch10b-algorithms) builds an acyclic graph D=(U,F)
and partition Z,H,Γ certifying the maximal minimizer of a submodular ρ once η≤0 (Eq.
(10.26)); this mission places the case-independent inequality its own legitimacy rests on, and
restates its correctness conclusion. The steepest descent algorithm for an L-convex function
g repeatedly minimizes the submodular set function ρ_p(X)=g(p+χ_X)-g(p) and moves to
p+χ_X for its minimal minimizer X (the tie-breaking rule (10.33)); this mission places the
resulting monotonicity fact and a domain-size bound for the L-convex adaptation.
Conjugate scaling replaces a dual-integral M-convex function's conjugate g with
g_α(p)=g(αp)/α, defining f⟨α⟩ via the resulting sup-formula (Eq. (10.77)) — a scaling
operation compatible with M-convexity where the naive ⌈f(·)/α⌉ is not.
For a dual-integral polyhedral M-convex function f (represented as the mixed real-primal/
integer-dual conjugate of an L-convex g), the conjugate scaling f⟨α⟩ is again
dual-integral M-convex, witnessed by g_α itself being L-convex, provided f⟨α⟩>-∞.
Chosen as goal: this is the fact the whole conjugate scaling algorithm — chapter 10's final and
most refined algorithm for the M-convex submodular flow problem — depends on, and the book's own
text singles it out as the "compatible scaling operation" that makes M-convex cost scaling work
where a naive approach provably does not.
Proposition 10.26 (the case-independent inequality underlying the IFF fixing algorithm's own
legitimacy) and Proposition 10.28 (that algorithm's correctness conclusion) close out mission
34-ch10b-algorithms's coverage of §10.2.3. Proposition 10.30 gives the steepest descent
algorithm's monotonicity property under its tie-breaking rule; Proposition 10.32 (found by direct
reading) bounds the L-convex adaptation's domain-size parameter in terms of the
original function's.
Conjugate scaling is chapter 10's demonstration that M-convexity, while a combinatorial rather
than a numeric-magnitude notion, still admits a genuine scaling technique compatible with its own
structure — completing the book's account of the M-convex submodular flow problem with an
algorithm whose polynomial running time depends on exactly this compatibility. Propositions
10.26/10.28 complete the correctness/legitimacy argument for the strongly polynomial submodular-
minimization algorithm mission 34-ch10b-algorithms began placing, and Propositions 10.30/10.32
are the analogous structural facts for L-convex function minimization, chapter 10's third major
algorithmic thread.
None of these results are open — they are Murota's own account of submodular-function- minimization (§10.2 continued), L-convex minimization (§10.3), and conjugate scaling (§10.4.5). What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Proposition 10.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).
As in mission 34-ch10b-algorithms, several numbered results in this block are excluded as
hard for being pure algorithmic-complexity bounds (Propositions 10.25, 10.27, 10.31); see
HARD.md. A further three (Propositions 10.37-10.39, on the primal-dual algorithm's maximum
submodular flow subproblem) are excluded for a distinct reason: the source text's own OCR
extraction demonstrably cannot distinguish the two visually different capacity-bound symbols
(c* overlined vs. underlined) central to their shared defining formula, confirmed directly
against the raw extracted bytes, making faithful reconstruction of that formula impossible from
the available text; see HARD.md.
Ground-set elements are a Fintype V with DecidableEq. All apparatus needed for Propositions
10.26/10.28 (Submodular, GammaSet, RhoTilde, ReachSet, Eta, IsMaximalMinimizer) is
redeclared fresh from mission 34-ch10b-algorithms, genericized over an arbitrary ground type
where the original was V-specific, since this draft cannot import that sibling. Proposition
10.26 is placed as the case-independent core inequality its own proof establishes, rather than by
replicating the three-case verification against Proposition 10.24's own internal proof objects
(Cases (i)-(iii)); see HARD.md. Proposition 10.30 omits its own trailing iteration-count
corollary (a pure complexity bound); see HARD.md. Six numbered results (Propositions 10.25,
10.27, 10.31, 10.37, 10.38, 10.39) are hard. Contributions completing any of the five sorrys
are welcome; the goal carries the most independent proof content (via the conjugacy theorem and
Theorem 7.10(2), both established elsewhere in this series).
34-ch10b-algorithms's own Proposition 10.24).In the capacitated vehicle routing problem (CVRP) a fleet of vehicles of capacity leaves a depot and serves customers; every customer is visited once, and the load of each route must not exceed . In practice customer demands are uncertain at planning time. The chance-constrained CVRP asks that each route respect the capacity with probability at least , but this presupposes a known demand distribution, which is rarely available. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) require the chance constraints to hold for every distribution in an ambiguity set built from the information that can actually be estimated: support, means and dispersion bounds.
Their branch-and-cut method separates rounded capacity inequalities whose right-hand side is the worst-case value-at-risk of the total demand of a customer set . This quantity is evaluated thousands of times during the search, so it matters whether it has a closed form or a small convex reformulation. This mission concerns the paper's covariance ambiguity sets (§5.2), which bound the whole covariance matrix of the demands and can therefore express that demands of nearby customers are correlated, as happens with geographically clustered demand. The covariance bound can be derived from data, for example analytically through McDiarmid's inequality (Delage and Ye, 2010) or by bootstrapping.
Customers are indexed by and their random demand vector is . Fix a box with , a mean vector in the interior of , and a symmetric positive definite matrix . The covariance ambiguity set is
where is the set of all probability distributions on and means that is positive semidefinite.
For a distribution and a real random variable , the value-at-risk at level , , is . For a customer set , the worst-case value-at-risk is . A route serving satisfies the chance constraint for every exactly when this number is at most .
Two componentwise bounds appear in the answer:
A route set is an ordered partition of the customers into nonempty ordered routes. It is feasible in the distributionally robust problem RVRP() if every route satisfies the chance constraint for every , and feasible in a deterministic instance with capacity and demands if every route's total demand is at most .
For every customer set ,
The right-hand side maximizes an affine function over the intersection of an ellipsoid and a box.
For a diagonal bound , program (17) collapses to a search over one parameter with :
over the for which the first bracket is nonnegative and the point of (17) that induces respects (see Formalization scope).
For some instance with the ambiguity set (16), no deterministic CVRP instance on the same customers and fleet has the same set of feasible route sets.
Theorem 7 makes the worst-case value-at-risk over (16) computable in polynomial time as a convex quadratically constrained program. With it, the rounded capacity inequalities of the two-index vehicle flow formulation can be separated for covariance information. Theorem 2 of the same paper shows that the resulting demand estimator is subadditive, so this formulation is exact. Corollary 4 gives a closed form for the diagonal case, which the paper uses to evaluate the estimator in time linear in after sorting. Theorem 6 explains why the paper needs this machinery: the robust feasible region cannot be reproduced by any deterministic demand vector and capacity.
The results are proved in the paper's online supplement. No part of them is formalized anywhere to our knowledge; the platform has no worst-case value-at-risk and no moment-based ambiguity set. A complete development would give machine-checked worst-case VaR bounds over moment sets with second-order information. These are used well beyond routing, in distributionally robust portfolio and inventory models.
The supremum ranges over an infinite-dimensional set of distributions, while (17) ranges over vectors. The inequality "" requires, for every feasible of (17), a sequence of distributions in (16) whose value-at-risk approaches . The value-at-risk is a lower quantile, so a distribution placing mass exactly on a high point does not attain the value: the construction has to be a limit. The inequality "" is harder. It must rule out every distribution, not only two-point ones, and a bound through the one-dimensional Chebyshev–Cantelli inequality for alone ignores the box: it yields , which is too large whenever the support bounds bind. The interaction between the Loewner constraint and the componentwise support bounds, which produces the unusual bound , is where the work lies. For Theorem 6 the difficulty is to exhibit the instance and to evaluate enough chance constraints exactly.
Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. Distributions are measures on Fin n → ℝ. The set (16) is covarianceSet qlo qhi μ Sig: a probability measure with P (Set.Icc qlo qhi) = 1, coordinate means μ, and Sig - M positive semidefinite, where M is the matrix of integrals . The covariance bound is called Sig because Σ is Lean syntax. The side conditions , , (Sig.PosDef) and are hypotheses of every theorem. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is a real sSup over the image of the set. That image is nonempty (the Dirac measure at lies in (16)) and bounded (the box), so the supremum is genuine. "The optimal objective value" of a maximization is stated as a supremum; attainment is not part of any claim. is Mathlib's matrix inverse.
The paper states Theorem 7 and Corollary 4 with "-VaR" without a level; the level , used in the sentence introducing Theorem 7 and everywhere else, is read in. Corollary 4 as printed is false. It maximizes over every with a nonnegative bracket. For , every large then gives the value , which can exceed and hence every value-at-risk. The formal statement adds the condition that makes each a feasible point of (17): for , where is the first bracket. With this condition the statement is the diagonal case of Theorem 7.
A theorem about the Lean set is trivial if the set is empty or the supremum is a junk value. Neither happens here, and replacing the Loewner constraint by a scalar variance bound on would state a different theorem. The dual second-order cone program printed after Theorem 7 is not a target: as printed it has the all-ones vector where Lagrangian duality gives , and it has no multiplier for .
Needed infrastructure: quantiles of pushforward measures, the Loewner order on moment matrices, and finite-support (two-point) distributions. The value-at-risk lemmas and the moment-matrix lemmas are reusable beyond this mission, and contributions of either kind are welcome. Theorem 6 needs only the route-set layer defined here and one explicit instance.
In the capacitated vehicle routing problem (CVRP) a depot serves customers with vehicles of capacity , and every route must respect the capacity. When customer demands are uncertain, the distributionally robust chance-constrained CVRP of Ghosal and Wiesemann (Oper. Res. 68(3), 2020) requires every route to meet its capacity with probability at least under every distribution in an ambiguity set , a family of distributions consistent with what is known about the demands. Such constraints are handled in a branch-and-cut scheme through rounded capacity inequalities, whose right-hand sides require one quantity for each customer subset : the worst-case value-at-risk of the cumulative demand of .
For ambiguity sets that describe each customer separately (marginal moment sets), this quantity is additive over customers and the problem reduces to a deterministic CVRP. Such sets cannot express that the demands of customers in the same municipality, county or state vary jointly within limits. The first-order generic moment ambiguity set does express this: it bounds the mean absolute deviation of the cumulative demand of prescribed customer groups. The mean absolute deviation is a standard robust dispersion measure, less sensitive to outliers than the standard deviation (see Casella and Berger, Statistical Inference, 2002). This mission formalizes the paper's description of the worst-case value-at-risk over such sets.
Demands form a random vector on . The data are a support box with , a mean vector in the interior of , customer subsets and bounds . For , is its indicator vector. The first-order generic moment ambiguity set, Eq. (12) of the paper, is
where is the set of probability distributions on and acts componentwise. The subsets are arbitrary: they may overlap and need not cover .
For a risk level and a random variable , the value-at-risk is . For a customer subset the quantity of interest is
Write (componentwise) and for the componentwise positive part. A route set partitions into nonempty ordered routes. It is feasible in the deterministic CVRP with demands if for all , and feasible in the distributionally robust CVRP if for all and all .
For every customer subset ,
The right-hand side is the optimal value of the paper's problem (13). The statement holds for every family of subsets and all data satisfying the standing assumptions, so it is the general form of which the milestones are special cases.
If are pairwise disjoint and cover and , then
If , for and , then
For some instance with an ambiguity set of the form (12), no deterministic CVRP instance on the same customers and vehicles (capacity , demands ) has the same set of feasible route sets.
Theorem 5 makes the worst-case value-at-risk over (12) computable in polynomial time as the value of a nonsmooth convex problem over the nonnegative orthant, which the paper notes can be written as a linear program. This gives the right-hand sides of the rounded capacity inequalities in a branch-and-cut scheme for the distributionally robust CVRP. Corollaries 2 and 3 give closed forms for two structured families of groups, evaluable in time linear in . Theorem 4 shows the gain in modelling power has a cost: unlike the marginal case, the problem cannot in general be replaced by a deterministic CVRP with altered demands. With a single customer and , Theorem 5 reduces to the closed form for marginalized first-order sets, so it extends that single-customer formula to joint dispersion constraints.
All four results are proved in the paper's online supplement. As far as a platform search shows, none has been machine-checked. The mission produces checked proofs of the equality in Theorem 5, the two closed forms, and an explicit instance for Theorem 4.
The supremum ranges over an infinite-dimensional set of joint distributions, and the value-at-risk is neither convex nor concave in the distribution. Bounding the value-at-risk of each group separately and adding the bounds does not work when groups overlap, and it ignores the total-dispersion constraint. It gives only an upper bound, and in the setting of Corollary 2 that bound is strict whenever the total bound is the binding term. Showing that the infimum in (13) is attained in the limit needs distributions that saturate several overlapping dispersion constraints at once while keeping the mean fixed and the support inside the box. For Theorem 4, the witness must separate the feasible-route-set family of the robust instance from every family defined by a single linear capacity inequality with nonnegative weights.
Customers are Fin n (0-based), subsets are Sfam : Fin p → Finset (Fin n), and a distribution is a Measure (Fin n → ℝ) that is required to be a probability measure. Support is P (Set.Icc qlo qhi) = 1, the mean condition is ∫ q, q j ∂P = μ j, and the dispersion condition is ∫ q, ∑ j ∈ Sfam l, |q j - μ j| ∂P ≤ ν l. The integrability clauses stated alongside are automatic for measures carried by the box. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is the real sSup of its image over the set; under the standing assumptions this image is nonempty (the Dirac at lies in the set) and bounded (bounded support), so the real supremum is the paper's. The optimal value of (13) is the real sInf of the objective over , a nonempty set on which the objective is bounded below by . Attainment is not claimed. All statements carry the standing assumptions , , and . Corollary 2 writes with the last subset Sfam (Fin.last r). Corollary 3 indexes the singleton of customer by Fin.castSucc i. In Theorem 4 route sets are Fin m → List (Fin n) and only feasibility is modelled; costs play no role.
The theorems are not trivialized by an empty ambiguity set or a junk supremum: membership of the Dirac distribution at is checked locally with a sorry-free proof. Theorem 4 needs a genuinely separating instance: an instance in which no route set is robustly feasible, for example, is matched by a deterministic instance in which none is feasible either.
Needed infrastructure: two-point and finitely supported distributions on and their value-at-risk; weak duality for moment problems over the box; the positive-part calculus of (13). The value-at-risk lemmas for finitely supported measures are reusable in the sibling missions on this paper. Contributions of any of the milestones, of lemmas for these building blocks, or of either inequality of Theorem 5 on its own are welcome.
The capacitated vehicle routing problem (CVRP) assigns customers to a fleet of identical vehicles of capacity and orders each vehicle's visits so as to minimize transportation cost, subject to each vehicle's total load not exceeding . In practice the customers' demands are not known when the routes are planned. Two classical responses are the robust CVRP, which requires feasibility for every demand vector in an uncertainty set, and the chance-constrained CVRP, which requires each capacity constraint to hold with probability at least under a known demand distribution. The first ignores all distributional information; the second assumes a distribution that is rarely known and usually requires independent demands.
Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP, RVRP(), in which each capacity constraint must hold with probability at least under every distribution of an ambiguity set . Whether this problem can be solved with existing CVRP technology depends on how the worst-case value-at-risk of a customer set's total demand behaves as a set function. This mission formalizes §4 of the paper, which treats ambiguity sets that only constrain each customer's demand separately.
There are customers with random demand vector and a risk level . For a probability distribution and a real random variable , the value-at-risk is
For an ambiguity set and a customer subset , the worst-case value-at-risk of is .
Fix a support box with , a mean vector in the interior of , and for each customer a componentwise convex dispersion measure with bound . The marginalized moment ambiguity set (5) is
It constrains marginal moments only, and so contains joint distributions of every dependence structure, from independent to perfectly correlated demands. Three special cases have their own closed forms: the first-order set (6), where bounds the mean absolute deviation ; the variance set (8), where bounds ; and the semivariance set (10), where bound and .
A route set partitions the customers into nonempty ordered routes. It is feasible in RVRP() if for all and all , and feasible in the deterministic CVRP with demands if for all .
For every marginalized moment ambiguity set (5) and every nonempty ,
The dispersion measures are left arbitrary (convex, componentwise, any number of components), so the goal covers every set of the form (5).
Theorem 3 says that over (5) the worst case of a sum is the sum of the worst cases. Because the value-at-risk is not additive for a fixed distribution, and the online supplement exhibits distributions in such a set for which the individual values-at-risk are not additive, the statement is about the ambiguity set, not about any of its members. Its consequence, Corollary 1, is that RVRP() over (5) is a deterministic CVRP with inflated demands, so existing branch-and-cut and branch-and-cut-and-price codes solve it unchanged. Propositions 2–4 make those inflated demands explicit for three standard dispersion measures, so that the whole reduction is in closed form. The corollary also exposes a limitation: under (5) the worst-case distribution does not depend on the route set, and the model cannot represent known dependencies between customers.
The results are proved in the paper's online supplement; none has a machine-checked proof. A formalization produces a checked worst-case value-at-risk calculus over moment sets with support constraints, including sharp one-sided Chebyshev-type bounds under mean-absolute-deviation, variance and semivariance constraints, which are reusable in distributionally robust optimization beyond vehicle routing.
The value-at-risk is neither subadditive nor superadditive in general, so neither inequality of Theorem 3 follows from properties of a single distribution. The inequality "" requires combining near-worst-case distributions of the individual customers into one joint distribution in that is simultaneously near-worst for the sum; the inequality "" requires bounding the value-at-risk of the sum for an arbitrary joint law using only marginal information. In Propositions 2–4 the supremum is typically not attained: the distribution concentrating mass at the claimed worst-case value violates the mean constraint, and the value is reached only as a limit of distributions in . An argument that exhibits a single maximizer therefore fails, and the statements must be proved as equalities of suprema.
Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. An ambiguity set is a set of measures on Fin n → ℝ, each required to be a probability measure; the support condition is P (Set.Icc qlo qhi) = 1 and expectations are Bochner integrals. The sets are sets of joint laws on , never products of marginals. In (5) each expectation is required to exist; this is automatic for convex on the bounded support. The value-at-risk is the published definition MultistageStochastic.valueAtRisk P Y (1 - ε), and the worst-case value-at-risk is the real supremum of its values over the ambiguity set; under the standing assumptions that set of values is nonempty (the Dirac law at belongs to ) and bounded (by the support), so the supremum is not a default value. The single-customer quantity is the case . The standing assumptions (, , convexity of , , , ) are explicit hypotheses. Routes are lists of customers; a route set has nonempty routes whose concatenation is a permutation of all customers. Costs are not formalized, since both routing problems minimize the same cost over their feasible route sets.
All targets are equalities or equivalences; a one-sided inequality, a statement asserting that some distribution attains the value, or a formulation over product measures is a different theorem and does not count.
Contributions welcome: the reduction of the chance constraint to a value-at-risk bound, the right-continuity lemmas for the value-at-risk of a measure on , two-point constructions in the ambiguity sets, and one-sided Chebyshev-type bounds with support constraints.
The capacitated vehicle routing problem (CVRP) asks for a set of minimum-cost routes by which a fleet of identical vehicles of capacity , based at a depot, serves every customer exactly once without any vehicle carrying more than its capacity. In practice customer demands are not known when routes are planned. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust CVRP: the demand vector is random, its distribution is known only to lie in an ambiguity set , and every route must respect its capacity with probability at least under every distribution in .
Exact CVRP solvers rely on compact two-index vehicle flow formulations strengthened by rounded capacity inequalities, which bound from below the number of vehicles entering any customer subset by a demand estimator . The paper shows (its Theorem 1) that the robust two-index formulation is exact whenever the demand estimator is subadditive and demands are nonnegative, and that this fails for some natural ambiguity sets: sets that fix the marginal distribution of each customer's demand violate it (Example 1). This mission formalizes the paper's positive result for the most widely used class of ambiguity sets, the moment ambiguity sets of distributionally robust optimization (see El Ghaoui et al. 2003, Delage and Ye 2010, Wiesemann et al. 2014).
There are customers, indexed ; the demand vector is . Fix
The moment ambiguity set is
where denotes all probability distributions on . The paper's standing assumptions are , each closed and convex, and .
For a distribution the value-at-risk of a random variable is , with risk level . The worst-case value-at-risk of a customer subset is , and the demand estimator (2) is
The Lean development names these momentAmbiguitySet qlo qhi μ φ σ, worstCaseVaR, demandEstimator and twoPointMeasure in the namespace DRCVRP.Moment.
For every moment ambiguity set satisfying the standing assumptions, every and every ,
This is condition (S) of the paper, stated for the rounded estimator (2) and for all pairs of subsets, overlapping or empty ones included.
For every customer subset there are two-point distributions with and such that
Combined with the paper's Theorem 1, Theorem 2 says that for every moment ambiguity set with nonnegative demands the robust CVRP can be solved through the compact two-index formulation with robust rounded capacity inequalities, i.e. by the branch-and-cut machinery of the deterministic CVRP. It also separates moment ambiguity sets from ambiguity sets built from marginal histograms, hypothesis tests, -divergences or Wasserstein balls, whose estimators can violate subadditivity. Proposition 1 describes the worst case: however many moment constraints the set contains, two demand scenarios suffice to approach the worst-case value-at-risk, strengthening the Richter–Rogosinski theorem for this functional.
Both results are proved in the paper's online supplement. They have not, to the best of current knowledge, been machine checked. This mission produces a checked statement and proof of both, together with a reusable encoding of moment ambiguity sets and of the worst-case value-at-risk over them. The companion missions of the series formalize the equivalence theorem (I) and the explicit worst-case VaR formulas for marginalized (III), first-order (IV) and covariance (V) ambiguity sets.
Value-at-risk is not subadditive for a single distribution, so the obvious route, subadditivity of the worst-case VaR followed by , needs an argument specific to the moment set; for the marginal-histogram set of Example 1 the worst-case VaR itself fails to be subadditive. The supremum over ranges over an infinite-dimensional set of distributions and is in general not attained, so an argument that picks a maximizer does not apply, and the classical finite-support reduction (Richter–Rogosinski) yields a number of support points that grows with the number of moment constraints, not two. The integer rounding and the must also be handled for all pairs of subsets, including overlapping ones.
Customers are Fin n (0-based) and customer subsets are Finset (Fin n). Distributions are measures on Fin n → ℝ; membership in the moment set requires a probability measure giving mass one to the closed box Set.Icc qlo qhi, integrable coordinates with ∫ q, q i ∂P = μ i (an equality), and integrable φ l with ∫ q, φ l q ∂P ≤ σ l. The integrability clauses hold automatically under the standing assumptions and do not shrink the set. The dispersion measure is an arbitrary real-valued function whose components are convex (convex real functions on are continuous, which covers "closed"); is allowed. The value-at-risk is the published platform definition MultistageStochastic.valueAtRisk at level . The worst-case VaR is a real sSup; over a moment set satisfying the standing assumptions the set of VaRs is nonempty (the Dirac measure at belongs to ) and bounded by the box, so this is the true supremum. The estimator is integer valued. Every standing assumption is a hypothesis of both theorems.
Neither statement can be satisfied trivially: the goal is about the rounded estimator of the true supremum over a nonempty set, not about subadditivity of an arbitrary set function, and the milestone requires the two-point laws to lie in and their VaRs to converge to the supremum, not to be attained. Extended-valued dispersion measures, such as the one expressing the covariance set of §5.2 as an instance of (4), are outside the scope of the real-valued encoding.
A complete development needs basic facts about quantiles of finitely supported measures, the structure of the moment set, and a duality or construction argument for the worst-case VaR. Lemmas about value-at-risk of two-point laws and about moment sets are reusable across the series. Proofs of the milestone, of the goal, and of intermediate lemmas are welcome.
Chapter 16 of Keller and Trotter's Applied Combinatorics (2017 Edition, CC BY-SA 4.0) is a survey of seven topics. Two of them are self-contained results with complete proofs on the page, and this mission formalizes both.
The first is the Lovász Local Lemma. It was introduced by Erdős and Lovász in 1975 to show that certain hypergraphs are 3-colourable (Erdős–Lovász 1975), and it has become a standard tool of the probabilistic method. The classical probabilistic argument shows that a random object has a property with probability close to one. The local lemma is different: it shows that a good object exists even when it is exceedingly rare, provided that each "bad" event depends on only a few of the others. It underlies lower bounds for Ramsey numbers such as , the subject of Section 16.8. It also underlies results on colouring, satisfiability and Latin transversals, and the algorithmic version of Moser–Tardos (2010).
The second is the Gale–Ryser Theorem, proved independently by Gale (1957) and Ryser (1957). It decides when a zero–one matrix with prescribed row and column sums exists. Equivalently, it decides when a pair of sequences is the degree sequence of a bipartite graph. Its condition is a comparison in the dominance order on integer partitions.
A finite probability space is a finite set with a function defined on all subsets, finitely additive, with and . Let be a finite family of events. For a subfamily write
the event that every event of fails; for it is . Fix, for each , a subfamily . The event is independent of any event not in if for every with and . In the formalization this condition is IndepOutside μ A N i, written as
A partition of a positive integer is a non-increasing string of positive integers with sum ; is the set of partitions of . It is partially ordered by iff is no longer than and every partial sum is at least (Dominates). covers when with nothing in between (Covers). The dual partition has entries, the -th being the number of with (dual). A zero–one matrix with row sum string and column sum string is an matrix with entries in whose row sums to and column to (IsZeroOneMatrixWithSums).
If and for every , then for every non-empty
If , , , and , then
If covers in , then arises from by moving one unit from a part to a later part (possibly a new part of size one), and all parts strictly between equal . For partitions of ,
The Erdős–Ko–Rado bound of Theorem 16.8 enters as the published reference FamousTheorems.erdos_ko_rado.
The local lemma is the entry point to the probabilistic method's rare-event side. A formal statement in the book's form — finite spaces and the book's conditional notion of independence — is a reusable interface for formalizing its applications: Ramsey lower bounds, hypergraph colouring and -SAT with bounded occurrences. The symmetric form is the version most applications call. Mathlib has no local lemma. The platform has a conditional-probability bound from an unrelated paper mission (Erdos390.WholePaper.finiteAsymmetricLocalLemma_conditionalBound), which bounds with and does not state the product lower bound for the joint failure.
Gale–Ryser is the prototype of margin problems for -matrices and of degree-sequence characterizations (compare Erdős–Gallai for graphs). Formalizing it produces the dominance order, conjugate partitions and covering relations on sorted lists of positive integers. Mathlib has Nat.Partition but no dominance order or conjugate. None of these results is formalized on the platform. The results themselves are classical and proved; the work is formalizing the proofs.
For the local lemma, the naive induction on fails. Conditioning on the joint failure of a subfamily requires that failure to have positive probability, and that is only known after the inductive bound has been proved for smaller subfamilies. The induction must therefore carry the lower bound and the positivity of every smaller joint failure at once. It must also split each conditioning family into the part inside and the part outside. The independence hypothesis controls only the part outside, and only through intersections of complements, not through arbitrary events.
For Gale–Ryser, necessity is an exchange argument, but sufficiency needs the fine structure of covers in the dominance order (Proposition 16.11): the case analysis of where the moved unit lands, including a new last part, and the fact that a maximal chain from down to exists. Converting the list-level statements into matrix constructions over Fin m × Fin n is the other main cost.
Fintype Ω with DiscreteMeasurableSpace Ω and a measure μ with IsProbabilityMeasure μ; every subset is an event and probabilities are μ.real, as in the book's finite probability spaces.A : ι → Set Ω over a Fintype ι, so repeated events are allowed. Neighbourhoods are N : ι → Finset ι with i ∉ N i.0 < x i < 1 is strict on both sides, as on the page.Fintype.card ι, together with positivity. Here and are real and is Real.exp 1.List ℕ, non-increasing with positive entries. Entries are 1-based through entry, and partial sums are (V.take j).sum.Matrix (Fin m) (Fin n) ℕ with entries in .Not included.
Welcome contributions. Reusable infrastructure: a finite-space conditional-probability API, and the dominance order as a PartialOrder on sorted partitions linked to Nat.Partition.
Many counting questions ask for the number of objects up to symmetry: necklaces of coloured beads that may be rotated and flipped, musical scales up to transposition, chemical isomers up to the symmetries of a molecule, graphs on vertices up to relabelling. Counting all configurations and dividing by the number of symmetries fails, because some configurations are fixed by some symmetries. The standard tool for such questions is the enumeration theorem of Redfield (1927) and Pólya (1937), which turns the symmetry group into a generating function recording not only how many inequivalent configurations there are but how many use each colour a prescribed number of times.
This mission formalizes Chapter 15 of Keller and Trotter's Applied Combinatorics (2017 Edition), which develops the theorem from Burnside's Lemma for an undergraduate audience. The chapter's footnotes record the history: the orbit-counting lemma was known to Cauchy and Frobenius before it appeared in Burnside's book, and Redfield's paper anticipating Pólya's work was rediscovered only around 1960.
Let be a finite set with . A permutation group of is a set of bijections containing the identity and closed under composition and inverses. Every permutation splits into disjoint cycles; a fixed point is a cycle of length . Write for the number of cycles of length , so that . The cycle index of is the polynomial with rational coefficients
For the eight symmetries of a square, .
A coloring of with colours is a map ; denotes the set of all of them. A permutation acts on colorings by , and two colorings are equivalent when some carries one to the other. The weight of is the monomial in commuting variables, where counts the points coloured . The pattern inventory is the polynomial whose coefficient of is the number of equivalence classes of colorings using each exactly times.
More generally, for a finite group acting on a finite set , the orbit (equivalence class) of is , the stabilizer of is , and the fixed set of is .
For a finite group acting on a finite set and every ,
If is the number of equivalence classes of induced by the action, then
For a permutation group of with and colours ,
an identity of polynomials in with rational coefficients: substituting power sums of the colours into the cycle index yields the pattern inventory.
The result itself. The theorem reduces counting inequivalent configurations to a computation with the cycle structure of the symmetry group, which is usually available in closed form (cyclic, dihedral and symmetric groups, and the pair group acting on edges of a graph). Setting all gives the number of inequivalent colorings, ; reading off one coefficient answers refined questions such as the number of necklaces with a prescribed number of beads of each colour. The book applies it to musical scales, isomers of hydrocarbons and nonisomorphic graphs.
Formalizing it. Burnside's Lemma is in Mathlib (MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group), and so is the orbit–stabilizer theorem, so the two milestones are short; they are kept because they are the book's route to the goal. Mathlib has Equiv.Perm.cycleType but no cycle index and no pattern inventory, and no statement of Pólya's theorem was found on the platform (searches for Pólya, cycle index, pattern inventory, necklace and orbit counting, September 2026). The mission therefore produces the first machine-checked cycle index and Pólya enumeration theorem in this environment.
Burnside's Lemma counts orbits by fixed points; Pólya's theorem is a weighted Burnside lemma. Two steps separate them. First, the weight-enumerator of the colorings fixed by must be matched with the monomial of evaluated at power sums. This needs the cycles of as subsets of , including its fixed points, whereas Mathlib's cycleType records only the lengths of the nontrivial cycles. Second, the weighted orbit count needs the weight to be invariant under the action and Burnside's argument to be carried out inside a polynomial ring rather than in . Neither step is a direct instance of a Mathlib lemma. Proving the identity only after substituting integers for the does not suffice: it determines the number of classes, not the coefficient of each monomial.
Fintype with decidable equality, = Fintype.card S; a permutation group is a Subgroup (Equiv.Perm S), and = Nat.card G .cycleCount π k: the number of fixed points for and the multiplicity of in Equiv.Perm.cycleType for . is cycleIndex G : MvPolynomial (Fin r) ℚ, the variable with index standing for .Fin m, colorings are S → Fin m, and ; the induced relation is colorSetoid G m. Composing with instead of gives the same classes.patternInventory G m : MvPolynomial (Fin m) ℚ, the sum over the quotient of the weight of a representative (Quotient.out); that the weight is a class invariant is part of the theorem.MvPolynomial.bind₁ sending to .MulAction G 𝒞 with Fintype G and Fintype 𝒞; is the number of MulAction.orbitRel classes and the identity is stated in .Reusable beyond this mission: the cycle index of a permutation group and the pattern inventory, both needed for any later count of necklaces, graphs up to isomorphism, or de Bruijn's generalization with a group acting on the colours. Contributions of cycle indices of specific groups (cyclic, dihedral, symmetric) are welcome.
Moving as much as possible of something — freight, water, data — from an origin to a destination through connections of limited capacity is one of the basic problems of operations research. Its mathematical form, the maximum flow problem, was posed in the 1950s in work on rail networks and solved independently by Ford and Fulkerson (Maximal flow through a network, Canadian J. Math. 8 (1956)) and by Elias, Feinstein and Shannon (A note on the maximum flow through a network, IRE Trans. Inform. Theory 2 (1956)). The answer, the Max Flow–Min Cut Theorem, is a min–max duality: the largest amount that can be shipped equals the smallest total capacity whose removal disconnects the destination from the origin. It is a standard example of linear-programming duality with a combinatorial proof, and it is the source of Hall's matching theorem, Menger's theorem and Dilworth's theorem via network constructions.
This mission formalizes Chapter 13 of Keller and Trotter's Applied Combinatorics (2017 Edition), together with the two theorems of Chapter 14 that apply it, in the book's own model of a network.
A network consists of a finite vertex set , a set of directed edges , a source and a sink with , and a capacity (a real number) on each edge. The underlying directed graph is an oriented graph: for any two vertices at most one of , is an edge. Every edge at points away from and every edge at points into .
A flow is a function on the edges with , extended by on pairs that are not edges, satisfying the conservation laws
The value of is .
A cut is a partition with , . Its capacity is
summed over the edges directed from to only.
Given a flow , an edge is used if and has spare capacity if . An augmenting path is a sequence of distinct vertices from to such that each step either follows an edge with spare capacity (a forward edge) or traverses a used edge backwards (a backward edge). Its augmentation amount is , where is the least spare capacity of a forward edge and the least flow on a backward edge ( when there is no backward edge).
For Chapter 14: in a finite simple graph with bipartition , a matching is a set of edges no two of which share an endpoint; it saturates a vertex that is an endpoint of one of its edges; and is the set of neighbors of the vertices in .
For every network there is a real number with
that is, is attained by some flow and bounds every flow value from above, and is attained by some cut and bounds every cut capacity from below.
The result. Theorem 13.10 turns every maximum-flow computation into a certified one: a flow and a cut of equal value prove each other optimal, and Theorem 13.4 shows no certificate can do better. Together with the integrality theorem 14.1 it is the engine behind the combinatorial applications of Chapter 14: maximum matchings in bipartite graphs, Hall's theorem, and the computation of the width of a poset with a minimum chain partition. Beyond the book, the same duality underlies Menger's theorem, König's theorem, the analysis of image segmentation by graph cuts, and the combinatorial theory of totally unimodular linear programs.
Formalizing it. The results are classical and proved. Mathlib has no theory of network flows. The platform has a Max-Flow Min-Cut theorem in the model of Bertsimas and Tsitsiklis (a general digraph on Fin n with capacities in , value compared in EReal), which does not cover the book's networks with zero capacities and is stated for a different encoding. This mission produces the theory in the book's model: finite oriented networks with real non-negative capacities, flows as functions on vertex pairs, cuts as vertex subsets, and the augmenting-path step that the Ford–Fulkerson labeling algorithm iterates. Hall's theorem is in Mathlib in its indexed-family form; the graph form stated here is new to the platform.
Theorem 13.4 is a finite-sum rearrangement. The difficulty of the goal is the existence of a maximum flow. The textbook argument runs the labeling algorithm until it halts, then reads off a cut from the labeled vertices. With real capacities this algorithm need not halt: with badly chosen augmenting paths and irrational capacities the flow values can converge to a limit strictly below the maximum, so "repeat until no augmenting path exists" does not by itself produce a maximum flow. The existence of an optimal flow is therefore not a by-product of the algorithm's description; it has to be established in its own right before the absence of augmenting paths can be turned into a cut of equal capacity. A formalization that assumes a maximum flow exists proves a strictly weaker statement. Proposition 13.7 is elementary but bookkeeping-heavy: backward edges subtract flow, and conservation must be checked at every interior vertex of the path.
The vertex set is a type V with [Fintype V] [DecidableEq V]. A network (AppliedComb.Flows.Network) bundles an edge relation adj, the source S and sink T with S ≠ T, and a real capacity function cap, together with the axioms of an oriented graph, the orientation of edges at S and T, and 0 ≤ cap x y on edges. Flows are functions ϕ : V → V → ℝ satisfying IsFlow, which includes off the edges and keeps the first conservation law as part of the definition, as on the page. The value is . A cut is its part L : Finset V with S ∈ L, T ∉ L. Augmenting paths are injective maps Fin (m + 1) → V, and are computed in WithTop ℝ so that an empty minimum is and when there is no backward edge. Hall's theorem uses Mathlib's SimpleGraph with a given bipartition into two Finsets and matchings as sets of Sym2 V edges.
No explicit constants arise: the chapter has no asymptotic or approximate statements.
The book's sentence of Theorem 13.10 reads "if is the maximum value of a flow and the minimum capacity of a cut, then ". A formalization that takes and as hypothetical extrema of possibly empty or unattained sets would be trivial or vacuous; the goal here asserts the existence of a maximum flow and a minimum cut at the same number, and the existence of a maximum flow for real capacities is part of what must be proved.
Needed infrastructure: finite-sum manipulation over Finset (reindexing, splitting over L and Lᶜ), existence of maximizers of a linear function over the set of flows, and, for Theorem 14.1, control of integrality. The definitions of networks, flows, cuts and augmenting paths are reusable for Menger's theorem, König's theorem and the chain-partition network of Section 14.3. Contributions of alternative proofs (via linear-programming duality) are welcome.
Ramsey theory studies the principle that complete disorder is impossible: every sufficiently large structure contains a large, perfectly uniform substructure. Its most familiar instance concerns graphs. In any graph on six vertices there are three vertices that are pairwise adjacent or three that are pairwise non-adjacent, and the same phenomenon persists at every scale. The quantity that measures it, the Ramsey number , is one of the most studied and least understood functions in combinatorics. Only a handful of values are known exactly (, ), while is only known to lie between 43 and 49 (Radziszowski, Small Ramsey Numbers).
The subject has a short, well-documented history. F. P. Ramsey proved the general theorem in 1930 as a lemma in decidability (Ramsey 1930). Erdős and Szekeres (1935) gave the upper bound (Erdős–Szekeres 1935). In 1947 Erdős proved an exponential lower bound for the diagonal numbers by counting graphs (Erdős 1947); this argument is now regarded as the origin of the probabilistic method. In 1959 Erdős used the same method to show that graphs of large girth and large chromatic number exist (Erdős 1959). For decades the exponential bases and stood essentially unchanged; the upper base was lowered below only in 2023 (Campos–Griffiths–Morris–Sahasrabudhe).
This mission formalizes these results as presented in Chapter 11 of Keller and Trotter, Applied Combinatorics (2017 Edition).
A graph is a finite simple graph: a finite vertex set with a symmetric, irreflexive adjacency relation (no loops, no multiple edges). A complete subgraph on vertices is a set of pairwise adjacent vertices; an independent set of size is a set of pairwise non-adjacent vertices.
A non-negative integer is a Ramsey bound for if every graph with at least vertices contains a complete subgraph on vertices or an independent set of size . The Ramsey number is the least positive Ramsey bound. In Lean these are AppliedComb.Ramsey.IsRamseyBound m n N and AppliedComb.Ramsey.ramseyNumber m n.
More generally, write and for the family of -element subsets of . For a string , the number is the least positive such that for every and every colouring some colour has a set of size all of whose -subsets receive colour (hypergraphRamseyNumber s r h).
The girth of a graph is the smallest number of vertices on a cycle, and infinite for a forest; the chromatic number is the least number of colours in a proper vertex colouring.
For every positive integer ,
Equivalently, below this threshold there is a graph on each number of vertices with neither a complete subgraph on vertices nor an independent set of size . The statement is for every , with no asymptotic slack.
A further item, not a milestone because the book does not number it, records the bound that the proof of Theorem 11.2 establishes: every graph with at least vertices has a complete subgraph on vertices or an independent set of size .
The goal is the diagonal lower bound that every later improvement is measured against. With the upper bound from the proof of Theorem 11.2 it shows that grows exponentially, with base between and . No explicit construction is known to give for any constant . Theorem 11.7 is the standard example of a statement whose only known proofs for decades were probabilistic, and it shows that chromatic number is not a local property.
On the formal side, Mathlib has cliques, independent sets, girth and chromatic number, but no Ramsey numbers, no Erdős lower bound and no high-girth theorem. The platform already has weaker or differently shaped relatives, all checked for this mission. Erdos1947.ramsey_lower_bound gives a graph on vertices without monochromatic -sets, a weaker bound than the goal's. BookSixth.high_girth_chromatic is a single-parameter form of Theorem 11.7 in another Lean environment. ramsey_theory_upper_bound is a diagonal bound. The goal statement carries the constant exactly, which requires an explicit, non-asymptotic lower bound for where the book writes "Stirling's approximation".
The obvious route to the goal is to count graphs with a large clique or independent set and compare the result with the total number of graphs. Two steps of that route do not go through as written in the text. First, the book replaces by its Stirling approximation, which is only asymptotic; a statement for every needs an inequality valid for all , and the constant leaves no room for a cruder estimate such as alone. Second, the counting argument yields a graph on each below the threshold, whereas is defined as a least threshold over all graphs with at least that many vertices; the two have to be connected.
Theorem 11.7 needs random graphs with edge probability depending on , a first-moment bound on short cycles and on independent sets, and a deletion step. The book states Theorem 11.6 without proof.
SimpleGraph V on a finite type V : Type (Theorems 11.1, 11.2, 11.4) or on Fin N (Theorem 11.7). Cliques and independent sets are SimpleGraph.IsNClique and SimpleGraph.IsNIndepSet on a Finset.IsRamseyBound m n N quantifies over every graph with at least vertices, as the book does; ramseyNumber m n is the sInf of the positive Ramsey bounds. Theorem 11.2 is stated as IsLeast {N | 0 < N ∧ IsRamseyBound m n N} (ramseyNumber m n), so its content is the nonemptiness of that set. The same pattern is used for Theorem 11.6.(n : ℝ) / (Real.exp 1 * Real.sqrt 2) * (2 : ℝ) ^ ((n : ℝ) / 2) ≤ (ramseyNumber n n : ℝ), with a real power. Explicit constant: the book says "use the Stirling approximation … after some algebra"; the statement keeps the book's constant and holds for every with no threshold.ramseyNumber, so it cannot hold through an empty defining set.SimpleGraph.egirth (valued in , for forests), not SimpleGraph.girth, which is on forests. Chromatic number is SimpleGraph.chromaticNumber in . The parameter of Theorem 11.7 is a natural number; negative is trivial.Fin n, with colours in Fin r.IsRamseyBound/ramseyNumber, the hypergraph version, an all- lower bound for , and counting over the labelled graphs on vertices. Proofs of any milestone are welcome contributions.Linear recurrences with constant coefficients are among the first tools of enumerative combinatorics and the analysis of algorithms: the Fibonacci numbers, the number of binary strings avoiding a pattern, the running time of a divide-and-conquer loop and the number of tilings of a strip all satisfy relations of the form . Chapter 9 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org) treats such relations as linear equations in an operator, the advancement operator, in direct analogy with linear differential equations with constant coefficients. The chapter's Principal Theorem says that the solution set of such an equation is a vector space whose dimension equals the order of the recurrence; everything else in the chapter (general solutions for distinct and repeated roots, and the reduction of nonhomogeneous equations to homogeneous ones) is organised around it.
This mission formalizes that theorem, in the book's model of functions on all of , together with the numbered lemmas of Section 9.5 on which its outline rests.
Let be the real vector space of all functions , with pointwise addition and scalar multiplication. The advancement operator is
a linear operator with for . For a nonnegative integer and real constants , the advancement operator polynomial is
so that . The solution space of the homogeneous equation is
the kernel of , a linear subspace of . In Lean, is AppliedComb.Recurrence.advance : Module.End ℝ (ℤ → ℝ), is opPoly k c for a coefficient vector c : Fin (k + 1) → ℝ with c i multiplying , and is solutionSpace k c := LinearMap.ker (opPoly k c). A factor is advance - r • 1.
For a positive integer and real constants with and ,
for some real constants .
The result itself. Theorem 9.18 is what justifies the standard recipe for solving a recurrence: once linearly independent solutions are found, every solution is a linear combination of them, and initial values pin down a unique solution. Theorems 9.21 and 9.22 name those solutions when the characteristic polynomial splits over , and Lemma 9.20 reduces nonhomogeneous recurrences, the ones arising from counting problems with a forcing term, to one particular solution plus the homogeneous space.
Formalizing it. The book states Theorem 9.18 without a full proof ("we won't prove the full result") and leaves Lemma 9.22 as an exercise, so a formalization supplies arguments the source omits. Mathlib's LinearRecurrence develops the -indexed, monic version (LinearRecurrence.solSpace_rank); the bi-infinite, two-sided setting of the book, in which the constant term must be nonzero, is not in Mathlib or on the platform as of this mission.
The subspace part of Theorem 9.18 is immediate; the content is the dimension count, in both directions. On a solution must extend to negative indices as well as positive ones, so an argument that works for sequences indexed by does not transfer: there the constant term plays no role and the dimension is whatever the constant term, while on a vanishing changes the answer. The outline in the book proceeds through factorisations of , which over need not exist (complex roots), so the goal cannot be obtained by combining Theorems 9.21 and 9.22 alone. Lemma 9.22 requires showing that the functions solve and that they exhaust its solutions, for ranging over all integers.
zpow), always of a nonzero base.Module.rank ℝ (solutionSpace k c) = k, a cardinal equality, so it also asserts finite-dimensionality.c : Fin (k + 1) → ℝ; c 0 is the leading coefficient and c (Fin.last k) the constant term .iff.Needed infrastructure: linear operators on the function space ℤ → ℝ, powers and products in Module.End, Module.rank/Module.finrank, and finite sums; Mathlib's LinearRecurrence may be adapted for the forward half. The definitions advance, opPoly and solutionSpace are reusable for any later mission on recurrences or on generating functions for bi-infinite sequences. Contributions of the milestone lemmas, of a proof of the goal that avoids factorisation over , and of a complex-valued variant are welcome.
Mathlib/Algebra/LinearRecurrence.lean (ℕ-indexed linear recurrences, LinearRecurrence.solSpace_rank). Mathlib docs