Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

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.

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

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.

≤ 7.103205334138Formalized record≤ 2Open frontier

7 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -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 $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

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.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

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.

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

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.

≤ 7.103205334138Formalized record≤ 2Open frontier

7 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

Bellman's Dynamic Programming V: Optimality of a Constant Stock Level for the Optimal Inventory EquationTextbook

Motivation

The optimal inventory problem asks how much of an item to stock when demand is random, ordering costs money, and running short costs more. Arrow, Harris and Marschak formulated it as a sequential decision problem in 1951 (Optimal inventory policy, Econometrica 19), and Dvoretzky, Kiefer and Wolfowitz studied its structure in 1952–53. Chapter V of Richard Bellman's Dynamic Programming (1957) treats the problem through a single functional equation for the minimal expected discounted cost. It shows that when ordering and shortage costs are proportional to quantity, the optimal policy is described by one number, a constant stock level $\bar x$ , computed from the demand distribution alone.

This result is an early form of the base-stock (order-up-to) policy. Base-stock policies are the standard structure in periodic-review inventory theory: Karlin (1958), Scarf's $(s,S)$ theorem (1960) and Veinott (1965) extend it. Chapter V is also a worked example of a point the book makes throughout: the method of successive approximations determines the shape of an optimal policy, and not only its existence.

Setting

A single item is stocked over an unbounded sequence of periods. At the start of a period the stock is $x \ge 0$ . The decision maker orders up to a level $y \ge x$ , at cost $k(y-x)$ with $k > 0$ . A demand $s \ge 0$ then arrives, with probability density $\varphi$ : $\varphi(s) > 0$ for $s > 0$ , $\int_0^\infty \varphi(s)\,ds = 1$ , and $\int_0^\infty s\,\varphi(s)\,ds < \infty$ . If $s \le y$ , the next period starts with stock $y - s$ . If $s > y$ , the excess $s - y$ is bought at the penalty rate $p > 0$ and the next period starts with stock $0$ . Costs one period ahead are multiplied by a discount factor $0 < a < 1$ .

Write $f(x)$ for the minimal expected discounted cost from stock $x$ . Enumerating the cases gives Bellman's equation (5.1):

f(x) = \min_{y \ge x} T(y,x,f),

T(y,x,f) = k(y-x) + a\Big[\int_y^\infty p(s-y)\varphi(s)\,ds + f(0)\int_y^\infty \varphi(s)\,ds + \int_0^y f(y-s)\varphi(s)\,ds\Big].

A policy assigns an order-up-to level $y(x) \ge x$ to each stock $x$ . It is optimal when $y(x)$ attains the minimum. The mission takes the equation itself as the model; no stochastic process is built.

Formalization targets

Goal: Chapter V, Theorem 1 (with (4b) corrected)

The equation has exactly one solution $f$ among measurable functions bounded on $[0,\infty)$ . If $ap > k$ , the equation

k = ap\int_{\bar x}^\infty \varphi(s)\,ds + ak\int_0^{\bar x}\varphi(s)\,ds

has exactly one root $\bar x \ge 0$ , and for every $x \ge 0$ the minimum is attained at

y(x) = \max(x, \bar x).

If $ap \le k$ , the minimum is attained at $y(x) = x$ : never order.

Milestones

Chapter IV, Theorem 6 (proportional costs): existence and uniqueness of a solution bounded on every finite interval, its continuity, and convergence of $f_{n+1}(x) = \min_{y\ge x} T(y,x,f_n)$ from any non-negative continuous $f_0$ .
Eq. (5.8): $\bar x$ is the unique root of $\int_0^{y}\varphi(s)\,ds = (ap-k)/a(p-k)$ .
Appendix, Theorem 9: the renewal equation $u(x) = f(x) + \int_0^x u(x-s)\varphi(s)\,ds$ with $\int_0^\infty|\varphi| < 1$ has a unique locally bounded solution. The solution is the limit of successive approximations, satisfies a derivative identity, and is non-negative when $f, \varphi \ge 0$ .
Theorem 3: in the undiscounted $n$ -stage process with $p > k$ , the optimal policy at each horizon is a constant stock level $\bar x_n$ , and $\bar x_n$ increases with $n$ .
Theorem 4: with a fixed stock-out charge $q$ added to the penalty, the constant-stock-level policy is still optimal when the last minimum of

\psi(y) = ky + a\Big[\int_y^\infty [p(s-y)+q]\varphi(s)\,ds - k\int_0^y (y-s)\varphi(s)\,ds\Big]

is its absolute minimum.

Significance

The theorem reduces an infinite-horizon stochastic control problem to a scalar equation. Rewriting it as $\int_0^{\bar x}\varphi = (ap-k)/a(p-k)$ gives the critical-fractile form familiar from the newsvendor problem, with the discount factor entering the fractile. The level depends on the demand law only through its distribution function, and the policy does not depend on the current stock except through $\max(x,\bar x)$ . This is what makes the policy implementable and its parameters estimable from data, the point Bellman makes in § 1. Theorem 3 shows the same structure over a finite horizon, with levels that rise as more periods remain. Theorem 4 marks where the structure starts to depend on the demand density.

As far as a search of the platform shows (queries recorded in the mission files), none of these results has a machine-checked proof. Base-stock theorems on the platform, Veinott's multi-product theorem and Gallego–Özer's advance-demand model, use discrete periods, different excess-demand conventions and different state spaces. They do not cover a continuous-demand, lost-sales-at-penalty, discounted functional equation. Formalizing Chapter V would produce an explicit solution of a nonlinear integral equation of renewal type, a uniqueness theorem for that equation, and a Lean treatment of the renewal equation that other applied-probability missions can reuse.

Difficulty

Two steps resist the obvious argument. First, the minimization is over the unbounded set $y \ge x$ , and the unknown $f$ enters through a convolution with $\varphi$ . The operator $f \mapsto \min_{y\ge x}T(y,x,f)$ is a contraction on bounded functions, which settles uniqueness in the bounded class. Uniqueness among functions bounded only on finite intervals (Chapter IV's class) is not a contraction statement, because the minimization reaches arbitrarily far to the right. Second, optimality of $\max(x,\bar x)$ for $x > \bar x$ requires $f(y) + ky$ to be nondecreasing on $[\bar x,\infty)$ . There $f$ is defined only implicitly, as the solution of a renewal-type equation, and this monotonicity is a positivity statement about that solution, not a consequence of the first-order condition. Checking that the first-order condition holds at $\bar x$ is not enough, and neither is checking that the candidate function satisfies the equation at the single level $\bar x$ .

Formalization scope

Functions are ℝ → ℝ; only their values on $[0,\infty)$ enter. Integrals over $(y,\infty)$ are Lebesgue integrals and $\int_0^y$ are interval integrals. The equation is stated with an infimum (IsGLB), as Chapter IV writes it, and every policy statement asserts that the minimum is attained (IsLeast) at the stated level. Uniqueness is asserted on $[0,\infty)$ (Set.EqOn … (Set.Ici 0)). Solution classes require measurability. This is the standing convention that makes $\int_0^y f(y-s)\varphi(s)\,ds$ meaningful; without it a non-measurable function would make the integral default to $0$ . " $\varphi(s) > 0$ " is read as positivity on $(0,\infty)$ .

Conventions and corrections, each stated in the items:

Theorem 1, (4b) is printed "for $x \ge \bar x$ , $y = \bar x$ ". Read literally, a stock $x > \bar x$ would be "ordered down" to $\bar x < x$ , which violates $y \ge x$ . The proof (p. 163, "the minimum occurs at $y = x$ ") and Theorem 4's (7) give $y = x$ , which is what the goal states. The printed text reads: "(4) a. for 0 ≤ x ≤ x̄, y = x̄, b. for x ≥ x̄, y = x̄."
The goal's uniqueness class is "uniformly bounded functions over $x \ge 0$ " (p. 164). Chapter IV, Theorem 6 is stated in its own larger class.
Theorem 4 gives no range for $q$ ; $q \ge 0$ is assumed. Its phrase "the last minimum of $\psi$ is the absolute minimum" is read as: $\bar x$ minimizes $\psi$ on $[0,\infty)$ and $\psi$ is nondecreasing on $[\bar x,\infty)$ . The bracket of (6), unbalanced in print, is closed at the end.
Theorem 3 assumes " $p > k$ "; $k > 0$ and the density conditions of Theorem 1 are carried over.
Theorem 9's derivative clause assumes $f$ continuously differentiable, where the book says "differentiable". The derivative identity is asserted for $x > 0$ .

A trivializing formalization is ruled out. The goal does not assume the stated policy is optimal, does not assume $f$ is given, and does not take $\bar x$ as a hypothesis. It asserts the existence of the root, the existence and uniqueness of the solution, and attainment of the minimum at $\max(x,\bar x)$ for every $x \ge 0$ .

Theorems 2 (two items, joint density), 5 (one-period delivery lag) and 6 (strictly convex ordering cost) are not part of this mission. Theorem 2 is printed with a sign error in (6) and garbled marginals. Theorem 5 states no hypotheses. Theorem 6's (9b) contradicts itself at $x = \bar x$ . Welcome contributions include a Lean library for the renewal equation (existence by successive approximation, positivity, differentiation under the convolution), which Theorem 9 needs and which is independent of inventory theory, and the contraction estimate for $\min_{y\ge x}T(y,x,\cdot)$ on bounded measurable functions.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter V and Chapter IV § 9. https://doi.org/10.2307/j.ctv1nxcw0f
R. Bellman, I. Glicksberg, O. Gross, On the optimal inventory equation, Management Science 2(1), 1955, 83–104. https://doi.org/10.1287/mnsc.2.1.83
K. J. Arrow, T. Harris, J. Marschak, Optimal inventory policy, Econometrica 19(3), 1951, 250–272. https://doi.org/10.2307/1906813
A. Dvoretzky, J. Kiefer, J. Wolfowitz, The inventory problem: I. Case of known distributions of demand, Econometrica 20(2), 1952, 187–222. https://doi.org/10.2307/1907847
A. F. Veinott, Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3), 1965, 206–222. https://doi.org/10.1287/mnsc.12.3.206

7 thms2 active usersReviewed

Completed

Dynamic Programming Functional Analysis Operations Research+1·Captain: mikedeng1

Bellman's Dynamic Programming IV: Existence and Uniqueness for Functional Equations of Types One, Two and ThreeTextbook

Motivation

A multi-stage decision process is summarized by its optimal return function $f$ , which satisfies a functional equation. In Chapters I and II of Dynamic Programming (Princeton University Press, 1957), Richard Bellman proves existence and uniqueness for particular processes: allocation of resources, gold mining. Chapter IV abstracts these arguments into theorems about whole classes of equations. The same scheme reappears in later chapters (multi-stage games, the calculus of variations) and in every later treatment of dynamic programming.

Two points explain why the chapter is still worth formalizing. First, uniqueness is always claimed within a stated function class, and the choice of class is part of the theorem: an equation of this kind can have many solutions, and only one of them lies in the class that the process singles out. Second, the chapter covers equations that are not contractions in the supremum norm, in particular Type One, where the shrinking happens in the state rather than in the function values.

Setting

Let $D \subseteq \mathbb{R}^N$ carry the Euclidean norm $\|p\|$ , let $S$ be a nonempty set of decisions, and let $g, h : D \times S \to \mathbb{R}$ and $T : D \times S \to D$ . The general equation (1.1) is

f(p) = \sup_{q \in S}\big[g(p,q) + h(p,q)\,f(T(p,q))\big].

Here $g$ is the one-stage return, $T(p,q)$ the next state and $h(p,q)$ a multiplier: a discount factor or a survival probability.

An equation is of Type One with constant $0 \le a < 1$ under the following conditions. $D$ contains the null vector $\theta$ . $g$ is bounded on bounded parts of $D$ , uniformly in $q$ , and $g(\theta, q) = 0$ . $|h| \le 1$ . $\|T(p,q)\| \le a\|p\|$ . Finally, with $v(c) = \sup_{\|p\| \le c}\sup_q |g(p,q)|$ , the series $\sum_{n \ge 0} v(a^n c)$ converges for every $c$ .

It is of Type Two under the following conditions. $g$ is bounded on bounded parts of $D$ . On each bounded part, $|h| \le a < 1$ for some $a$ . $T$ maps $D$ into $D$ , and either $\|T(p,q)\| \le \|p\|$ or $D$ is bounded.

The successive approximations are $f_0(p) = \sup_q g(p,q)$ and $f_{n+1}(p) = \sup_q[g(p,q) + h(p,q) f_n(T(p,q))]$ .

The equation of the third type of § 8 lives on the probability simplex $\Delta$ of distributions $p = (p_0, \dots, p_n)$ , with vertices $x_k$ . It reads

f(p) = \min\Big[\,1 + \sum_{k=0}^{n} p_k f(x_k),\ \min_{1 \le l \le M}\big[1 + f(T_l p)\big]\Big] \quad (p \ne x_0), \qquad f(x_0) = 0.

Each $T_l$ maps $\Delta$ into itself, and the $0$ -th coordinate of $T_l p$ is never $1$ . $f(p)$ is the minimal expected time to drive a system into state $0$ with certainty, by observing the state (cost $1$ , then continuing from the observed vertex) or by applying one of the operations $T_l$ (cost $1$ ).

Formalization targets

Goal: Chapter IV, Theorem 1

For a Type One equation there is exactly one solution on $D$ , among functions continuous at $\theta$ and zero there, of

f(p) = \sup_{q \in S}\big[g(p,q) + h(p,q)\,f(T(p,q))\big] \ (p \ne \theta), \qquad f(\theta) = 0.

It is the pointwise limit of the successive approximations from $f_0 = \sup_q g$ , and also from any $f_0$ that is continuous and zero at $\theta$ and bounded on bounded parts of $D$ . If $g$ , $h$ and $T$ are continuous in $p$ on bounded portions of $D$ , uniformly in $q$ , the solution is continuous on every bounded portion of $D$ .

Milestones

Lemma 1 (the fundamental inequality): for nonnegative measures $dG$ ,

|f_2(p) - F_2(p)| \le \sup_q\Big[\,|g - h| + \int_{D} |f_1 - F_1|\,dG\Big].

Theorem 2: a Type Two equation has a unique solution bounded in every finite part of $D$ , obtained by successive approximations and continuous under the same conditions as in Theorem 1.
Theorem 3 (stability, Type One): $\sup_{\|p\| \le c} |F - f| \le \sum_{n \ge 0} u(a^n c)$ , where $u(c) = \sup_{\|p\| \le c}\sup_q |G - g|$ .
Theorem 4 (stability, Type Two, corrected): $\sup_{\|p\| \le c} |F - f| \le u(c)/(1-a)$ .
Lemma 2: two bounded solutions of the third-type equation satisfy $\sup_{p} |f(p) - g(p)| = \max_k |f(x_k) - g(x_k)|$ .
Theorem 5: if $\sum_{k=1}^n (T_l p)_k \le c_1 < 1$ for every $l$ and $p$ , the third-type equation has a unique bounded solution, and it is positive off $x_0$ .

Significance

Theorem 1 guarantees that the optimal return of a process whose decisions shrink the state is well defined and computable by iteration. It applies without assuming that the supremum over decisions is attained and without regularity of the maximizing decision. Theorems 3 and 4 give quantitative continuous dependence of the solution on the reward. This is what justifies approximating a process by a simpler one. Theorem 5 is a uniqueness result for an undiscounted minimum-time problem, where no contraction in the supremum norm is available.

All of these results are classical and proved in the book. None is formalized: the platform's related statements treat finite state spaces with a fixed policy (FoundationsML.ReinforcementLearning.bellman_equations_unique_solution), or Karlin's compact-decision-set setting with nonnegative rewards and an explicit vanishing-tail hypothesis (KarlinDP.Deterministic.unique_solution_of_vanishing_tail), or finite-state stochastic shortest paths (BertsekasDP.ssp_main_theorem). This mission adds machine-checked versions over a continuum of states and an arbitrary decision set, with the function classes stated exactly.

Difficulty

For Type One, the natural idea is to apply the Banach fixed-point theorem in the space of bounded functions. That fails: $|h| \le 1$ allows no contraction in the supremum norm, and the solution need not be bounded on $D$ . Contraction happens only along trajectories, $\|T(p,q)\| \le a\|p\|$ , so every estimate must be localized to balls $\|p\| \le c$ and summed along radii $a^n c$ . Uniqueness then rests on continuity at $\theta$ rather than on a global norm.

The suprema over an arbitrary, possibly infinite, decision set are not attained in general, so no argument may select a maximizing decision. For the third-type equation, neither a contraction nor a shrinking of the state is available: the operations $T_l$ need not move $p$ towards $x_0$ . Uniqueness among bounded solutions requires controlling how long a solution can keep choosing an operation other than observation.

Formalization scope

The state space is EuclideanSpace ℝ (Fin N), $D$ is a Set, the decision set is a nonempty type S, and functions are total, EuclideanSpace ℝ (Fin N) → ℝ. Only their values on $D$ matter, and uniqueness is asserted on $D$ . The equation is encoded with IsLUB, so the supremum is genuine and has no junk value. The successive approximations and the radii $v(c)$ , $u(c)$ use real iSup/sSup, evaluated only where the book's boundedness conditions hold. "Continuous at $\theta$ " is continuity within $D$ .

Conventions and corrections:

In Type One the book writes "for some $a < 1$ ". The formalization takes $0 \le a < 1$ , which loses no generality.
Condition (1a) of both types is read for every radius $c_1$ .
"Continuous in $p$ in any bounded portion of $D$ , uniformly for all $q$ " is read as uniform equicontinuity on each $\{p \in D : \|p\| \le c\}$ . For closed $D$ this is the pointwise reading.
Theorem 4 is printed with " $|F(p) - (p)|$ ", a misprint for $|F(p) - f(p)|$ . As printed, it is also false under the bounded-domain alternative of Type Two. Take $N = 1$ , $D = [-2,2]$ , $T \equiv 2$ , $h \equiv \tfrac12$ , $g \equiv 0$ , and $G = 1$ at $p = 2$ , $G = 0$ elsewhere. Then $|F(0) - f(0)| = 1$ while $u(1)/(1-a) = 0$ . The formal statement adds that $T$ maps $\{p \in D : \|p\| \le c\}$ into the ball of radius $c$ . This holds for every $c$ under the first alternative, where the statement is the book's.
Lemma 1 is stated for nonnegative measures $dG(p,q,\cdot)$ on $\mathbb{R}^N$ , integrated over $D$ . The right-hand supremum may be infinite, so it is expressed through its real upper bounds.
In § 8 the number of states is written both $N+1$ and $n+1$ ; the formalization uses $n+1$ , with $M \ge 1$ transformations indexed by Fin M.

A trivializing formalization would state uniqueness among all solutions of the equation, which is false because constants solve it when $g = 0$ and $h = 1$ . Equally trivializing would be to encode the supremum with a junk-valued sSup, so that unbounded return sets pass for solutions. Both are excluded: the class is part of each statement, and the equation is an IsLUB.

Theorem 6 of the chapter (the optimal inventory equation) is not part of this mission; it is treated in the inventory mission of the series. Welcome contributions include a reusable library for localized successive approximations and the equicontinuity lemmas that the continuity statements need.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010, Chapter IV. https://doi.org/10.2307/j.ctv1nxcw0f
S. Karlin, "The structure of dynamic programming models", Naval Research Logistics Quarterly 2 (1955), 285–294. https://doi.org/10.1002/nav.3800020408
D. P. Bertsekas and J. N. Tsitsiklis, "An analysis of stochastic shortest path problems", Mathematics of Operations Research 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580

10 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

Bellman's Dynamic Programming III: Index Rules for the Stochastic Gold-Mining ProcessTextbook

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) treats the stochastic gold-mining process, the first stochastic multi-stage decision process of the book whose optimal policy can be written down in closed form. There Bellman introduces decision regions, the sets of states at which a given first choice is optimal, and where he obtains an index rule: at every state, compute one number per alternative and choose the largest. The same kind of rule was later developed in general form as the Gittins index for multi-armed bandits (Gittins 1979), and the gold-mining process is an early instance of what that literature calls a deteriorating bandit, in which each alternative's index can only decrease when it is used.

Bellman first described the process in his 1954 survey The theory of dynamic programming, with the two-mine index rule stated as Eq. (8.3), and it appears on Prove2Me in a mission on that paper. The book gives the full chapter: existence and uniqueness, the rule for two mines, its extension to several outcomes per use and to any number of mines, the finite-horizon process, and a stability estimate.

Setting

Two mines, Anaconda and Bonanza, hold amounts of gold $x \ge 0$ and $y \ge 0$ . A single machine is used in one mine at a time. Used in Anaconda, it mines the fraction $r_1$ of the gold there and stays in working order with probability $p_1$ , or is destroyed without mining anything with probability $1 - p_1$ . Bonanza has the corresponding data $p_2$ and $r_2$ . Before each use the operator chooses a mine (choice A or B), and the process stops when the machine is destroyed. The aim is to maximize the expected total amount of gold mined.

The expected return $f(x, y)$ under an optimal policy satisfies the functional equation

f(x,y) = \max\Big[\,A_f(x,y),\; B_f(x,y)\,\Big], \qquad x, y \ge 0, \tag{5.1}

where $A_f(x,y) = p_1\big[r_1x + f((1-r_1)x,\,y)\big]$ is the return of an A-choice followed by optimal continuation and $B_f(x,y) = p_2\big[r_2y + f(x,\,(1-r_2)y)\big]$ that of a B-choice. The $N$ -stage returns are $f_1(x,y) = \max(p_1r_1x,\ p_2r_2y)$ and $f_{N+1} = \max(A_{f_N}, B_{f_N})$ . The A-region of a value function is the set of points of the closed quadrant where the A-branch attains the maximum; the B-region is defined in the same way.

In the generalization, a use of mine $i$ has $K$ outcomes: outcome $k$ occurs with probability $p_{ik}$ , yields $c_{ik}x_i$ and leaves $c'_{ik}x_i = (1-c_{ik})x_i$ in the mine, and $1 - \sum_k p_{ik}$ is the probability that the machine is destroyed. With $n$ mines the equation is

