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?
Control problems for queueing systems (admission control, routing, service rate selection, inventory replenishment) are naturally modelled as Markov decision chains with a countable state space, such as the number of customers in a buffer, and with costs that grow without bound in the state, such as holding costs proportional to queue length. The expected discounted cost criterion is the first infinite horizon criterion applied to such models, and it is also the tool through which the average cost criterion is treated later in the same book (Chapters 6–8 of Sennott's text reach average cost optimal policies through limits of discounted problems as the discount factor tends to one).
Classical treatments of discounted dynamic programming assume bounded costs, under which the dynamic programming operator is a contraction and has a unique bounded fixed point. That assumption fails for queueing models. This mission formalizes Chapter 4, Sections 4.1–4.4, of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), which develops the discounted theory for nonnegative, possibly unbounded costs, where value functions may be infinite.
Timeline of the underlying theory:
A Markov decision chain has a countable state space ; for each state a finite nonempty action set ; for each a nonnegative finite cost and a probability distribution of the next state. A policy chooses the action at time at random from a distribution on that may depend on the entire history . A stationary policy always chooses in state ; for it one writes and .
Fix a discount factor . For an initial state and a policy , the -horizon cost with terminal cost zero and the infinite horizon discounted cost are
and the value functions are and , infima over all policies. All of these lie in . A policy is discount optimal if . The discount optimality equation is
With , denotes the set of actions attaining the minimum at .
solves (4.9); every solving (4.9) satisfies ; and every stationary policy with
is discount optimal. No boundedness of costs and no finiteness of is assumed.
In attack order: Lemma 4.1.1 (); Proposition 4.1.2 (a supersolution of the one-policy equation dominates and ); Corollary 4.1.3 (a supersolution of the optimality inequality dominates ); then, beyond the goal, Corollary 4.1.5 ( where ), Proposition 4.2.2 and Corollary 4.2.4 (conditions under which a solution of (4.9) equals ), Proposition 4.3.1 (, and limit points of finite horizon optimal stationary policies are discount optimal) and Proposition 4.4.1 (optimal policies are exactly those concentrated on the sets along histories of positive probability).
Theorem 4.1.4 is the foundation for everything in the book that concerns discounted costs: it produces an optimal stationary deterministic policy, identifies among the many solutions of (4.9) (Example 4.2.1 of the book gives a one-parameter family of finite solutions), and underlies value iteration (Proposition 4.3.1) and the approximating-sequence method of Sections 4.6–4.7. The average cost results of Chapters 6–8 are proved from it by letting . Proposition 4.4.1 describes the full set of optimal policies, including randomized and history-dependent ones.
These are known results with published proofs. The contribution of this mission is a machine-checked development of the discounted theory for countable state spaces with unbounded costs and infinite values, over the general policy class. Related statements on the platform (the monotone-mapping propositions of Bertsekas 1977 in the MonotoneDP missions, and bounded-cost or finite-state discounted results) use different models and are open; no machine-checked proof of the present statements is known to this mission.
The contraction argument that settles the bounded case is unavailable: with unbounded costs the operator in (4.9) has many fixed points, and can equal at some states, so neither uniqueness of fixed points nor subtraction of values is available. The optimality equation compares the infimum over all history-dependent randomized policies with a one-step minimum, so the general policy class and the law of the process under it must be handled directly; restricting attention to Markov or stationary policies begs the question. Every limit exchange (monotone limits of finite horizon costs, the passage to limit points of policies in Proposition 4.3.1) takes place in , where finite-valued arguments do not transfer verbatim.
The Lean development lives in the namespace SennottDP.Discounted. Conventions:
S with [Countable S]; actions form a type Act and A i : Finset Act is nonempty. Costs are ℝ≥0; transition probabilities are ℝ≥0∞ with ∑' j, P i a j = 1 for a ∈ A i.Fin (n+1) → S, Fin n → Act; a policy assigns to every history a distribution on the action set of its last state. The probability of a history is the product of the policy and transition probabilities; expectations are ℝ≥0∞ sums over histories, so no integrability conditions arise.ℝ≥0∞-valued; . The discount factor is α : ℝ≥0 with 0 < α and α < 1. Terminal costs are zero.Useful infrastructure, reusable by the later missions of this series (approximating sequences, average cost): the shift of a general policy after its first step, the Chapman–Kolmogorov identity for the history law, and the computation for stationary policies. Contributions of such lemmas, and proofs of any milestone, are welcome.
Controlled queueing systems (admission control, routing, service-rate selection) are naturally modelled as Markov decision chains whose state is a buffer content and therefore ranges over a countably infinite set. Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, DOI 10.1002/9780470317037) develops the dynamic programming theory for exactly this setting: countable state space, finite action sets, nonnegative and possibly unbounded costs, and value functions that are allowed to be infinite. The book's computational method, the approximating sequence method (ASM), replaces the infinite chain by a sequence of finite truncations and asks when optimal values and policies of the truncations converge to those of the original chain.
This mission is the first of a series on the book. It covers Chapter 3, finite horizon optimization, together with the model of Chapter 2 and three results from Appendices A and B that the chapter uses. The finite horizon theory is the entry point: it is where the book's general policy class, its extended-valued cost criteria and its approximating sequences are first used together.
A Markov decision chain has a countable state space ; for each a finite nonempty action set ; a finite cost ; and for each a transition distribution . A history at time is , and a general policy chooses the action at time from a distribution on : it may use the whole history and may randomize. Stationary policies () and deterministic Markov policies (a stationary policy for each time) are special cases.
Fix a finite terminal cost and a discount factor ( is the undiscounted case). The horizon expected discounted cost of from initial state is
and the value function is over all general policies. Both may be . A policy is optimal for the horizon if it attains at every . For put and let be the set of minimizing it.
An approximating sequence has finite nonempty state spaces increasing to , the same actions and costs, and transition distributions on converging to as . Its value functions are . In an augmentation type approximating sequence, the probability of leaving to is redistributed over by an augmentation distribution . Assumption FH(, ) requires to be finite and at most for every . A stationary policy is a limit point of stationary policies if, along a subsequence, eventually for each .
For fixed ,
and under either condition every limit point of stationary policies with satisfies for all .
Theorem 3.1.2 is the finite horizon dynamic programming equation in the generality the rest of the book needs: the value function is an infimum over history-dependent randomized policies, and the equation holds with infinite values allowed. Its characterization of optimal policies is Bellman's principle of optimality in necessary-and-sufficient form. Corollary 3.1.4 shows that deterministic Markov policies suffice. The discounted chapter builds on these results, since its value function is the limit of finite horizon ones, and so does the value iteration algorithm of the average cost chapters.
Theorem 3.2.3 is the finite horizon case of the approximating sequence method. It says exactly when finite truncations give the right answer, and it reduces the question to Assumption FH, for which Section 3.3 gives checkable conditions. The same structure (a lim inf inequality, a lim sup assumption, a limit point of optimal truncated policies) recurs for the discounted and the average cost criteria in later chapters.
The results are proved in the book. None of them is formalized: the platform has finite horizon dynamic programming only for Markov policies, abstract monotone mappings or finite reward-maximizing MDPs, and nothing on approximating sequences. A formalization contributes a Lean model of Markov decision chains with general policies and extended-valued criteria, which the later missions of the series restate and can merge with this one.
The obvious proof of the optimality equation conditions on the first action and state and then applies the induction hypothesis to the rest of the trajectory. With general policies the rest of the trajectory is governed by a continuation policy that depends on the first state and action, and the decomposition of the path law into a first step and a continuation must be proved from the definition of the process, not assumed. Infinite values also make the "only if" direction delicate: a strict inequality between expected costs becomes an equality once both sides are infinite.
For approximating sequences, the natural idea is to pass to the limit in the optimality equation of . This fails in general. Example 3.2.1 of the book has , because truncation moves probability onto states of high cost and dominated convergence is not available. Only the lim inf inequality holds for free, through a generalized Fatou lemma for approximating distributions. The lim sup side is exactly what Assumption FH supplies. The limit point argument then needs the compactness statement of Appendix B and the fact that a lim inf can be passed through a minimum over a finite set.
The state space is a type S with [Countable S], the actions a type Act, and A i : Finset Act is nonempty. Costs are ℝ≥0, transition probabilities ℝ≥0∞ summing to 1 over S, and all values and expectations are in ℝ≥0∞, so infima over policies are lattice infima and +∞ is a genuine value. A history is the list of past state–action pairs, most recent first, with the current state, and a policy gives a distribution on A i for every history. Expectations are sums over histories of the path probabilities , which is the book's (2.6) and (2.9), not the dynamic programming recursion. The discount factor satisfies in every statement. An approximating sequence is indexed by with a start level ; its value functions are set to for the finitely many at which a given state is not yet in , which does not affect limits.
The optimality equation must not be made definitional by defining or through the recursion (3.2). The policy class must not be restricted to deterministic Markov policies either, since that would make the characterization in Theorem 3.1.2 a different statement. Theorem 3.1.2(ii)(2) is stated with the guard ; the book omits it, and without it the "only if" direction is false (see the item's note).
A complete development needs the first-step decomposition of the path law under a general policy, the generalized Fatou lemma for approximating distributions (Proposition A.2.5, a milestone of the Appendix A mission of this series), and lim inf / lim sup manipulations in ℝ≥0∞. The model definitions are reusable by every later mission of the series. Contributions are welcome at every milestone, including proofs of the definitional sanity facts (for instance ).
The irrationality of rules out an exact representation as a rational number. A quantitative question asks how closely rational numbers can approximate it as their denominators grow. The irrationality measure records the threshold exponent for exceptionally accurate rational approximations. This mission formalizes the historical upper-bound milestone listed as in the optimization constants project.
Mahler's 1953 paper establishes a stronger, explicit inequality in Theorem 1. The mission extracts its consequence for the irrationality measure and states that consequence through a shared Lean predicate. The number 42 is the chosen historical milestone; it is neither a claim about the exact value of the measure nor a claim to the strongest bound mentioned anywhere in Mahler's paper. Mahler, original p. 33.
Write for a numerator and for a positive denominator. The approximation error is the real number . The exponent describes an upper bound on the irrationality measure through an eventual lower bound on this error.
The shared predicate PiIrrationality.UpperBound B means that for every real , some natural-number threshold satisfies
for every integer and every natural number with . The threshold can depend on and on the chosen bound ; it cannot depend on the later choices of or . Numerators may be negative, zero, or positive. Fractions need not be in lowest terms. This is the epsilon characterization used in the definition of .
The goal is
represented by PiIrrationality.UpperBound (42 : ℝ). Expanded, the target is
The mission contains one shared definition and one goal theorem. The definition introduces the proposition without asserting any bound. The theorem has no additional hypotheses, and its proof is intentionally left open. Future historical-bound missions can import the same definition and state a different numeric bound without changing the quantity being tracked.
A finite upper bound restricts the quality of rational approximations to and excludes approximation at arbitrarily large exponents. The formal result would supply a reusable quantitative fact beyond the assertion that is irrational. The published mathematical result is known; the work requested here is a machine-checked proof of the stated consequence.
The shared definition also fixes the meaning of all entries in the accompanying campaign. A smaller bound makes a stronger claim. A proof of a stronger entry may establish this historical goal as a consequence, provided it uses the same definition and no extra hypotheses. The mission remains mathematically valid after further improvements to the numerical bound.
A proof that is irrational only establishes nonzero approximation errors. The target requires a uniform lower estimate over every numerator once the denominator passes a threshold. Checking finitely many rational approximations cannot establish the quantified conclusion. A formal development must control the dependence of its estimates and thresholds, and justify every passage between an analytic estimate and the final rational-approximation inequality.
The exact theorem from Mahler should be distinguished from this goal: his explicit uniform inequality is stronger than the eventual epsilon statement recorded here. A proof may pass through that uniform result, but the goal does not require a particular proof method, a particular threshold, or a separate treatment of every auxiliary theorem in the original paper.
The circle constant is Mathlib's Real.pi. Absolute value, division, and exponentiation in the displayed inequality are operations on the real numbers; in particular, is a real power. The denominator is explicitly positive, so division by zero cannot satisfy the premises. Allowing does not remove the positivity requirement on .
The definition is stored in Definitions.Def_PiIrrationality_UpperBound. The goal imports this definition instead of introducing another version of it. The conclusion is not placed among the theorem's assumptions. The definition contains no proof placeholder; the sole sorry is the open proof of the goal theorem. Contributions may establish supporting estimates or a complete proof while preserving these conventions.
Chess, checkers, Go and Backgammon share a feature that card games such as Poker lack: whenever a player moves, the player knows everything that has happened so far. von Neumann and Morgenstern call this perfect information and devote §15 of Theory of Games and Economic Behavior (1944; 3rd ed. 1953) to it. Their result is that such a game, viewed as a zero-sum two-person game, is strictly determined: it has a value that each player can secure with a pure strategy, without any randomization. For Chess this means that exactly one of three statements is true: White can force a win, Black can force a win, or both can force at least a draw ((15:D:a)–(15:D:c)).
Timeline. Zermelo (1913, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels) showed for Chess that either one side can force a win or both can avoid losing; his argument is not phrased in terms of strategies and a value, and was later corrected and completed by König (1927) and Kalmár (1928/29). von Neumann and Morgenstern (1944, §15) proved strict determinateness for every finite zero-sum two-person game with perfect information, including chance moves (15.7.1), and gave the explicit formula (15:12) for the value. Kuhn (1953, Extensive games and the problem of information, Annals of Mathematics Studies 28) recast games in tree form and extended the pure-strategy existence result to general-sum games with perfect information (subgame-perfect equilibria by backward induction).
A game tree is a finite rooted tree. Each leaf is a finished play and carries the payoff to player 1; player 2 receives . Each internal node is a move of one of three kinds , with alternatives leading to subtrees :
A pure strategy of player 1 is a complete plan choosing an alternative at every node of kind 1; does the same at every node of kind 2. The normalized form is the expected payoff to player 1, the expectation being over the chance moves. With the maxima and minima taken over the finitely many pure strategies,
Always ; the game is strictly determined when (14.4.2).
For a function of the alternatives of the first move , of kind , the operation of (15:8) is , or for . Applying these operations from the leaves back to the root gives the backward-induction value .
For every finite game tree ,
Both the equality and the value formula are part of the goal.
The theorem is the first existence result for the value of a class of games in pure strategies. It shows that the whole difficulty of the general zero-sum two-person game, the need for mixed strategies (§17), comes from imperfect information. It gives a construction as well as an existence proof: the value and optimal strategies are computed by backward induction, the procedure behind retrograde analysis of endgames, minimax search in game-playing programs, and the dynamic programming recursions of sequential decision problems with an adversary. The Chess trichotomy (15:D) is its best-known consequence.
Formalizing it adds a checked account of the passage from the extensive to the normalized form for a whole class of games, which the book carries out informally (15.4.2, 15.5.1: "the reader may verify it from the formalistic point of view"). The result is classical and fully proved in the book; the work is to formalize that proof on a tree model. Mathlib has saddle points (Order/SaddlePoint) and the minimax theorem for continuous functions (Topology/Sion), but no game trees, strategies of extensive games, or backward induction. No machine-checked version of this theorem with chance moves and the normalized form over complete plans is known to the mission.
The recursions (15:2)–(15:7) are not formal consequences of the definitions: and are extrema over whole plans of , while the right-hand sides are extrema over plans of the separate games . At a personal move of player 1, requires interchanging a Min over player 2's plans, which are functions of player 1's first choice, with a Max over that choice: this is exactly (13:E), a max-min equality that fails for general functions of two variables and holds here because the minimizing variable is a function of the maximizing one. A proof that treats the Max over and the Min over as interchangeable without this step is circular.
A second difficulty is the strategy spaces themselves. A complete plan chooses at nodes the plan itself excludes, so the pure strategies of are not simply pairs of a first choice and one strategy of the chosen subgame; the identification the book uses in 15.5.1 has to be justified by showing that the extra coordinates do not change .
A game is an inductive type GameTree with constructors leaf w, chance α p next hp hsum, move1 α hα next, move2 α hα next; alternatives are Fin α (numbered from ). The conditions , and at personal moves are constructor fields, so every tree is a legitimate game. Pure strategies are dependent types Strategy1 t, Strategy2 t defined by recursion on the tree (complete plans), with Fintype and Nonempty instances; is payoff t τ₁ τ₂, the expected leaf payoff; v1, v2 are Finset.sup'/Finset.inf' over all strategies, so every Max and Min is attained.
Standing hypotheses and conventions taken from the book:
The book's formal model is the set-theoretic one of §§9–10, with partitions of the set of plays; the tree restates it for the perfect-information case and does not formalize §§9–10. The book fixes one length for all plays; trees with plays of different lengths contain the book's games as a special case, so the goal is at least as strong as the book's theorem.
Strategies are plans, never responses: a strategy of player 1 is fixed before play and cannot depend on player 2's strategy, which would make trivial. Chance moves are part of the goal; a version without them proves only the Chess case and is weaker than the book.
Reusable beyond this mission: the tree model, its strategy types and the normalized form, which later chapters on extensive games can import. Welcome contributions: proofs of the milestones, and a lemma identifying the strategies of with the book's recursive description (15.4.2, 15.5.1).
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.
Traffic information systems (TIS) such as navigation apps send drivers noisy signals about the state of a road network: incidents, weather, closures. When several such systems coexist, each with its own subscriber base and its own information, a natural question for operators and regulators is whether subscribing to one system rather than another actually lowers a driver's expected travel cost in equilibrium, and how this advantage depends on how many drivers use each system. More information for one population also changes the congestion everybody else faces, so the answer is not simply "more information is better".
Wu, Amin and Ozdaglar (Operations Research 69(1), 2021) answer this question for nonatomic routing games with heterogeneous, possibly correlated information. Their model builds on the weighted potential game framework of Sandholm (2001) and on sensitivity analysis of convex programs. This mission formalizes their Section 5 result: for any two populations the sign of the relative value of information is determined by which of three explicitly computable size regimes the population sizes lie in, and the relative value decreases as one population grows at the expense of the other.
A Bayesian routing game has a finite set of populations , one per TIS, a finite set of network states , and for each population a finite nonempty type space of signals. A common prior is a probability distribution on , . A network with a single origin–destination pair has edges and a finite nonempty set of routes ; each edge has a state-dependent cost that is positive, strictly increasing and differentiable. The total demand is , and population carries the fraction of it, with and .
A strategy profile assigns to each population and type a split of its demand over routes. It induces the route flow and the edge load . With the belief , type evaluates route by its expected cost . A Bayesian Wardrop equilibrium (BWE) is a feasible in which every type uses only routes of minimal expected cost. The equilibrium population cost is at a BWE .
The game has a weighted potential ; its minimum over feasible profiles is the equilibrium potential value . For two populations , the direction moves demand share from to , and is the total share of the other populations. The impact of information measures how much of population 's demand is moved by its signal. Two thresholds are computed from the optimal set of an auxiliary convex program over route flows in which the separate information constraints of and are merged. They define three regimes: (), () and (). The relative value of information is .
For and admissible (in the simplex with ), and every BWE of ,
and is nonincreasing along : for with both endpoints admissible.
The route to the goal follows the paper: Lemma 1 (weighted potential), Lemma 2 (strict convexity of the edge-load potential), Theorem 1 (equilibria are the minimizers of ; unique edge load), Lemma 3 (unique Lagrange multipliers), Proposition 1 (the feasible route flows form a polytope ), Proposition 2 (equilibrium route flows minimize over ), Lemma 4 (), Theorem 2 (equilibrium flows in each regime), Proposition 3 ( decreases, stays constant, increases along in the three regimes) and Lemma 5 ( is convex and directionally differentiable, and ).
Theorem 3 says that a population has an advantage over another exactly when it is the minor population of the pair, relative to thresholds that depend only on the other populations' sizes. Both populations face the same equilibrium cost in the middle regime. It gives a procedure for comparing two information systems without computing equilibria for each size vector: solve one convex program, read off two thresholds, and locate . The paper's Section 6 uses the same machinery, through Lemma 5, to characterize the equilibrium adoption rates of information systems.
The paper proves these results with the main proofs in the article and the sensitivity-analysis lemmas (Lemmas EC.1–EC.4) in its e-companion. None of them has a machine-checked proof. The formalization requires a Lean account of Bayesian Wardrop equilibria, of the equivalence between equilibria and a convex program, and of directional derivatives of the optimal value of a parametric convex program. Parts of this are reusable for any nonatomic routing or congestion game.
The equilibrium strategy profile is not unique and changes discontinuously with . Differentiating equilibrium costs in directly therefore fails. The paper instead works with the optimal value , whose one-sided directional derivative is expressed through Lagrange multipliers. That requires a sensitivity theorem for convex programs whose constraints depend affinely on the parameter, together with uniqueness of multipliers, which fails for populations of size zero. The regime analysis also needs a characterization of the route flows that are induced by feasible strategy profiles. That set is described by the nonlinear-looking constraint , a minimum over types inside a sum over routes. Strict monotonicity of in the side regimes needs the tightness of an information constraint at every equilibrium, not only at one.
The model is a Lean structure BayesRouting.VOI.Game over finite types of populations, type spaces, states, edges and routes. Routes are given by their edge sets, and the directed-graph structure is not used. Type spaces and the route set are nonempty. The prior is a probability distribution, , and costs are positive on nonnegative loads, strictly increasing and differentiable on . One assumption is added: every type profile has positive probability. It makes beliefs well defined and the equilibrium edge load unique, and it excludes perfectly correlated signals.
Conventions: is the last form of eq. (7), which does not divide by . is the maximum of eq. (16) over the reference profile, so that is exactly (14d). and the thresholds are sInf/sSup over sets that are nonempty and compact for size vectors in the simplex, and every statement keeps size vectors there. Statements about "the" equilibrium are stated for every BWE, and existence of a BWE is a separate item, so they are not vacuous. The thresholds are defined from the optimal set of the auxiliary program, not assumed as parameters. Taking them as parameters constrained only by Lemma 4 would give a different theorem.
Disclosed deviations: Lemma 2's clause assumes costs; Lemma 3 is stated for populations of positive size; Lemma 5 assumes ; Proposition 3 is stated with strict monotonicity in the side regimes, as used in the proof of Theorem 3. Contributions of reusable infrastructure are welcome: interval-integral potentials of monotone costs, KKT theory for polyhedral constraints, and directional derivatives of parametric optimal values.
Extremal graph theory asks how many edges a graph on vertices can have without containing a fixed graph . The answer, the Turán number , and the graphs attaining it, the set of extremal graphs, are known precisely only for special ; the Erdős–Stone–Simonovits theorem gives , where is the chromatic number.
Spectral extremal graph theory asks the same question with the number of edges replaced by the spectral radius , the largest eigenvalue of the adjacency matrix. Since , a spectral bound implies an edge bound, and spectral extremal results are usually stronger than their edge versions. Nikiforov (Linear Algebra Appl. 427, 2007) showed that the Turán graph maximises among -free graphs, so for the spectral and the edge extremal graphs coincide. Whether this happens for other is the subject of the paper.
Timeline:
All graphs are finite and simple. For a graph on vertices, is its adjacency matrix and is the largest eigenvalue of . A graph is -free if no subgraph of is isomorphic to . The Turán number is the maximum number of edges over -free graphs on vertices, and is the set of -free -vertex graphs with edges. The Turán graph is the complete -partite graph on vertices with parts of sizes or .
The hypothesis on is: for fixed integers and and all large , and every graph in contains a spanning copy of , i.e. is plus edges. The paper states "adding edges" and fixes the constant at the start of Section 3 (p. 4): "We may assume that the graphs in are obtained from by adding edges." The mission follows that reading. Examples: with , the friendship graphs, and the intersecting cliques .
A graph is spectral extremal for if it is -free and for every -free on the same vertices.
For , and satisfying the hypothesis, there is such that for all every spectral extremal graph for on vertices satisfies
The statement contains no numerical constant, and depends only on , , .
The milestones follow the proof, in order: strict monotonicity of under proper subgraphs of a connected graph (Lemma 2.3); connectivity of (Lemma 3.1); the bound (Lemma 3.2); spectral stability for (Corollary 2.6); for every maximum -cut , and (Lemma 3.3); a counting inequality for intersections (Lemma 2.8); and minimum degree above (Lemma 3.6); at most vertices of each part have a neighbour in that part, and all others see every other part completely (Lemma 3.7); Perron entries for (Lemma 3.8); (Lemma 3.9); balancing two parts of a complete multipartite graph increases (Lemma 2.7); and the maximum partition is balanced, (Lemma 3.10).
The theorem settles the Cioabă–Desai–Tait conjecture: for every whose extremal graphs are Turán graphs plus a bounded number of edges, the spectral extremal problem reduces to the edge extremal problem for large . This recovers the earlier cases (friendship graphs, the graphs , intersecting cliques) at once, and it turns any future determination of of this type into a spectral result with no further work.
The result is proved on paper; it has no machine-checked proof. Mathlib has Turán's theorem (extremalNumber_top, uniqueness of turanGraph) and the definition of extremalNumber, but no spectral extremal graph theory: no Perron–Frobenius theorem for graphs, no spectral Turán theorem, no stability theorem. The formalization would supply these, and the milestone statements are independently reusable: strict monotonicity of (Lemma 2.3), the spectral comparison of complete multipartite graphs (Lemma 2.7) and spectral stability (Corollary 2.6) are standard tools of the area.
The natural first idea, comparing with an extremal graph by Rayleigh quotients, fails at the start: gives only , far from . Closing an additive gap of edges requires control of the Perron vector to within at every vertex and exact control of the part sizes. The second is the delicate step: an imbalance of one vertex between two parts costs in , while the extra edges contribute only beyond the Turán graph, so the two effects must be compared at different scales. Further, the proof needs the deep spectral stability theorem of Nikiforov (Lemma 2.5), whose own proof is long.
Graphs on vertices are SimpleGraph (Fin n), matching Mathlib's extremalNumber n F; is a graph on any finite type. is the largest eigenvalue of G.adjMatrix ℝ (index of Mathlib's decreasingly sorted eigenvalues₀), not an absolute value and not a norm. "-free" is F.Free G (no copy of , not necessarily induced). "Sufficiently large " is ∃ N, ∀ n ≥ N with chosen after and before ; "sufficiently small " is ∃ ε₀ > 0, ∀ ε ∈ (0, ε₀). Partitions are labellings Fin n → Fin r whose parts may be empty; the Section 3 lemmas hold for every partition maximising the number of crossing edges. Lemma 3.8 carries the extra hypothesis , because as printed it is false for (for and the Perron vector of has entries below ); the goal does not assume it.
Trivializing formalizations are ruled out: is not defined from the edge count (which would make spectral and edge extremality the same), the hypothesis on does not contain the conclusion and is satisfiable (a sorry-free check for , was compiled), the conclusion is and not a weaker bound, and the threshold is not chosen after .
A complete development needs the Perron–Frobenius theorem for irreducible nonnegative symmetric matrices, the Rayleigh quotient characterisation of , the spectrum of complete multipartite graphs, Nikiforov's spectral stability lemma, and max-cut partition arguments. All of these are reusable beyond this mission, and proofs of any milestone, of the cited Lemmas 2.1, 2.2 and 2.5, or of Nikiforov's spectral Turán theorem are welcome.
How many times can points and lines in the plane meet? The question is the prototype of incidence geometry, and the answer controls a long list of problems in discrete and computational geometry: the number of lines rich in points, the number of distinct distances or unit distances among points, the complexity of arrangements, and sum–product estimates in additive combinatorics. Erdős asked for the order of magnitude when and conjectured that the answer is ; Erdős and Purdy asked for the matching bound on the number of lines containing at least of the points.
Szemerédi and Trotter settled both questions in Extremal Problems in Discrete Geometry (Combinatorica 3 (1983) 381–392, doi:10.1007/BF02579194). Their principal theorem bounds the number of point–line incidences by over the whole range , and the same paper derives from it the Erdős–Purdy bound on -rich lines, a version of Dirac's conjecture (proved independently by Beck, Combinatorica 3 (1983)), and a bound on the number of sequences of line densities.
Timeline.
Work in the Euclidean plane , written Plane in the Lean development. A line is an affine subspace whose direction space has dimension one (IsLine l). Let be a finite set of points and a finite family of distinct lines. The number of incidences is
written incidences P L. The degree of a point is the number of lines of through it (degree L p), and the density of a line is the number of points of on it (density P l); so .
For the covering lemma, coordinate axes are fixed and a square is a closed axis-parallel square with side (closedSquare (a, b, s)); its interior is the open square (openSquare). A square contains the points of in the closed square, and a family of squares covers the points lying in at least one of them.
There is an absolute constant such that for every finite point set with and every finite family of distinct lines,
The goal leaves unspecified. The paper's proof gives , and later proofs give much smaller values; any improvement of the constant still proves this statement.
The result. The bound is sharp up to the constant throughout the range , as integer-grid configurations show. Outside that range the trivial bounds and take over. Theorem 1 is the source of the bound on -rich lines (the paper's Theorem 2), of Beck's theorem (Theorem 3), and, through them, of the unit-distance bound , of the Elekes sum–product estimate and of many algorithmic bounds on arrangements. It is the first nontrivial case of the polynomial-partitioning incidence theory developed since 2010.
Formalizing it. The theorem has been proved, and reproved in several ways, for four decades. To the best of the mission's knowledge Mathlib has no statement of it, of the crossing lemma, or of any point–line incidence bound in the Euclidean plane. This mission produces a checked statement of the theorem with lines as genuine one-dimensional affine subspaces and an absolute constant. It also produces checked statements of the auxiliary facts the 1983 proof uses. A complete proof may follow the original argument, the cutting argument or Székely's crossing-lemma argument; any of them closes the goal.
Counting pairs of lines through common points (milestone 1) gives only , and its dual gives . These Cauchy–Schwarz bounds use only the fact that two lines meet at most once, a property shared by lines in finite projective planes, where the incidence count genuinely reaches order . Any proof of the bound must therefore use a property of the real plane that the finite geometries lack: order, continuity, or the planarity of drawings. Szemerédi and Trotter use it through a covering lemma for axis-parallel squares, whose proof is only cited in the paper ([7]). The remaining difficulty is keeping the constants of a multi-stage minimal-counterexample argument under control.
The plane is EuclideanSpace ℝ (Fin 2). A line is an AffineSubspace ℝ Plane whose direction has Module.finrank equal to . Every statement requires IsLine of each member of , so neither the whole plane nor a single point counts as a line. The points form a Finset Plane and the lines a Finset (AffineSubspace ℝ Plane), which makes the lines distinct. Incidences, degrees and densities are Finset.filter cardinalities under classical decidability. Powers , are Real.rpow of the counts cast to , and is Nat.choose.
In the goal, the constant is quantified before the points and the lines. The form "for every configuration there is a " is trivially true (take ) and is not this theorem. Both ends of the range are kept exactly: without the lower end, a single line through collinear points has incidences, more than for large .
The goal follows the wording of p. 381 ("at most"). The restatement on p. 383 says "less than", which fails at and is equivalent for after doubling . The covering lemma is stated with the added non-degeneracy hypotheses . As printed it fails when (no square can hold points), and when with .
A full development needs a real-plane incidence toolkit: a crossing lemma or a cutting lemma, or the covering lemma with its quadtree proof. That toolkit is reusable for -rich lines, Beck's theorem, unit distances and sum–product bounds, and contributions of such infrastructure as separate theorems are welcome. The three numerical milestones are self-contained real-analysis exercises.
The security of the RSA cryptosystem rests on the assumed difficulty of factoring large integers, and the best known classical algorithms for factoring run in super-polynomial time. In 1994 Peter Shor showed that a quantum computer can factor an -digit integer in time polynomial in (Shor, SIAM J. Comput. 1997; conference version FOCS 1994). The algorithm has two parts. A classical reduction, due to Miller (1976), turns factoring into order finding: given coprime to , find the least with . The quantum part solves order finding.
This mission formalizes the quantum part as Shor analyzes it in §5 of the journal paper: the construction of the quantum state, the probability of each measurement outcome, and the classical post-processing that reads off the measured value. The paper's claim is that one run of this procedure returns with probability at least .
Timeline:
Fix an integer and an integer coprime to . Its order is the least with ; since is a unit, . Let be the power of with .
A quantum state on two registers, the first holding and the second a residue , is a complex vector indexed by the basis states . Measuring it returns with probability .
The Fourier matrix is the matrix with entries , with rows indexing inputs and columns outputs. The algorithm
The observed gives us if some fraction with lowest-terms denominator below is within of , and every such fraction has lowest-terms denominator exactly . In the Lean development these objects are preFourierState, finalState, outcomeProb and yieldsOrder, in the namespace ShorAlgorithms.OrderFinding, and the shared definition ShorAlgorithms.Shared.fourierMatrix.
For all sufficiently large , with , and as above,
where is the state (5.4). The threshold on is uniform in and ; it is the paper's "for sufficiently large " from the per-state bound.
The goal is the quantitative statement behind "order finding is in bounded-error quantum polynomial time": since for a constant (Hardy and Wright, Thm. 328), repetitions find with high probability, and Miller's reduction then factors . Without the bound, the algorithm is a procedure with no guarantee.
The result is proved, in the paper and in textbooks (Nielsen and Chuang, 2000, §5.3), usually with a phase-estimation analysis rather than Shor's direct count. What this mission adds is a machine-checked proof of Shor's own argument, with his choice of and his constants, starting from the state built by applying to (5.2). Formal proofs of idealized versions exist elsewhere, for instance in the exact-period model where divides and the output is uniform on peaks, but that model removes the approximation that the bound is about. Legendre's theorem on continued fractions is already on the platform (FamousTheorems.legendre_continued_fraction_theorem) and is included as a reference item.
The obvious route is to compute the output distribution in closed form. That works only when divides ; here is a power of and is arbitrary, so the amplitudes are geometric sums of terms whose phases do not cancel exactly. The per-state bound requires a lower bound on such a sum that is uniform in , and , with error terms of order controlled against a main term of order . The constant leaves only a small margin below the limiting value , so the errors must be bounded explicitly, not merely shown to vanish.
The second difficulty is the counting: distinct coprime numerators must give distinct outcomes in , and each good must determine uniquely, which uses and .
Conventions the statements commit to:
Fin q × ZMod n → ℂ; the matrix convention is row = input, so applying to the first register gives the amplitude at .orderOf (x : ZMod n). enters through the three hypotheses , , , not through a function of .Rat.den.Typing the closed form (5.4)–(5.6) in as the definition of the final state would make milestone 1 trivial and hide whether the probability model is the paper's; the definitions exclude this by construction.
Not stated: the polynomial running time of any step, the repetition count (no explicit constant), the reversible modular exponentiation of §3, and the post-processing heuristics on p. 1501. Needed infrastructure: bounds on geometric exponential sums, Euler's totient, Diophantine approximation by fractions with bounded denominator, and Mathlib's continued fractions. Lemmas on geometric sums of roots of unity and on the order of units mod are reusable in the companion discrete logarithm mission.
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.
Periodic solutions are the simplest non-stationary long-time behaviour of an autonomous system : limit cycles in oscillators and population models, closed orbits of conservative systems. The first question about a periodic orbit is whether it is stable. Poincaré introduced the first-return map on a transversal section, which turns this question into a question about a fixed point of a map in one dimension less. Floquet theory attacks the same question through the linear periodic system obtained by linearizing along the orbit. This mission formalizes Chapter 12, §§12.1–12.2 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version, DOI of the published book). That chapter proves the two approaches agree and derives the standard stability and persistence criteria from this.
Let be open, with , and let be the flow of with maximal intervals : is the unique maximal solution with . A point is periodic with period if and for . Its orbit is then a closed curve.
Linearization along the orbit. Put , a -periodic matrix. The first variational equation is , and denotes its principal matrix solution: , . The monodromy matrix based at is
The Poincaré map. A transversal section is with open, , and on . If there is a return time near with and . The Poincaré map is
Its derivative is a linear map of the -dimensional tangent space into itself.
Stability. The orbit is stable if every neighborhood of contains a neighborhood of from which solutions stay in for all . It is asymptotically stable if moreover for all in some neighborhood of . A periodic orbit is hyperbolic if has no eigenvalue on the unit circle.
For every ,
where is the characteristic polynomial. So the eigenvalues of together with the single value are exactly the eigenvalues of the monodromy matrix, with multiplicities. In particular they depend neither on the section nor on the base point on the orbit.
The result. Theorem 12.4 is the bridge between the two standard tools for periodic orbits. The Floquet multipliers of can often be computed or estimated, for instance through Liouville's formula . The Poincaré map is where the dynamics is decided, for instance through the fixed-point stability theory of maps. Corollaries 12.3 and 12.5 and Lemma 12.6 are the resulting stability tests. Lemma 12.7 is the structural-stability statement for hyperbolic orbits that bifurcation theory starts from. Theorems 12.8–12.10 (stable manifolds of periodic orbits) build on the same objects.
Formalizing it. All results are classical and proved in the book. None has a machine-checked proof on the platform or, as far as is known, in Mathlib, which has neither Poincaré maps nor the linearization of flows along orbits. The work is a formalization of the known proofs. It needs differentiability of the flow with respect to initial conditions, and that part is reusable across the whole of qualitative ODE theory.
The algebra of Theorem 12.4 is short. The two linear maps act on different spaces: on , and on the hyperplane . That hyperplane is in general not orthogonal to , not a coordinate hyperplane, and not invariant under . Any comparison has to go through the derivative of , which involves the derivative of the implicitly defined return time. Behind all this sits the differentiability of in and the variational equation it satisfies, which Mathlib does not provide for local flows. For the stability milestones, the delicate step is passing from the discrete iterates of on back to the continuous flow near the whole orbit. That requires uniform control over one period.
The state space is Fin n → ℝ. Norm-dependent notions (distance to the orbit, neighborhoods) do not depend on the choice of norm. The flow is local: IsMaximalFlow f M I Φ characterizes and by maximality and uniqueness, and 's values outside its domain are never used. Derivatives are Mathlib's fderiv. The section is the book's general with , not a hyperplane chosen orthogonal to . The return time is any function on a neighborhood of with and ; such a function agrees with the book's near . is an endomorphism L of LinearMap.ker (fderiv ℝ S x₀) that agrees with the derivative of there (IsPoincareDerivative). Theorems 12.4 and 12.5 assert that it exists. Eigenvalues are complex roots of characteristic polynomials.
Conventions and readings:
Needed infrastructure: existence, uniqueness and dependence on initial conditions for local flows; the implicit function theorem (Mathlib); characteristic polynomials and determinants of endomorphisms of finite-dimensional subspaces (Mathlib); Liouville's formula; stability of fixed points of maps with contracting linearization. Contributions of any of these as standalone lemmas are welcome.
Several classical theorems of combinatorial optimization say that a family of sets arising from a graph packs: the maximum number of pairwise disjoint members equals the minimum size of a set meeting every member. König's theorem on bipartite graphs, Menger's theorem, the max-flow min-cut theorem of Ford and Fulkerson, Edmonds' branching theorem and the Lucchesi–Younger theorem all have this form (Seymour 1977, (1.1)–(1.5)). In the capacitated version (weights on elements, integral flows) the max-flow min-cut theorem says more: the packing property survives every deletion and replication of elements. Clutters with this stronger property are called Mengerian. For each – matrix they are exactly the systems whose covering linear program and its dual have integral optima for every integral weight vector, which is why the notion matters to integer programming and polyhedral combinatorics.
Seymour's paper answers the question for the class of binary clutters, the clutters coming from binary matroids, which includes path collections, cut collections and odd-circuit collections of graphs. Earlier, Gallai's theorem implied that ports of regular matroids are Mengerian (Seymour 1977, p. 200); combined with Tutte's excluded-minor characterization of regular matroids, this showed that binary clutters without or minors are Mengerian. Seymour shows that the second excluded minor is unnecessary, so a single small clutter is the only obstruction.
All sets are finite. A clutter is a finite collection of finite sets, no member of which is contained in another; and are the two trivial clutters. Its ground set is . The blocker is the collection of minimal subsets of that meet every member of , and is the minimum cardinality of a member of .
is Mengerian if , or if for every weight map there is an integral packing with for each and
For a set , the deletion is and the contraction is the collection of minimal members of (minimal, not minimal nonempty). A minor of is any clutter obtained by a finite sequence of deletions and contractions.
A clutter is binary if is odd for all and ; this is condition (3.2)(ii) of the paper, which is equivalent to being a port of a binary matroid. Finally
the triangles of with its edges labelled .
For the structure theory, a circuit of a binary clutter is a minimal nonempty with even for every ; and are parallel when is a circuit, and the point is the parallel class of . With , is critical if . In a critical binary clutter, means that every member of containing contains while , and is initial if no has . MBC abbreviates "Mengerian binary clutter".
For every binary clutter ,
In the order the proof uses them:
The theorem is an excluded-minor characterization of the max-flow min-cut property. For binary clutters it decides exactly when the covering system , has integral optimal primal and dual solutions for every integral cost vector, and it identifies as the single obstruction. Its matroid form (the Corollary, p. 220) states that for a matroid the port is Mengerian for every element if and only if is binary and has no minor. Consequences discussed in the paper include the two-commodity setting of (3.5): the clutter of minimal edge sets joining to or to is Mengerian exactly when the graph does not reduce to the configuration of its Figure 2. The theorem is also a basis for later work on ideal and Mengerian clutters, such as Cornuéjols' book Combinatorial Optimization: Packing and Covering (SIAM, 2001).
The result has been proved since 1977. To our knowledge no machine-checked proof exists. Mathlib at the pinned revision has matroids but no clutters, blockers, clutter minors, or matroids representable over GF(2). This mission builds that layer. The minor-closedness of the Mengerian property (2.3), the parity decomposition (3.6)(iii) and the structure theory of critical Mengerian binary clutters (4.3)–(4.6) are results in their own right and are useful beyond the main theorem.
The "only if" direction is short: minors of Mengerian clutters are Mengerian, and fails with unit weights. The "if" direction is, in the author's words, "very much harder". A natural first idea is to show directly, by LP duality, that the covering polyhedron of a -free binary clutter is integral. This does not work: integrality of the polyhedron is the weak max-flow min-cut property, and itself has that property while not being Mengerian, so no argument that sees only fractional optima can separate the two cases. The paper's proof works with a minimal counterexample and derives the minor from the structure of critical Mengerian binary clutters in Section 4; its intermediate claims (5.2)–(5.39) hold only for that minimal counterexample, which is why they are not milestones here.
Elements form a type α with decidable equality. A clutter is L : Finset (Finset α) with the clutter axiom as a hypothesis, is the union of members, and deletion and contraction take an arbitrary finite set . Weights and packings are -valued. The minimum in the Mengerian condition is expressed as "some of least weight has weight equal to the packing value", never as an infimum. is Mengerian by the paper's convention, and , which the paper leaves undefined, has the junk value in Lean; every item reading excludes or is vacuous there. "Minor" is the reflexive–transitive closure of single deletions and contractions. "Has a minor" means that some minor equals the image of (on Fin 6, with the paper's labels shifted down by one) under an injective relabelling Fin 6 ↪ α. Binary clutters are defined by (3.2)(ii); the paper defines them as ports of binary matroids and quotes (3.2) [15, 28] for the equivalence, and Mathlib has no GF(2)-representable matroids at this revision. Circuits are defined intrinsically, which makes (3.6)(ii) hold by definition.
Four readings would change the theorem and are ruled out: real-valued packings (the weak max-flow min-cut property, which has, so the goal would be false), a non-minimal blocker or one not restricted to , dropping the exception, and reading " minor" as literal equality instead of isomorphism.
A complete development needs the blocker calculus ((2.1), (2.2), cited from [28] with proofs omitted), the parity theory of binary clutters, and the replication operation . The clutter layer (blocker, minors, Mengerian, binary, circuits) is reusable for later work on ideal clutters, Lehman's theorem and the Corollary's matroid form. Proofs of any milestone, of the helper facts , (2.1) and (2.2), and of the equivalences in (3.2) are welcome.
The quantum harmonic oscillator is the Schrödinger operator of a particle in a quadratic potential. It describes small vibrations around an equilibrium, the modes of the electromagnetic field, and phonons in a crystal. It is also one of the very few Schrödinger operators whose spectrum and eigenfunctions are known in closed form. The eigenvalues are equally spaced, and the eigenfunctions are Hermite functions. Its algebraic treatment by creation and annihilation operators goes back to Dirac (The Principles of Quantum Mechanics, 1930). That treatment became the template for second quantization and Fock space.
The same chapter of G. Teschl's Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009, Chapter 8, AMS page) contains two further results that use commutation relations. The first is the Heisenberg uncertainty principle (Heisenberg 1927; the general form for two observables is due to Robertson, Phys. Rev. 34 (1929)). The second is an abstract statement that and have the same spectrum away from . Physicists call this supersymmetric quantum mechanics, and Teschl uses it later for the hydrogen atom. This mission follows Teschl's Sections 8.1–8.4.
Let be a complex Hilbert space. A linear operator is a linear map defined on a subspace , its domain. is symmetric if is dense and for all . For a closed operator and , the resolvent exists when maps bijectively onto with a bounded inverse. The resolvent set is the set of such , and the spectrum is . An operator is essentially self-adjoint on its domain if its closure is self-adjoint.
For with (a state), the expectation is and the mean-square deviation is . The commutator is for , where .
Fix a frequency . On with Lebesgue measure, let
where and is the Euclidean norm. With and Teschl's units (, mass , so the free Hamiltonian is ), the harmonic oscillator is the operator
In one dimension the ladder operators on are
The Hermite polynomials are . The Hermite functions are
and on , .
For every the operator above exists. It is essentially self-adjoint on , the functions , , form an orthonormal basis of consisting of eigenvectors of , and
with equality if for a real , or if is an eigenvector of or .
The last two milestones do not enter the goal. They are the chapter's other two theorems and use the same operator-theoretic layer.
Theorem 8.5 is the rigorous form of the most used exactly solvable model of quantum mechanics. Once it is available, the Hermite functions become an orthonormal basis of that diagonalizes a concrete differential operator. That basis underlies Mehler's formula and the Fourier transform's action (Eq. (8.46)). Perturbation arguments around the oscillator also start from it, and so does the construction of Fock space. The uncertainty principle is the basic quantitative constraint on simultaneous measurement. Theorem 8.6 gives an eigenvalue transfer mechanism that Teschl reuses to compute the hydrogen spectrum (Section 10.4).
Formally, the mission asks for a machine-checked proof about an unbounded differential operator on , stated on a concrete core. Mathlib has unbounded operators (LinearPMap, closure, adjoint), spaces, Gaussian integrals and the probabilists' Hermite polynomials. It has no statement identifying the spectrum of a concrete Schrödinger operator. These results are proved in every textbook, but none of them has been formalized in this form.
The algebra of Eqs. (8.36)–(8.41) is a finite computation with polynomials times a Gaussian. The work in the goal is analytic. Essential self-adjointness is a statement about the closure of an operator on a non-closed domain. Symmetry of together with a family of eigenvectors in does not give it by definition, and the relevant criterion for unbounded operators is not in Mathlib. Completeness of the eigenfunctions in is a density statement about a concrete function space (Lemma 8.3), and it has to be transferred from one dimension to three. The spectrum is asked for the closure , not for on : the eigenvalues are easy to exhibit, but showing that no other point of lies in requires control of on all of . Finally, the Rodrigues formula (8.42) and the ladder construction (8.40) define the same functions only after an identity for all derivatives of .
is a complex inner product space with CompleteSpace; separability is not assumed, and no statement needs it. Operators are Mathlib LinearPMaps H →ₗ.[ℂ] H. is LinearPMap.adjoint, and every statement using it assumes a dense domain. Self-adjointness is Mathlib's IsSelfAdjoint, and essential self-adjointness is IsSelfAdjoint H.closure. and are defined in the mission for LinearPMaps (bounded two-sided inverse of ); Mathlib's Banach-algebra spectrum is not used. is Lp ℂ 2 volume on EuclideanSpace ℝ (Fin n). The Laplacian is the sum of second Fréchet derivatives along the unit vectors. Hermite polynomials are defined by the Rodrigues formula, not as Mathlib's probabilists' Polynomial.hermite. No projection-valued measure, functional calculus or Fourier transform is taken as data.
The oscillator is not defined as a construction. IsHarmonicOscillator ω H states that and that acts on a representative as . This determines uniquely, and the goal also asserts that such an exists. Trivializing formalization ruled out: defining as the diagonal operator would make the spectrum immediate. Here is the differential operator on , and its eigenvalues must be derived.
Two choices differ from the printed text. First, Teschl's (8.34) writes the domain with , but his (8.39)–(8.41) and the conclusion use . The mission uses , which equals (8.34) for . Lemma 8.3 is stated for (8.20)'s itself. Second, Theorem 8.6 prints "", and the mission states the intended . The uncertainty principle adds explicitly; the book assumes it through its definition of a state.
Reusable pieces are the product of LinearPMaps, spectrum and resolvent for unbounded operators, the Gauss–polynomial core and its density, and the Hermite-function API. Contributions of general lemmas are welcome, for example "an operator with an orthonormal eigenbasis in its domain is essentially self-adjoint" and the spectrum of such an operator.
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.
A second-order elliptic equation in divergence form, , is usually solved in a weak sense: the Lax–Milgram theorem or the Fredholm alternative produces a function , which has only first-order weak derivatives, and the equation holds after one integration by parts against every test function. The phrase "solution of a PDE" then covers objects for which the second derivatives appearing in need not exist. Regularity theory closes this gap: under smoothness of the coefficients and the data, weak solutions have exactly as many derivatives as the equation suggests. It is used throughout the calculus of variations, spectral theory and nonlinear PDE.
The interior estimate for divergence-form operators with coefficients goes back to the difference-quotient technique of L. Nirenberg (1955) and is standard in textbooks such as Evans, Partial Differential Equations, §6.3, and Gilbarg–Trudinger, Chapter 8. This mission follows the treatment in J. K. Hunter's lecture notes, §4.11 and Appendix 4.C.
Points of are written , and is the th standard unit vector. Let be an open set. A set is compactly contained in , written , if is nonempty and open, its closure is compact, and .
A test function is an infinitely differentiable with compact support inside (the space ). A function is the weak derivative of a locally integrable (multi-index ) if for all test functions . The Sobolev space consists of the functions whose weak derivatives of order at most exist and lie in , with norm ; more generally uses . The space is the closure of in .
The coefficients are functions , , which are bounded (), symmetric () and uniformly elliptic: for some ,
Given , a function is a weak solution of if
No boundary condition is imposed on .
For the th difference quotient of is , and with pointwise length .
If moreover , then for every there is a constant , depending only on , , and the coefficients, such that every weak solution of with satisfies and
The goal theorem shows that weak solutions of divergence-form equations with coefficients are strong solutions: their second weak derivatives are square integrable on compact subsets, so the equation holds pointwise almost everywhere. The iterated version (Theorem 4.28) and its corollary turn the existence theory for weak solutions into existence of smooth solutions whenever the coefficients and data are smooth; in combination with Sobolev embedding this is how one proves that eigenfunctions of the Dirichlet Laplacian on an open set are smooth in its interior.
All of these results are classical and fully proved in the literature. To the best of the platform's records, none is formalized: Mathlib has Lebesgue spaces, Fréchet derivatives and Hilbert-space tools, but neither weak derivatives nor Sobolev spaces on open sets, and there is no elliptic regularity result in any proof assistant known to the maintainers. A complete development would therefore also deliver reusable infrastructure: weak derivatives, and its norm, difference quotients and their calculus, and cut-off functions subordinate to .
The formal computation behind the estimate — testing the equation against for a cut-off and using ellipticity — is illegitimate for a weak solution, because the test function involves second derivatives of that are not yet known to exist. Replacing derivatives by difference quotients makes every step meaningful but requires a separate theory: commuting difference quotients with weak derivatives, a discrete product rule and integration by parts, and a compactness argument in (reflexivity) that turns an -uniform bound into a weak derivative. The error terms involve difference quotients of the coefficients, which is where enters, and the final estimate has to be closed with a Cauchy inequality and a second localization to replace by .
Space is = EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; coordinates are 0-based (i : Fin n), so the book's are EuclideanSpace.single 0 1, …. Functions are real-valued on all of and only their values on the relevant open set matter. Weak derivatives (HasWeakDeriv, weakDeriv), (MemW), its norm (sobolevNorm, valued in ℝ≥0∞) and (MemW0) are defined in the mission; weakDeriv is a chosen representative and is only used under hypotheses guaranteeing existence. Exponents are p : ℝ≥0∞; conjugate exponents use ENNReal.HolderConjugate. and are ContDiffOn ℝ k and ContDiffOn ℝ ∞ on (smooth, not analytic); "" for a Sobolev function means a.e. equality on with such a function.
Conventions committed to:
∃ C : ℝ is quantified after , the coefficients, the ellipticity constant and (and ), and before and .The theorems are not trivialized by junk values: the difference quotient is only used at , the weak formulation's Bochner integrals are integrable under the stated and hypotheses, and the conclusion asserts existence of all weak derivatives of order at most two, not merely a bound on a norm that could be computed from junk representatives.
Contributions welcome: a library of weak derivatives and Sobolev spaces on open subsets of compatible with these definitions, cut-off functions for (Mathlib's ContDiffBump and exists_smooth_tsupport_subset are natural starting points), and Banach–Alaoglu for , .
One-dimensional maps are the smallest systems in which deterministic dynamics becomes unpredictable. Chapter 11 of Gerald Teschl's graduate text Ordinary Differential Equations and Dynamical Systems (author's version; AMS Graduate Studies in Mathematics 140, 2012, doi:10.1090/gsm/140) uses them to make the word "chaos" precise. The chapter proves that a period-three orbit of a continuous interval map forces orbits of every period (Li and Yorke, 1975, the first case of Sarkovskii's theorem), adopts Devaney's topological definition of chaos, codes the tent map by sequences of two symbols, and ends by computing the Hausdorff dimension of the tent map's invariant Cantor set. The same pattern (a Cantor set, a conjugacy to a shift, a fractal dimension) returns in the Smale horseshoe of Chapter 13 and in hyperbolic dynamics generally, so the chapter is the standard entry point to symbolic dynamics.
For a real parameter the tent map is , a map of the real line. For the peak exceeds , points leave and then escape to . The repellor of the tent map is the set of points that never leave,
which the book builds as a nested intersection of intervals of length ; for it is all of . With and , the itinerary map sends to the sequence with when .
The sequence space , , carries the metric and the shift .
A continuous map of a metric space is topologically transitive if for all nonempty open some iterate , , meets . It is chaotic if in addition is infinite and the periodic points of are dense. This is the definition used in the book, and it has no sensitivity clause. It has sensitive dependence on initial conditions if some has the property that every has points arbitrarily close to it with for some . A compact set with is repelling if some neighborhood of is eventually left by every orbit starting in . A repelling set is a repellor if is transitive. It is a strange repellor if moreover is chaotic and is fractal, meaning its Hausdorff dimension is not an integer. A Cantor set is a compact, totally disconnected, perfect set.
The book states the strange-repellor clause for . At , however, has dimension , which is an integer, so the goal restricts that clause to .
The dimension formula is the simplest non-trivial instance of the principle that the Hausdorff dimension of an expanding repellor is determined by the number of branches and the expansion rate. For conformal repellors this principle becomes Bowen's formula. Theorem 11.23 of the same chapter extends the bound to general two-branch expanding interval maps, with . The conjugacy with the full shift is the device that reduces the dynamics on to combinatorics of sequences. It is reused verbatim for the horseshoe.
On formalization: Mathlib has Hausdorff measure and dimension (MeasureTheory.Measure.hausdorffMeasure, dimH) together with Hölder and Lipschitz image bounds. It has no dimension computation for a self-similar Cantor set and no symbolic-dynamics layer. On Prove2Me, the Devaney series proves period three implies all periods and Sarkovskii's theorem for continuous maps , the density of periodic points and a dense orbit for the two-symbol shift, and a Cantor-set statement for the quadratic family. None of these states the results for self-maps of a compact interval, for symbols, or for the tent map, and none computes a Hausdorff dimension. All results here are proved in the book, except that the proof of Theorem 11.20 is terse. None is formalized in the form stated here.
The upper bound comes from the natural covers. The lower bound is the hard direction: it has to hold for every cover, including covers by sets of very different sizes that do not line up with the construction intervals. So the natural covers alone do not decide it. Counting the construction intervals that an arbitrary set of a given diameter can meet needs the gaps between them to be controlled uniformly. The heuristic self-similarity identity fixes only once is known, and that is exactly what has to be proved. For the strange-repellor clause, every part of the definition (repelling, transitive, infinite, dense periodic points, fractal) has to be checked for with the subspace topology. Transferring transitivity and density of periodic points from requires the homeomorphism of Theorem 11.5 in both directions, not just a continuous surjection. In Lemma 11.1 the difficulty is showing that the periodic point found has prime period , not a divisor of .
Everything is stated in namespace TeschlODE.IntervalMaps against Mathlib.
ℕ → Fin N, and the metric (11.28) is a function symDist N (a tsum, summable for ). Density and continuity on are stated in explicit – form with this function. Each theorem assumes , the book's .ℝ → (ℕ → Fin 2). Its values off are meaningless and never used. "Homeomorphism" in Theorem 11.5 means: is a bijection of onto , it is continuous on , and its inverse is continuous, all in metric form.Function.periodicPts, and the prime period in Lemma 11.1 is Function.minimalPeriod on the subtype .dimH, valued in . "Not an integer" means finite and different from every natural number. The goal's right-hand side is ENNReal.ofReal (log 2 / log μ).There are no "sufficiently small" or readings in this chapter. The only quantifier choices are the explicit – forms above and the nonempty open sets in transitivity.
The goal is not a dimension-only statement. For , a statement that proved only (11.49), or that restricted to a single value such as , would be a different and weaker theorem. The full strange-repellor conclusion, with every clause of the definition, is required. Solvers can reuse the symbolic-dynamics lemmas (11.6, 11.8, 11.9) and the conjugacy (11.5). General Mathlib contributions on as a metric space are welcome.
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.
Planar flows are tame: the Poincaré–Bendixson theorem says that a bounded forward orbit in the plane tends to a fixed point or a periodic orbit. From dimension three on this fails, and the long-time behavior of a flow has to be described through sets rather than single orbits. Chapter 8 of Gerald Teschl's graduate text Ordinary Differential Equations and Dynamical Systems (AMS GSM 140, 2012; author's preliminary version at mat.univie.ac.at) develops two tools for this. The first is the attracting set produced by a trapping region, the device used to show that the Lorenz equation (Lorenz 1963) has an attractor. The second is volume: Liouville's formula for volumes measures how a flow expands or contracts phase space, which shows that the Lorenz attractor has Lebesgue measure zero, and in the special case of a Hamiltonian system gives Liouville's theorem, that the flow preserves volume. Liouville's theorem, with Poincaré's recurrence theorem as its companion, underlies Hamiltonian mechanics and equilibrium statistical mechanics.
This mission states those results for the local flow of a vector field on an open subset of , as in the book.
Let be open and of class . An integral curve of is a differentiable on an open interval with . For each there is a unique maximal one through at time , defined on the open interval . Its value at time is , the flow. The flow is local: may be bounded.
For , the -limit set is the set of for which there are and with . The stable and unstable sets of are , where is the distance to a set. A set is invariant if it contains the full orbit of each of its points. An invariant is attracting if is a neighborhood of . A trapping region is an open connected with compact closure such that for all .
The divergence of is . On phase space , a Hamilton function defines Hamilton's equations , , whose right-hand side is the Hamiltonian vector field . The Lorenz equation is , , with . Volume is Lebesgue measure.
For on an open , with the flow of on , every measurable and every time at which all points of are alive satisfy
The result itself. Liouville's theorem is the basic structural fact of Hamiltonian dynamics. It rules out asymptotically stable equilibria and attractors of positive measure for Hamiltonian systems. It makes Lebesgue measure invariant, which is the starting point of ergodic theory for mechanical systems. Combined with Theorem 8.11, it gives recurrence for any Hamiltonian motion confined to a bounded energy region. Lemma 8.8 is the quantitative version for arbitrary flows: for the Lorenz equation it gives , so the attractor from Lemma 8.5 has measure zero. Lemmas 8.5 and 8.6 produce attractors and show that they contain the unstable manifolds of their points.
Formalizing it. All of these results are classical and proved in the book. Mathlib has the change-of-variables formula, Poincaré recurrence for conservative measure-preserving maps (MeasureTheory.Conservative), and an -limit set for global flows (omegaLimit). It has no flow of a nonlinear ODE with its differentiable dependence on initial conditions, no volume formula along such a flow, and no Hamiltonian formalism. The mission asks for those pieces in the book's local-flow setting, with its hypotheses made explicit.
Lemma 8.8 and Theorem 8.10 need the flow map to be a diffeomorphism of the set of points alive at time onto its image. They also need its Jacobian to satisfy the first variational equation , whose determinant obeys Liouville's formula for linear systems. None of this is available for a general vector field in Mathlib, which provides local existence and uniqueness of integral curves but not differentiability of the flow in the initial condition. Differentiating under the integral also needs uniform control on a compact set of initial points. That is why Lemma 8.8 asks the closure of , not just , to be alive at . Without that, can have infinite volume (, , ).
Lemmas 8.5 and 8.6 are point-set topology. The obstacle there is the local flow: every statement about must first establish that the points involved are alive at time . The book avoids this by assuming completeness at the start of the chapter. For Lemma 8.7, the Liapunov function from the text has , not , so convergence to the origin requires the Krasovskii–LaSalle argument, not a plain Liapunov one.
is EuclideanSpace ℝ (Fin n) and phase space is EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with points , momenta first. volume on it is Lebesgue measure on . The flow is a pair satisfying IsMaximalFlow, which makes the unique maximal integral curve on . Nothing assumes . The chapter's standing completeness assumption is replaced by explicit aliveness hypotheses, and these are implied by completeness. The explicit readings are:
A trivializing formalization is excluded. The goal is not stated for a complete or globally Lipschitz flow, not for sets of measure zero or bounded open sets only, and not with assumed. It must be proved for the flow of built from itself.
A complete development needs differentiability of the flow in the initial condition and the first variational equation. It also needs Liouville's formula for linear systems, and change of variables for the flow map. Each is reusable beyond this mission; contributions of any of them as separate lemmas are welcome.
Mathlib/Dynamics/Ergodic/Conservative.lean. https://github.com/leanprover-community/mathlib4