f(x_1,\dots,x_n) = \max_i \sum_{k=1}^{K} p_{ik}\big[c_{ik}x_i + f(x_1,\dots,c'_{ik}x_i,\dots,x_n)\big]. \tag{4}

"The solution" of an equation always means its unique solution in the class of functions bounded in every rectangle $0 \le x \le \bar X$ , $0 \le y \le \bar Y$ (or every box $0 \le x_i \le \bar X_i$ ), per Bellman's footnote 7.

Formalization targets

Goal: Chapter II, Theorem 4 (the index rule for $n$ mines)

Under $p_{ik} \ge 0$ , $\sum_k p_{ik} < 1$ , $0 \le c_{ik} \le 1$ , $c_{ik} + c'_{ik} = 1$ , equation (4) has a unique solution bounded on boxes, and at every state $x$ any index maximizing

D_i(x) = \frac{\sum_{k} p_{ik}c_{ik}}{1-\sum_{k} p_{ik}}\;x_i

attains the maximum in (4). Ties among the maximizers may be broken arbitrarily.

Milestones

Theorem 1: for $|p_i| < 1$ and $0 \le r_i < 1$ , (5.1) has a unique solution bounded in every rectangle, and it is continuous on the closed quadrant.
Theorem 2: for $0 \le p_i < 1$ , $0 \le r_i \le 1$ , the solution takes the A-branch when $p_1r_1x/(1-p_1) > p_2r_2y/(1-p_2)$ , the B-branch when the reverse inequality holds, and both on equality.
Theorem 3: the same rule for two mines with $K$ outcomes per use.
Theorem 5: for each $N$ , the $N$ -stage process has exactly two decision regions: a sector along the $x$ -axis where A is optimal and a sector along the $y$ -axis where B is optimal, separated by a ray through the origin.
Theorem 6: as $N$ grows, the regions of $f_N$ move monotonically, and from some $N_0$ on they coincide with those of $f$ .
Theorem 7: if $g$ solves (5.1) with an added term $h$ , then $|f - g| \le \max_R|h|/q$ on every rectangle $R$ , where $q = \min(1-p_1, 1-p_2)$ .

Significance

The index rule reduces the choice among $n$ mines to computing $n$ numbers. Each one depends only on its own mine, as the ratio of immediate expected gain to immediate expected loss. Without the theorem, an optimal policy for the $N$ -stage process is a word in $n$ letters whose number of candidates grows like $n^N$ . The finite-horizon theorems show that the same rule is exactly optimal for every horizon beyond a finite $N_0$ , and the stability theorem bounds how much the solution moves when the equation is perturbed.

Theorem 2's content is also the target of the 1954-paper mission, where it is stated for the supremum of expected returns over choice sequences. Those statements (BellmanTheoryDP.GoldMining.gold_mining_decision_rule, …optimal_return_functional_equation) are included here as reference items. They concern a different object: the book's theorems are about the unique bounded solution of (5.1), and the two coincide once (5.1) is known to characterize the optimal return. None of the chapter's results has a machine-checked proof on the platform yet. The $n$ -mine rule (Theorem 4) and the finite-horizon results (Theorems 5 and 6) are not stated anywhere on the platform.

Difficulty

The equation for the boundary between the regions involves the unknown function $f$ , so equating the two branches of (5.1) does not by itself locate the boundary. Comparing the orders "A then B" and "B then A" determines the index line, but only on the assumption that there are just two regions. Bellman's Figure 1 shows why that assumption carries real content: homogeneity alone only makes the regions unions of sectors, which could alternate. The assumption is not automatic either. In § 13 a third, compromise choice is added, and a counterexample shows that the three-choice problem need not have the analogous three-sector structure. For the finite-horizon process the boundary ray of $f_N$ generally differs from the index line, and Theorems 5 and 6 are statements about how it differs.

Formalization scope

Namespace BellmanDP.GoldMining. Values are real functions ℝ → ℝ → ℝ (two mines) or (Fin n → ℝ) → ℝ (n mines); equations are imposed only on the closed quadrant or orthant, and uniqueness means agreement there. Mines are Fin n with $n \ge 1$ added (with no mine the maximum in (4) is empty). Outcomes are Fin K (Theorem 3's $N$ ). A maximum over two branches is max, and a maximum over mines is encoded as "every alternative is at most $f(x)$ and one equals it". The class "bounded in any rectangle" is BoundedOnRectangles, and for $n$ mines it is BoundedOnBoxes. The $N$ -stage returns are goldIter N, with goldIter 0 = 0 so that goldIter 1 is the book's $f_1$ .

Choices made explicit:

Theorem 1 keeps the book's signed range $|p_i| < 1$ (footnote 2), while Theorems 2, 5, 6 and 7 use the range of § 8 and Theorem 2, $0 \le p_i < 1$ , $0 \le r_i \le 1$ .
The goal asserts existence and uniqueness of the bounded solution of (4) together with the index rule. This is how "the solution" is meant in the book; the extension of Theorem 1 to (4) is not a separate numbered result.
The goal's conclusion is the book's: a maximizer of $D$ is optimal. It does not also assert that the other indices are suboptimal.
Theorem 5's printed statement is only "there are two decision regions". It is formalized as the ray-separation statement its proof establishes, and is titled as the precise reading. Theorem 6's "converge in a monotone fashion" is formalized as monotonicity of the regions as sets, in one of the two directions.
Theorem 7 adds the hypothesis that $h$ is bounded in every rectangle, which is what gives the perturbed equation a solution in the class. $\max_R|h|$ is expressed through any bound $M$ of $|h|$ on $R$ .

A statement of the index rule that assumes the index policy's return satisfies (5.1) and calls it "the solution" without the bounded-class uniqueness would prove nothing about optimality. Here every theorem is about solutions in the bounded class, whose uniqueness is Theorem 1 (and part of the goal).

Contraction estimates on rectangles (Theorems 1 and 7) are reusable across the other functional-equation chapters of this series. Proofs of the goal via general index theory are welcome, provided they discharge the statements as written.

Selected references

Richard Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter II, pp. 61–80. https://doi.org/10.2307/j.ctv1nxcw0f
Richard Bellman, The theory of dynamic programming, Bulletin of the American Mathematical Society 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society, Series B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x

11 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Bellman's Dynamic Programming II: Fibonacci Search for the Maximum of a Unimodal FunctionTextbook

Motivation

Many optimization routines contain an inner step that maximizes a function of one variable whose values are expensive to compute: a line search inside a multivariate method, a tuning parameter chosen by simulation, a stage of a dynamic program in which each evaluation requires solving a subproblem. When the only structural information is that the function has a single peak, the natural question is how to place the evaluations so that the peak is pinned down as tightly as possible with a fixed budget. Richard Bellman's Dynamic Programming (1957) takes up this question in Chapter I, § 22, as an illustration of the functional-equation method, and answers it with the Fibonacci numbers.

Timeline.

1953. J. Kiefer, Sequential minimax search for a maximum (Proc. Amer. Math. Soc. 4, 502–506), proves that Fibonacci search is minimax optimal among sequential procedures for a unimodal function on an interval. doi:10.1090/S0002-9939-1953-0055639-3
1957. Bellman, Dynamic Programming, Chapter I, § 22 (pp. 34–36), recasts the result in the language of the principle of optimality: Theorem 11 for the continuous problem and Theorem 12 for its discrete version.

Setting

Let $L > 0$ . A function $f : [0, L] \to \mathbb R$ is strictly unimodal with maximum at $m \in [0, L]$ if $f$ is strictly increasing on $[0, m]$ and strictly decreasing on $[m, L]$ . No continuity is assumed, and the peak may sit at an endpoint. The point $m$ is then the unique maximizer of $f$ .

A search procedure is a finite decision tree. At each internal node it names a point $x$ at which $f$ is evaluated and moves to a subtree chosen by the observed value $f(x)$ ; at a leaf it announces a closed interval $[a, b]$ . The $k$ -th evaluation point may depend on all values seen so far, but on nothing else about $f$ . The cost of the procedure on $f$ is the number of evaluations along the path that $f$ determines.

The procedure locates the maximum on $[0, L]$ within unit length using at most $n$ values if, for every strictly unimodal $f$ on $[0, L]$ with maximum at $m$ , it evaluates $f$ at most $n$ times and announces $[a, b]$ with $b - a \le 1$ and $m \in [a, b]$ . Write $\mathcal L_n$ for the set of lengths $L > 0$ for which such a procedure exists, and following Bellman's Eq. (22.1),

F_n = \sup \mathcal L_n .

The book's Fibonacci numbers are $F_0 = F_1 = 1$ , $F_n = F_{n-1} + F_{n-2}$ for $n \ge 2$ (in Lean, bookFib).

In the discrete version, $f$ is defined on the points $0, 1, \dots, N-1$ , strictly increasing up to its maximizer $m$ and strictly decreasing after it. $K_n$ is the largest $N$ for which some procedure evaluates at most $n$ values and then names $m$ exactly, for every such $f$ .

Formalization targets

Goal: Chapter I, Theorem 11

\sup \mathcal L_n = F_n \qquad \text{for every } n \ge 0 .

The supremum is not attained once $n \ge 2$ (with two evaluations every length $2 - \varepsilon$ is searchable, the length $2$ is not), which is why the statement is about the supremum rather than a maximum.

Milestones

$\sup \mathcal L_1 = 1$ : one value carries no information (proof of Theorem 11, p. 34).
$\sup \mathcal L_2 = 2$ (p. 35).
Eq. (22.3): for $n \ge 2$ every $L \in \mathcal L_n$ satisfies $L < F_{n-1} + F_{n-2}$ .
For $n \ge 2$ every $0 < L < F_{n-1} + F_{n-2}$ lies in $\mathcal L_n$ (p. 36).
Eq. (22.4): $F_{20} > 10{,}000$ , hence for every $L > 0$ twenty evaluations locate the maximum within an interval of length $10^{-4} L$ .
Eqs. (22.5)–(22.6): with $r_{1,2} = (1 \pm \sqrt5)/2$ ,

F_n = \frac{r_2 - 1}{r_2 - r_1} r_1^{\,n} + \frac{1 - r_1}{r_2 - r_1} r_2^{\,n}, \qquad \frac{F_{n+1}}{F_n} \to r_1 .

Theorem 12, corrected: $K_0 = K_1 = 1$ , $K_2 = 2$ , $K_3 = 4$ , and

K_n = F_{n+1} - 1 \qquad (n \ge 3).

Significance

The result. Theorem 11 is an exact minimax statement: $n$ evaluations shrink the interval of uncertainty for the peak of a unimodal function by a factor of at most $F_n \approx r_1^{\,n}/\sqrt5$ , and no adaptive rule, however clever, does better. It certifies Fibonacci search as optimal and golden-section search as asymptotically optimal, which is the reason these methods are the default line searches when derivatives are unavailable. Eq. (22.4) quantifies the rate: twenty evaluations give four decimal digits.

Formalizing it. The theorem has been proved since 1953; the work here is a machine-checked proof of the full minimax statement over all adaptive procedures, including the lower bound. That half is a statement about every decision tree and requires an adversary argument, which is exactly the kind of reasoning that is informal in the book and easy to get wrong. The discrete Theorem 12 is misprinted in the book (see below), so a formal proof also settles the correct values. We are not aware of an existing formalization of the optimality of Fibonacci search in Lean or another proof assistant. The Binet formula and the ratio limit are in Mathlib for Mathlib's indexing (Real.coe_fib_eq, tendsto_fib_succ_div_fib_atTop); milestone 6 only transfers them to the book's indexing.

Difficulty

The upper bound $L < F_{n-1} + F_{n-2}$ must hold for every procedure, not only for procedures that follow the "compare two points, discard a piece, keep the surviving point" pattern of the book's figures. A procedure may place its second point depending on the first value, may re-evaluate points, may evaluate outside $[0, L]$ , and may branch on the exact values rather than on their order. The book's argument tacitly restricts to that pattern, so the lower bound has to be established for arbitrary trees, where the information carried by exact values, repeated or wasted evaluations and branch-dependent placements all have to be accounted for. The bookkeeping is delicate because the surviving sets are half-open or open intervals, and whether the endpoints are included decides that the supremum is not attained.

The naive attempt of proving a bound only for "one new point per step inside the current bracket" procedures does not prove the goal: the goal quantifies over all decision trees.

Formalization scope

Model fixed. Deterministic adaptive procedures (decision trees branching on the exact real value observed), exact function values, cost equal to the number of evaluations; this is one of the models that Bellman's footnote 8 alludes to ("It is actually not easy to specify precisely what we mean by an optimal search procedure"). Functions are ℝ → ℝ, constrained only on $[0, L]$ ; evaluations outside $[0, L]$ are allowed and useless.
Output. A closed interval $[a, b]$ with $a \le b$ , $b - a \le 1$ containing the maximizer. It need not lie inside $[0, L]$ or have length exactly one; for $L \ge 1$ this is equivalent to Bellman's "sub-interval of unit length".
Indexing. The book's $F_n$ is a separate definition bookFib with $F_0 = F_1 = 1$ ; in Mathlib's indexing $F_n$ is Nat.fib (n + 1). The goal is stated for every $n \ge 0$ ; the book calls $F_0$ a convention, and in this model $\sup \mathcal L_0 = 1$ agrees with it.
Sup, not max. Theorem 11 is stated with IsLUB, never as "a procedure exists for $L = F_n$ ", which is false for $n \ge 2$ . Theorem 12 is stated with IsGreatest, which asserts that the maximum exists.
Implicit ranges. Eq. (22.3) is stated unconditionally for all $n \ge 2$ (the book proves it under the induction hypothesis). "Within $10^{-4}$ of the original interval length" is read as an interval of length at most $10^{-4} L$ .
Misprint corrected. Theorem 12 prints $K_n = 1 + F_n$ for $n \ge 3$ . On seven points, four evaluations suffice: evaluate points 3 and 5; if $f(3) > f(5)$ the peak is among points 1–4 with $f(3)$ known, and evaluating point 2 and then point 1 or 4 finds it; the case $f(5) > f(3)$ is symmetric, and $f(3) = f(5)$ forces the peak at point 4. So $K_4 \ge 7 > 6 = 1 + F_4$ . The mission states $K_n = F_{n+1} - 1$ for $n \ge 3$ , which agrees with the printed $K_3 = 4$ and keeps all printed initial values. The printed text is kept verbatim in the milestone.
Ruling out trivializations. The procedure never sees $f$ except through the values it requests, and it must succeed for every strictly unimodal $f$ with one fixed tree; "some interval of length one contains the maximizer" with no procedure, or a procedure allowed to depend on $f$ , would make the problem trivial and is not what is stated.
Contributions welcome. A reusable decision-tree framework for query-complexity lower bounds, lemmas about which finite sets of observed values are consistent with a strictly unimodal function, and the Fibonacci search tree itself as a construction.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter I, § 22, pp. 34–36. doi:10.2307/j.ctv1nxcw0f
J. Kiefer, Sequential minimax search for a maximum, Proceedings of the American Mathematical Society 4 (1953), 502–506. doi:10.1090/S0002-9939-1953-0055639-3

9 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Bellman's Dynamic Programming I: Existence and Uniqueness for the Multi-Stage Allocation EquationTextbook

Motivation

Chapter I of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) opens the book with a multi-stage allocation process: a resource is divided, stage after stage, between two activities, each of which yields an immediate return and leaves behind a depleted remainder that is re-divided at the next stage. The chapter uses this process as its prototype for "a number of multi-stage processes, of diverse origin, but similar analytic structure" (§ 8, p. 11), and the techniques it introduces here — the functional equation of the infinite process, successive approximations, approximation in policy space, transfer of convexity and concavity through the recurrence, and a stability estimate — reappear throughout the book and in the later theory of Markov decision processes.

When the number of stages is large, Bellman replaces the finite sequence of recurrences by a single equation for the infinite process. As the book stresses (p. 11), this replacement is only useful once one knows that the equation has a solution and possesses "no extraneous solutions". This mission formalizes that existence and uniqueness theorem and the chapter's main structural results that rest on it.

Setting

A quantity $x \ge 0$ is split into $y \in [0,x]$ , assigned to a first activity with return $g(y)$ , and $x - y$ , assigned to a second activity with return $h(x-y)$ . After the stage the first allocation has been reduced to $ay$ and the second to $b(x-y)$ , and the process continues with the quantity $ay + b(x-y)$ . Writing

T(f,y) = g(y) + h(x-y) + f\big(ay + b(x-y)\big),

the total return $f(x)$ of the infinite process satisfies the allocation equation (Bellman's (8.1))

f(x) = \max_{0 \le y \le x} T(f,y), \qquad x \ge 0.

The standing hypotheses of Chapter I, Theorem 1 are:

$g$ and $h$ are continuous on $[0,\infty)$ and $g(0) = h(0) = 0$ ;
with $m(x) = \max_{0 \le y \le x} \max(|g(y)|, |h(y)|)$ and $c = \max(a,b)$ , the series $\sum_{n=0}^\infty m(c^n x)$ converges for every $x \ge 0$ ;
$0 \le a < 1$ and $0 \le b < 1$ .

The successive approximations from an initial function $f_0$ are $f_{N+1}(x) = \max_{0 \le y \le x} T(f_N, y)$ . A policy is a function $y_0(x)$ with $0 \le y_0(x) \le x$ ; its return is the total of the stage returns obtained by using $y_0$ at every stage.

In Lean all objects live in the namespace BellmanDP.Allocation: allocT is $T$ , allocM is $m$ , AllocationHyp g h a b bundles the three hypotheses, IsAllocationSolution g h a b f is the equation with the maximum attained, allocIter is the sequence $f_N$ , and policyReturn is the return of a policy.

Formalization targets

Goal: Chapter I, Theorem 1

Under the three hypotheses, there is a function $f$ with

f(x) = \max_{0 \le y \le x}\big[g(y) + h(x-y) + f(ay + b(x-y))\big] \quad (x \ge 0), \qquad f(0) = 0,\ f \text{ continuous at } 0,

this $f$ is continuous on $[0,\infty)$ , and every solution continuous at $0$ with value $0$ there coincides with $f$ on $[0,\infty)$ .

Milestones

Theorem 2 — from any $f_0$ continuous on $[0,\infty)$ with $f_0(0) = 0$ , the successive approximations converge to $f$ uniformly on every finite interval.
Theorem 3 — started from the return of a continuous policy, the successive approximations increase monotonically and converge to $f$ uniformly on every finite interval.
Lemma 1 — if $G(x,y)$ is jointly concave on $x,y \ge 0$ , then $x \mapsto \max_{0 \le y \le x} G(x,y)$ is concave.
Theorem 4 — if $g$ and $h$ are convex, $f$ is convex and for each $x$ the maximum is attained at $y = 0$ or $y = x$ .
Theorem 5 — if $g$ and $h$ are strictly concave, $f$ is strictly concave and the maximizing $y$ is unique for every $x$ .
Theorem 9 — for the general equation $f(x) = \max_{0\le y\le x}[u(x,y) + f(ay+b(x-y))]$ , the continuous solutions for returns $u$ and $v$ satisfy $|f(x) - F(x)| \le \sum_{n \ge 0} D(c^n x)$ , where $D(z)$ is the maximum of $|u - v|$ over $0 \le y \le x \le z$ .

Significance

Theorem 1 is what gives meaning to "the solution" of the allocation equation, which every later result of the chapter refers to. Without the side condition at $0$ uniqueness fails: when $g = h = 0$ , every constant function and the indicator of $(0,\infty)$ solve the equation. Theorems 2 and 3 turn the existence proof into computational procedures (value iteration and policy improvement), and Theorem 3's monotonicity is the prototype of the policy-improvement property. Theorems 4 and 5 are the first structural results on optimal policies — all-or-nothing allocation under convex returns, a unique interior-or-boundary allocation under strictly concave returns — and Theorem 9 bounds the error made by replacing a return function with a simpler approximation.

These are classical results with published proofs in the book. No machine-checked version of any of them is known to this mission; the work is to formalize the proofs, building reusable infrastructure for functional equations of the form $f(x) = \max_{y \in D(x)}[r(x,y) + f(\tau(x,y))]$ with a contracting transition $\tau$ .

Difficulty

The equation is not a contraction in the supremum norm on $[0,\infty)$ : $g$ and $h$ may be unbounded, so no global Banach fixed-point argument applies. Control comes instead from the shrinking of the argument, $ay + b(x-y) \le cx$ , which propagates a local estimate near $0$ out to every finite interval, and the summability hypothesis (1b) is what makes the resulting series converge uniformly on bounded sets. Uniqueness cannot come from a norm estimate either; it rests on continuity at $0$ alone. The maximum in the equation must be shown to be attained, which requires continuity of the limit function; the book notes (p. 13) that the monotone argument for nonnegative $g,h$ gives only a supremum. For Theorems 4 and 5, convexity and concavity must be carried through each approximation and preserved in the limit, and strict concavity must be recovered for the limit, where a pointwise limit of strictly concave functions is only concave.

Formalization scope

Functions are ℝ → ℝ; only their values on $[0,\infty)$ enter any hypothesis or conclusion. Continuity at $0$ is one-sided (ContinuousWithinAt f (Set.Ici 0) 0), and uniqueness is equality on $[0,\infty)$ .
The maximum in the equation is encoded as IsGreatest of $\{T(f,y) : 0 \le y \le x\}$ , so a solution attains its maximum at every $x \ge 0$ . The maxima inside definitions ( $m$ , $f_{N+1}$ , the triangle maximum of Theorem 9) are real suprema (sSup) of images of compact nonempty sets of continuous functions, which equal the book's maxima under the stated hypotheses.
The later theorems refer to "the solution" of Theorem 1 by quantifying over solutions that are continuous at $0$ and vanish there; they never quantify over arbitrary solutions of the equation, for which the conclusions are false.
Theorem 3's "converges uniformly" is stated uniformly on every finite interval $[0,R]$ , the sense in which Theorem 2 and the series (11.10) used in its proof converge. Its initial function is defined explicitly as the series of stage returns along the trajectory of the policy.
Theorem 4's " $y$ will equal $0$ or $x$ " is stated as: an endpoint is a maximizer. It does not say every maximizer is an endpoint, which fails for $g = h = 0$ .
Each theorem carries its own parameter range as printed: $0 \le a, b < 1$ for Theorems 1–5, $0 < a, b < 1$ for Theorem 9.
Not included: Theorem 6 (the policy structure under strict concavity, which uses $f'$ without a hypothesis making $f$ differentiable), Theorems 7 and 8 (explicit solutions), Theorem 10 (the multi-dimensional process), and Theorems 11–12 on Fibonacci search, which form a separate mission.

Welcome contributions: a general existence-and-uniqueness theorem for equations $f(x) = \sup_{y \in D(x)}[r(x,y) + f(\tau(x,y))]$ with $\|\tau(x,y)\| \le c\|x\|$ , and a lemma that parametric maxima over $[0,x]$ of continuous functions are continuous in $x$ .

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. https://doi.org/10.2307/j.ctv1nxcw0f — Chapter I, §§ 8–14 and 18, pp. 11–29.
R. Bellman, "On the theory of dynamic programming", Proceedings of the National Academy of Sciences 38 (1952), 716–719. https://doi.org/10.1073/pnas.38.8.716

10 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Assumptions of Physics IV: Ensemble Spaces Are CancellativeTextbook

Motivation

This is the fourth mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing the axiomatic core of Part II, Chapter 4, "Ensemble spaces". The chapter proposes three physically motivated axioms (ensemble, mixture, entropy) that every space of statistical states should satisfy, covering classical probability distributions and quantum density operators alike, and derives from them structure that is usually postulated, for example that mixtures can be "un-mixed" (cancellativity). That is the first step towards embedding ensembles in a vector space. Unlike missions II and III, this mission does not depend on earlier missions.

Setting

An ensemble space is a $T_0$ , second countable topological space $E$ with a continuous mixing operation $(p,a,b)\mapsto pa+\bar pb$ ( $p\in[0,1]$ , $\bar p=1-p$ ) that is idempotent, commutative and associative, and a continuous entropy $S:E\to\mathbb R$ . The entropy is strictly concave, $S(pa+\bar pb)\ge pS(a)+\bar pS(b)$ with equality iff $a=b$ , and bounded above by $I(p,\bar p)+pS(a)+\bar pS(b)$ for a universal function $I$ . Two ensembles are orthogonal, $a\perp b$ , when this bound is saturated, and mixtures preserve orthogonality. An ensemble $c$ is a component of $a$ if $a=pc+\bar pd$ with $p\in(0,1]$ ; two ensembles are separate if they have no common component. The mixing entropy is $MS(a,b)=S(\tfrac12a+\tfrac12b)-\tfrac12S(a)-\tfrac12S(b)$ .

Formalization targets

Goal (Theorem 4.73, Ensemble spaces are cancellative)

pa+\bar pe=pb+\bar pe \text{ for some } p\in(0,1)\implies a=b.

Milestones

Proposition 4.67: orthogonality is irreflexive and symmetric, components are not orthogonal, and orthogonality implies separateness.
Corollary 4.102: $pa+\bar pb=b$ for some $p\in(0,1]$ implies $a=b$ .
Proposition 4.116 (items 1, 2, 3, 5): $MS(a,b)\ge0$ , $MS(a,b)=0\iff a=b$ , $MS(a,b)\le I(\tfrac12,\tfrac12)$ , $MS(a,b)=MS(b,a)$ .

Significance

Cancellativity is what allows affine combinations with negative coefficients, the origin, in this framework, of the vector-space embedding of ensembles (Theorem 4.94) and of negative quasi-probabilities such as Wigner functions. It holds in classical and quantum statistics, and here it is derived from continuity and strict concavity of the entropy instead of being postulated. The results are proved informally in the book; no machine-checked formalization is known to the drafters.

Difficulty

The convex-space axioms are stated in a two-sided associativity form, so every rearrangement of mixtures must be derived from it. The book's proof of cancellativity first propagates the equality $pa+\bar pe=pb+\bar pe$ from one coefficient to all of $(0,1)$ by an iteration $p\mapsto 2p/(1+p)$ , and then uses a limit $p\to1$ together with continuity of mixing and of the entropy. Strict concavity has to be applied only to non-trivial coefficients.

Formalization scope

The structure EnsembleSpace I E bundles Axioms 4.4, 4.7 and 4.55 for a topological space E; mixing coefficients are elements of Mathlib's unitInterval. Real coefficient expressions in the associativity axiom pass through clampI, the projection $\mathbb R\to[0,1]$ , and lie in $[0,1]$ on the stated domain. The universal function $I$ is a parameter. Orthogonality is saturation of the upper bound for every $p\in(0,1)$ . Strict concavity is required for $p\in(0,1)$ only, since at $p\in\{0,1\}$ equality is automatic. The book's Proposition 4.67 uses $I(p,\bar p)>0$ for $p\in(0,1)$ , which follows from universality of $I$ (any space with two distinct ensembles forces it); the milestone carries this as an explicit hypothesis. Items 3 and 4 of Proposition 4.116 in the book use the normalization $I(\tfrac12,\tfrac12)=1$ from Theorem 4.59; item 3 is stated with $I(\tfrac12,\tfrac12)$ and item 4 is omitted. Hull operators, the vector-space embedding (Theorem 4.94), boundedness of lines (Theorem 4.105), the entropic geometry and the standard classical/quantum models (Propositions 4.5, 4.9, 4.56) are left for later missions.

Selected references

G. Carcassi, C. A. Aidala, Assumptions of Physics, Ver. 3.0, December 31, 2025. https://assumptionsofphysics.org/book — Part II, Chapter 4 "Ensemble spaces", pp. 197–284.

5 thms2 active usersReviewed

Dynamical Systems Geometry & Topology·Captain: Lucas

Building Anosov flows on 3-manifolds (Béguin–Bonatti–Yu)Research Paper

Motivation

Anosov flows are the model of uniformly hyperbolic, chaotic continuous-time dynamics: a nonsingular vector field $X$ on a closed manifold $M$ is Anosov when the tangent bundle splits as $TM=E^s\oplus\mathbb RX\oplus E^u$ , with $E^s$ uniformly contracted and $E^u$ uniformly expanded by the derivative of the flow. They are structurally stable, so one can hope to classify them up to topological equivalence. In dimension three this classification is far from complete: it is not known which closed 3-manifolds carry Anosov flows, nor how many inequivalent Anosov flows a given manifold can carry.

The classical examples — suspensions of hyperbolic toral automorphisms and geodesic flows of hyperbolic surfaces — are rigid (Plante; Ghys). Non-algebraic examples were built by Franks–Williams (a nontransitive Anosov flow, 1980), Handel–Thurston, Goodman, Fried, Bonatti–Langevin, Fenley, Barbot and others. Several of these examples glue together neighbourhoods of hyperbolic sets along their boundaries. Béguin, Bonatti and Yu (Geom. Topol. 21 (2017)) turned this into a general theory, and used it to answer questions of Katok and of Barbot–Fenley.

Setting

A plug $(U,X)$ is a compact 3-manifold $U$ with boundary and a nonsingular C¹ vector field $X$ transverse to $\partial U$ . The boundary splits into the entrance boundary $\partial^{in}U$ (where $X$ points inwards) and the exit boundary $\partial^{out}U$ . The maximal invariant set $\Lambda$ consists of the points whose orbit stays in $U$ for all times. The plug is hyperbolic if $\Lambda$ is a hyperbolic set with one-dimensional strong stable and strong unstable bundles. The entrance lamination $L^s_X=W^s(\Lambda)\cap\partial^{in}U$ and the exit lamination $L^u_X=W^u(\Lambda)\cap\partial^{out}U$ are one-dimensional laminations of the boundary surfaces. The plug has filling MS laminations when every component of $\partial^{in}U\setminus L^s_X$ (and of $\partial^{out}U\setminus L^u_X$ ) is a strip: a disc whose accessible boundary consists of two leaves asymptotic to each other at both ends.

A diffeomorphism $\varphi:\partial^{out}U\to\partial^{in}U$ is a strongly transverse gluing map if $\varphi_*(L^u_X)$ and $L^s_X$ are transverse and cut $\partial^{in}U$ into squares with sides alternately on leaves of the two laminations. Gluing then gives a closed manifold $U/\varphi$ with an induced vector field $Z$ . Two triples $(U,X,\varphi)$ and $(U,Y,\psi)$ are strongly isotopic if they are joined by a continuous path of such data.

Formalization targets

Goal: the gluing theorem (Theorem 1.5)

\begin{gathered}(U,X)\ \text{hyperbolic plug with filling MS laminations},\ \Lambda\ \text{without attractors or repellers},\ \varphi\ \text{strongly transverse}\\ \Longrightarrow\ \exists\,(Y,\psi)\ \text{strongly isotopic to}\ (X,\varphi)\ \text{with the field induced by } Y \text{ on } U/\psi\ \text{Anosov}.\end{gathered}

Milestones

Proposition 1.1: gluing two hyperbolic plugs along transverse laminations gives a hyperbolic plug. Proposition 1.3: strongly transverse gluing preserves filling MS laminations.
Lemma 3.27 (self-gluing case): the glued manifold $U/\varphi$ exists as a closed smooth manifold with an induced vector field.
Proposition 1.6: if the graph of basic pieces is strongly connected, the Anosov flow of Theorem 1.5 is transitive.
Theorem 1.8: every transitive Anosov flow on a closed 3-manifold is a factor of a transitive Anosov flow on another closed 3-manifold, restricted to a compact invariant set.
Theorem 1.9: some closed orientable 3-manifold carries both a transitive and a nontransitive Anosov flow.
Theorem 1.10 and Corollary 1.11: every MS foliation of a closed orientable surface is the entrance foliation of a transitive attracting hyperbolic plug; in particular incoherent transitive hyperbolic attractors exist.
Theorem 1.12: every hyperbolic plug with filling MS laminations embeds, up to topological equivalence, in an Anosov flow on a closed orientable 3-manifold, which can be taken transitive when $\Lambda$ has no attractors or repellers.
Theorem 1.13: for every $n\ge1$ some closed orientable 3-manifold carries $n$ pairwise inequivalent transitive Anosov flows.
Theorem 1.15: some transitive Anosov flow admits infinitely many pairwise nonisotopic transverse tori.

Significance

Theorem 1.5 lets one build Anosov flows on closed 3-manifolds by gluing hyperbolic plugs. Proposition 1.6 gives a combinatorial criterion for the result to be transitive. Together they answer a question of Katok (Theorem 1.9) and questions of Barbot and Fenley on manifolds with several hyperbolic JSJ pieces supporting transitive Anosov flows (Theorem 1.13). They also show that transitive Anosov flows admit no fully canonical decomposition into finitely many transverse tori (Theorem 1.15). The results are proved in the source paper. None of them is formalized, and Mathlib has no theory of hyperbolic sets for flows, stable manifolds or laminations. A formal proof therefore needs a substantial amount of reusable smooth dynamics.

Difficulty

The glued vector field is generally not hyperbolic: perturbing the gluing map can create solid tori of parallel periodic orbits. The difficulty is to choose the gluing map (and the vector field within its topological equivalence class) so that cone fields on $\partial^{in}U$ are mapped into themselves by the return map. The return map is the composition of the crossing map of the plug with the gluing map. Contraction and expansion must therefore be controlled simultaneously along two transverse invariant foliations. The paper achieves this after reducing to plugs with an affine Markov partition. The naive approach — fixing $\varphi$ and trying to verify hyperbolicity — fails in general (Question 1.4 of the paper remains open).

Formalization scope

Manifolds are modelled on the half-space EuclideanHalfSpace 3 with a $C^\infty$ structure; closed manifolds are compact, Hausdorff and BoundarylessManifold, and connected where the paper's statements concern a single manifold. Orientability is given by an atlas with positive Jacobians.
Vector fields are C¹ sections; flows are encoded by integral curves, so that partial flows on manifolds with boundary make sense; flowMap X t x is $x$ when the orbit is undefined.
Hyperbolicity is quantified over a continuous Riemannian metric, invariant line fields and constants $C,\lambda>0$ ; continuity of the splitting is not imposed (it is automatic).
Filling MS laminations are encoded through the strip condition (Lemma 3.21); leaves of $L^s$ are path components of intersections of weak stable manifolds with $\partial^{in}U$ .
The glued manifold $U/\varphi$ is not a quotient type: statements quantify over every closed smooth 3-manifold $N$ with a surjective C¹ immersion $q:U\to N$ realising the identification. Lemma 3.27 (a milestone) guarantees such $N$ exists, so these statements are not vacuous. The induced field is not required to be C¹ and "Anosov" there means hyperbolicity of the whole manifold.
Useful reusable infrastructure: flows of C¹ vector fields on compact manifolds (with boundary), stable manifold theory, the λ-lemma, laminations and foliations of surfaces, and gluing of manifolds along boundary components.

Selected references

F. Béguin, C. Bonatti, B. Yu, Building Anosov flows on 3-manifolds, Geom. Topol. 21 (2017) 1837–1930. https://doi.org/10.2140/gt.2017.21.1837

59 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+2·Captain: mikedeng1

Linear Programming: Foundations and Extensions III: Network Flows, the Integrality Theorem and König's TheoremTextbook

Motivation

Minimum-cost network flow problems are the largest special class of linear programs met in practice: transportation, distribution, assignment, communication and electric networks, facility location and financial planning all reduce to moving material along the arcs of a directed network from supply nodes to demand nodes at least cost. Chapter 14 of R. J. Vanderbei's Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) develops the network simplex method, and closes with two structural facts that explain why this class is special: simplex bases are spanning trees of the network, and a network problem with integer supplies has integer basic solutions. Vanderbei then uses integrality to prove a classical theorem of combinatorics, König's theorem on regular bipartite graphs. Chapter 15, §5 treats the maximum-flow problem on the same objects and proves the Max-Flow Min-Cut Theorem.

The combinatorial results are older than linear programming. D. König proved in 1916 that every regular bipartite graph has a perfect matching (Math. Ann. 77). The Max-Flow Min-Cut Theorem is due to Ford and Fulkerson (1956, Canad. J. Math. 8) and, independently, Elias, Feinstein and Shannon (1956). The integrality of network bases is the total unimodularity of incidence matrices, known since the 1950s (Hoffman and Kruskal, 1956).

Setting

A network $(N,A)$ has a finite set $N$ of $m$ nodes and a set of directed arcs $A\subseteq\{(i,j): i,j\in N,\ i\ne j\}$ . Node $i$ carries a supply $b_i$ (negative values are demands) with $\sum_i b_i=0$ , and arc $(i,j)$ carries a cost $c_{ij}$ . The flow $x_{ij}$ on arc $(i,j)$ is the decision variable. The node–arc incidence matrix $A$ has in the column of $(i,j)$ an entry $+1$ in row $j$ , $-1$ in row $i$ , and $0$ elsewhere. The network flow problem (14.1) is

\text{minimize } c^{T}x\quad\text{subject to}\quad Ax=-b,\ x\ge 0 .

A flow satisfying $Ax=-b$ is balanced; a balanced flow with $x\ge0$ is feasible. Paths ignore arc directions; the network is connected if every two nodes are joined by a path, which is assumed throughout Chapter 14. A spanning tree is a set of arcs that, on all of $N$ and without directions, is connected and has no cycle. Fixing a root node $r$ and deleting its row gives the matrix $\tilde A$ . A set $T$ of arcs is a basis if its columns form an invertible square submatrix of $\tilde A$ , and a basic feasible solution is a feasible flow vanishing off some basis.

For maximum flow, a source $s$ , a sink $t$ and finite upper bounds $u_{ij}$ are given; all $b_i=0$ and an extra arc $(t,s)$ of infinite capacity is added. A feasible flow satisfies $0\le x_{ij}\le u_{ij}$ , $x_{ts}\ge0$ and flow balance. A cut is a node set $C$ with $s\in C$ , $t\notin C$ , and its capacity is $\kappa(C)=\sum_{(i,j)\in A,\ i\in C,\ j\notin C}u_{ij}$ .

Formalization targets

Goal: König's Theorem (Theorem 14.3, p. 216)

If $n$ girls and $n$ boys are such that every girl knows exactly $k\ge1$ boys and every boy knows exactly $k$ girls (knowing being symmetric), then there is a bijection $\sigma$ from girls to boys with

\text{girl } i \text{ knows boy } \sigma(i)\qquad\text{for all } i .

Milestones

Theorem 14.1 (p. 205): for a connected network, a set $T$ of arcs indexes a basis of $\tilde A$ if and only if $T$ is a spanning tree.
Theorem 14.2, Integrality Theorem (p. 216): with integer supplies, every basic feasible solution is integral,

x_{ij}\in\mathbb Z\qquad\text{for all }(i,j)\in A .

Eq. (15.8) (p. 234): $x_{ts}\le\kappa(C)$ for every feasible flow and every cut.
Theorem 15.1, Max-Flow Min-Cut (p. 234):

\max\{x_{ts}\}=\min_C \kappa(C),

both extrema attained.

The goal is independent of the network definitions in its statement; the milestones are the book's route to it (14.1, 14.2) and the chapter's other duality theorem on the same objects (15.8, 15.1).

Significance

König's theorem is the base case of matching theory: it gives perfect matchings in regular bipartite graphs, hence edge colourings of bipartite graphs with $\Delta$ colours, and via Birkhoff–von Neumann-type arguments the decomposition of doubly stochastic matrices. The Integrality Theorem is the reason assignment, transportation and shortest-path problems can be solved as linear programs without an integrality constraint. Theorem 14.1 is the correspondence the network simplex method is built on. Max-Flow Min-Cut is the prototype of combinatorial min–max theorems.

All four theorems are classical and proved. This mission adds machine-checked versions in the book's own formulation: the incidence matrix with Vanderbei's sign convention $Ax=-b$ , bases as square submatrices of $\tilde A$ with a chosen root, and maximum flow as a circulation through an added return arc. The platform already has network integrality, a tree-solution characterisation and max-flow min-cut in the Bertsimas–Tsitsiklis formulation and a Keller–Trotter max-flow statement; none is stated in this form, and Mathlib has Hall's marriage theorem but no regular-bipartite corollary.

Difficulty

The combinatorial content is small; the difficulty is in the passage between matrices and graphs. Theorem 14.1 needs both directions: the book shows that a spanning tree gives a triangularisable, hence invertible, submatrix and leaves the converse (independent columns form a spanning tree) as an exercise, which requires showing that any cycle, including a pair of antiparallel arcs, yields a linearly dependent set of columns and that $m-1$ acyclic arcs span. The book's proof of König's theorem applies the Integrality Theorem to the girl–boy network, which need not be connected, while Chapter 14 assumes connectedness throughout: the statement of 14.2 does not apply to it verbatim. The step "a feasible problem has a basic optimal solution" is also used and is not stated in the chapter.

Formalization scope

Nodes are a Fintype with decidable equality; arcs are a Finset (N × N), so parallel arcs are excluded as in the book, and IsNetwork excludes loops. Flows are real functions on ordered pairs; only their values on arcs matter.
"Connected" is preconnectedness of the undirected simple graph of the arcs; a spanning tree is an arc set whose undirected graph is a tree and in which no two arcs join the same pair of nodes.
A basis is $m-1$ linearly independent columns of the $(m-1)$ -row matrix $\tilde A$ , the same as an invertible square submatrix. The root $r$ is arbitrary, as in the book ("say, the last one").
Integer data means integer supplies; costs do not enter Theorem 14.2, since a basic optimal solution is a basic feasible solution.
In König's theorem both sides are Fin n, knowing is one relation between girls and boys, and $k\ge1$ is a hypothesis: the book's proof divides by $k$ , and for $k=0<n$ the claim is false. No connectedness is assumed.
For maximum flow, the return arc $(t,s)$ is a separate variable; $s\ne t$ and $u_{ij}\ge0$ are hypotheses that the book leaves implicit. Maximum and minimum are stated with attainment.
No statement involves a constant the book leaves implicit.

A formalization of the goal as a matching of size $n$ in some larger graph, or with the degree conditions on one side only, would be a different theorem; the conclusion is a bijection between exactly the $n$ girls and the $n$ boys using only acquainted pairs.

Useful infrastructure, reusable beyond this mission: the incidence matrix and its total unimodularity, the undirected graph of an arc set. Proofs of König's theorem through Hall's theorem (Mathlib Finset.all_card_le_biUnion_card_iff_exists_injective) are welcome alongside the book's route.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer, 2014. DOI 10.1007/978-1-4614-7630-6
D. König, Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre, Math. Ann. 77 (1916), 453–465. DOI 10.1007/BF01456961
L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956), 399–404. DOI 10.4153/CJM-1956-045-5
A. J. Hoffman and J. B. Kruskal, Integral boundary points of convex polyhedra, in Linear Inequalities and Related Systems, Ann. of Math. Studies 38, Princeton University Press, 1956, 223–246.

7 thms2 active usersReviewed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XIV: Conforming Approximating Sequences for Markov ChainsTextbook

Motivation

Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set $S_N$ and redistribute the probability of leaving $S_N$ back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.

Setting

A Markov chain with costs $\Gamma$ on a denumerable state space $S$ has transition probabilities $P_{ij}$ with $\sum_jP_{ij}=1$ and a finite nonnegative cost $C(i)$ at each state. For a set $G\subseteq S$ and a start $i$ , $T_{iG}\ge 1$ is the first passage time to $G$ . The taboo probability ${}_GP^{(t)}_{ik}$ is the probability of moving from $i$ to $k$ in $t$ steps with no intermediate state in $G$ . The expected visits ${}_Gu_{ik}$ count the visits to $k$ at times $0\le t<T_{iG}$ . The mean first passage time is $m_{iG}=E[T_{iG}]$ , infinite when $G$ is missed with positive probability. The first passage cost is $c_{iG}=E\big[\sum_{t<T_{iG}}C(X_t)\big]$ . A state $i$ is positive recurrent when $m_{ii}<\infty$ , and the steady state probability is $\pi_i=m_{ii}^{-1}$ . On a positive recurrent class $R$ the average cost is $J_R=\sum_{j\in R}\pi_jC(j)$ . The chain is $z$ standard when $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ . Such a chain has one positive recurrent class $R\ni z$ with $J_R<\infty$ , and every other state is transient.

An approximating sequence (AS) $(\Gamma_N)_{N\ge N_0}$ consists of increasing nonempty finite sets $S_N$ with $\bigcup_NS_N=S$ and, for each $N$ , a chain $\Gamma_N$ on $S_N$ with the same costs and transition probabilities $P_{ij}(N)\to P_{ij}$ . The quantities of $\Gamma_N$ are written $m_{iG}(N)$ , $c_{iG}(N)$ , $\pi_i(N)$ and $J(i)(N)$ . An AS is conforming (for a $z$ standard $\Gamma$ ) if, for large $N$ , $\Gamma_N$ is unichain with $z$ in its positive recurrent class, and $m_{iz}(N)\to m_{iz}$ and $c_{iz}(N)\to c_{iz}$ for all $i$ . It is conforming on $R$ if $\pi_i(N)\to\pi_i$ and $J(i)(N)\to J_R$ on $R$ .

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the probability of each excluded target $r\notin S_N$ according to an augmentation distribution $q_\cdot(i,r,N)$ on $S_N$ :

P_{ij}(N)=P_{ij}+\sum_{r\in S-S_N}P_{ir}\,q_j(i,r,N),\qquad j\in S_N.

It sends excess probability to $G$ if every $q_\cdot(i,r,N)$ is concentrated on $G$ .

Formalization targets

Goal: Proposition C.5.2

For a $z$ standard chain $\Gamma$ and a finite nonempty $G\subseteq S$ ,

\text{every ATAS that sends excess probability to } G \text{ is conforming},

and if $G\subseteq R$ it is also conforming on $R$ . No rate of convergence and no constants are involved, and $G$ need not contain $z$ .

Milestones

Proposition C.4.2: for fixed $t$ , $\lim_N{}_GP^{(t)}_{ik}(N)={}_GP^{(t)}_{ik}$ ; also $\liminf_N{}_Gu_{ik}(N)\ge{}_Gu_{ik}$ and $\liminf_Nm_{iG}(N)\ge m_{iG}$ .
Proposition C.4.3: $\pi_i(N)\to0$ off the positive recurrent states, and along subsequences $\pi_i(N_s)\to b\pi_i$ on a class, with $0\le b\le1$ .
Proposition C.4.5: $\liminf_Nc_{iG}(N)\ge c_{iG}$ .
Proposition C.4.6: on a positive recurrent class, convergence of $\pi$ , of $m_{zz}$ and of all $m_{iG}$ are equivalent. Given these, convergence of $J(i)$ , of $c_{zz}$ and of all $c_{iG}$ are equivalent.
Proposition C.4.9: conformity implies $\pi_i(N)\to\pi_i$ for all $i$ , and that the constant average costs $J(N)$ of $\Gamma_N$ converge to $J_R$ .

Further results

Proposition C.5.3: an ATAS is conforming when, for $N\ge N^*$ , the augmentation distributions satisfy $\sum_{j\ne z}q_j(i,r,N)m_{jz}\le m_{rz}$ and $\sum_{j\ne z}q_j(i,r,N)c_{jz}\le c_{rz}$ .
Corollary C.5.4: for a $0$ standard chain on $\{0,1,2,\dots\}$ with an upper Hessenberg transition matrix, truncated to $S_N=\{0,\dots,N\}$ with the excess sent to $N$ , the ATAS is conforming.

Significance

The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching $z$ is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple $b\pi$ with $b<1$ . First passage costs can converge to the wrong value even when the steady state probabilities converge.

Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between $\liminf$ bounds and limits in $[0,\infty]$ explicit, and produces a reusable library of first passage quantities for countable chains.

Difficulty

The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in $\Gamma_N$ , a first passage that leaves $S_N$ is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation $m_{iz}(N)=1+\sum_{j\ne z}P_{ij}(N)m_{jz}(N)$ fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: $\Gamma_N$ may have several recurrent classes, or a recurrent class not containing $z$ , and ruling this out is part of the conclusion rather than an assumption.

Formalization scope

The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, $m_{iG}$ , $c_{iG}$ , $\pi_j=(m_{jj})^{-1}$ and $J_R=\sum_{j\in R}\pi_jC(j)$ are defined as sums in $[0,\infty]$ . $m_{iG}=\sum_{t\ge0}P(T_{iG}>t)$ is infinite whenever $G$ is missed with positive probability. The average cost $J(i)$ is the $\limsup$ of the Cesàro cost averages.

An AS is a structure carrying $N_0$ , the finite sets $S_N$ (as Finset S) and $P_{ij}(N)$ . $\Gamma_N$ is built as an MC on the subtype of $S_N$ , and a set $G$ is read in $\Gamma_N$ as $G\cap S_N$ . Quantities of $\Gamma_N$ are lifted to functions of $N$ and of states of $S$ with the value $0$ where they are undefined ( $N<N_0$ or a state outside $S_N$ ). For fixed states this affects finitely many $N$ , and all statements are limits, $\liminf$ s or eventual equalities. All convergence is in $[0,\infty]$ . The conformity predicate includes the standing assumption that $\Gamma$ is $z$ standard. The positive recurrent class $R$ of a $z$ standard chain is the communicating class of $z$ .

A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class $\{N\}$ excludes $z=0$ , is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce $P_{ij}(N)$ exactly by (C.27).

A complete development needs first passage decompositions for countable chains, the renewal-reward identity $J_R=c_{zz}/m_{zz}$ , and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.

Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, Sections C.4–C.5. https://doi.org/10.1002/9780470317037
L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997) 114–137 (cited in the book as Sennott 1997a).
L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR Mathematical Methods of Operations Research 45 (1997) 45–62 (cited in the book as Sennott 1997b).
D. Gibson and E. Seneta, "Augmented truncations of infinite stochastic matrices", Journal of Applied Probability (1987).

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior VI: Splitting Sets and the Decomposition Partition of a GameTextbook

Motivation

Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the $n$ -person game becomes unmanageable as $n$ grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.

The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition $\Pi_\Gamma$ ; and every splitting set is a union of blocks of $\Pi_\Gamma$ . The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.

Setting

Let $I$ be a finite set of players. A characteristic function is a real number $v(S)$ for every subset $S \subseteq I$ (every coalition, including the empty set $\ominus$ and $I$ ). Write $-S = I - S$ . From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying

\text{(42:6:a)}\ v(\ominus) = 0,\qquad \text{(42:6:b)}\ v(S) + v(-S) = v(I),\qquad \text{(42:6:c)}\ v(S) + v(T) \leqq v(S \cup T)\ \text{ if } S \cap T = \ominus .

For $J \subseteq I$ with complement $K = I - J$ , the game is decomposable with respect to $J$ and $K$ if there are constant-sum games $\Delta$ on the players $J$ and $\mathrm H$ on the players $K$ with $v(R) = v_\Delta(R \cap J) + v_{\mathrm H}(R \cap K)$ for all $R \subseteq I$ — formula (41:3). The $J$ -constituent $\Delta$ is the game on $J$ with $v_\Delta(S) = v(S)$ for $S \subseteq J$ (41:4).

A splitting set (43.1) is a $J \subseteq I$ satisfying (41:6),

v(S \cup T) = v(S) + v(T) \quad \text{for } S \subseteq J,\ T \subseteq I - J .

The game is indecomposable if $\ominus$ and $I$ are its only splitting sets (43.3.1). A minimal splitting set is a splitting set $J \neq \ominus$ none of whose proper subsets $J' \neq \ominus$ is splitting (43.3.2), and $\Pi_\Gamma$ is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. $v(S) + \sum_{k \in S} \alpha^0_k = 0$ for all $S$ , for some reals $\alpha^0_k$ (the transformation (42:5)).

Formalization targets

Goal: (43:F), (43:G), (43:H)

For every $v$ satisfying (42:6:a)–(42:6:c):

J_1 \neq J_2 \in \Pi_\Gamma \Rightarrow J_1 \cap J_2 = \ominus, \qquad \bigcup_{J \in \Pi_\Gamma} J = I, \qquad K \text{ splitting} \iff K = J_1 \cup \dots \cup J_p,\ J_i \in \Pi_\Gamma .

The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that $\Pi_\Gamma$ is a partition.

Milestones

In attack order: the criterion (42:G) (decomposability $\iff$ (41:6) $\iff$ (41:7)); the closure properties (43:A) (complements), (43:B) ( $\ominus$ , $I$ ), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ( $K$ splits iff every block of $\Pi_\Gamma$ lies inside or outside $K$ ); and the two extreme cases (43:J) ( $\Pi_\Gamma$ = all singletons iff the game is inessential) and (43:K) ( $\Pi_\Gamma = \{I\}$ iff the game is indecomposable).

Significance

The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of $\Pi_\Gamma$ . The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.

The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.

Difficulty

The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that $J' \cup J''$ is splitting one cannot simply add the identities (41:6) for $J'$ and for $J''$ , since a pair $S \subseteq J' \cup J''$ , $T \subseteq I - (J' \cup J'')$ is not of the form those identities control, and $J' \cap J''$ may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of $J$ (players of the constituent) and subsets of $I$ .

Formalization scope

Players. The set of players $I$ is an arbitrary finite type ι with decidable equality (the book's $I = (1, \dots, n)$ ; in Chapter IX players are also named $1', \dots, k', 1'', \dots, l''$ ). Coalitions are Finset ι, $-S$ and $I - J$ are the complement Sᶜ in $I$ , and $v$ is a function Finset ι → ℝ.
Standing hypotheses. Every theorem assumes (42:6:a)–(42:6:c) (the structure IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). $v(I)$ is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes $I$ nonempty ([Nonempty ι], the book's $n \geqq 1$ ); every other statement holds without it. (43:E) assumes $J \neq \ominus$ , since the book's constituent is a game and has at least one player.
Characteristic functions only. Games are represented by their characteristic functions, as the book does throughout §§42–43 by (42:D). Decomposability quantifies over constant-sum characteristic functions $v_\Delta$ , $v_{\mathrm H}$ on the subtypes ↥J, ↥Jᶜ; the $J$ -constituent is $v$ restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.
Π_Γ. decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives $\ominus$ .
No trivialization. A definition of splitting sets that quantified over $T \subseteq I$ instead of $T \subseteq I - J$ , or complements taken in an ambient type larger than $I$ , would change the theorems; here the complement is in the finite type of players itself. With $I$ empty all statements except (43:K) hold trivially, and (43:K) carries the nonemptiness hypothesis.
Contributions welcome. Proofs of the milestones in the listed order; general Mathlib-style lemmas on Boolean subalgebras of Finset ι and their atoms, which would shorten (43:F)–(43:H).

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (page-for-page reprint of the 3rd edition, 1953), Chapter IX, §§41–43, pp. 339–357. https://doi.org/10.1515/9781400829460
C. Carathéodory, Vorlesungen über reelle Funktionen, Teubner, Leipzig–Berlin, 1918, Chapter V (the measurability criterion to which (41:7) corresponds, cited by the book on p. 343).

16 thms2 active usersReviewed

Graph Theory·Captain: Lucas

Hadwiger's ConjectureOpen Problem

Motivation

Hadwiger's conjecture (1943) asserts that for every integer $t\ge 0$ , every graph with no $K_{t+1}$ minor is $t$ -colourable. It is a far-reaching strengthening of the four-colour theorem, and it is widely described as one of the central open problems of graph theory (Bollobás, Catlin and Erdős called it "one of the deepest unsolved problems in graph theory"). The interest is structural: the four-colour theorem concerns planar graphs, and Hadwiger's conjecture proposes that the only obstruction to $t$ -colourability that matters is the presence of a complete graph $K_{t+1}$ as a minor.

Timeline.

1937 — Wagner shows that the case $t=4$ is equivalent to the four-colour theorem, via a clique-sum decomposition of graphs with no $K_5$ minor.
1943 — Hadwiger poses the conjecture and proves it for $t\le 3$ (graphs with no $K_4$ minor have a vertex of degree at most two).
1964 — Wagner proves that graphs with no $K_{t+1}$ minor are $2^t$ -colourable.
1967 — Mader proves that excluding any fixed minor forces a linear number of edges, and determines the exact extremal function for $K_t$ minors when $t\le 7$ .
1976 — Appel and Haken prove the four-colour theorem, hence the case $t=4$ .
1982 — Duchet and Meyniel prove that every $n$ -vertex graph has a $K_t$ minor with $t\ge n/(2\alpha(G)-1)$ .
1984 — Kostochka and Thomason independently show that graphs with no $K_t$ minor have average degree $O(t\sqrt{\log t})$ , hence are $O(t\sqrt{\log t})$ -colourable.
1993 — Robertson, Seymour and Thomas prove the case $t=5$ (using the four-colour theorem).
2023–2024 — Norin, Postle and Song, then Delcourt and Postle, improve the general bound to $O(t\log\log t)$ colours.
(Date not recorded in the survey) Albar and Gonçalves prove that graphs with no $K_7$ minor are $8$ -colourable and graphs with no $K_8$ minor are $10$ -colourable.

The case $t=6$ (graphs with no $K_7$ minor are $6$ -colourable) is the first open case.

Setting

All graphs are finite and simple. A minor of a graph $G$ is any graph obtained from a subgraph of $G$ by contracting edges. Equivalently, a graph $H$ on vertex set $W$ is a minor of $G$ if there are branch sets $B_w\subseteq V(G)$ , $w\in W$ , which are pairwise disjoint, each inducing a connected (nonempty) subgraph of $G$ , and such that for every edge $w_1w_2$ of $H$ some vertex of $B_{w_1}$ is adjacent to some vertex of $B_{w_2}$ . $G$ has a $K_t$ minor if the complete graph $K_t$ is a minor of $G$ , i.e. $G$ contains $t$ pairwise disjoint connected vertex sets, every two joined by an edge.

A graph is $t$ -colourable if its vertices can be coloured with $t$ colours so that adjacent vertices receive different colours; $\chi(G)$ is the least such $t$ . Write $\mathrm{HC}(t)$ for the statement "every graph with no $K_{t+1}$ minor is $t$ -colourable". A graph is $k$ -degenerate if every nonempty set of vertices contains a vertex with at most $k$ neighbours inside the set. The stability number $\alpha(G)$ is the largest size of a set of pairwise non-adjacent vertices.

Formalization targets

Goal

\forall t\ge 0:\qquad K_{t+1}\not\preceq G\ \Longrightarrow\ \chi(G)\le t\qquad\text{for every finite graph } G.

Proved special cases

\mathrm{HC}(t)\ \text{for } t\le 3,\qquad \mathrm{HC}(4),\qquad \mathrm{HC}(5).

Weaker colouring bounds

no $K_{t+1}$ minor $\Rightarrow$ $\chi(G)\le 2^t$ (Wagner);
no $K_t$ minor $\Rightarrow$ $\chi(G)=O(t\sqrt{\log t})$ (Kostochka, Thomason) and $\chi(G)=O(t\log\log t)$ (Delcourt–Postle);
no $K_7$ minor $\Rightarrow$ $\chi\le 8$ ; no $K_8$ minor $\Rightarrow$ $\chi\le 10$ (Albar–Gonçalves).

Supporting extremal and structural results

non-null graphs with no $K_4$ minor have a vertex of degree $\le 2$ ;
$k$ -degenerate graphs are $(k+1)$ -colourable;
for every $H$ there is $c$ with $|E(G)|\le c|V(G)|$ whenever $H\not\preceq G$ (Mader);
the exact edge bounds $n-1$ , $2n-3$ , $3n-6$ for no $K_3$ , $K_4$ , $K_5$ minor, and $(t-2)n-\binom{t-1}{2}$ for no $K_t$ minor, $t\le 7$ (Mader);
every $n$ -vertex graph has a $K_t$ minor with $t\ge n/(2\alpha(G)-1)$ (Duchet–Meyniel);
a graph with no $K_{t+1}$ minor has a $t$ -colourable induced subgraph on at least half of its vertices.

Significance

A proof of the conjecture would give a structural explanation of the four-colour theorem that does not depend on planarity, and would settle the chromatic number of every minor-closed class defined by excluding a single complete graph. Partial results already drive the theory of graph minors: bounds on the average degree of $K_t$ -minor-free graphs are the standard input to colouring, and linear Hadwiger-type bounds are used in structural and algorithmic graph theory.

On the formal side, only the smallest cases have Lean proofs: the platform already contains proofs of the cases $t\le 2$ under a different encoding of minors (namespace Hadwiger), which may be reused after bridging the definitions. The cases $t\le 3$ , Wagner's $2^t$ bound, the degeneracy lemma, the small extremal bounds and the Duchet–Meyniel theorem have elementary proofs and are realistic targets. The cases $t=4,5$ depend on the four-colour theorem, whose formal proof exists in Coq but not in Lean; formalizing them here requires either porting that proof or proving the reduction to it. The general conjecture is open.

Difficulty

The natural approach — contracting the colour classes of an optimal colouring — does not produce a minor, because colour classes are independent sets and contraction is only allowed along edges. Degeneracy arguments only give bounds of order $t\sqrt{\log t}$ , since dense random graphs with no large clique minor have average degree of that order; closing the gap to $t$ requires using large chromatic number itself, not just density. Already for $t=4$ the statement is equivalent to the four-colour theorem, so no short proof is expected for any $t\ge 4$ .

Formalization scope

Graphs are SimpleGraph V on a finite vertex type V : Type. Minors are encoded by branch sets (IsMinor), complete minors by HasCompleteMinor G t (the complete graph on Fin t is a minor of G), colourability by Mathlib's SimpleGraph.Colorable, and edge counts by the cardinality of the edge set. $\mathrm{HC}(t)$ is the definition HC t. Logarithms are natural logarithms; asymptotic bounds are stated with an explicit existential constant and a ceiling. The case $t=0$ is included; HasCompleteMinor G 0 holds for every graph, so no statement becomes vacuous through a degenerate minor definition.

Useful reusable infrastructure: minor models and their composition, contraction of connected sets, greedy colouring of degenerate graphs, and edge-counting for minor-free graphs. Contributions of intermediate lemmas along the milestones are welcome.

Selected references

P. Seymour, Hadwiger's conjecture, in: Open Problems in Mathematics, Springer, 2016 (survey; source of the milestone numbering).
Wikipedia, Hadwiger conjecture (graph theory). https://en.wikipedia.org/wiki/Hadwiger_conjecture_(graph_theory)
H. Hadwiger, Über eine Klassifikation der Streckenkomplexe, Vierteljschr. Naturforsch. Ges. Zürich 88 (1943).
K. Wagner, Über eine Eigenschaft der ebenen Komplexe, Math. Ann. 114 (1937).
N. Robertson, P. Seymour, R. Thomas, Hadwiger's conjecture for $K_6$ -free graphs, Combinatorica 13 (1993).
A. Kostochka, Lower bound of the Hadwiger number of graphs by their average degree, Combinatorica 4 (1984).
A. Thomason, An extremal function for contractions of graphs, Math. Proc. Cambridge Philos. Soc. 95 (1984).
M. Delcourt, L. Postle, Reducing linear Hadwiger's conjecture to coloring small graphs (2024).

16 thms2 active usersReviewed

Completed

Convex Optimization Information Theory Linear algebra+2·Captain: naimengye

Decoding by Linear Programming: Exact Recovery by ℓ1 Minimization under the Restricted Isometry ConditionResearch Paper

Motivation

Consider the classical error-correcting problem. An input vector $f \in \mathbb{R}^n$ (the plaintext) is encoded as $Af \in \mathbb{R}^m$ by a coding matrix $A$ with $m > n$ , and an unknown, arbitrary vector of errors $e$ corrupts the result, so that only $y = Af + e$ is observed. Can $f$ be recovered exactly, and by an algorithm whose running time is polynomial in $m$ ? Candès and Tao (2005) answer both questions at once: if a matrix $F$ annihilating $A$ satisfies a restricted orthonormality condition, then $f$ is the unique solution of the convex program $\min_g \|y - Ag\|_{\ell^1}$ , which is a linear program, whenever at most $S$ entries of $y$ are corrupted, whatever their positions and values. Read for the matrix $F$ alone, the same theorem says that $\ell^1$ minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.

Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of $\ell^0$ and $\ell^1$ minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order $\sqrt{m}$ , through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order $m/\log m$ . Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction $\rho m$ of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, $\delta_S + \theta_{S,S} + \theta_{S,2S} < 1$ , valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition $\delta_{2S} < \sqrt{2} - 1$ , sharpened the sufficient condition; those later results are not part of this mission.

Setting

Let $F$ be a real $p \times m$ matrix with columns $v_1, \dots, v_m \in \mathbb{R}^p$ , and let $H$ be the linear span of these columns. For an index set $T \subseteq \{1,\dots,m\}$ and real coefficients $c = (c_j)_{j \in T}$ , write $F_T c = \sum_{j \in T} c_j v_j$ . A vector $c \in \mathbb{R}^m$ is supported on $T$ when $c_j = 0$ for all $j \notin T$ ; with this convention $F_T c$ is just the product $Fc$ . Norms are the Euclidean norm $\|c\| = (\sum_j c_j^2)^{1/2}$ and the $\ell^1$ norm $\|c\|_{\ell^1} = \sum_j |c_j|$ .

Definition 1.1. For an integer $S$ , the $S$ -restricted isometry constant $\delta_S$ is the smallest quantity such that

(1 - \delta_S)\|c\|^2 \le \|F_T c\|^2 \le (1 + \delta_S)\|c\|^2

for all $T$ of cardinality at most $S$ and all real coefficients $(c_j)_{j \in T}$ . The $S, S'$ -restricted orthogonality constant $\theta_{S,S'}$ is the smallest quantity such that

|\langle F_T c, F_{T'} c' \rangle| \le \theta_{S,S'} \, \|c\| \, \|c'\|

for all disjoint $T, T'$ with $|T| \le S$ and $|T'| \le S'$ . The paper writes $\theta_S$ for $\theta_{S,S}$ . These numbers measure how far the columns of $F$ are from an orthonormal system when only linear combinations of at most $S$ columns are considered.

The two optimization problems are

(P_1)\quad \min_{d \in \mathbb{R}^m} \|d\|_{\ell^1} \ \text{ subject to } \ Fd = f, \qquad\qquad (P_1')\quad \min_{g \in \mathbb{R}^n} \|y - Ag\|_{\ell^1}.

A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.

Formalization targets

Goal: Theorem 1.5 (decoding by linear programming)

Let $A$ be a real $m \times n$ matrix of full rank with $m > n$ , and $F$ a real $p \times m$ matrix with $FA = 0$ . Let $S \ge 1$ satisfy

\delta_S(F) + \theta_{S,S}(F) + \theta_{S,2S}(F) < 1 . \tag{1.10}

If $y = Af + e$ where $e$ is supported on a set of size at most $S$ , then $f$ is the unique minimizer of $(P_1')$ .

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)

Let $S \ge 1$ satisfy (1.10) for $F$ , and let $c$ be supported on a set $T$ with $|T| \le S$ . Then $c$ is the unique minimizer of $(P_1)$ with $f := Fc$ .

Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the $\delta$ numbers control the $\theta$ numbers), Lemma 1.3 (uniqueness of sparse representations under $\delta_{2S} < 1$ ), and the two dual sparse reconstruction properties, Lemma 2.1 ( $\ell^2$ version) and Lemma 2.2 ( $\ell^\infty$ version).

Significance

The result. The guarantee is deterministic and uniform: one condition on $F$ , checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of $S/m$ , and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.

Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of $\delta_S$ and $\theta_{S,S'}$ exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.

Difficulty

The whole proof rests on a dual certificate: a vector $w \in H$ with $\langle w, v_j \rangle = \operatorname{sgn}(c_j)$ for $j \in T$ and $|\langle w, v_j \rangle| < 1$ for $j \notin T$ . Given such a $w$ , the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is $w = F_T (F_T^* F_T)^{-1} \operatorname{sgn}(c)$ ; this interpolates the signs on $T$ and, by restricted orthogonality, its inner products off $T$ are small in an $\ell^2$ sense, but not in the $\ell^\infty$ sense required. That is exactly Lemma 2.1: the $\ell^\infty$ bound holds only outside an exceptional set of at most $S'$ indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on $T$ fixed, and summing a geometrically convergent series.

Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to $2S$ ( $T_0 \cup T_n$ ) at each step, while the per-step factors it quotes, $\theta_{S,2S}/(1-\delta_S)$ , are what Lemma 2.1 gives for a set of size $S$ ; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with $\theta_S$ in its $\ell^2$ bound on the exceptional set, while the inequality (2.3) its proof establishes gives $\theta_{S,S'}$ ; the mission states the lemma with $\theta_{S,S'}$ , which coincides with the printed form in the case $S' = S$ used by Lemma 2.2.

Formalization scope

Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on $T$ is a vector in Fin m → ℝ supported on the finite set $T$ , and $F_T c$ is F.mulVec c. The Euclidean and $\ell^1$ norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. $H$ is the span of the columns.

The constants $\delta_S$ and $\theta_{S,S'}$ are the infimum of the set of nonnegative $\delta$ (resp. $\theta$ ) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as $S = 0$ . The definitions are total in $S, S'$ , and each theorem carries the paper's domain conditions ( $S \ge 1$ , and $2S \le m$ , $3S \le m$ or $S + S' \le m$ as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has $\delta_S = \theta_{S,S'} = 0$ , so none of the statements is vacuous.

"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the $m \times n$ matrix $A$ with $m > n$ is injectivity of $g \mapsto Ag$ ; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant $K > 0$ depending only on $\delta_S$ " is a positive function of the real number $\delta_S$ , quantified before all other data.

Out of scope, with the reason for each: Theorem 1.6 refers to a threshold $r^*(p,m)$ "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for $m$ and $p$ "large enough", with an unspecified threshold and an $o(1)$ term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant $C$ and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.

Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix $F_T^* F_T$ and its inverse under $\delta_S < 1$ , and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to $\delta_{2S} < \sqrt{2} - 1$ ) belong to a separate mission.

Selected references

E. J. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51 (12), 2005, 4203–4215. https://doi.org/10.1109/TIT.2005.858979 (arXiv: https://arxiv.org/abs/math/0502327)
E. J. Candès, J. Romberg and T. Tao, Robust uncertainty principles: exact signal reconstruction from highly incomplete frequency information, IEEE Trans. Inform. Theory 52 (2), 2006. https://arxiv.org/abs/math/0409186
E. J. Candès and T. Tao, Near optimal signal recovery from random projections: universal encoding strategies?, IEEE Trans. Inform. Theory 52 (12), 2006. https://arxiv.org/abs/math/0410542
D. L. Donoho and X. Huo, Uncertainty principles and ideal atomic decomposition, IEEE Trans. Inform. Theory 47, 2001, 2845–2862. https://doi.org/10.1109/18.959265
S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20, 1999, 33–61. https://doi.org/10.1137/S1064827596304010
E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Acad. Sci. Paris, Ser. I 346, 2008, 589–592. https://doi.org/10.1016/j.crma.2008.03.014

9 thms2 active usersReviewed

Number Theory·Captain: Lucas

Chebotarëv's Density Theorem (Stevenhagen–Lenstra 1996)Research Paper

Motivation

Given a monic polynomial $f$ with integer coefficients, one can reduce it modulo each prime $p$ and factor it over the finite field $\mathbb F_p$ . The way $f$ factors changes with $p$ , and the question of how often each factorization pattern occurs has a precise answer: Chebotarëv's density theorem (1922). It is the common generalization of Dirichlet's theorem on primes in arithmetic progressions (1837) and a theorem of Frobenius (1880, published 1896), and it underlies a large part of algebraic number theory, for example the fact that a Galois extension of a number field is determined by the set of primes that split completely in it. This mission follows the elementary exposition of P. Stevenhagen and H. W. Lenstra, Jr. (Math. Intelligencer 18 (1996)), which states all three theorems over $\mathbb Q$ with a minimum of terminology.

Timeline.

1837 — Dirichlet: primes are equidistributed (in analytic density) over the invertible residue classes modulo $m$ .
1880/1896 — Frobenius: the density of primes with a given decomposition type of $f$ modulo $p$ equals the proportion of Galois group elements with that cycle pattern; he conjectures the sharper statement for conjugacy classes.
1896 — de la Vallée-Poussin: Dirichlet's theorem for natural density.
1922/1925 — Chebotarëv proves Frobenius's conjecture, without class field theory.
1935 — Deuring's proof via Artin reciprocity, now the textbook route.

Setting

Let $f\in\mathbb Z[X]$ be monic of degree $n$ with nonzero discriminant $\Delta(f)$ , so that $f$ has $n$ distinct complex zeros $\alpha_1,\dots,\alpha_n$ . Let $K=\mathbb Q(\alpha_1,\dots,\alpha_n)$ be its splitting field and $G=\mathrm{Gal}(K/\mathbb Q)$ its Galois group. Every $\sigma\in G$ permutes the zeros; the lengths of the cycles (including cycles of length 1) form the cycle pattern of $\sigma$ , a partition of $n$ .

For a prime $p\nmid\Delta(f)$ , the degrees of the irreducible factors of $f \bmod p$ over $\mathbb F_p$ form the decomposition type of $f$ modulo $p$ , again a partition of $n$ .

A Frobenius substitution of $p$ is an element $\sigma\in G$ such that, for some prime ideal $\mathfrak Q$ of the ring of integers $\mathcal O_K$ lying over $p$ ,

\sigma(x)\equiv x^p \pmod{\mathfrak Q}\qquad\text{for all }x\in\mathcal O_K .

For $p\nmid\Delta(f)$ these elements form a single conjugacy class of $G$ , written $\sigma_p$ .

A set $S$ of primes has (analytic, or Dirichlet) density $\delta$ if

\frac{\sum_{p\in S}p^{-s}}{\log\frac{1}{s-1}}\longrightarrow\delta\qquad(s\downarrow 1),

and natural density $\delta$ if $\#\{p\le x:p\in S\}/\#\{p\le x\}\to\delta$ as $x\to\infty$ .

Formalization targets

Goal: Chebotarëv's density theorem

For every conjugacy class $C$ of $G$ ,

\text{the set }\{p \text{ prime}: p\nmid\Delta(f),\ \sigma_p\in C\}\text{ has analytic density }\frac{\#C}{\#G}.

Milestones

Theorem of Dirichlet: for $m\ge1$ and $\gcd(a,m)=1$ , the primes $p\equiv a \pmod m$ have density $1/\varphi(m)$ .
A set of primes with natural density $\delta$ has analytic density $\delta$ .
Galois theory of finite fields: for a squarefree $g\in\mathbb F_p[X]$ , the cycle pattern of $x\mapsto x^p$ on the zeros of $g$ equals the decomposition type of $g$ .
For $p\nmid\Delta(f)$ , the Frobenius substitutions of $p$ form exactly one conjugacy class of $G$ .
For $p\nmid\Delta(f)$ , the cycle pattern of $\sigma_p$ equals the decomposition type of $f$ modulo $p$ .
For $f=X^m-1$ and $p\nmid m$ , $\sigma_p(\zeta)=\zeta^p$ for every primitive $m$ -th root of unity $\zeta$ ; that is, $\sigma_p$ corresponds to $p \bmod m$ under $G\cong(\mathbb Z/m\mathbb Z)^\times$ .
Theorem of Frobenius: the primes $p\nmid\Delta(f)$ for which $f$ has a given decomposition type $t$ have density $\#\{\sigma\in G:\text{cycle pattern }t\}/\#G$ .

Significance

Chebotarëv's theorem shows that every conjugacy class of the Galois group occurs as a Frobenius class for infinitely many primes, with a predictable frequency. Its standard consequences include: the Frobenius elements are equidistributed; a Galois extension is determined by its completely split primes; if $f$ has a zero modulo almost every prime then $f$ is linear or reducible; prime ideals are equidistributed over ideal classes. The theorem is the first step in many arguments in arithmetic geometry (e.g. Serre's work on $\ell$ -adic representations).

The theorem is classical and proved; this mission is about formalizing it. Mathlib contains Frobenius elements in Galois extensions of Dedekind domains and Dirichlet's theorem in the form "infinitely many primes in each coprime residue class", but, to our knowledge, neither the density form of Dirichlet's theorem nor Frobenius's or Chebotarëv's density theorem.

Difficulty

The Galois-theoretic parts (milestones 3–6) are standard but require connecting Frobenius elements in $\mathcal O_K$ with factorization of $f$ modulo $p$ , including the fact that $p\nmid\Delta(f)$ forces $p$ to be unramified in $K$ . The analytic core is harder: one needs Dedekind zeta functions and $L$ -functions of number fields and their behaviour at $s=1$ . The reduction of the general case to the cyclotomic case (Chebotarëv's "crossing" with cyclotomic extensions) needs the density statement over an arbitrary number field as base, not only over $\mathbb Q$ ; in particular, the statement over $\mathbb Q$ alone cannot be proved by induction on itself.

Formalization scope

All declarations live in the namespace ChebotarevDensity and share one definition file.

$K$ is Mathlib's SplittingField of $f$ viewed in $\mathbb Q[X]$ ; $G$ is Polynomial.Gal; $\Delta(f)$ is Mathlib's Polynomial.discr.
A Frobenius substitution is expressed with Mathlib's IsArithFrobAt at some prime ideal of $\mathcal O_K$ containing $p$ ; " $\sigma_p\in C$ " means that some Frobenius substitution of $p$ lies in $C$ (for $p\nmid\Delta(f)$ this is equivalent to all of them lying in $C$ , by milestone 4).
The cycle pattern is Equiv.Perm.partition of the permutation induced on the complex zeros of $f$ ; it includes fixed points.
The decomposition type is the multiset of degrees of the normalized (monic) irreducible factors of $f \bmod p$ .
Analytic density uses $\sum' p^{-s}$ over the primes of $S$ and the limit $s\to1^+$ within $(1,\infty)$ ; natural density compares prime counts up to $x\in\mathbb N$ .
The hypotheses $\Delta(f)\neq0$ and " $f$ monic" are those of the source; the theorems are not vacuous, since e.g. $f=X^m-1$ satisfies them.

Welcome contributions: Dedekind zeta functions and Hecke $L$ -functions at $s=1$ , the density form of Dirichlet's theorem, unramifiedness of primes not dividing the discriminant, and the general number-field version of the theorem.

Selected references

P. Stevenhagen, H. W. Lenstra, Jr., Chebotarëv and his density theorem, Math. Intelligencer 18 (1996), no. 2, 26–37. doi:10.1007/BF03027290
N. Tschebotareff, Die Bestimmung der Dichtigkeit einer Menge von Primzahlen, welche zu einer gegebenen Substitutionsklasse gehören, Math. Ann. 95 (1925), 191–228. doi:10.1007/BF01206606
S. Lang, Algebraic Number Theory, Addison-Wesley, 1970, Chap. VIII.
J. Neukirch, Class Field Theory, Springer, 1986, Chap. V.
Chebotarev density theorem, Wikipedia. link

16 thms2 active usersReviewed

Algebraic Geometry Number Theory·Captain: Lucas

Lam–Litt conjecture: algebraicity and integrality of solutions to algebraic ODEsOpen Problem

Motivation

A classical way to recognize an algebraic function is through the arithmetic of its Taylor coefficients. Eisenstein's theorem (1852) says that if a power series $f\in\mathbb{Q}[[z]]$ is algebraic over $\mathbb{Q}[z]$ , only finitely many primes occur in the denominators of its coefficients. The converse fails in general: many transcendental power series have integer coefficients. Lam and Litt (arXiv:2501.13175) conjecture that the converse does hold for power series that solve an algebraic differential equation at a non-singular point, and that even a weak control on denominators — primes $p$ may appear, but only after roughly $\omega(p)\gg p$ coefficients — already forces algebraicity.

For linear differential equations, the conjecture is a strengthening of the Grothendieck–Katz $p$ -curvature conjecture, one of the central open problems about algebraic solutions of linear differential equations (arXiv:2501.13175). The bounded-denominator form is Problem 1 on Litt's list of open problems (problemsilike.com/1).

Timeline.

1852 — Eisenstein: algebraic power series over $\mathbb{Q}$ have bounded denominators (implication (1)⇒(2) below).
1970s — Grothendieck and Katz: the $p$ -curvature conjecture for linear differential equations.
2025 — Lam and Litt formulate the conjecture for (possibly non-linear) algebraic differential equations and prove it for many equations and initial conditions of algebro-geometric interest, including Picard–Fuchs equations at initial conditions corresponding to cycle classes, and isomonodromy equations such as Painlevé VI and the Schlesinger system at initial conditions corresponding to Picard–Fuchs equations (arXiv:2501.13175).

Setting

Let $f=\sum_{k\ge0}a_kz^k\in\mathbb{Q}[[z]]$ be a formal power series with rational coefficients and write $f^{(i)}$ for its $i$ -th formal derivative. Let $g\in\mathbb{Q}(z,y_0,\dots,y_{n-1})$ be a rational function in $n+1$ variables. The series $f$ solves the algebraic ODE defined by $g$ if

f^{(n)}(z)=g\bigl(z,f(z),f'(z),\dots,f^{(n-1)}(z)\bigr)

and $g$ is defined at $\bigl(0,f(0),\dots,f^{(n-1)}(0)\bigr)$ . Concretely, $g=p/q$ for polynomials $p,q$ with $q\bigl(0,f(0),\dots,f^{(n-1)}(0)\bigr)\neq0$ and $f^{(n)}\cdot q(z,f,\dots,f^{(n-1)})=p(z,f,\dots,f^{(n-1)})$ .

For $N\in\mathbb{N}$ , $\mathbb{Z}[1/N]\subseteq\mathbb{Q}$ is the subring generated by $1/N$ . For a function $\omega$ from the primes to $\mathbb{Z}$ , the coefficients of $f$ are $\omega$ -integral if for every prime $p$ the numbers $a_0,\dots,a_{\omega(p)}$ lie in $\mathbb{Z}_{(p)}$ (denominators prime to $p$ ); $\omega$ is superlinear if $\omega(p)/p\to\infty$ .

Formalization targets

Goal: the Lam–Litt conjecture

For $f$ solving an algebraic ODE as above, the following are equivalent:

\text{(1) } f \text{ is algebraic over } \mathbb{Q}[z];\qquad \text{(2) } \exists N,\ \forall k,\ a_k\in\mathbb{Z}[1/N];\qquad \text{(3) } \exists\,\omega \text{ superlinear with } (a_k) \ \omega\text{-integral}.

Milestones

(1)⇒(2), Eisenstein's theorem (no ODE hypothesis needed).
(2)⇒(3), elementary (no ODE hypothesis needed).
(3)⇒(2), open.
(2)⇒(1), open; Litt's Problem 1.

Together the four milestones imply the goal; the last two are the open content of the conjecture.

Significance

A proof would give an arithmetic criterion for algebraicity of solutions of arbitrary algebraic differential equations, and, for linear equations, would imply the Grothendieck–Katz $p$ -curvature conjecture (arXiv:2501.13175). Lam and Litt draw algebro-geometric consequences from the cases they prove.

For formalization: the conjecture is open, so the goal and the two open milestones are research targets. Eisenstein's theorem is a classical result; formalizing it is concrete, self-contained work. The implication (2)⇒(3) is elementary. The cases proved by Lam and Litt are candidates for further milestones.

Difficulty

Integrality of coefficients alone does not detect algebraicity: there are transcendental power series with integer coefficients that satisfy linear differential equations, such as $\sum_k\binom{2k}{k}^2z^k$ . Its equation is singular at $z=0$ , which the non-singularity hypothesis on $g$ excludes; the conjecture asserts that at non-singular points such examples cannot occur. Even for linear equations the statement contains the Grothendieck–Katz conjecture, which is open in general.

Formalization scope

Power series are PowerSeries ℚ with the formal derivative; rational functions are the fraction field of MvPolynomial (Fin (n + 1)) ℚ, where variable 0 is $z$ and variable i + 1 is $f^{(i)}$ .
The ODE hypothesis is existential: some representation $g=p/q$ with $q$ nonzero at the initial point and $f^{(n)}q(\dots)=p(\dots)$ as power series. This non-singularity requirement is essential and must not be dropped.
Algebraicity is IsAlgebraic (Polynomial ℚ) f, i.e. over $\mathbb{Q}[z]$ (equivalently over $\mathbb{Q}(z)$ ).
$\mathbb{Z}[1/N]$ is the subalgebra of $\mathbb{Q}$ generated by $1/N$ ; since $1/0=0$ in Lean, $N=0$ gives $\mathbb{Z}$ .
$\omega$ takes values in $\mathbb{Z}$ ; negative values impose no condition at that prime. Superlinearity is the limit $\omega(p)/p\to\infty$ along the primes.
The goal is a List.TFAE of the three conditions.

Useful infrastructure: formal derivatives and substitution for power series, algebraic power series and their coefficient arithmetic (Eisenstein), and $p$ -adic valuations of coefficients. Formalizations of Eisenstein's theorem and of the special cases proved by Lam and Litt are welcome.

Selected references

Y. H. J. Lam, D. Litt, Algebraicity and integrality of solutions to differential equations, arXiv preprint, 2025. https://arxiv.org/abs/2501.13175
D. Litt, Problem 1, problems list. https://www.problemsilike.com/1
G. Eisenstein, Über eine allgemeine Eigenschaft der Reihen-Entwicklungen aller algebraischen Funktionen, Bericht der Königl. Preuss. Akademie der Wissenschaften zu Berlin, 1852.
Formal Conjectures project, FormalConjectures/LittProblems/1.lean. https://github.com/google-deepmind/formal-conjectures

6 thms2 active usersReviewed

Completed

Dynamic Programming Dynamical Systems Optimization·Captain: Lucas

Lindgren 2022: Dynamic-Programming Price Adjustment and Lyapunov StabilityResearch Paper

Motivation

In a Walrasian pure exchange economy, agents trade a fixed stock of $l$ commodities, and a price vector $p\in\mathbb R^l$ is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), $dp_i/ds = c_i Z_i(p)$ , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).

Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.

Setting

There are $l$ commodities and $n$ agents. Prices are vectors $p=(p_1,\dots,p_l)\in\mathbb R^l$ , and the paper's implicit summation $x^iy_i=\sum_{i=1}^l x_iy_i$ is written $\langle x,y\rangle$ . Agent $j$ has an expenditure function $e_j(p)$ (minimal cost of reaching a fixed utility level), and the market weighs agents with constants $\lambda_j>0$ ; the aggregate expenditure is

E(p)=\lambda^je_j(p)=\sum_{j=1}^n\lambda_je_j(p).

The economy controls the price velocity $v=dp/ds$ and minimizes the cost functional (eq. (7))

\int_t^T\Big(\tfrac12 m\langle v,v\rangle+E(p)\Big)\,ds,\qquad m>0,

whose value function is $J(t,p)$ . The Hamiltonian (eq. (8)) is

H(v)=\tfrac12 m\langle v,v\rangle+E(p)+\langle\nabla J,v\rangle ,

the optimal policy (eq. (9)) is $v=-\tfrac1m\nabla J$ , and the HJB equation (eq. (10)) reads

\frac{\partial J}{\partial t}=\frac1{2m}\langle\nabla J,\nabla J\rangle-E(p).

Here $\nabla$ always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent $j$ with $h^j=\nabla e_j$ . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: $\partial J/\partial s=-\frac1{2m}\langle\nabla J,\nabla J\rangle+E(p)$ .

Formalization targets

Goal — Lyapunov stability condition (Section 3)

If $J$ is $C^1$ and solves the time-reversed HJB equation, and the price path follows the optimal policy $\dot p(s)=v(s)=-\frac1m\nabla J(s,p(s))$ , then on any interval $[t,T]$ on which

E(p(s))<\tfrac32\,m\,\langle v(s),v(s)\rangle,

the function $s\mapsto J(s,p(s))$ is strictly decreasing; if moreover $J(T,p(T))=0$ , it is strictly positive on $[t,T)$ .

Milestones

Eq. (4): under the normalization $\langle p,p\rangle=1$ , $\langle p,\dot p\rangle=0$ .
Eq. (9): for $m>0$ , $v$ minimizes $H$ if and only if $mv=-\nabla J$ .
Eq. (10): the HJB equation $-\partial_tJ=\min_vH$ takes the explicit form above.
Eq. (12): for a $C^2$ solution of (10), $v=-\frac1m\nabla J$ satisfies

m\frac{\partial v_i}{\partial t}+\tfrac12 m\,\nabla_i\langle v,v\rangle=\nabla_iE .

Eq. (14): with Shephard's lemma, the right-hand side becomes $\sum_j\lambda_jh^j_i$ .
Eq. (19): along the optimal path, $\dfrac{dJ}{ds}=E(p)-\tfrac32 m\langle v,v\rangle$ .

Significance

The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of $J$ left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a $C^2$ value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.

Difficulty

Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on $\mathbb R\times\mathbb R^l$ , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on $J$ rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.

Formalization scope

All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption $m>0$ is kept; positivity of $\lambda_j$ and $e_j$ is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. $l=1$ , $J=ap^2+cs$ , $E=2a^2p^2/m+c$ with small $c>0$ on a bounded interval), so the goal is not vacuous.

Selected references

J. Lindgren, General Equilibrium with Price Adjustments — A Dynamic Programming Approach, Analytics 1 (2022) 27–34. https://doi.org/10.3390/analytics1010003
S. Smale, Dynamics in General Equilibrium Theory, American Economic Review 66 (1976) 288–294. https://www.jstor.org/stable/1817235
H. Scarf, Some Examples of Global Instability of the Competitive Equilibrium, International Economic Review 1 (1960) 157–172.
A. Mas-Colell, M. Whinston, J. Green, Microeconomic Theory, Oxford University Press, 1995.
V. Bala, M. Majumdar, Chaotic Tatonnement, Economic Theory 2 (1992) 437–445. https://www.jstor.org/stable/25054664

8 thms2 active usersReviewed

Algebra Analysis·Captain: Lucas

Smale's Mean Value ConjectureOpen Problem

Motivation

The mean value problem, also called Smale's mean value conjecture, was posed by Stephen Smale in 1981 in his study of the complexity of root-finding algorithms for polynomials (Smale 1981). For a real differentiable function the mean value theorem produces, between two points, a point where the derivative equals a difference quotient. For a complex polynomial no such point need exist on a segment, and Smale asked for a substitute in which the special point is a critical point of the polynomial (a zero of its derivative). Estimates of this kind control how far Newton-type iterations can move, which is where Smale's original interest came from. The problem appears in lists of unsolved problems in mathematics, including Smale's own list of problems for the next century.

Timeline

1981 — Smale poses the problem and proves the inequality below with constant $K = 4$ (Smale 1981). The example $P(z) = z^d - dz$ shows that the constant cannot be smaller than $\frac{d-1}{d}$ in degree $d$ , so no constant below $1$ works in all degrees.
1989 — Tischler proves the inequality with the optimal constant $K = \frac{d-1}{d}$ when all roots of $P$ are real, and when all roots of $P$ have the same absolute value (Tischler 1989).
2007 — Conte, Fujikawa and Lakic prove $K \le 4\frac{d-1}{d+1}$ (Conte–Fujikawa–Lakic 2007). Crane proves $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$ (Crane 2007).
2009 — Dubinin and Sugawa prove the reverse (dual) inequality with constant $\frac{1}{d\,4^d}$ (Dubinin–Sugawa 2009); optimizing this lower bound is the dual mean value problem (Ng–Zhang 2016).

No absolute constant $K < 4$ is known that works in every degree.

Setting

Let $P$ be a polynomial with complex coefficients of degree $d \ge 2$ , and write $P'$ for its derivative. A critical point of $P$ is a complex number $c$ with $P'(c) = 0$ ; since $d \ge 2$ , $P'$ is a nonconstant polynomial of degree $d-1$ , so $P$ has at least one and at most $d-1$ distinct critical points. Fix a complex number $z$ that is not a critical point, $P'(z) \ne 0$ . For every critical point $c$ we then have $c \ne z$ , and the difference quotient

\frac{P(z) - P(c)}{z - c}

is well defined. The question is how small this quotient can be made, relative to $|P'(z)|$ , by choosing the critical point $c$ well.

Formalization targets

Goal: Smale's mean value conjecture ( $K = 1$ )

For every complex polynomial $P$ of degree $d \ge 2$ and every $z \in \mathbb C$ with $P'(z) \ne 0$ there is a critical point $c$ of $P$ with

\left| \frac{P(z) - P(c)}{z - c} \right| \le |P'(z)|.

Stronger: the optimal constant

The same with $|P'(z)|$ replaced by $\frac{d-1}{d}\,|P'(z)|$ ; the example $z^d - dz$ shows this constant cannot be lowered.

Known results (milestones)

Smale's inequality with $K = 4$ .
The extremal example $P(z) = z^d - dz$ at $z = 0$ , where every critical point gives exactly $\frac{d-1}{d}|P'(0)|$ , and its consequence that no constant $K < 1$ works in all degrees.
Tischler's optimal inequality for polynomials with only real roots, and for polynomials whose roots all have the same absolute value.
The Conte–Fujikawa–Lakic bound $K \le 4\frac{d-1}{d+1}$ .
Crane's bound $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$ .
The Dubinin–Sugawa dual inequality $\left|\frac{P(z)-P(c)}{z-c}\right| \ge \frac{|P'(z)|}{d\,4^d}$ for some critical point $c$ .

Significance

The result itself. A positive answer gives a sharp, degree-independent mean value inequality for complex polynomials: for every non-critical point, some critical value is reachable along a chord whose slope is at most the local derivative. Bounds of this type feed into the analysis of Newton's method and of path-following root finders, and into the study of how critical values of a polynomial are distributed relative to its values. The conjecture is part of a family of open extremal problems on the geometry of critical points, alongside Sendov's conjecture.

Formalizing it. The goal and the optimal-constant form are open. The milestones are published theorems, none of which is known to have a machine-checked proof. Formalizing Smale's $K = 4$ bound and Tischler's special cases would put the classical tools of the subject (critical points of polynomials, univalent function estimates, root location) on a formal footing that later attempts can reuse.

Difficulty

The obvious strategies control the quotient through one critical point at a time: for instance, bounding $|P(z) - P(c)|$ by integrating $P'$ along the segment from $c$ to $z$ . Such estimates lose a constant factor that depends on how the critical points are spread out, and the known uniform arguments all pass through distortion theorems for univalent functions, whose constants lead to $K$ close to $4$ . Reaching $K = 1$ requires using all critical points simultaneously, and no argument doing this in every degree is known. The equality case $z^d - dz$ , in which every critical point is equally bad, shows that any successful argument must be sharp for polynomials with maximally symmetric critical configurations.

Formalization scope

Polynomials are elements of ℂ[X] (Mathlib's Polynomial ℂ); the degree is natDegree, the derivative is Polynomial.derivative, evaluation is Polynomial.eval, and the roots of $P$ are the multiset P.roots (counted with multiplicity). A critical point is a c : ℂ with P.derivative.eval c = 0. The absolute value is the norm ‖·‖ on ℂ, and the constants $\frac{d-1}{d}$ and $4\frac{d-1}{d+1}$ are computed in ℝ from the cast of natDegree.

Every statement assumes $P'(z) \ne 0$ . This is the standard normalization and is essential in Lean: division by zero returns $0$ , so without it the choice $c = z$ would make the inequality trivially true whenever $z$ is itself a critical point. With the hypothesis, every critical point $c$ differs from $z$ and the quotient is a genuine difference quotient.

Crane's bound is stated as the existence, for each degree $d \ge 8$ , of a constant strictly below $4 - \frac{2.263}{\sqrt d}$ that works for all polynomials of degree exactly $d$ ; this is equivalent to the best constant in degree $d$ being strictly below that value.

A complete development needs basic facts on critical points of complex polynomials (existence, the Gauss–Lucas theorem), and, for the classical bounds, results from the theory of univalent functions such as the Koebe quarter theorem and coefficient estimates. These are reusable well beyond this mission. Contributions of any milestone, of supporting lemmas, and of partial results in fixed small degree are welcome.

Selected references

S. Smale, The fundamental theorem of algebra and complexity theory, Bull. Amer. Math. Soc. (N.S.) 4 (1981), 1–36. https://doi.org/10.1090/S0273-0979-1981-14858-8
D. Tischler, Critical points and values of complex polynomials, J. Complexity 5 (1989), 438–456. https://doi.org/10.1016/0885-064X(89)90019-8
A. Conte, E. Fujikawa, N. Lakic, Smale's mean value conjecture and the coefficients of univalent functions, Proc. Amer. Math. Soc. 135 (2007), 3295–3300. https://doi.org/10.1090/S0002-9939-07-08861-2
E. Crane, A bound for Smale's mean value conjecture for complex polynomials, Bull. London Math. Soc. 39 (2007), 781–791. https://doi.org/10.1112/blms/bdm063
V. Dubinin, T. Sugawa, Dual mean value problem for complex polynomials, Proc. Japan Acad. Ser. A 85 (2009), 135–137. https://arxiv.org/abs/0906.4605
T.-W. Ng, Y. Zhang, Smale's mean value conjecture for finite Blaschke products, J. Anal. 24 (2016), 331–345. https://arxiv.org/abs/1609.00170
Wikipedia, Mean value problem. https://en.wikipedia.org/w/index.php?title=Mean_value_problem&oldid=1374678764

10 thms2 active usersReviewed

Linear Optimization Numerical Analysis Theoretical Computer Science·Captain: Lucas

Extended Smale's 9th Problem I: no algorithm computes K digits of LP minimisersResearch Paper

Motivation

Linear programming is usually described as "solvable in polynomial time", but that statement is about rational inputs given exactly. In Smale's list of problems for the 21st century (Smale 1998), Problem 9 asks for a polynomial-time algorithm over the reals deciding the feasibility of $Ax \ge y$ , and Smale explicitly calls for "models which process approximate inputs and which permit round-off computations". Real data such as $\sqrt 2$ , entries of a discrete cosine transform, or even $1/3$ in floating point can only be accessed approximately.

Bastounis, Hansen and Vlačić pose the extended Smale's 9th problem: in a model where the algorithm can only query approximations of the input to any requested accuracy, can one compute minimisers of linear programming, basis pursuit and Lasso to $K$ correct digits? Their Main Theorem I (Theorem 3.4) shows that the answer depends on $K$ in a sharp way: for a suitable class of well-conditioned, bounded inputs, no algorithm at all (not only no efficient one) produces $K$ correct digits, while $K-1$ digits are computable (but not in bounded time) and $K-2$ digits are computable in polynomial time.

This mission targets the first, impossibility, half of Theorem 3.4(i) for linear programming.

Setting

Linear program. For $A \in \mathbb R^{m\times N}$ , $y\in\mathbb R^m$ and $c = \mathbf 1_N=(1,\dots,1)$ , the solution set is

\Xi(y,A) = \operatorname*{argmin}_{x\in\mathbb R^N}\ \langle x, c\rangle \quad\text{subject to}\quad Ax = y,\ x\ge 0 .

It is a subset of $M_N = \mathbb R^N$ with the $\ell^p$ norm, $p\in[1,\infty]$ . An input is a pair $\iota = (y,A)$ , and the evaluations of $\iota$ are its coordinates $y_i$ and entries $A_{ij}$ .

Extended model ( $\Delta_1$ -information). Let $D_n = \{k2^{-n} : k\in\mathbb Z\}$ . An oracle representation of $\iota$ is a family $\tilde\iota = (\tilde\iota_{j,n})$ , indexed by evaluations $j$ and accuracies $n = 1,2,\dots$ , with $\tilde\iota_{j,n}\in D_n + iD_n$ and $|\tilde\iota_{j,n} - f_j(\iota)|\le 2^{-n}$ . An algorithm must succeed on every oracle representation of every input.

General algorithm. To make impossibility results independent of the machine model, the paper uses general algorithms (Definition 9.3): a map $\Gamma$ from inputs to $M\cup\{\mathrm{NH}\}$ ( $\mathrm{NH}$ = no output) together with a nonempty set $\Lambda_\Gamma(\iota)$ of evaluations read on $\iota$ . This set is finite whenever $\Gamma$ halts. The output is determined by the values read, and any input that agrees on those values reads the same set. Turing machines and BSS machines with an oracle are special cases; general algorithms can even solve the halting problem.

Error and breakdown epsilon. The error is $\operatorname{dist}(\Gamma(\iota),\Xi(\iota)) = \inf_{\xi\in\Xi(\iota)} d(\Gamma(\iota),\xi)$ , with distance $\infty$ from $\mathrm{NH}$ . The strong breakdown epsilon $\varepsilon_B^s$ is the supremum of all $\varepsilon\ge 0$ such that every general algorithm has error $>\varepsilon$ on some input (Definition 9.17).

Formalization targets

Goal: Theorem 3.4(i), deterministic part, for LP

For every integer $K\ge1$ , all dimensions $4\le m<N$ and every $p\in[1,\infty]$ there is a nonempty class $\Omega_{m,N}$ of inputs $(y,A)$ with nonempty solution sets, $\|y\|_\infty\le 2$ and $\|A\|_{\max}=1$ , such that

\neg\,\exists\,\Gamma\ \text{general algorithm on oracle representations}:\quad \forall\,\tilde\iota,\ \ \operatorname{dist}_{\ell^p}\big(\Gamma(\tilde\iota),\,\Xi(\iota)\big)\le 10^{-K}.

Milestones

Lemma 11.1: the explicit solution sets of the LP inputs $(y_1e_1, A(\alpha,\beta,m,N))$ .
Proposition 10.5 (ii), deterministic part: two input sequences that converge in evaluation to a common input and whose solutions stay $\kappa$ apart force $\varepsilon_B^s\ge\kappa/2$ for a suitable choice of $\Delta_1$ -information.
§9.6, (i) ⇒ (ii): a lower bound on $\varepsilon_B^s$ for one specific $\Delta_1$ -information transfers to the problem with all oracle representations.
Proposition 9.32 (i) (deterministic consequence via Proposition 10.1): $\varepsilon_B^s>10^{-K}$ for LP on a suitable $\Omega_{m,N}$ .

Significance

The theorem shows that for LP with inexact input, being non-computable in Turing's sense does not rule out a finer complexity theory. The paper builds a " $K$ / $K-1$ / $K-2$ digits" classification on this. It also explains why established solvers can return wrong answers with a success flag on small, well-conditioned LPs (§4 of the paper), and it bears on computer-assisted proofs that rely on inexact LP, such as the Flyspeck proof of the Kepler conjecture.

The result is proved on paper. As far as the proposer knows, it has not been machine-checked. This mission formalizes the deterministic impossibility part for LP and puts in place reusable infrastructure: general algorithms, breakdown epsilons and $\Delta_1$ -information. That infrastructure is the base for later missions on the randomised parts of Theorem 3.4(i)–(ii), the weak breakdown epsilon (iii), the exit-flag theorem (Theorem 5.1), and basis pursuit and Lasso.

Difficulty

The obvious objection is that LP is in P for rational inputs, so some rounding scheme ought to work. It fails because an algorithm must halt after reading finitely many approximations. Two inputs that agree to that accuracy but have minimisers far apart then receive the same output. Setting this up needs a notion of algorithm strong enough to cover every computational model, a precise $\Delta_1$ -information model in which the adversary controls the approximations, and explicit LP geometry in which an arbitrarily small perturbation of $A$ moves the minimiser by a fixed amount.

Formalization scope

Inputs are $(y,A)\in(\mathrm{Fin}\,m\to\mathbb R)\times\mathrm{Matrix}(\mathrm{Fin}\,m)(\mathrm{Fin}\,N)\,\mathbb R$ . Evaluations are complex-valued, as in Definition 9.2. Outputs lie in PiLp p (Fin N → ℝ).
A general algorithm is a structure with an output run : Ω → Option M (none = NH) and a read set queried, satisfying the axioms (i)–(iii) of Definition 9.3.
Errors take values in $[0,\infty]$ (ℝ≥0∞), and the error of NH is $\infty$ . The infimum over an empty solution set is $\infty$ . The goal also requires nonempty solution sets, so no junk value enters.
Oracle accuracies are indexed by $n\in\{1,2,\dots\}$ (ℕ+). An oracle input is stored as a pair (input, oracle family), and algorithms can read only the oracle family.
Out of scope: randomised algorithms, the positive statements (iii)–(iv), runtime, and the condition-number bounds $\mathrm{Cond}(AA^*)\le3.2$ , $C_{FP}\le4$ , $\mathrm{Cond}(\Xi)\le179$ .

Selected references

A. Bastounis, A. C. Hansen, V. Vlačić, The extended Smale's 9th problem — On computational barriers and paradoxes in estimation, regularisation, computer-assisted proofs, and learning, preprint (2021).
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20 (1998). https://doi.org/10.1007/BF03025291

8 thms2 active usersReviewed

Completed

Group Theory·Captain: dbenbenn

Monod: groups of piecewise projective homeomorphisms are non-amenable without free subgroupsResearch Paper

This mission formalizes N. Monod, Groups of piecewise projective homeomorphisms, Proceedings of the National Academy of Sciences 110 (2013) 4524–4527, doi:10.1073/pnas.1218426110: the groups $H(A)$ of piecewise projective homeomorphisms of the line are non-amenable and have no free subgroups whenever $A \neq \mathbf{Z}$ .

Motivation

The paper opens with the Banach–Tarski paradox and von Neumann's notion of amenability: "Tarski readily proved that amenability is the only obstruction to paradoxical decompositions. However, the known paradoxes relied more prosaically on the existence of non-abelian free subgroups. Therefore, the main open problem in the subject remained for half a century to find non-amenable groups without free subgroups" (p. 1). That problem, the so-called von Neumann conjecture, was answered by Ol'shanskii around 1980, with Tarski monsters. Monod's groups give "straightforward torsion-free counter-examples", "so simple that many additional properties can be established" (p. 1).

Monod's groups are close relatives of Thompson's groups: Thurston's model identifies Thompson's group $F$ with piecewise $\mathrm{PSL}_2(\mathbf{Z})$ maps of the line with rational breakpoints (p. 2). Whether $F$ is amenable is a notorious open problem, and whether $H(\mathbf{Z})$ is amenable is Monod's Problem 12 (p. 2).

Timeline

1914–1929. Hausdorff's paradox (1914); Banach–Tarski (1924); von Neumann introduces amenable groups (1929); Tarski characterizes amenability by the absence of paradoxical decompositions.
1950s. Day's classes; the question whether every non-amenable group contains a free subgroup of rank two becomes attached to von Neumann's name.
c. 1965–1975. Thompson's groups $F$ , $T$ , $V$ ; Thurston's piecewise projective models of $F$ and $T$ .
1979–1982. Ol'shanskii proves Tarski monsters non-amenable; Adyan does the same for free Burnside groups.
1985. Brin–Squier: groups of piecewise linear homeomorphisms of the line have no free subgroups.
2003. Ol'shanskii–Sapir: finitely presented non-amenable groups without free subgroups.
2013. Monod: the piecewise projective groups $H(A)$ (this paper).
2016. Lodha–Moore: a finitely presented subgroup of Monod's group, non-amenable and without free subgroups.

Setting

The projective line $\mathbf{P}^1$ is OnePoint ℝ, on which $\mathrm{SL}_2(A)$ acts through $\mathrm{GL}_2(\mathbf{R})$ by Möbius transformations (mob, using Mathlib's action on OnePoint). For a subring $A$ of $\mathbf{R}$ (A : Subring ℝ; $\mathbf{Z}$ is ⊥, $\mathbf{R}$ is ⊤), P A is $P_A$ , the set of fixed points of hyperbolic elements (trace of absolute value greater than $2$ ).

A homeomorphism of $\mathbf{P}^1$ is piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $E$ (IsPiecewiseProjOn A E f) when, off some finite subset of $E$ , it agrees near every point with a Möbius transformation from $\mathrm{SL}_2(A)$ . Monod's $G$ (Gpp) is the group generated by the homeomorphisms piecewise in $\mathrm{PSL}_2(\mathbf{R})$ , with breakpoints anywhere, and $H$ (Hpp) is its stabilizer of $\infty$ (fixInf). For a subring $A$ , $G(A)$ (G A) is the subgroup of $G$ generated by its elements that are piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $P_A$ (IsPiecewiseProj A), and $H(A)$ (H A) is its stabilizer of $\infty$ ; $H(\mathbf{Z})$ is H ⊥. GRat is the subgroup of $G$ generated by its elements piecewise in $\mathrm{PSL}_2(\mathbf{Z})$ with breakpoints in $\mathbf{Q} \cup \{\infty\}$ , and HRat its stabilizer of $\infty$ : the rational-breakpoint variants of $G(\mathbf{Z})$ and $H(\mathbf{Z})$ (p. 2).

Amenability is Garrido.IsAmenable (a finitely additive left-invariant probability measure on all subsets), and "no non-abelian free subgroup" is Chou.NoFreeSubgroupOfRankTwo; both are published definitions, in the bundles Garrido_Amenability and Chou_Classes. Co-amenable subgroups (IsCoamenable), inner amenability (IsInnerAmenable) and pointwise stabilizers (fixSubgroup), all on p. 3, are defined in the bundle in the same style.

A relation $R \subseteq X \times X$ is amenable for a measure $\mu$ (IsAmenableRel μ R, p. 2) when it has a left invariant mean in the sense of Connes–Feldman–Weiss: a positive, unital map from bounded measurable functions on $R$ to functions on $X$ , linear up to $\mu$ -null sets and invariant under the partial transformations of $R$ . volP1 is the Lebesgue measure class on $\mathbf{P}^1$ .

Target

The goal is Theorem 1, "The group $H(A)$ is non-amenable if $A \neq \mathbf{Z}$ " (p. 1), introduced as "the main result of this article". The proof (p. 2) passes to a countable dense subring $A'$ of $A$ , compares the orbits of $H(A')$ and $\mathrm{PSL}_2(A')$ on $\mathbf{P}^1 \setminus \{\infty\}$ (Proposition 9), and concludes from two facts about measured equivalence relations: the orbit relation of an amenable group's action is amenable, and, by a theorem of Carrière and Ghys, the orbit relation of $\mathrm{PSL}_2(A')$ on $\mathbf{P}^1$ is not.

The milestones are, in the paper's order: $G(A)$ consists exactly of the elements of $G$ piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $P_A$ ; $H = H(\mathbf{R})$ ; $H$ preserves orientation, is left-orderable and torsion-free; Proposition 9; the countable dense subring; the orbit relation of a measurable action of an amenable group is amenable; the orbit relation of $\mathrm{PSL}_2(A)$ on $\mathbf{P}^1$ is not amenable (Carrière–Ghys, external); Lemma 13 and Theorem 14 leading to Theorem 2 ( $H$ has no free subgroups); Corollary 3; Proposition 6 (bi-orderability); Lemma 16, Proposition 7 (co-amenability of pointwise stabilizers), Proposition 15 and Proposition 5 (inner amenability); and Thurston's identification of the rational-breakpoint variants of $H(\mathbf{Z})$ and $G(\mathbf{Z})$ with $F$ and $T$ .

Significance

The result. Theorem 1 and Theorem 2 together make $H(A)$ , for instance $A = \mathbf{Z}[\sqrt 2]$ , a torsion-free counterexample to the von Neumann conjecture, with finitely generated examples (Corollary 3). The groups are concrete enough to carry many further properties (Propositions 5–7).

Formalizing it. Nothing on amenability of groups of homeomorphisms of the line, or on measured equivalence relations, is in Mathlib. Amenability and Følner's theorem are on this platform from Garrido I, the Banach–Tarski paradox from Garrido II, Brin–Squier's theorem from its own mission, and Thompson's $F$ and $T$ (CannonFloydParry, CannonFloydParry_T) from the Cannon–Floyd–Parry missions.

Difficulty

The algebraic half, Theorem 2 and Propositions 5–9, follows Brin–Squier and elementary dynamics on the circle. The analytic half is the passage through measured equivalence relations in the proof of Theorem 1. The mission defines amenability of a relation as Connes–Feldman–Weiss do, by an invariant mean valued in $L^\infty$ , which is the form under which an amenable group's orbit relation is amenable without extra set-theoretic hypotheses. The step taken from the literature, that the orbit relation of $\mathrm{PSL}_2(A)$ on $\mathbf{P}^1$ is not amenable for $A$ countable and dense, rests on Carrière–Ghys's theorem and on Zimmer's theory of amenable actions (Adams–Elliott–Giordano). The milestone is proved (Monod.not_isAmenableRel_mob) by an elementary route that needs neither: a ping-pong argument in $\mathrm{SL}_2(A)$ that contradicts an invariant mean directly.

What is left out

The second sentence of Proposition 6 (no non-trivial homomorphism from a Kazhdan group) and Proposition 8 (actions on CAT(0) spaces): property (T) and CAT(0) spaces are not in Mathlib.
Proposition 4 ( $L^2$ -Betti numbers), the remarks on group laws, on the Dixmier problem and on bounded cohomology.
Remarks 10 and 11, which discuss alternative proofs of the step taken from Carrière–Ghys.

Formalization scope

$\mathbf{P}^1$ is OnePoint ℝ and $\mathrm{PSL}_2(A)$ acts through Matrix.SpecialLinearGroup (Fin 2) A; since $-1$ acts trivially the orbits are those of $\mathrm{PSL}_2(A)$ .
"Piecewise with finitely many pieces, each an interval" is stated locally: off a finite set of breakpoints, $f$ agrees near each point with one Möbius transformation. Pieces then extend over arcs because two Möbius maps agreeing near a point agree everywhere.
The groups are subgroups of the homeomorphism group of OnePoint ℝ, each defined as the subgroup generated by the maps the paper describes; the milestones state that $G(A)$ is exactly its set of such maps and that $G = G(\mathbf{R})$ .
An amenable measured equivalence relation (p. 2) is one with a left invariant mean in the sense of Connes–Feldman–Weiss (an operator from $L^\infty$ of the relation to $L^\infty(X, \mu)$ , their Definition 6), as in Schmidt, whom the paper cites. The paper describes it as a measurable assignment of means on the orbits, the motivating form in Connes–Feldman–Weiss; for that form, "an amenable group's action produces an amenable relation" is known only assuming CH. $\mathbf{P}^1$ carries its Borel σ-algebra and the Lebesgue measure class (volP1).
"Metabelian" is the vanishing of the second derived subgroup, and "contains a free abelian group of rank two" is an injective homomorphism from $\mathbf{Z}^2$ .
Reused platform items, which solutions may import: the amenability and free-subgroup definitions (Garrido, Chou), Brin–Squier's Theorem 3.1, and Thompson's $F$ and $T$ (Cannon–Floyd–Parry).

Selected references

N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
Y. Carrière, É. Ghys, Relations d'équivalence moyennables sur les groupes de Lie, C. R. Acad. Sci. Paris Sér. I Math. 300 (1985) 677–680 (no DOI).
A. Connes, J. Feldman, B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450. doi:10.1017/S014338570000136X
K. Schmidt, Algebraic ideas in ergodic theory, CBMS Regional Conference Series in Mathematics 76, AMS (1990) (a book; no DOI).
M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985) 485–498. doi:10.1007/BF01388519

25 thms2 active usersReviewed

Completed

Group Theory·Captain: dbenbenn

Is Thompson's group F amenable? (Geoghegan's conjecture)Open Problem

This mission formalizes Geoghegan's conjecture that Thompson's group $F$ is not amenable, in the form stated by Cannon, Floyd and Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996), §4, p. 227 (doi:10.5169/seals-87877), together with the landmark results of the literature on the question.

Motivation

A discrete group is amenable when it carries a finitely additive, translation-invariant probability measure on all of its subsets. Groups containing a non-abelian free subgroup are not amenable, and the question whether every non-amenable group contains one (the von Neumann problem) made Thompson's group $F$ the first natural candidate for a counterexample: it contains no non-abelian free subgroup, and it is not elementary amenable. Geoghegan conjectured in 1979 that $F$ is not amenable; several announced solutions in each direction did not survive. In 2026 OpenAI released a proof that $F$ is not amenable, with a Lean formalization; adapted to this mission's definitions, it is the solution of the goal.

Timeline.

1965: Richard Thompson defines the groups $F$ , $T$ and $V$ (Cannon–Floyd–Parry, p. 215).
1979: Geoghegan conjectures that $F$ contains no non-abelian free subgroup and is not amenable (Cannon–Floyd–Parry, p. 227).
1985: Brin and Squier prove that $F$ contains no non-abelian free subgroup (doi:10.1007/BF01388519).
1996: Cannon, Floyd and Parry prove, using Chou's work on elementary amenable groups, that $F$ is not elementary amenable (Theorem 4.10).
2009–2014: announced proofs of amenability (Shavgulidze, 2009; Moore, 2012) and of non-amenability (Akhmedov, 2009; Beklaryan, 2011; Wajnryb–Witowicz, 2014) are withdrawn by their authors or found to contain serious errors.
2013: Moore proves that if $F$ is amenable, its Følner sets grow at least like a tower of exponentials (doi:10.4171/GGD/201).
2013: Monod introduces the groups $H(A)$ of piecewise-projective homeomorphisms of the line, proves that they have no non-abelian free subgroup and are not amenable for every subring $A \ne \mathbf Z$ of $\mathbf R$ , and asks whether $H(\mathbf Z)$ is amenable (Problem 12) (doi:10.1073/pnas.1218426110).
2015: Juschenko, Matte Bon, Monod and de la Salle introduce extensive amenability of group actions, and prove that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable (Theorem 6.4; arXiv 2015; published 2018, doi:10.1017/etds.2016.32).
2017: Kaimanovich proves that random walks on $F$ with finitely supported, strictly non-degenerate step distributions have non-trivial Poisson boundary (doi:10.1017/9781316576571.013).
2019: Chornyi shows that $F$ is amenable if and only if its action on the dyadic rationals in $(0,1)$ is extensively amenable (arXiv:1907.01440).
2019: Kim, Koberda and Lodha show that large powers of two homeomorphisms of the line with overlapping supports generate a copy of $F$ (doi:10.24033/asens.2397).
2021: Stankov records, from Kim–Koberda–Lodha, that $H(\mathbf Z)$ contains a copy of $F$ , so that amenability of $H(\mathbf Z)$ would imply amenability of $F$ (doi:10.1017/etds.2019.76).
2023: Monod shows that the Thompson group $H_{\mathbf Q}(\mathbf Z) \cong F$ is not co-amenable in the group $H_{\mathbf Q}(\mathbf Q)$ (doi:10.4171/ggd/883).
2023: Guba's survey records that "the famous problem about amenability of $F$ remains open" (doi:10.46298/jgcc.2023.15.1.11315).
2026: OpenAI proves that $F$ is not amenable: a Lipschitz self-map of the Hilbert ball with no approximate fixed point (Benyamini–Sternfeld), composed with a recursive colouring of dyadic partitions that $F$ transports exactly, gives a uniform lower bound on the Følner ratios of $F$ . The proof comes with a Lean formalization (Thompson's group F is nonamenable, September 23, 2026, github.com/openai/math).

Setting

Let UI be the unit interval $[0,1]$ . Thompson's group $F$ (CannonFloydParry.F) is the group, under composition, of the order-preserving homeomorphisms of $[0,1]$ that are piecewise linear with finitely many breakpoints, every breakpoint a dyadic rational $k/2^n$ and every slope a power of $2$ . It is generated by two elements and finitely presented (Cannon–Floyd–Parry, Corollary 2.6 and Theorem 3.4).

A mean on a set $S$ is a function $m$ from the subsets of $S$ to $[0,\infty]$ with $m(\emptyset) = 0$ , $m(A \cup B) = m(A) + m(B)$ for disjoint $A, B$ , and $m(S) = 1$ . A group $G$ is amenable (Garrido.IsAmenable G) when it carries a mean with $m(gA) = m(A)$ for all $g \in G$ and $A \subseteq G$ , where $gA = \{ga : a \in A\}$ . This is equivalent to the definition Cannon, Floyd and Parry give on p. 227, whose means take values in $[0,1]$ .

The milestones use four further notions, defined precisely in the definitions item and in their own statements:

A finite set $A \subseteq G$ is $\varepsilon$ -Følner for a finite $\Gamma \subseteq G$ when $\sum_{\gamma\in\Gamma}|\gamma A \mathbin{\triangle} A| < \varepsilon|A|$ ; by Følner's criterion, $G$ is amenable exactly when it has such sets for every $\varepsilon > 0$ .
A finitely supported probability measure $\mu$ on $G$ drives a random walk; $\mu$ is strictly non-degenerate when its support generates $G$ as a semigroup, and the walk is Liouville when every bounded $\mu$ -harmonic function, $f(g) = \sum_h \mu(h) f(gh)$ , is constant.
An action of $G$ on a set $X$ is extensively amenable when the finite subsets of $X$ carry a $G$ -invariant mean that, for each finite $E_0 \subseteq X$ , gives full weight to the finite sets containing $E_0$ .
For a subring $A$ of $\mathbf R$ , Monod's group $H(A)$ consists of the homeomorphisms of the real line that are piecewise projective, $x \mapsto (ax+b)/(cx+d)$ with $\left(\begin{smallmatrix} a & b \\ c & d \end{smallmatrix}\right) \in \mathrm{SL}_2(A)$ , with finitely many breakpoints, each a fixed point of a hyperbolic element of $\mathrm{SL}_2(A)$ . $H_B(A)$ allows breakpoints in a set $B$ instead; $H_{\mathbf Q}(\mathbf Z)$ is isomorphic to $F$ (Thurston). A subgroup $K$ of $J$ is co-amenable when $J/K$ carries a $J$ -invariant mean.

Formalization targets

Goal: Geoghegan's conjecture

\neg\,\mathrm{IsAmenable}(F).

The question was open until 2026. OpenAI's proof of the conjecture (see the timeline), transferred to CannonFloydParry.F and Garrido.IsAmenable, proves this statement.

Landmarks

The milestones are results from the literature, stated as their sources state them: $F$ has no non-abelian free subgroup (Cannon–Floyd–Parry, Corollary 4.9) and is not elementary amenable (Theorem 4.10), and Følner's criterion, all three already proved and linked as references; Moore's tower lower bound on Følner sets of $F$ ; Kaimanovich's theorem that random walks on $F$ with finitely supported strictly non-degenerate steps are not Liouville; Chornyi's reformulation of amenability of $F$ as extensive amenability of its action on the dyadic rationals; Stankov's embedding of $F$ into Monod's $H(\mathbf Z)$ ; Monod's theorem that $H_{\mathbf Q}(\mathbf Z) \cong F$ is not co-amenable in $H_{\mathbf Q}(\mathbf Q)$ ; and the theorem of Juschenko, Matte Bon, Monod and de la Salle that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable.

A second open statement

Monod's Problem 12 asks whether $H(\mathbf Z)$ is amenable; it is stated as ¬ Garrido.IsAmenable (Monod.H ⊥), where ⊥ is the smallest subring of $\mathbf R$ , namely $\mathbf Z$ ; this is parallel to the goal. Through Stankov's embedding, the proof of the goal proves it. By the theorem of Juschenko, Matte Bon, Monod and de la Salle, it is equivalent to the statement that the action of $H(\mathbf Z)$ on the line is not extensively amenable; that theorem is proved on this platform, through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn), and for the subgroups of $H(\mathbf Z)$ also in a sharper form, with extensive amenability on the set of possible breakpoints only (the breakpoint criterion).

Significance

The result. A proof of the conjecture would make $F$ a finitely presented, torsion-free, non-amenable group with no non-abelian free subgroup, with a concrete description as a group of homeomorphisms of the interval. A disproof would make $F$ an amenable group that is not elementary amenable, and by Moore's theorem one whose Følner sets are at least tower-sized.

Formalizing it. Corollary 4.9 and Theorem 4.10 of Cannon–Floyd–Parry are formalized and proved on this platform and enter as references. Chornyi's corollary is proved here; its "if" direction is proved directly, by establishing the case that Chornyi applies of the Juschenko–Matte Bon–Monod–de la Salle criterion. Moore's theorem is formalized and published together with the lemmas of its proof, and the milestone here has a solution that reduces it to that statement. Kaimanovich's theorem, Stankov's embedding, Monod's 2023 theorem and the theorem of Juschenko, Matte Bon, Monod and de la Salle are proved here as well, the last through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn). The definitions of Følner sets, harmonic functions on groups and extensive amenability are reusable beyond this mission.

Difficulty

The obstructions to amenability that settle the question for most groups are absent here: $F$ has no non-abelian free subgroup, and its elementary structure is well understood. In the other direction, the usual constructions of invariant means fail: by Moore's theorem any Følner set of $F$ is at least tower-sized, so no explicit search can exhibit one, and by Kaimanovich's theorem the finitely supported random walks on $F$ are not Liouville, so the random-walk route to amenability through a trivial Poisson boundary is closed.

Formalization scope

Lean representation and conventions.

$F$ is a subgroup of the order isomorphisms of UI; $H(A)$ and $H_B(A)$ are subgroups of the homeomorphisms of OnePoint ℝ. Groups of maps multiply by composition, $(fg)(x) = f(g(x))$ ; statements from sources that write the product in the other order are restated for this convention, with the equivalence explained in their natural-language statements.
Means take values in $[0,\infty]$ ; total mass $1$ and finite additivity keep every value in $[0,1]$ .
Extensive amenability is stated for an action on $[0,1]$ relative to the set of dyadic rationals in $(0,1)$ ; the statement of Chornyi's corollary includes that $F$ maps this set to itself.
The goal cannot be satisfied vacuously: amenability is a single existential statement about means on $F$ , and $F$ is a fixed, nontrivial, finitely generated group.

What is left out.

The Poisson boundary is not formalized: "Liouville" is Kaimanovich's equivalent reformulation through bounded harmonic functions on $\operatorname{sgr}\mu$ (p. 8).
The "in particular" clause of Moore's Theorem 1.1, on the Følner function, is not stated separately; with Følner's criterion it follows from the stated bound.
The withdrawn and disputed proofs in the timeline are not formalized.

What a development needs. Thompson's group $F$ and its dyadic action (Cannon–Floyd–Parry §4), its tree diagrams and presentations, and amenability, Følner's criterion and the closure properties of amenable groups (Garrido I) are published and proved on this platform, as are Monod's groups and the isomorphism $H_{\mathbf Q}(\mathbf Z) \cong F$ (Monod.contDiff_and_exists_mulEquiv_HRat_F). Mathlib has Følner filters for measurable groups and Schreier graphs of quivers, but no random walks on groups; the proofs of the landmarks here supply what they need, and the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn) is reusable beyond this mission. Reductions of the goal or of Problem 12 to new, sharper statements are welcome, as is a disproof of either.

Selected references

J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996) 215–256. doi:10.5169/seals-87877
M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985) 485–498. doi:10.1007/BF01388519
J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651. doi:10.4171/GGD/201
V. A. Kaimanovich, Thompson's group F is not Liouville, in Groups, Graphs and Random Walks, LMS Lecture Note Ser. 436 (2017) 300–342. doi:10.1017/9781316576571.013
N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
K. Juschenko, N. Matte Bon, N. Monod, M. de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219. doi:10.1017/etds.2016.32
M. Chornyi, Superharmonic functions on the Lamplighter graph of Thompson's group F, preprint (2019). arXiv:1907.01440
V. Guba, Amenability problem for Thompson's group F: state of the art, J. Groups Complex. Cryptol. 15 (2023), no. 1. doi:10.46298/jgcc.2023.15.1.11315
S.-h. Kim, T. Koberda, Y. Lodha, Chain groups of homeomorphisms of the interval, Ann. Sci. Éc. Norm. Supér. (4) 52 (2019) 797–820. doi:10.24033/asens.2397
B. Stankov, Non-triviality of the Poisson boundary of random walks on the group H(ℤ) of Monod, Ergodic Theory Dynam. Systems 41 (2021) 1160–1189. doi:10.1017/etds.2019.76
OpenAI, Thompson's group F is nonamenable, OpenAI Math Release preprint (September 23, 2026). github.com/openai/math
N. Monod, Some comments on piecewise-projective groups of the line, Groups Geom. Dyn. 19 (2025) 459–476. doi:10.4171/ggd/883

56 thms2 active usersReviewed

Differential Geometry Dynamical Systems·Captain: Lucas

Pugh's Closing LemmaResearch Paper

Motivation

A periodic point of a map $f\colon M\to M$ is a point $x$ with $f^n(x)=x$ for some $n\ge 1$ . A nonwandering point is a much weaker form of recurrence: every neighbourhood $U$ of $x$ eventually returns to meet itself, $f^n(U)\cap U\ne\emptyset$ for some $n\ge 1$ . Every periodic point is nonwandering, but a nonwandering point need not be periodic, and the orbit of such a point may never come back to $x$ exactly.

Pugh's closing lemma asserts that this gap can be closed by an arbitrarily small change of the system: if $x$ is nonwandering for a $C^1$ diffeomorphism $f$ of a compact manifold, then some diffeomorphism $g$ , as close to $f$ as desired in the $C^1$ topology, has $x$ as a periodic point (Wikipedia, "Pugh's closing lemma"). The result was proved by C. C. Pugh in 1967 (Pugh 1967), in the same paper as the General Density Theorem: for a $C^1$ -generic diffeomorphism the periodic points are dense in the nonwandering set. The source article describes the lemma as establishing a close relationship between chaotic and periodic behaviour and notes that it underlies some autonomous convergence theorems. The article also points to Smale's problems as related material.

Setting

Let $M$ be a compact smooth manifold of dimension $d$ , Hausdorff and without boundary. Write $\mathrm{Diff}^1(M)$ for the set of $C^1$ diffeomorphisms $g\colon M\to M$ : bijections such that $g$ and $g^{-1}$ are continuously differentiable. For $g\in\mathrm{Diff}^1(M)$ , $Tg\colon TM\to TM$ denotes its tangent map on the tangent bundle.

The $C^1$ topology on $\mathrm{Diff}^1(M)$ is the coarsest topology for which $g\mapsto Tg$ is continuous, where the space $C(TM,TM)$ of continuous self-maps of $TM$ carries the compact-open topology. Two diffeomorphisms are $C^1$ -close when they, and their derivatives, are uniformly close.

For a map $h\colon X\to X$ of a topological space:

$x$ is nonwandering if for every neighbourhood $U$ of $x$ there is $n\ge 1$ with $h^n(U)\cap U\ne\emptyset$ ; the nonwandering set is $\Omega(h)$ ;
$\mathrm{Per}(h)=\{x : \exists\, n\ge 1,\ h^n(x)=x\}$ is the set of periodic points.

Formalization targets

Goal: Pugh's closing lemma

For every $f\in\mathrm{Diff}^1(M)$ and every $x\in\Omega(f)$ ,

\forall\ \mathcal U \text{ a } C^1\text{-neighbourhood of } f,\quad \exists\, g\in\mathcal U,\ \ x\in\mathrm{Per}(g).

Milestones

$\mathrm{Per}(f)\subseteq\Omega(f)$ for any map $f$ .
$\Omega(f)$ is closed for any map $f$ .
$f(\Omega(f))=\Omega(f)$ for a homeomorphism $f$ .
$\Omega(f)\ne\emptyset$ for any map of a nonempty compact space.
General Density Theorem (Pugh 1967): there is a residual set $\mathcal G\subseteq\mathrm{Diff}^1(M)$ with

\overline{\mathrm{Per}(g)}=\Omega(g)\qquad (g\in\mathcal G).

Milestones 1–4 are elementary background facts that are not stated in the source article; milestone 5 is the second theorem named in the title of the source's reference.

Significance

The result. The closing lemma turns a topological recurrence property into periodicity after a $C^1$ -small perturbation. Combined with genericity arguments it gives the General Density Theorem, so that for generic $C^1$ diffeomorphisms the whole nonwandering set is the closure of the periodic orbits. It is one of the basic perturbation tools of $C^1$ generic dynamics.

Formalizing it. The theorem is classical and proved in the literature. The drafter is not aware of a machine-checked proof. A formalization needs the $C^1$ topology on diffeomorphism groups, local perturbation lemmas in charts and the combinatorics of the closing argument. None of these is currently available in Mathlib as far as the drafter knows.

Difficulty

The first idea is to take the returning piece of orbit near $x$ and push it back to $x$ with a small local perturbation. This fails in the $C^1$ topology. Moving a point by distance $\delta$ with a bump supported in a ball of radius $r$ costs $C^1$ size about $\delta/r$ , and the return may happen at a distance comparable to the size of the only available ball. The perturbation then fails to be $C^1$ -small. The derivative $Df^n$ along the return can also distort any fixed neighbourhood shape without bound. Controlling this distortion is the central difficulty.

Formalization scope

$\mathrm{Diff}^1(M)$ and its $C^1$ topology come from the published definition file BCWCentralizer_Basic. $\mathrm{Diff}^1(M)$ is M ≃ₘ^1⟮𝓡 d, 𝓡 d⟯ M, and the topology is induced by $g\mapsto Tg$ into C(TangentBundle, TangentBundle) with the compact-open topology. On a compact manifold this is the usual $C^1$ topology.
"Compact smooth manifold": a Hausdorff compact space with a $C^\infty$ atlas modelled on $\mathbb R^d$ , so without boundary. $d$ is arbitrary.
"Arbitrarily close" means that every neighbourhood of $f$ in the $C^1$ topology contains a suitable $g$ . "Periodic" requires a period $n\ge 1$ . Allowing $n=0$ would make every point periodic and the statement trivial.
The perturbation $g$ is only required to be a $C^1$ diffeomorphism, matching $\mathrm{Diff}^1(M)$ in the source.
The nonwandering notion is the definition item PughClosingLemma_nonwandering, shared by all statements. It is reusable for any topological dynamics mission.

Welcome contributions: a general theory of the $C^1$ topology on $\mathrm{Diff}^1(M)$ (for example, that it is Baire), local perturbation lemmas, and proofs of the milestones.

Selected references

C. C. Pugh, An Improved Closing Lemma and a General Density Theorem, American Journal of Mathematics 89 (4), 1967, 1010–1021. https://doi.org/10.2307/2373414
Wikipedia, Pugh's closing lemma, revision 1304222873. https://en.wikipedia.org/w/index.php?title=Pugh%27s_closing_lemma&oldid=1304222873
V. Araújo, M. J. Pacifico, Three-Dimensional Flows, Springer, 2010, ISBN 978-3-642-11414-4.

8 thms2 active usersReviewed

Dynamical Systems·Captain: Lucas

The C¹-generic diffeomorphism has trivial centralizer (Bonatti–Crovisier–Wilkinson)Research Paper

Motivation

Two commuting diffeomorphisms $f,g$ of a manifold $M$ share all of their dynamics: $g$ permutes the orbits of $f$ and preserves every smooth and topological invariant of $f$ . The centralizer of $f\in\mathrm{Diff}^r(M)$ ,

Z^r(f)=\{g\in\mathrm{Diff}^r(M): fg=gf\},

always contains the cyclic group $\langle f\rangle=\{f^n:n\in\mathbb Z\}$ , and $f$ has trivial centralizer when $Z^r(f)=\langle f\rangle$ . S. Smale asked whether diffeomorphisms with trivial centralizer are dense, residual, or even open and dense in $\mathrm{Diff}^r(M)$ (one of Smale's problems for the 21st century).

Timeline: Kopell (1970) answered the question for $r\ge2$ on the circle; Palis–Yoccoz, Fisher and Burslem obtained results under hyperbolicity or partial hyperbolicity assumptions; Togawa treated generic Axiom A diffeomorphisms in the $C^1$ topology; Bonatti–Crovisier–Vago–Wilkinson showed that trivial-centralizer diffeomorphisms do not contain an open dense set in $\mathrm{Diff}^1(M)$ ; and Bonatti–Crovisier–Wilkinson (this paper, arXiv:0804.1416) proved residuality in $\mathrm{Diff}^1(M)$ for every compact manifold.

Setting

$M$ is a closed (compact, boundaryless), connected smooth manifold of dimension $d$ . $\mathrm{Diff}^1(M)$ is the space of $C^1$ diffeomorphisms of $M$ with the $C^1$ topology; a subset is residual if it contains a countable intersection of open dense sets.

Formalization targets

Goal (Main Theorem, p. 3)

There is a residual subset $\mathcal R\subset\mathrm{Diff}^1(M)$ such that for every $f\in\mathcal R$ and every $g\in\mathrm{Diff}^1(M)$ with $fg=gf$ , one has $g=f^n$ for some $n\in\mathbb Z$ .

Milestones

Following Section 2 of the paper: the classical upper-semicontinuity lemma used for Proposition 2.5, the wandering part of Theorem A (unbounded distortion is $C^1$ -generic), Proposition 2.5 (density of trivial Lipschitz centralizers implies residuality) and Theorem 2.3 (residuality of trivial Lipschitz centralizers when $\dim M\ge2$ ).

Significance

The theorem answers the second (and hence the first) part of Smale's question in the $C^1$ topology, and exhibits a precise link between dynamical properties of $f$ (large derivative and unbounded distortion) and the algebraic structure of $f$ inside the group $\mathrm{Diff}^1(M)$ . The result is proved in the literature; it has not been formalized.

Difficulty

The density of trivial centralizers comes from perturbation results (Theorems A and B) that change the derivative without changing the topological dynamics (tidy perturbations in topological towers). Density alone does not give residuality, since the set of diffeomorphisms with the large derivative property is not residual (Appendix); the passage from dense to residual needs the Lipschitz centralizer and a semicontinuity argument.

Formalization scope

$M$ is a charted space over $\mathbb R^d$ with a $C^\infty$ atlas, Hausdorff, compact and connected; $\mathrm{Diff}^1(M)$ is Mathlib's type of $C^1$ diffeomorphisms. The $C^1$ topology is encoded as the topology induced by $f\mapsto Tf$ into the compact-open topology on continuous self-maps of the tangent bundle $TM$ . Powers $f^n$ , $n\in\mathbb Z$ , are taken in the permutation group of $M$ . Bi-Lipschitz homeomorphisms are defined chart-locally (equivalent on a compact manifold to bi-Lipschitz for a Riemannian distance). Jacobians $|\det Df^n|$ are computed with respect to an arbitrary continuous Riemannian metric; the unbounded-distortion property does not depend on this choice.

Contributions welcome: the $C^1$ topology API (Baire property, continuity of composition), the Kupka–Smale and closing-lemma genericity results, and the perturbation machinery of Sections 3–7.

Selected references

C. Bonatti, S. Crovisier, A. Wilkinson, The $C^1$ generic diffeomorphism has trivial centralizer, Publ. Math. IHÉS 109 (2009); arXiv:0804.1416. https://arxiv.org/abs/0804.1416
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20 (1998).
N. Kopell, Commuting diffeomorphisms, Proc. Sympos. Pure Math. 14 (1970).

7 thms2 active usersReviewed

Discrete Geometry Mathematical Physics·Captain: Lucas

Thomson Problem: Seven Electrons and the Known Exact SolutionsOpen Problem

Motivation

The Thomson problem asks for the configuration of $N$ electrons, constrained to the surface of the unit sphere and repelling each other according to Coulomb's law, that minimises the total electrostatic potential energy. J. J. Thomson posed it in 1904 in connection with his "plum pudding" atomic model. The same energy-minimisation question reappears in the arrangement of protein subunits in spherical virus shells, in colloidosomes, in fullerene patterns and in multi-electron bubbles, and it is a special case ( $s=1$ ) of the Riesz $s$ -energy problem on the sphere; the logarithmic variant is Smale's 7th problem.

Despite its elementary statement, the minimum is rigorously known only for a handful of values of $N$ .

Timeline of exact solutions (as reported in the source).

$N=1,2$ : trivial; for $N=2$ the optimum is an antipodal pair with $U=1/2$ .
$N=3$ : equilateral triangle on a great circle — L. Föppl (1912).
$N=4$ : regular tetrahedron (listed in the source without a citation).
$N=6$ : regular octahedron — V. A. Yudin (1992).
$N=12$ : regular icosahedron — N. N. Andreev (1996).
$N=5$ : triangular bipyramid — R. Schwartz (2013), computer-assisted.
$N=7$ : pentagonal bipyramid — long observed numerically; in September 2026 an exact, Lean-kernel-checked proof was claimed (H. Tran, Vals AI).
$N=8$ and $N=20$ : numerically, the optimum is not the cube, resp. the dodecahedron.

Setting

A configuration of $N$ points is a map $x:\{0,\dots,N-1\}\to\mathbb R^3$ . It is admissible if every point lies on the unit sphere, $\|x_i\|=1$ , and the points are pairwise distinct. In units with $e=1$ and $k_e=1$ its Coulomb energy is

U(x)=\sum_{0\le i<j\le N-1}\frac{1}{\|x_i-x_j\|}.

An admissible $x$ is an energy minimiser (solves the Thomson problem for $N$ ) if $U(x)\le U(y)$ for every admissible $N$ -point configuration $y$ .

Explicit candidate configurations are fixed in the definitions file: the antipodal pair ( $N=2$ ), an equatorial equilateral triangle ( $N=3$ ), the regular tetrahedron ( $N=4$ ), the triangular bipyramid ( $N=5$ ), the regular octahedron ( $N=6$ ), the pentagonal bipyramid ( $N=7$ : the two poles plus a regular pentagon $(\cos\tfrac{2\pi k}5,\sin\tfrac{2\pi k}5,0)$ on the equator) and the regular icosahedron ( $N=12$ ).

Formalization targets

Goal: $N=7$

\text{the pentagonal bipyramid is an energy minimiser for } N=7 .

This asserts admissibility of the seven points and the inequality $U(P_7)\le U(y)$ against every admissible seven-point configuration $y$ . It fixes no numerical value of the minimum and does not assert uniqueness.

Milestones: the other known exact solutions

N=1:\ U\equiv 0;\qquad N=2:\ \text{antipodal pair optimal},\ U=\tfrac12;

N=3,4,5,6,12:\ \text{triangle, tetrahedron, triangular bipyramid, octahedron, icosahedron are energy minimisers.}

Significance

The result. Among the values of $N$ listed in the source, $N=7$ is the smallest one whose optimum was, until the 2026 claim, supported only by numerical computation; the cases $N\le 6$ and $N=12$ were settled earlier. Settling $N=7$ extends the short list of rigorously known Thomson minimisers.

Formalizing it. The $N=7$ result reported in the source is recent and described there as a claimed Lean-kernel-checked proof; a formalization on this platform against a public, reviewed statement would corroborate it independently. For the milestones, the source attributes the $N=3,5,6,12$ cases to published proofs (Föppl 1912, Schwartz 2013, Yudin 1992, Andreev 1996); the source does not describe machine-checked proofs of these, and each is a self-contained formalization target.

Difficulty

The energy is a non-convex function on the configuration space $(S^2)^N$ with many critical points, so numerical minimisation — which is how most entries of the source's table of smallest known energies were obtained — does not certify global optimality. The $N=5$ case, the most recent classical entry before $N=7$ , was resolved only with a computer-assisted proof (Schwartz 2013).

Formalization scope

Points live in EuclideanSpace ℝ (Fin 3); configurations are functions Fin N → EuclideanSpace ℝ (Fin 3). Admissibility requires unit norm and injectivity (distinct points), matching the source's " $N$ distinct points". The energy sums $1/\mathrm{dist}(x_i,x_j)$ over $i<j$ ; Lean's $1/0=0$ convention is harmless because coincident points are excluded by admissibility. The candidate configurations are fixed in one particular orientation; since the energy is invariant under orthogonal maps and relabelling, this is no loss of generality. The statement " $x$ is an energy minimiser" includes admissibility of $x$ itself, so the goal cannot be satisfied by a degenerate candidate.

Reusable infrastructure welcome: energy invariance under isometries and permutations, existence of minimisers by compactness, linear-programming (Delsarte–Yudin) bounds on the sphere, and interval-arithmetic tooling for certified numerical bounds.

Selected references

Wikipedia, Thomson problem (source of this mission). https://en.wikipedia.org/wiki/Thomson_problem
J. J. Thomson, On the Structure of the Atom…, Philosophical Magazine 7 (1904), 237–265.
L. Föppl, Stabile Anordnungen von Elektronen im Atom, J. Reine Angew. Math. 141 (1912), 251–301. https://doi.org/10.1515/crll.1912.141.251
V. A. Yudin, The minimum of potential energy of a system of point charges, Discrete Math. Appl. 3 (1993), 75–81. https://doi.org/10.1515/dma.1993.3.1.75
N. N. Andreev, An extremal property of the icosahedron, East J. Approx. 2 (1996), 459–462.
R. Schwartz, The five-electron case of Thomson's problem, Experimental Mathematics 22 (2013), 157–186. https://arxiv.org/abs/1001.3702
S. Smale, Mathematical Problems for the Next Century, Math. Intelligencer 20 (1998), 7–15. https://doi.org/10.1007/bf03025291
Vals AI, A Lean Proof of the Thomson Problem for Seven Electrons (2026). https://www.vals.ai/blogs/thomson-n7-lean-proof

9 thms2 active usersReviewed

Dynamical Systems·Captain: Lucas

Hilbert's 16th Problem for Algebraic Limit Cycles (Llibre's Conjecture)Open Problem

Motivation

The second part of Hilbert's 16th problem (Paris, 1900) asks for the maximal number and the relative position of the limit cycles of a planar polynomial differential system

\dot x = P(x,y),\qquad \dot y = Q(x,y),

where $P,Q$ are real polynomials of degree at most $d$ . Smale listed it in 1998 among the mathematical problems for the next century and remarked that, apart from the Riemann hypothesis, it seems the hardest of Hilbert's problems (Smale 1998). Even for $d = 2$ it is not known whether the number of limit cycles is uniformly bounded.

J. Llibre's survey Sobre el problema 16 de Hilbert (La Gaceta de la RSME 18 (2015), 543–554) organises the question into seven problems and concentrates on a more tractable restriction: algebraic limit cycles, i.e. limit cycles contained in a real algebraic curve. For this restriction there is an explicit conjecture for the maximal number (Conjecture 1 of the survey, first stated in Llibre–Ramírez–Sadovskaia 2010). This mission formalizes that conjecture as its goal, together with the results of the survey on which it rests.

Timeline (as reported in the survey):

1891–1897 — Poincaré introduces limit cycles and proves finiteness for systems without saddle connections.
1900 — Hilbert poses the 16th problem.
1923 — Dulac claims every polynomial system has finitely many limit cycles; in 1985 Ilyashenko finds a gap.
1957/1959 — Petrovskii and Landis claim $H(2)=3$ and later find an error; 1979 (Chen–Wang) and 1982 (Shi) give quadratic systems with 4 limit cycles.
1986 — Bamon proves finiteness for quadratic systems; 1991/1992 — Ilyashenko and Écalle independently prove finiteness for all polynomial systems.
2001 — Christopher realises any non-singular algebraic curve's bounded components as hyperbolic limit cycles of a system of the same degree (Christopher 2001).
2004 — Llibre and Rodríguez show every configuration of limit cycles is realisable by algebraic limit cycles (Llibre–Rodríguez 2004).
2007 — Llibre and Zhao give a cubic system with two algebraic limit cycles (Llibre–Zhao 2007).
2010 — Llibre, Ramírez and Sadovskaia bound the number of algebraic limit cycles when all invariant algebraic curves are generic, and state the conjecture.

Setting

A polynomial vector field is a pair $V = (P, Q)$ of real polynomials in $x,y$ ; its degree is $\max(\deg P, \deg Q)$ . A solution is a differentiable curve $\gamma:\mathbb R\to\mathbb R^2$ with $\gamma'(t) = (P,Q)(\gamma(t))$ for all $t$ . A periodic orbit is the image of a non-constant periodic solution. A limit cycle is a periodic orbit $O$ that is isolated among periodic orbits: some open set $U \supseteq O$ contains no periodic orbit other than $O$ .

A limit cycle is algebraic if it is contained in the zero set $\{f = 0\}$ of a non-zero real polynomial $f$ . The algebraic Hilbert number $H_a(d)$ is the supremum, over all polynomial vector fields of degree at most $d$ , of the number of algebraic limit cycles (a value in $\mathbb N \cup \{\infty\}$ ).

A curve $f = 0$ is invariant with cofactor $K$ if $P\,f_x + Q\,f_y = K f$ . A family of irreducible curves is generic if (i) no curve is singular, (ii) the top-degree homogeneous part of each curve is square-free, (iii) distinct curves meet transversally, (iv) no three distinct curves share a point, and (v) the top-degree homogeneous parts of distinct curves are coprime.

Formalization targets

Goal — Conjecture 1 (Llibre–Ramírez–Sadovskaia)

H_a(d) = 1 + \frac{(d-1)(d-2)}{2}\qquad (d \ge 2).

The equality asserts both that the number of algebraic limit cycles is bounded by the right-hand side for every field of degree at most $d$ , and that the bound is attained.

Milestones (in the order of the survey)

§2, Problem 1 — every polynomial vector field has finitely many limit cycles (Écalle, Ilyashenko).
§3 — $H(1) = 0$ : vector fields of degree at most $1$ have no limit cycles.
Theorem 1(a),(b) — every configuration of limit cycles is realised, and realised by algebraic limit cycles in degree $\le 2(n+r)-1$ .
Theorem 2 (Christopher) — the bounded components of a non-singular curve $f = 0$ are exactly the limit cycles, all hyperbolic, of $\dot x = \alpha f - D f_y$ , $\dot y = \beta f + D f_x$ .
Proposition 3 — invariance of $f$ is equivalent to invariance of its irreducible factors, with $K_f = \sum n_i K_{f_i}$ .
Theorem 4(a),(b) — for degree $d \ge 2$ and generic invariant curves, at most $1 + \frac{(d-1)(d-2)}{2}$ (even $d$ ) or $\frac{(d-1)(d-2)}{2}$ (odd $d$ ) algebraic limit cycles, and the bounds are attained.
§7 example — the cubic system $\dot x = 2y(10+xy)$ , $\dot y = 20x + y - 20x^3 - 2x^2 y + 4y^3$ has two algebraic limit cycles in $2x^4 - 4x^2 + 4y^2 + 1 = 0$ .
Conjecture 2 — $H_a(2) = 1$ .
Theorem 5 (Giacomini–Llibre–Viano) — an inverse integrating factor vanishes on every limit cycle.

Significance

A proof of the goal would settle Problems 6 and 7 of the survey: it would give a uniform bound, depending only on the degree, for the number of algebraic limit cycles, and identify the sharp value. The conjecture is consistent with every example known to the survey: the generic bound of Theorem 4 is sharp for even $d$ , and the known non-generic examples exceed the generic bound only in odd degree and by one. Conjecture 2 ( $d = 2$ ) is its first open case.

On the formal side, the milestones require a reusable library of planar dynamics that is currently absent from Mathlib: periodic orbits and limit cycles of planar vector fields, hyperbolicity via the divergence integral, inverse integrating factors, invariant algebraic curves and Darboux-type arguments, and topological configurations of Jordan curves. Theorems 1, 2, 4 and 5, Proposition 3 and the cubic example are proved in the literature but, as far as the proposal author knows, not formalized; the goal and Conjecture 2 are open.

Difficulty

The obvious route bounds the number of ovals of the invariant curve (Harnack's theorem) and relates the degree of the curve to the degree of the field. This fails because a field of degree $d$ can have invariant curves of arbitrarily high degree, so no a-priori degree bound on the curve is available; Theorem 4 obtains one only under the genericity conditions (i)–(v), and the degree-3 example shows that non-generic curves behave differently. On the formal side, the dynamical milestones (Theorems 2 and 5, the cubic example) need Poincaré–Bendixson-type planar topology and uniqueness of solutions, which Mathlib does not yet provide.

Formalization scope

Polynomials are MvPolynomial (Fin 2) ℝ with variable 0 as $x$ and 1 as $y$ ; points are ℝ × ℝ. The degree of a field is the maximum of the total degrees of $P$ and $Q$ , and $H_a(d)$ ranges over fields of degree at most $d$ , matching equation (1) of the survey.
Counts of limit cycles are Set.encard values in ℕ∞, so an infinite family is $\infty$ , never silently $0$ ; $H_a(d)$ is an iSup in ℕ∞, so the goal also asserts finiteness.
Solutions are global (HasDerivAt at every real time). A limit cycle is isolated among periodic orbits contained in a neighbourhood. An algebraic limit cycle lies in the zero set of some non-zero polynomial, with no degree restriction on the curve.
Genericity conditions (i), (iii), (iv) are imposed at complex points of $\mathbb C^2$ ; (ii), (v) use square-freeness and coprimality in $\mathbb R[x,y]$ ; "distinct curves" means non-associated polynomials.
Hyperbolicity of a limit cycle is encoded by a non-zero divergence integral over one period.
Theorem 1(b) is formalized without its final sentence (existence of a Darboux first integral).
Trivializing encodings are ruled out: algebraic limit cycles require a non-zero polynomial, and the conjecture is an equality in ℕ∞, not an inequality over a possibly empty family.

Contributions welcome: a planar ODE library (uniqueness, flows, Poincaré–Bendixson), Darboux theory of integrability, and proofs of the classical milestones.

Selected references

J. Llibre, Sobre el problema 16 de Hilbert, La Gaceta de la RSME 18 (2015), no. 3, 543–554 (source of this mission).
J. Llibre, R. Ramírez, N. Sadovskaia, On the 16th Hilbert problem for algebraic limit cycles, J. Differential Equations 248 (2010), 1401–1409. https://doi.org/10.1016/j.jde.2009.11.023
J. Llibre, G. Rodríguez, Configurations of limit cycles and planar polynomial vector fields, J. Differential Equations 198 (2004), 374–380. https://doi.org/10.1016/j.jde.2003.10.008
C. Christopher, Polynomial vector fields with prescribed algebraic limit cycles, Geom. Dedicata 88 (2001), 255–258. https://doi.org/10.1023/a:1013171019668
H. Giacomini, J. Llibre, M. Viano, On the nonexistence, existence and uniqueness of limit cycles, Nonlinearity 9 (1996), 501–516. https://doi.org/10.1088/0951-7715/9/2/013
J. Llibre, Y. Zhao, Algebraic limit cycles in polynomial systems of differential equations, J. Phys. A 40 (2007), 14207–14222. https://doi.org/10.1088/1751-8113/40/47/012
Yu. Ilyashenko, Centennial history of Hilbert's 16th problem, Bull. Amer. Math. Soc. 39 (2002), 301–354. https://doi.org/10.1090/s0273-0979-02-00946-1
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20 (1998), no. 2, 7–15. https://doi.org/10.1007/bf03025291

15 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains II: The Single-Unit Single-Customer DecompositionTextbook

Motivation

A base-stock (order-up-to) policy orders, in every period, exactly enough to bring the inventory position (stock on hand plus stock on order minus backorders) up to a target level. It is the policy used in practice for repairable and consumable service parts, and the analysis of every later chapter of Muckstadt's book assumes it. Its optimality is therefore a foundational question, and there are three classical ways to prove it.

1960, Clark and Scarf proved optimality of echelon base-stock policies for finite-horizon serial systems by dynamic programming, decomposing the cost into one term per echelon (Management Science 6(4)).
1984, Federgruen and Zipkin gave a lower-bound argument for the infinite-horizon average-cost case (Operations Research 32(4)); Chen and Song (2001) used it for Markov-modulated demand (Operations Research 49(2)).
2008, Muharremoglu and Tsitsiklis introduced the single-unit single-customer approach: every unit of stock is paired with one future customer, and the inventory problem splits into countably many independent two-action problems (Operations Research 56(5)).

This mission formalizes the third approach, in the finite-horizon single-location form presented in Section 2.2.1 of Muckstadt (2005).

Setting

A single item is reviewed in periods $n = 1, \dots, N$ . An exogenous, time-homogeneous Markov chain $s_n$ on a finite set $\Sigma$ is observed at the start of period $n$ ; given $s_n = s$ , the demand $D_n \in \{0,1,2,\dots\}$ has law $\kappa(s,\cdot)$ and is independent of $s_{n+1}$ . Excess demand is backordered.

Every unit of demand is a customer, and customers are indexed in arrival order, the $v_0$ initially waiting customers first. A customer's distance is $0$ once served, $1$ while waiting, and $2, 3, \dots$ for future customers in the order they will arrive. Units are indexed by location: $0$ (used), $1$ (on hand), $2, \dots, m$ (in transit) and $m+1$ (at the supplier, which holds countably many units). The state is

x_n = \big(s_n, (z_{1n}, y_{1n}), (z_{2n}, y_{2n}), \dots\big),

with $z_{jn}$ the location of unit $j$ and $y_{jn}$ the distance of customer $j$ . In period $n$ : units in transit move one location closer and the released units move from $m+1$ to $m$ (so an order is on hand $m-1$ periods later); the demand $D_n$ brings the customers at distances $2, \dots, D_n+1$ to distance $1$ and moves the others $D_n$ steps closer; units on hand serve waiting customers, lowest indices first; then $h$ is charged per unit on hand and $b$ per waiting customer, with $0 < h < b$ . The criterion is the expected cost over the $N$ periods, discounted by $\alpha \in (0,1]$ .

A policy for the whole system $\mathcal S$ chooses a finite set of units at the supplier to release. It is monotone if it releases lower-indexed units first, and committed if unit $j$ only ever serves customer $j$ . The subsystem $\mathcal S_w$ is unit $w$ with customer $w$ under commitment, with state $x^w_n = (s_n, z_{wn}, y_{wn})$ and actions Release and Hold. The set $R^*_n(s,y)$ contains the optimal actions of a subsystem whose unit is at the supplier and whose customer is at distance $y$ , and the critical distance is

y^*(n,s) = \max\{\, y : R^*_n(s,y) \ni \mathit{Release} \,\}.

Formalization targets

Goal: Theorem 5 (p. 29)

Every policy that, in each period $n$ and Markov state $s_n$ , releases the lowest-indexed units at the supplier to raise the inventory position to

y^*(n, s_n) - 1

is optimal for $\mathcal S$ among all policies, from every starting state. Such a policy exists. The levels are not fixed numbers but the critical distances of the single-unit problem, so the goal asserts the structure of an optimal policy and identifies its levels, without committing to any constant.

Milestones

Lemma 1 (p. 26): some monotone policy is optimal, every monotone policy is committed, and so some committed policy is optimal.
Theorem 4 (p. 27): the optimal cost of $\mathcal S$ is the sum over $w$ of the optimal costs of $\mathcal S_w$ ,

V^{\mathcal S}_1(s, x_1) = \sum_{w} V_1\big(s, (z_{w1}, y_{w1})\big),

and managing every subsystem independently and optimally is optimal for $\mathcal S$ . 3. Lemma 2 (p. 28): $R^*_n(s, y+1) = \{\mathit{Release}\}$ implies $\mathit{Release} \in R^*_n(s, y)$ . 4. Section 2.2.1.2.2 (p. 29): the critical distance policy, release if and only if $y \le y^*(n,s)$ , is optimal for every subsystem.

Significance

The result shows that under Markov-modulated demand a single-location system is optimally run by a state-dependent base-stock policy. The same unit–customer argument gives echelon base-stock optimality in serial systems with noncrossing stochastic lead times (Sections 2.2.2–2.2.3). The decomposition also yields the levels themselves: they are the critical distances of a two-action problem, which can be solved one customer at a time.

The theorems are proved in the literature (Muharremoglu and Tsitsiklis 2008) and in the book. To our knowledge no machine-checked proof of any base-stock optimality theorem exists, by dynamic programming or by decomposition. The book's proof is informal in three places a formalization has to settle:

Lemma 1 is asserted as "clearly" true;
Lemma 2's proof by contradiction covers only uniquely optimal releases, while the critical distance policy also needs the case of ties;
the passage from the subsystem policy to the inventory position (Theorem 5) is an "intuitive argument".

A formal development makes each of these precise.

Difficulty

The obvious argument says that costs are linear, so the cost of $\mathcal S$ is the sum of unit–customer costs and everything decouples. That is only half of Theorem 4. The pairing of unit $j$ with customer $j$ holds only under monotone policies, and a general policy for $\mathcal S$ observes the whole infinite state $x_n$ , not just $x^w_n$ . The lower bound therefore needs Lemma 1 together with the fact that extra information about the demand history does not help a Markov decision problem. The upper bound needs the lowest-index matching to cost no more than committed matching.

The second difficulty is that the threshold structure is not the obvious consequence of Lemma 2. The set of distances at which releasing is optimal must be shown to be an initial segment $\{1, \dots, y^*\}$ when ties are allowed. Unbounded demand makes that set possibly unbounded (it is, in the last $m-1$ periods). Finally, the release decisions of the subsystems must be counted to recover an inventory position, which uses the invariant that future customers occupy consecutive distances.

Formalization scope

Everything is in the namespace ServiceParts.UnitDecomp, with three definition files.

Model. Model bundles the chain, the demand law, $m$ , $h$ , $b$ and $\alpha$ with the standing assumptions $1 \le m$ , $0 < h < b$ , $0 < \alpha \le 1$ , together with the per-unit and per-customer motions and a generic finite-horizon expected-cost recursion. Costs are in $[0,\infty]$ .

Subsystem. Subsystem defines a subsystem, its optimal cost, $R^*_n$ , $y^*(n,s)$ and the critical distance policy.

System. System defines $\mathcal S$ with lowest-index matching, its policies (finite release sets), monotone and committed policies, starting states, the inventory position and the order-up-to release.

Conventions and pinnings:

Indexing. Units and customers are indexed from $0$ ; Lean index $j$ is the book's $j+1$ .
Policy class. Policies are Markov: functions of the period, the Markov state and the configuration, as on p. 25.
Optimality. Optimal means attaining the infimum over all policies for $\mathcal S$ . Restricting the class to monotone or base-stock policies would make Theorem 5 circular and is ruled out.
Starting states. The book's "any starting state $x_1$ " is the configuration built on pp. 23–24 from $v_0$ and the stock at locations $1, \dots, m$ . For arbitrarily labelled states Theorem 4 is false.
Critical distance. $y^*(n,s)$ is a supremum in $\mathbb N \cup \{\infty\}$ . Where it is $\infty$ (a released unit cannot arrive before the horizon), Theorem 5 leaves the policy free.
Distance 0. Lemma 2 and the optimality of $R_n$ are stated for customers at distance at least 1. At distance 0 with the unit at the supplier (a configuration committed policies never reach), both are false as printed.

Corrections to the book:

$h > 0$ is added. With $h = 0$ an optimal policy with finite orders need not exist, so Theorem 5 fails.
Chain structure is pinned. The chain's ergodicity is unused on a finite horizon and omitted. The conditional independence of $D_n$ and $s_{n+1}$ given $s_n$ is added as a reading of "given $s_n$ , the distribution of $D_n$ is known".
Vacuous corner. If some state's demand has infinite mean, every policy may cost $\infty$ and the optimality statements hold vacuously.

Out of scope: stochastic noncrossing lead times (Section 2.2.2), serial systems (Section 2.2.3; compare the disproved platform statement SupplyChainTheory.clark_scarf_sequential), and continuous review (Section 2.2.4, which the book calls intuitive).

Proofs of any milestone are welcome. A reusable by-product would be a general lemma that Markov policies are optimal among history-dependent ones for finite-horizon problems with countable randomness and costs in $[0,\infty]$ .

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Section 2.2, pp. 22–31. https://doi.org/10.1007/b138879
A. Muharremoglu and J. N. Tsitsiklis, A single-unit decomposition approach to multiechelon inventory systems, Operations Research 56(5), 2008. https://doi.org/10.1287/opre.1080.0620
A. J. Clark and H. Scarf, Optimal policies for a multi-echelon inventory problem, Management Science 6(4), 1960. https://doi.org/10.1287/mnsc.6.4.475
A. Federgruen and P. Zipkin, Computational issues in an infinite-horizon, multiechelon inventory model, Operations Research 32(4), 1984. https://doi.org/10.1287/opre.32.4.818
F. Chen and J.-S. Song, Optimal policies for multiechelon inventory problems with Markov-modulated demand, Operations Research 49(2), 2001. https://doi.org/10.1287/opre.49.2.226.13528

8 thms2 active usersReviewed

Completed

Functional Analysis·Captain: savarin

Sharp diagonal Hlawka constants: formalize the supplied proof at cutoff 90Research Paper

The Hlawka inequality for Schatten $p$ -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. The question is how large a comparison constant is needed to make this inequality hold.

This mission extends the best possible constant for complex diagonal matrices from $p\ge256$ to every real $p\ge90$ . The result is proved in Lean. The constant and its formula are unchanged from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. For each exponent, it works for every triple of diagonal matrices, whatever their size, and no smaller constant does.

The mission started from a supplied pen-and-paper proof. Lowering the cutoff took more than replacing 256 with 90: several estimates in the original argument had to be strengthened. The research note proves the bound for real entries first, then transfers it to complex entries and shows that the constant cannot be improved. The goal theorem below gives the exact formula and statement.

This is the second step of the sharp diagonal Hlawka campaign, and it reuses the foundation's definitions and supporting results. The campaign invites further improvements below 90, keeping the same formula.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

61 thms2 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Bellman's Dynamic Programming V: Optimality of a Constant Stock Level for the Optimal Inventory EquationTextbook

Motivation

Setting

Formalization targets

Goal: Chapter V, Theorem 1 (with (4b) corrected)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bellman's Dynamic Programming IV: Existence and Uniqueness for Functional Equations of Types One, Two and ThreeTextbook

Motivation

Setting

Formalization targets

Goal: Chapter IV, Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bellman's Dynamic Programming III: Index Rules for the Stochastic Gold-Mining ProcessTextbook

Motivation

Setting

Formalization targets

Goal: Chapter II, Theorem 4 (the index rule for nnn mines)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bellman's Dynamic Programming II: Fibonacci Search for the Maximum of a Unimodal FunctionTextbook

Motivation

Setting

Formalization targets

Goal: Chapter I, Theorem 11

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bellman's Dynamic Programming I: Existence and Uniqueness for the Multi-Stage Allocation EquationTextbook

Motivation

Setting

Formalization targets

Goal: Chapter I, Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Assumptions of Physics IV: Ensemble Spaces Are CancellativeTextbook

Motivation

Setting

Formalization targets

Goal (Theorem 4.73, Ensemble spaces are cancellative)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Building Anosov flows on 3-manifolds (Béguin–Bonatti–Yu)Research Paper

Motivation

Setting

Formalization targets

Goal: the gluing theorem (Theorem 1.5)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Linear Programming: Foundations and Extensions III: Network Flows, the Integrality Theorem and König's TheoremTextbook

Motivation

Setting

Formalization targets

Goal: Chapter II, Theorem 4 (the index rule for $n$ mines)

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)