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.996001Formalized record

3 provers on it4 of 4 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.996001Formalized record

3 provers on it4 of 4 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

Analysis Markov Chain Operations Research+2·Captain: mikedeng1

Fundamentals of Queueing Theory III: The Transient M/M/1 Queue via Modified Bessel FunctionsTextbook

Motivation

Steady-state formulas describe a queue that has been running forever. Many practical questions are about a queue that has not: a call centre just after opening, a server just after a reset, a system under a burst of load. For these, the relevant quantity is the transient distribution $p_n(t) = \Pr\{N(t) = n\}$ of the number $N(t)$ in the system at a finite time $t$ . It is also what determines how fast the steady state is approached, and it is needed for the busy period: the length of time a server stays busy once a customer arrives at an idle server.

For the single-server Markovian queue M/M/1 the transient distribution has an explicit closed form in modified Bessel functions. Its history is short and well documented. Ledermann and Reuter (1954) obtained it by spectral analysis of the birth–death process. Bailey (1954) found it by generating functions and Laplace transforms, and Champernowne (1956) by combinatorial methods. Bailey's route is the standard textbook derivation, and it is the one Gross, Shortle, Thompson and Harris outline in §2.11 of Fundamentals of Queueing Theory (4th ed., 2008). Abate and Whitt (1989) showed that computing with the resulting series is numerically delicate, which is one reason for having the formula pinned down exactly.

This mission formalizes §§2.11–2.12 of that book: the transient laws of M/M/1/1, M/M/1 and M/M/∞, and the M/M/1 busy period.

Setting

Customers arrive in a Poisson stream of rate $\lambda > 0$ . Each service takes an exponential time of rate $\mu > 0$ , and $\rho = \lambda/\mu$ . The number in the system is a continuous-time Markov chain on $\{0, 1, 2, \dots\}$ , and its state probabilities $p_n(t)$ satisfy the forward (differential–difference) equations. For M/M/1 started with $N(0) = i$ they are, for $t \ge 0$ ,

p_n'(t) = -(\lambda+\mu)p_n(t) + \lambda p_{n-1}(t) + \mu p_{n+1}(t)\ (n > 0), \qquad p_0'(t) = -\lambda p_0(t) + \mu p_1(t), \tag{2.72}

with $p_n(0) = 1$ if $n = i$ and $0$ otherwise. The other systems are variants:

M/M/1/1, no waiting room: two states and equations (2.70).
M/M/∞, ample service: the death rate in state $n$ is $n\mu$ , giving (2.76).
The busy-period system: (2.72) with $0$ made absorbing ( $\lambda_0 = 0$ ) and $N(0) = 1$ . Its $p_0(t)$ is the distribution function of the busy period $T_{bp}$ .

A family $(p_n)$ solves a system on $[0,\infty)$ when each $p_n$ has, at every $t \ge 0$ , the prescribed derivative (a right derivative at $t = 0$ ). It is a probability solution when $p_n(t) \ge 0$ and $\sum_n p_n(t) = 1$ for every $t \ge 0$ . The modified Bessel function of the first kind is

I_n(y) = \sum_{k=0}^{\infty} \frac{(y/2)^{n+2k}}{k!\,(n+k)!}, \qquad I_{-n} = I_n,

and the Laplace transform of $f$ is $\bar f(s) = \int_0^\infty e^{-st} f(t)\,dt$ for $\operatorname{Re} s > 0$ .

Formalization targets

Goal: the transient M/M/1 law, (2.75)

With $y = 2t\sqrt{\lambda\mu}$ ,

p_n(t) = e^{-(\lambda+\mu)t}\Big[\rho^{(n-i)/2} I_{n-i}(y) + \rho^{(n-i-1)/2} I_{n+i+1}(y) + (1-\rho)\rho^n \sum_{j=n+i+2}^{\infty} \rho^{-j/2} I_j(y)\Big].

The goal asserts five things for every $\lambda, \mu > 0$ and every $i$ , with no restriction on $\rho$ :

the series converges;
these functions solve (2.72);
they meet the initial condition;
they form a probability distribution at every $t$ ;
they are the only probability solution.

Milestones

(2.71): the M/M/1/1 solution $p_1(t) = \frac{\lambda}{\lambda+\mu}(1-e^{-(\lambda+\mu)t}) + p_1(0)e^{-(\lambda+\mu)t}$ , and the matching formula for $p_0$ .
(2.74) and Rouché's theorem: for $\operatorname{Re} s > 0$ , the quadratic $(\lambda+\mu+s)z - \mu - \lambda z^2$ has exactly one zero in $|z| < 1$ , namely $z_1 = (\lambda+\mu+s-\sqrt{(\lambda+\mu+s)^2-4\lambda\mu})/(2\lambda)$ .
The transform of $p_0$ : $\bar p_0(s) = z_1^{i+1}/(\mu(1-z_1))$ .
The limit of (2.75): $p_n(t) \to (1-\rho)\rho^n$ if $\rho < 1$ , and $p_n(t) \to 0$ if $\rho \ge 1$ .
(2.77), M/M/∞: started empty, $p_n(t) = a(t)^n e^{-a(t)}/n!$ with $a(t) = (1-e^{-\mu t})\lambda/\mu$ . The statement says that this family solves (2.76), is the unique probability solution, and has generating function $\exp((z-1)a(t))$ .
The busy-period transform: $\bar p_0(s) = 2\mu/(s[\lambda+\mu+s+\sqrt{(\lambda+\mu+s)^2-4\lambda\mu}])$ .
The busy-period density: $p_0'(t) = \sqrt{\mu/\lambda}\,e^{-(\lambda+\mu)t} I_1(2\sqrt{\lambda\mu}\,t)/t$ .
(2.79): for $\lambda < \mu$ , $E[T_{bp}] = 1/(\mu-\lambda)$ and $E[T_{bc}] = 1/\lambda + 1/(\mu-\lambda)$ .

Significance

The formula (2.75) is the exact finite-time law of the most basic queue. It gives the rate at which M/M/1 approaches equilibrium, and it gives the distribution of the queue under overload ( $\rho \ge 1$ ), where no steady state exists. It is the reference against which numerical transient methods, such as the uniformization of Chapter 8 of the same book, are checked. The busy-period density and its mean (2.79) enter server-utilisation and vacation models, and the Laplace-transform method used here recurs in the M/G/1 analysis of Chapter 5.

All of these results are classical and proved in the literature. None of them is machine-checked, as far as the platform's catalogue and Mathlib show. The chain from a countable system of linear ODEs, through generating functions and a root-location argument, to a Bessel series is a standard pattern in applied probability, and a formal version of it is what this mission adds. The formal statements also make explicit what the book leaves implicit: the sense in which the equations hold at $t = 0$ , and the class in which the solution is unique.

Difficulty

The forward equations (2.72) form an infinite linear system. The obvious approach is to treat it like a finite system of ODEs, whose solution is a matrix exponential, and read off (2.75). That fails for two reasons. The generator is an infinite matrix, so its exponential needs a functional-analytic setting. And uniqueness is not automatic for infinite systems: it needs a class, such as probability solutions, and an argument that works in that class.

The Bessel form is a second, independent difficulty. The transform $\bar p_0(s)$ is fixed by a root-location argument in the complex plane. Inverting the transform, or verifying (2.75) directly, requires manipulating the three-term Bessel recurrence and exchanging infinite sums. The tail sum $\sum_{j} \rho^{-j/2} I_j$ has to be controlled uniformly enough to be differentiated term by term. For $\rho \ge 1$ the factor $(1-\rho)$ is non-positive, so the nonnegativity of $p_n(t)$ is not visible from the formula.

Formalization scope

Conventions committed to:

Parameters. Rates are real with $\lambda, \mu > 0$ , and $\rho = \lambda/\mu$ . States are ℕ (Fin 2 for M/M/1/1).
Solutions. "Solves on $[0,\infty)$ " is HasDerivWithinAt on Set.Ici 0 at every $t \ge 0$ . Uniqueness is asserted among solutions that are probability distributions at every time.
Special functions. Half-integer powers of $\rho$ are real powers, and $I_{-m} = I_m$ is part of the definition. Laplace transforms are complex Bochner integrals over $(0,\infty)$ , and each statement also asserts the integrability it needs. Square roots with positive real part are hypotheses $r^2 = (\lambda+\mu+s)^2 - 4\lambda\mu$ , $\operatorname{Re} r > 0$ .

The closed forms stated exactly as in the book are:

(2.71);
$z_1$ and $z_2$ of (2.74);
$\bar p_0(s) = z_1^{i+1}/(\mu(1-z_1))$ ;
(2.75), with the Bessel series of p.101;
the M/M/∞ law and (2.77);
the busy-period transform and density of p.102;
(2.79).

The book derives (2.79) by a steady-state ratio argument valid for M/G/1. Here it is stated for M/M/1, as the mean of the explicit density.

A statement of (2.75) that only asserts the right-hand side is well defined, or checks only $n = 0$ , is ruled out: the goal requires the ODE system, the initial condition, the probability property and uniqueness. For the same reason, the M/M/∞ law is tied to the system (2.76) and does not reduce to a Taylor expansion.

Needed infrastructure that Mathlib lacks:

modified Bessel functions of integer order;
Laplace transforms;
a Rouché-type zero count or a direct root-location lemma;
uniqueness for countable linear ODE systems with bounded or linearly growing rates.

The Bessel and Laplace definitions, and the uniqueness lemma for birth–death forward equations, are reusable beyond this mission. Contributions of those as separate lemmas are welcome.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§2.11–2.12, pp.97–103. https://doi.org/10.1002/9781118625651
N. T. J. Bailey, "A continuous time treatment of a simple queue using generating functions", J. Royal Statistical Society B 16 (1954) 288–291. https://doi.org/10.1111/j.2517-6161.1954.tb00172.x
W. Ledermann, G. E. H. Reuter, "Spectral theory for the differential equations of simple birth and death processes", Phil. Trans. Royal Society A 246 (1954) 321–369. https://doi.org/10.1098/rsta.1954.0001
D. G. Champernowne, "An elementary method of solution of the queueing problem with a single server and constant parameters", J. Royal Statistical Society B 18 (1956) 125–128. https://doi.org/10.1111/j.2517-6161.1956.tb00217.x
J. Abate, W. Whitt, "Calculating time-dependent performance measures for the M/M/1 queue", IEEE Trans. Communications 37 (1989) 1102–1104. https://doi.org/10.1109/26.41165

15 thms2 active usersReviewed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Fundamentals of Queueing Theory II: Erlang's Formulas and the Halfin–Whitt Square-Root Staffing LawTextbook

Why birth–death queues and Erlang's formulas

Every call center, hospital ward, cloud server pool and telephone exchange that is sized by formula is sized by one of a handful of explicit expressions from Markovian queueing theory. The two oldest are A. K. Erlang's: the Erlang-B (loss) formula of 1917, which gives the fraction of calls lost when $c$ trunks carry an offered load of $r$ erlangs, and the Erlang-C formula, which gives the probability that a customer of a $c$ -server queue must wait. Both are still the default dimensioning rules of telecommunications and call-center workforce management (Gans, Koole & Mandelbaum 2003).

This mission formalizes Chapter 2, §§2.1–2.10, of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), which derives these formulas from a single result about birth–death processes and closes with the modern answer to the staffing question.

Timeline. Erlang (1917) obtained the loss formula; Vaulot (1927), Pollaczek (1932), Palm (1938) and Kosten (1948) completed its proof for general service times. Halfin and Whitt (1981) showed that in the $M/M/n$ queue the delay probability converges to a limit strictly between $0$ and $1$ exactly when the number of servers exceeds the offered load by an amount of order $\sqrt n$ . This is the quality-and-efficiency-driven (QED) regime on which square-root staffing rests.

Setting

A birth–death process is a continuous-time Markov chain on the states $n \in \{0, 1, 2, \dots\}$ that moves from $n$ to $n+1$ at rate $\lambda_n \ge 0$ (a birth, or arrival) and, for $n \ge 1$ , from $n$ to $n-1$ at rate $\mu_n > 0$ (a death, or departure). A steady-state solution is a probability sequence $\{p_n\}$ ( $p_n \ge 0$ , $\sum_n p_n = 1$ ) solving the global balance equations (2.1):

(\lambda_n + \mu_n)p_n = \lambda_{n-1}p_{n-1} + \mu_{n+1}p_{n+1}\ (n \ge 1), \qquad \lambda_0 p_0 = \mu_1 p_1.

The queues of the chapter are birth–death processes with particular rates. The $M/M/1$ queue has $\lambda_n = \lambda$ , $\mu_n = \mu$ and traffic intensity $\rho = \lambda/\mu$ . The $M/M/c$ queue has $\lambda_n = \lambda$ , $\mu_n = \min(n, c)\mu$ (2.30), offered load $r = \lambda/\mu$ and $\rho = r/c$ . The $M/M/c/c$ loss system is the same with $\lambda_n = 0$ for $n \ge c$ . The $M/M/\infty$ queue has $\mu_n = n\mu$ .

The explicit functions are the Erlang-B formula

B(c, r) = \frac{r^c/c!}{\sum_{i=0}^{c} r^i/i!},

the Erlang-C formula, defined for $\rho = r/c < 1$ ,

C(c, r) = \frac{r^c/(c!(1-\rho))}{r^c/(c!(1-\rho)) + \sum_{n=0}^{c-1} r^n/n!},

and, with $\phi$ , $\Phi$ the standard normal density and distribution function,

\alpha(\beta) = \frac{\phi(\beta)}{\phi(\beta) + \beta\Phi(\beta)}.

Formalization targets

Goal: the Halfin–Whitt theorem (§2.4, p.75)

For offered loads $0 < r_n < n$ ,

\lim_{n\to\infty} C(n, r_n) = \alpha \in (0,1) \iff \lim_{n\to\infty} \frac{n - r_n}{\sqrt n} = \beta > 0, \qquad \alpha = \alpha(\beta).

It is stated as three facts: $\alpha$ maps $(0, \infty)$ into $(0, 1)$ ; each $\alpha \in (0, 1)$ has exactly one preimage $\beta > 0$ ; and for every $\beta > 0$ the two limits are equivalent.

Milestones

(2.3)–(2.4): the steady-state solution of a general birth–death process, $p_n = p_0\prod_{i=1}^n \lambda_{i-1}/\mu_i$ , and its existence if and only if $1 + \sum_{n\ge1}\prod_{i=1}^n \lambda_{i-1}/\mu_i < \infty$ .
(2.9): $M/M/1$ , $p_n = (1-\rho)\rho^n$ , existing iff $\rho < 1$ .
(2.31)–(2.32): the $M/M/c$ law, existing iff $\lambda/(c\mu) < 1$ .
(2.33): $L_q = r^c\rho\,p_0/(c!(1-\rho)^2)$ .
(2.37)–(2.38): $1 - \sum_{n<c} p_n = C(c, r)$ .
(2.52)–(2.53): the $M/M/c/c$ law and $p_c = B(c, r)$ .
(2.54): $B(c, r) = rB(c-1, r)/(c + rB(c-1, r))$ , $B(0, r) = 1$ .
(2.55): $C(c, r) = cB(c, r)/(c - r + rB(c, r))$ .
(2.57): $M/M/\infty$ , $p_n = r^n e^{-r}/n!$ .

Significance

The results. Items 1–9 are the working formulas of Markovian capacity planning: a stationary law for each basic model and the measures read off from it. (2.54) and (2.55) are how $B$ and $C$ are computed in practice, since the factorials of the closed forms overflow for $c > 170$ . The Halfin–Whitt theorem is the reason the rule $c \approx r + \beta\sqrt r$ holds a fixed service level, and it is the entry point to the QED heavy-traffic literature (diffusion limits of many-server queues, Garnett–Mandelbaum–Reiman, Gamarnik–Momčilović).

Formalizing them. All results are classical and proved in the literature. The book states the Halfin–Whitt theorem without proof, and (2.54)–(2.55) are left to exercises. The formalization would supply machine-checked versions of the Erlang identities and of the Halfin–Whitt limit theorem. No Lean development of either was found on the platform when this mission was drafted. A related Erlang-B statement from Kelly and Yudovina is on the platform, stated with detailed balance on a finite state space.

Difficulty

The stationary laws are induction plus geometric and exponential series, and the Erlang identities are finite algebra. The difficulty is concentrated in the goal. $C(n, r_n)$ is a ratio of a Poisson-type tail to a truncated exponential sum in which both $n$ and $r_n$ grow. The naive route, substituting Stirling's formula term by term, fails: the sums have $\Theta(\sqrt n)$ significant terms, each of relative size $\exp(-k^2/2n)$ , and the error has to be controlled uniformly over them. The converse direction also requires showing that $\alpha(\cdot)$ is strictly monotone. Without that, convergence of $C(n, r_n)$ does not force convergence of $(n - r_n)/\sqrt n$ .

Formalization scope

Rates are real sequences indexed by $\mathbb N$ , and a steady-state solution is a real sequence with HasSum p 1, nonnegative entries, and the balance equations (2.1) exactly as printed (global balance, not detailed balance). Every "the steady-state solution is X" is stated in both halves: X is a steady-state solution, and every steady-state solution equals X; the book's existence conditions ( $\rho < 1$ , $\lambda/(c\mu) < 1$ , convergence of the series) are part of the statements. The $M/M/c/c$ system is the $\mathbb N$ -indexed process with $\lambda_n = 0$ for $n \ge c$ , as §2.5 sets it up; the statement records that states above $c$ carry no mass.

The closed forms that are fixed in Lean: $\prod_{i=1}^n \lambda_{i-1}/\mu_i$ over Finset.Icc 1 n; $B(c, r)$ and $C(c, r)$ exactly as displayed above; $\phi$ = gaussianPDFReal 0 1, $\Phi$ = the CDF of gaussianReal 0 1; $W_q(0) = \sum_{n=0}^{c-1} p_n$ , as evaluated on p.69; $L_q = \sum_{n > c}(n - c)p_n$ as a convergent series.

$C(c, r)$ is a total function in Lean, but its value for $r \ge c$ carries no meaning. The goal assumes $0 < r_n < n$ for $n \ge 1$ , the book's standing condition $\rho < 1$ . A statement about some other function with the same limiting behaviour, or with $B$ and $C$ left abstract, would not be this mission. Neither would one-directional or existence-only versions of the stationary laws.

Not included: the waiting-time distributions (2.28) and (2.39), which need an FCFS waiting-time model with arrival-point probabilities; the $M/M/c/K$ measures (2.45)–(2.48); finite-source and state-dependent models (§§2.8–2.10). Useful contributions beyond the milestones are Poisson tail estimates at the $\sqrt n$ scale and monotonicity of $\alpha(\beta)$ . Both are reusable in other many-server heavy-traffic statements.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 567–588, 1981. https://doi.org/10.1287/opre.29.3.567
N. Gans, G. Koole, A. Mandelbaum, Telephone call centers: tutorial, review, and research prospects, Manufacturing & Service Operations Management 5(2), 79–141, 2003. https://doi.org/10.1287/msom.5.2.79.16071
A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917 (English translation in The Life and Works of A. K. Erlang, 1948).
F. P. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Mechanism Design+1·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design IX: Monotone Direct Mechanisms Are Dictatorial (Gibbard–Satterthwaite)Textbook

Motivation

Voting rules, committee procedures and any other method that turns individual rankings into one collective choice face the same question: can the rule be designed so that no participant ever gains by misreporting their ranking? The Gibbard–Satterthwaite theorem (Gibbard, 1973; Satterthwaite, 1975) answers no. When at least three alternatives can be chosen and all strict rankings are admissible, the only rules immune to manipulation are dictatorships. The result is the starting point of mechanism design without money. It explains why the positive results of the transferable-utility chapters of the book (Groves, VCG, posted prices) depend on quasi-linear preferences, and why research on voting turned to restricted preference domains and weaker solution concepts.

This mission formalizes Chapter 8 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), §§8.2–8.3. The book's route to the theorem follows Reny (2001). Strategy-proofness implies Maskin monotonicity, and every monotone rule with full range over at least three alternatives is dictatorial. The second step is the Muller–Satterthwaite theorem (Muller and Satterthwaite, 1977), which is stronger than Gibbard–Satterthwaite because monotonicity is weaker than strategy-proofness. The chapter closes with the classical escape route: on single-peaked preferences (Moulin, 1980) the median voting rule is strategy-proof and not dictatorial.

Timeline. Arrow (1951/1963) proved the impossibility of non-dictatorial preference aggregation under independence of irrelevant alternatives. Gibbard (1973) and Satterthwaite (1975) proved the manipulation version independently, and Satterthwaite showed the two theorems are equivalent. Muller and Satterthwaite (1977) showed that on the full domain strategy-proofness is equivalent to a monotonicity condition (strong positive association). Moulin (1980) characterized strategy-proof rules on single-peaked domains that depend only on reported peaks. Reny (2001) gave the short common proof of Arrow's and the Muller–Satterthwaite theorems that the book follows.

Setting

There is a finite set $I=\{1,\dots,N\}$ of agents and a finite set $A$ of alternatives. Each agent $i$ has a preference relation $R_i$ over $A$ ; $a\,R_i\,b$ reads " $a$ is weakly preferred to $b$ ". Every $R_i$ is a linear order: complete, transitive, and the only indifference is among identical alternatives. Its strict part is $P_i$ . The set of all linear orders over $A$ is $\mathcal R$ , and a profile is $R=(R_1,\dots,R_N)\in\mathcal R^N$ . $(R_i',R_{-i})$ is the profile obtained from $R$ by replacing agent $i$ 's preference with $R_i'$ .

A direct mechanism is a function $f:\mathcal R^N\to A$ (Definition 8.1). It is

dominant strategy incentive-compatible (DSIC) if $f(R_i,R_{-i})\,R_i\,f(R_i',R_{-i})$ for all $i$ , $R$ , $R_i'$ (Definition 8.2);
dictatorial if some agent $i$ satisfies $f(R)\,R_i\,a$ for all profiles $R$ and all $a\in A$ (Definition 8.3);
monotone if $f(R)=a$ and, for every $i$ , $a\,R_i\,b\Rightarrow a\,R_i'\,b$ for all $b$ , together imply $f(R')=a$ (Definition 8.4);
set-monotone if $f(R)\in B$ and, for every $i$ , $R_i'$ differs from $R_i$ only in the ranking of elements of $B$ , together imply $f(R')\in B$ (Definition 8.5);
unanimity-respecting if $f(R)=a$ whenever every agent ranks $a$ at the top (Definition 8.6).

"The range of $f$ is $A$ " means that every alternative is chosen at some profile.

For §8.3 the alternatives are labelled $1,\dots,K$ . A preference is single-peaked if it has a top alternative $k(i)$ and declines monotonically to the right and to the left of it. $\hat{\mathcal R}$ is the set of single-peaked preferences, and on the restricted domain $\hat{\mathcal R}^N$ DSIC and dictatorship are read with all profiles and deviations taken from $\hat{\mathcal R}$ .

Formalization targets

Goal: Proposition 8.5 (Muller–Satterthwaite)

|A|\ge 3,\quad f(\mathcal R^N)=A,\quad f\ \text{monotone}\ \Longrightarrow\ \exists\, i\in I\ \ \forall R\in\mathcal R^N\ \forall a\in A:\ f(R)\,R_i\,a.

This is the book's own capstone ("the core of the proof", p.144). No constant needs to be fixed, and the statement is strictly stronger than the necessity half of Gibbard–Satterthwaite.

Milestones

Proposition 8.2: DSIC $\Rightarrow$ monotone.
Proposition 8.3: monotone $\Rightarrow$ set-monotone.
Proposition 8.4: monotone and full range $\Rightarrow$ respects unanimity.
Proposition 8.1 (Gibbard–Satterthwaite): for $|A|\ge3$ and full range, $f$ is DSIC $\iff$ $f$ is dictatorial.
Proposition 8.6: for $|A|\ge3$ and at least two agents, there is a mechanism on $\hat{\mathcal R}^N$ with range $A$ that is DSIC on $\hat{\mathcal R}^N$ and not dictatorial on $\hat{\mathcal R}^N$ .

Significance

The result itself. Proposition 8.5 turns an incentive question into a purely ordinal one: any full-range rule that is Maskin monotone is a dictatorship once three alternatives are available. With Proposition 8.2 it gives Gibbard–Satterthwaite. Proposition 8.6 marks the boundary of the impossibility: with a one-dimensional ordering of alternatives and single-peaked preferences, the median voter rule escapes it.

Formalizing it. All results are classical and proved. The platform already has a proved Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite, Algorithmic Game Theory III), derived from Arrow's theorem in the alternative Mathlib environment c5ea0035…. It uses strict-order profiles and a one-agent-deviation monotonicity. This mission adds Maskin monotonicity, the Muller–Satterthwaite theorem, Reny's direct proof route, and the single-peaked possibility result, none of which is on the platform, all in the default environment.

Difficulty

Propositions 8.2–8.4 are short. The difficulty is in Proposition 8.5. Its proof moves one alternative up or down agents' rankings one agent at a time, and it has to keep the chosen alternative pinned at every step using only monotonicity, set-monotonicity and unanimity. It needs a pivotal agent, whose identity depends on the pair of alternatives, and then an argument that the pivots for different alternatives coincide. The argument uses a third alternative $c$ in an essential way. With two alternatives the conclusion is false (majority rule), so any argument that never uses $|A|\ge3$ cannot succeed. Formally, each "move $b$ just below $a$ in agent $j$ 's ranking" is an explicit construction of a new linear order, together with a check that the monotonicity hypothesis applies. The figures on pp.146–149 describe these orders only partially ("the other alternatives in arbitrary order"). For Proposition 8.6, the obstacle is that DSIC must be checked against every single-peaked misreport, not only misreports of the peak.

Formalization scope

A linear order is the structure LinPref A (relation rel, completeness, transitivity, antisymmetry). A profile is ι → LinPref A for a finite agent type ι, and a direct mechanism is (ι → LinPref A) → A. $A$ is a Fintype. "The range of $f$ is $A$ " is Function.Surjective f, and $|A|\ge3$ is 3 ≤ Fintype.card A.
Monotonicity is the book's Definition 8.4 for arbitrary pairs of profiles, with the lower-contour condition required for each agent separately. Dictatorship is ∃ i, ∀ R a, f R ≥_{R_i} a, with the agent chosen before the profile. A weaker monotonicity (one-agent deviations only) or a weaker dictatorship ("some agent's top is chosen at some profile") would trivialize the goal and is ruled out.
§8.3: the labelling is lab : A ≃ Fin K (labels $0,\dots,K-1$ ). The restricted domain is a predicate on LinPref A, and DSIC, dictatorship and full range are relativized to profiles in the domain (IsDSICOn, IsDictatorialOn, HasFullRangeOn). Values of the mechanism off the domain are never consulted.
Two corrections of the page. The left-hand clause of single-peakedness is printed as $(\ell-1)\,R_i\,\ell$ and is used as $\ell\,R_i\,(\ell-1)$ (the book's words "decline monotonically to the left"). Proposition 8.6 carries the added hypothesis $N\ge2$ , since with one agent every onto strategy-proof rule is dictatorial.
Proposition 8.6 is an existence statement. The median voting mechanism is the book's witness, but the statement does not fix it.
Reusable beyond this mission: the linear-order profile model, Maskin monotonicity and the restricted-domain notions, which apply to Arrow-type results, implementation theory and Moulin's characterization. Proofs of any milestone, or an independent formal proof of Proposition 8.5, are welcome.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Ch. 8. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
A. Gibbard, "Manipulation of voting schemes: a general result", Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
M. A. Satterthwaite, "Strategy-proofness and Arrow's conditions", Journal of Economic Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
E. Muller and M. A. Satterthwaite, "The equivalence of strong positive association and strategy-proofness", Journal of Economic Theory 14 (1977) 412–418. https://doi.org/10.1016/0022-0531(77)90140-5
P. J. Reny, "Arrow's theorem and the Gibbard–Satterthwaite theorem: a unified approach", Economics Letters 70 (2001) 99–105. https://doi.org/10.1016/S0165-1765(00)00332-3
H. Moulin, "On strategy-proofness and single peakedness", Public Choice 35 (1980) 437–455. https://doi.org/10.1007/BF00128122
S. Barberà, "An introduction to strategy-proof social choice functions", Social Choice and Welfare 18 (2001) 619–653. https://doi.org/10.1007/s003550100151

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization Mechanism Design+2·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design VII: Crémer–McLean Full Surplus Extraction with Correlated TypesTextbook

Motivation

Bayesian mechanism design asks which collective decisions and payments a designer can implement when every agent holds private information, the type, drawn from a commonly known prior. Most of the classical theory (Myerson's optimal auction, the Myerson–Satterthwaite impossibility, the public goods results) assumes that types are independent. Once types are correlated, as they are when bidders' values share a common component, the theory changes in a way that is best read as a paradox: Crémer and McLean (Econometrica 1988) showed that a designer can then extract the entire surplus, leaving agents no information rents. This mission formalizes Chapter 6 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press 2015), which sets up Bayesian mechanism design in general, treats independent types, and proves the Crémer–McLean theorem, together with the one numbered result of Chapter 9, the impossibility theorem of Jehiel and Moldovanu for interdependent values.

Timeline of the results formalized here:

Rochet (1987) characterized implementable decision rules by cyclical monotonicity; Proposition 6.1 is its interim version for independent types.
Crémer and McLean (1988): under their condition on the prior, every direct mechanism can be made Bayesian incentive-compatible without changing its decision rule or interim payments (Proposition 6.4).
Krishna and Maenner (2001): revenue equivalence for convex type sets and convex utilities (Proposition 6.2).
Jehiel and Moldovanu (2001): with interdependent values, efficient decisions are generically not Bayesian implementable (Proposition 9.1).
Kosenok and Severinov (2008): an identifiability condition added to Crémer–McLean gives ex post budget balance as well (Proposition 6.6).

Setting

There are finitely many agents $i \in I$ and a set $A$ of alternatives. Agent $i$ has a type $\theta_i \in \Theta_i$ and utility $u_i(a,\theta_i) - t_i$ from alternative $a$ and payment $t_i$ . Types $\theta = (\theta_1,\dots,\theta_N) \in \Theta = \prod_i \Theta_i$ are drawn from a common prior $\mu$ ; $\mu(\cdot\mid\theta_i)$ is the conditional distribution of the others' types $\theta_{-i}$ given $\theta_i$ . Types are independent if $\mu(\cdot\mid\theta_i)$ does not depend on $\theta_i$ .

A direct mechanism $(q, t_1,\dots,t_N)$ is a decision rule $q:\Theta\to A$ and payment rules $t_i:\Theta\to\mathbb R$ . It is Bayesian incentive-compatible (BIC) if for every $i$ and all $\theta_i,\theta_i'$ ,

\int_{\Theta_{-i}} u_i(q(\theta_i,\theta_{-i}),\theta_i) - t_i(\theta_i,\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i) \ \ge\ \int_{\Theta_{-i}} u_i(q(\theta_i',\theta_{-i}),\theta_i) - t_i(\theta_i',\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i).

The interim decision rule $Q_i(\theta_i)$ is the distribution of $q(\theta_i,\theta_{-i})$ given $\theta_i$ , and the interim expected payment is $T_i(\theta_i) = \int t_i(\theta_i,\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i)$ . A mechanism is ex post budget balanced if $\sum_i t_i(\theta) = 0$ for every $\theta$ , and ex ante budget balanced if $\int_\Theta \sum_i t_i\,d\mu = 0$ .

In §6.4 every $\Theta_i$ is finite and $\mu(\theta) > 0$ for every $\theta$ . The prior satisfies the Crémer–McLean condition if for no agent $i$ and type $\theta_i$ there are weights $\lambda \ge 0$ on $\Theta_i\setminus\{\theta_i\}$ with

\mu(\theta_{-i}\mid\theta_i) = \sum_{\theta_i'\ne\theta_i}\lambda(\theta_i')\,\mu(\theta_{-i}\mid\theta_i')\quad\text{for all }\theta_{-i}.

Identifiability requires that for every full-support distribution $\nu\ne\mu$ some agent's type $\theta_i$ has a belief $\nu(\cdot\mid\theta_i)$ that is not a nonnegative combination of the beliefs $\mu(\cdot\mid\theta_i')$ .

Formalization targets

Goal: Crémer–McLean (Proposition 6.4)

If $\mu$ satisfies the Crémer–McLean condition, then for every direct mechanism $(q,t)$ there is a BIC direct mechanism $(q,t')$ with

\sum_{\theta_{-i}} t_i(\theta_i,\theta_{-i})\,\mu(\theta_{-i}\mid\theta_i) = \sum_{\theta_{-i}} t_i'(\theta_i,\theta_{-i})\,\mu(\theta_{-i}\mid\theta_i)\quad\text{for all } i,\theta_i.

Milestones

Proposition 6.1 (independent types): $q$ is part of a BIC mechanism iff it is interim cyclically monotone, $\sum_{\kappa=1}^{k-1}\big(\int_A u_i(a,\theta_i^{\kappa+1})\,dQ_i(\theta_i^\kappa) - \int_A u_i(a,\theta_i^\kappa)\,dQ_i(\theta_i^\kappa)\big)\le 0$ for every cycle $\theta_i^k = \theta_i^1$ .
Proposition 6.2 (independent types, convex type sets, convex utilities): two BIC mechanisms with $Q_i' = Q_i$ have $T_i' = T_i + \tau_i$ .
Proposition 6.3 (independent types): every ex ante budget balanced mechanism has an equivalent ex post budget balanced one.
Proposition 6.5 (Farkas's alternative), already proved on the platform as Polyhedral.farkas_lemma.
Proposition 6.6 (Kosenok–Severinov): under Crémer–McLean and identifiability, every ex ante budget balanced mechanism has an equivalent BIC and ex post budget balanced one.
Proposition 9.1 (Jehiel–Moldovanu): in the linear interdependent-values model, under a regularity condition on first best rules and the weight condition $\alpha^i_{ai}/\alpha^i_{bi}\ne\sum_j\alpha^i_{aj}/\sum_j\alpha^i_{bj}$ for some $i,a,b$ , no first best direct mechanism is BIC. It uses its own model (§9.3) and is not on the goal's proof path.

Significance

The Crémer–McLean theorem says that, with correlated finite types, incentive compatibility imposes essentially no constraint: every decision rule and every interim payment rule can be implemented. In a single-unit auction this gives full surplus extraction. The result is the benchmark against which the literature on risk aversion, limited liability, collusion and the genericity of priors (Robert 1991, Laffont–Martimort 2000, Heifetz–Neeman 2006) measures its departures, and Proposition 6.6 extends it to budget-balanced mechanisms, which is what bilateral trade and public goods applications need. Propositions 6.1–6.3 are the independent-types counterpart that the correlated case breaks: they show why revenue equivalence and the ex ante/ex post budget-balance equivalence hold there and fail here. Proposition 9.1 shows the opposite failure, for interdependent values, where efficient decisions cannot be implemented even without participation or budget constraints.

All results are proved in the literature (Kosenok–Severinov's proof is omitted in the book). Apart from Farkas's alternative (Proposition 6.5), which is proved on the platform, none of them is formalized in Mathlib or on the platform; the platform's other mechanism design results (dominant-strategy results in a valuation model, revenue equivalence for symmetric independent auctions) do not cover correlated types.

Difficulty

For the goal the difficulty is the uniformity of the construction: a single payment adjustment must make truth-telling optimal against every possible deviation of every type of every agent, while leaving each type's expected payment unchanged. The obvious scoring-rule adjustment, charging $-\ln\mu(\theta_{-i}\mid\theta_i')$ , changes interim payments, and removing that change is where the Crémer–McLean condition enters. For Proposition 6.2 the envelope argument must handle convex type sets that are not open and utilities that are only convex, not differentiable. For Proposition 9.1 the obvious argument differentiates interim utility twice; the proposition does not assume that interim utility is twice differentiable, so that regularity has to be derived from the hypotheses on the interim probabilities.

Formalization scope

Three definition files carry the three models. Independent types (§6.2–6.3): type sets are arbitrary measurable spaces, the prior is the product of probability measures $\rho_i$ , and interim quantities are integrals against it. Finite correlated types (§6.4): finite type sets, a prior $\mu:\Theta\to\mathbb R$ with $\mu(\theta)>0$ and $\sum_\theta\mu(\theta)=1$ , and conditional beliefs $\mu(\theta_{-i}\mid\theta_i) = \mu(\theta)/\mu(\theta_i)$ ; the alternative set $A$ is arbitrary. Interdependent values (§9.3): finite $A$ , signals in $[0,1]^A$ with positive densities, independent across agents, linear utilities with nonzero weights $\alpha^j_{ai}$ .

Committed conventions and explicit formulas:

The Crémer–McLean condition uses nonnegative weights without a sum-to-one constraint, as Definition 6.7 prints it.
"Equivalent" in Propositions 6.4 and 6.6 means the same decision rule and the same interim expected payments at truthful reports, as Proposition 6.4 states; in Proposition 6.3 it is the report-by-report notion, which under independence is equality of the interim payment rules $T_i$ .
Proposition 6.2 adds continuity of $u_i(a,\cdot)$ on $\Theta_i$ , and Proposition 6.3 adds at least two agents; without them the printed statements are false.
Measurability, which the book omits throughout, is made explicit: decision rules are measurable, and the payment sections and utilities are integrable against the relevant interim distributions.
In Proposition 9.1 the partial derivatives are derivatives within the closed cube $[0,1]^K$ , and the weight condition is the displayed ratio inequality.

A trivializing formalization of the goal, one that proves it only for mechanisms that are already incentive compatible, or with a payment rule that is not a function of the reported type profile, or with "equivalent" weakened to "some BIC mechanism exists", is ruled out: the statement quantifies over every direct mechanism and fixes both the decision rule and every interim payment.

Reusable infrastructure: finite conditional expectations under a full-support prior, the Crémer–McLean and identifiability conditions, and the interim model with product priors. Proofs of any milestone and of the goal, including via the Farkas reference, are welcome.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
J. Crémer and R. P. McLean, "Full extraction of the surplus in Bayesian and dominant strategy auctions", Econometrica 56(6), 1988. https://doi.org/10.2307/1913096
G. Kosenok and S. Severinov, "Individually rational, budget-balanced mechanisms and allocation of surplus", Journal of Economic Theory 140(1), 2008.
P. Jehiel and B. Moldovanu, "Efficient design with interdependent valuations", Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00237
V. Krishna and E. Maenner, "Convex potentials with an application to mechanism design", Econometrica 69(4), 2001. https://doi.org/10.1111/1468-0262.00225
J.-C. Rochet, "A necessary and sufficient condition for rationalizability in a quasi-linear context", Journal of Mathematical Economics 16(2), 1987. https://doi.org/10.1016/0304-4068(87)90007-3

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Mechanism Design+1·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design VI: Rochet's Theorem — Implementability Is Cyclical MonotonicityTextbook

Motivation

Almost every screening, auction and regulation model asks the same preliminary question: which allocation rules can be made incentive-compatible by some choice of payments? In the one-dimensional models of auction theory and nonlinear pricing the answer is monotonicity: higher types must receive higher allocations. Many applications are not one-dimensional, though. Examples are multi-object auctions, multi-product pricing, and lotteries over several outcomes. For those, a characterization that uses no structure at all is needed. Rochet (1987) gave one: an allocation rule is implementable exactly when it is cyclically monotone, a condition that originates in Rockafellar's characterization of subdifferentials of convex functions. Later work on dominant-strategy implementation, the "weak monotonicity" literature of algorithmic mechanism design, and revenue equivalence all build on it.

This mission formalizes Chapter 5 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): all nine numbered results of the chapter.

Timeline. Rockafellar (1970, Theorem 24.8) characterized the cyclically monotone maps between vector spaces as the subgradient selections of convex functions. Rochet (1987) extended the idea to arbitrary alternatives and types with quasi-linear utility and proved that implementability is exactly cyclical monotonicity. Krishna and Maenner (2001) proved revenue equivalence on convex type spaces with utilities convex in the type. Bikhchandani, Chatterji, Lavi, Mu'alem, Nisan and Sen (2006) showed that for finitely many alternatives, weak monotonicity (the two-type case of cyclical monotonicity) already suffices on rich, order-based domains. Saks and Yu (2005) proved the same on convex domains.

Setting

A designer and one agent choose an alternative $a$ from a set $A$ . The agent has a type $\theta$ in a nonempty set $\Theta$ . With utility function $u : A \times \Theta \to \mathbb R$ , her payoff from $a$ when she pays $t$ is $u(a,\theta) - t$ . Neither $A$ nor $\Theta$ carries any structure.

A direct mechanism is a decision rule $q : \Theta \to A$ and a transfer rule $t : \Theta \to \mathbb R$ . It is incentive-compatible if $u(q(\theta),\theta) - t(\theta) \ge u(q(\theta'),\theta) - t(\theta')$ for all $\theta,\theta'$ . A decision rule is implementable if some $t$ makes it incentive-compatible. It is weakly monotone if $u(q(\theta_1),\theta_1) - u(q(\theta_2),\theta_1) \ge u(q(\theta_1),\theta_2) - u(q(\theta_2),\theta_2)$ for all pairs of types. It is cyclically monotone if for every finite sequence of types $\theta^1,\dots,\theta^k$ with $\theta^k = \theta^1$ ,

\sum_{\kappa=1}^{k-1}\bigl(u(q(\theta^\kappa),\theta^{\kappa+1}) - u(q(\theta^\kappa),\theta^\kappa)\bigr) \le 0 .

A complete and transitive order $R$ of $A$ induces a partial order on types: $\theta \succ_R \theta'$ if $\theta$ values every $R$ -higher alternative strictly more, relative to an $R$ -lower one, than $\theta'$ does, and neither type distinguishes $R$ -indifferent alternatives. The type set is one-dimensional if any two distinct types are $\succ_R$ -comparable, and bounded if all utility differences lie in $(-c,c)$ for some $c > 0$ . It is rich if, for some reflexive and transitive relation $R$ , every function $v : A \to \mathbb R$ with $aRb \Rightarrow v(a) \ge v(b)$ is some type's utility function. A mechanism is individually rational with outside option $a$ if every type does at least as well as with $a$ and no payment.

Formalization targets

Goal: Proposition 5.2 (Rochet)

q \text{ implementable} \iff q \text{ cyclically monotone},

for arbitrary $A$ , nonempty $\Theta$ and $u$ .

Milestones

Proposition 5.1: implementable $\Rightarrow$ weakly monotone.
Proposition 5.3: for lotteries over finitely many outcomes, $\Theta \subseteq \mathbb R^\Omega$ convex and $u(p,\theta) = p\cdot\theta$ , $q$ is implementable iff there is a convex $U$ on $\Theta$ with $U(\theta') \ge U(\theta) + q(\theta)\cdot(\theta'-\theta)$ for all $\theta,\theta'$ .
Proposition 5.4: weakly monotone $\Rightarrow$ ( $\theta \succ_R \theta' \Rightarrow q(\theta)\,R\,q(\theta')$ ), for every complete transitive $R$ .
Proposition 5.5: on one-dimensional type sets, weak monotonicity $\iff$ monotonicity with respect to $R$ .
Proposition 5.6: $A$ finite, $\Theta$ bounded and one-dimensional: monotone with respect to $R$ $\Rightarrow$ implementable.
Proposition 5.7 (Bikhchandani et al.): $A$ finite, rich and consistent domain: weakly monotone $\Rightarrow$ implementable.
Proposition 5.8 (revenue equivalence): on convex $\Theta \subseteq \mathbb R^n$ with $u(a,\cdot)$ convex and continuous, if $(q,t)$ is incentive-compatible then $(q,t')$ is iff $t' = t + \tau$ for a constant $\tau$ .
Proposition 5.9: on one-dimensional type sets with a lowest type $\underline\theta$ and a worst alternative $\underline a$ , an incentive-compatible mechanism is individually rational with outside option $\underline a$ iff $u(q(\underline\theta),\underline\theta) - t(\underline\theta) \ge u(\underline a,\underline\theta)$ .

Significance

Rochet's theorem turns the existence of payments, an infinite system of linear inequalities in unknowns $t(\theta)$ , into a condition on the decision rule alone. It underlies the characterization of implementable rules in multidimensional screening, the taxation principle, and the dominant-strategy characterizations of Chapter 7 (applied agent by agent). Propositions 5.4–5.6 recover the "monotone allocation" results of the one-dimensional chapters from it. Proposition 5.8 is the general form of the payoff-equivalence lemmas used for optimal auctions.

All results are classical and proved on paper, except Propositions 5.7 and 5.8, whose proofs the book omits and refers to the literature. None of them is formalized on Prove2Me. The platform's algorithmic-game-theory series has the weak-monotonicity half in a multi-agent valuation model (types are valuations $A \to \mathbb R$ ), not the abstract-type statement, and has no cyclical-monotonicity or Rochet result.

Difficulty

Necessity is a two-line telescoping argument. Sufficiency needs a transfer rule built from the decision rule, and the first idea fails: prices attached to alternatives chosen pair by pair (which weak monotonicity supplies) need not be globally consistent. Figure 5.1 of the book gives a three-type example that is weakly monotone but not implementable. The transfer must come from a supremum over all finite chains of types starting at a fixed type. The supremum is finite only because of cyclical monotonicity, and no finiteness, compactness or boundedness is available. Proposition 5.8 needs an envelope argument along segments in $\Theta$ without differentiability. Proposition 5.7 needs a combinatorial argument that uses richness of the domain.

Formalization scope

Alternatives and types are arbitrary Lean types A, Θ with Nonempty Θ, and the utility is u : A → Θ → ℝ. A cycle of length $k = m+1$ is a map Fin (m+1) → Θ with equal first and last entries, and its $m$ summands are indexed by Fin m. Relations are predicates A → A → Prop. For Propositions 5.3 and 5.8, types form a subset S of Ω → ℝ (resp. Fin n → ℝ) used as a subtype. Lotteries are stdSimplex ℝ Ω, and the subgradient inequality is required only at points of S.

The explicit statements are fixed as follows:

Proposition 5.8's conclusion is the exact translation form $t'(\theta) = t(\theta) + \tau$ for one $\tau$ and all $\theta$ .
Proposition 5.9's condition is the single inequality at $\underline\theta$ .
Boundedness in Proposition 5.6 is Definition 5.9's strict two-sided bound with some $c > 0$ .

Two statements are corrected from the page, each with a counterexample to the literal version recorded in its item:

Proposition 5.7 adds Bikhchandani et al.'s requirement that every type's utility respects $R$ .
Proposition 5.8 adds continuity of $u(a,\cdot)$ on $\Theta$ (automatic in the relative interior).

Both directions of Rochet's theorem are required. The necessity half alone, or a version with finite $\Theta$ , finite $A$ or bounded utilities, is a different and much weaker theorem and does not close the goal.

The development needs finite telescoping sums, suprema of sets of reals (sSup with an explicit bounded-above argument), convex functions on sets and one-dimensional convex analysis (Proposition 5.8). The definitions file is reusable for Chapters 6–8 of the series. Contributions of alternative proofs, for example Proposition 5.6 through Rochet's theorem, are welcome.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 5. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
J.-C. Rochet, "A necessary and sufficient condition for rationalizability in a quasi-linear context," Journal of Mathematical Economics 16 (1987) 191–200. https://doi.org/10.1016/0304-4068(87)90007-3
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, Theorem 24.8.
V. Krishna and E. Maenner, "Convex potentials with an application to mechanism design," Econometrica 69 (2001) 1113–1119. https://doi.org/10.1111/1468-0262.00233
S. Bikhchandani, S. Chatterji, R. Lavi, A. Mu'alem, N. Nisan and A. Sen, "Weak monotonicity characterizes deterministic dominant-strategy implementation," Econometrica 74 (2006) 1109–1132. https://doi.org/10.1111/j.1468-0262.2006.00695.x
M. Saks and L. Yu, "Weak monotonicity suffices for truthfulness on convex domains," Proceedings of the 6th ACM Conference on Electronic Commerce (2005) 286–293. https://doi.org/10.1145/1064009.1064039

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

Bellman's Dynamic Programming VIII: Multi-Stage Games, Games of Survival and the Extended Min-Max TheoremTextbook

Why multi-stage games

Chapter X of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; Princeton Landmarks edition 2010, DOI 10.2307/j.ctv1nxcw0f) carries the functional-equation method of the earlier chapters from one-player decision processes to two-player zero-sum games that are played over many stages. At each stage the two players make simultaneous choices, and those choices change the state in which the next stage is played. Games of survival are the standard example. They generalize the gambler's ruin: two players with finite resources play until one of them is ruined. The same framework is the discrete-time form of what Shapley (1953) called stochastic games. It underlies pursuit games, attrition models and the later theory of dynamic games in operations research and economics.

The chapter builds on von Neumann's min-max theorem (1928), which Bellman assumes without proof (§ 3, Eq. (3.4)). It proves three kinds of result: existence and uniqueness for the general multi-stage game equation (§§ 11–16), existence and uniqueness for games of survival with integer payoffs (§ 19), and an extended min-max theorem for ratios of bilinear forms (§ 23). Bellman proposes the ratio as a criterion for non-zero-sum games.

Setting

A matrix game is given by a real $M\times N$ matrix $A=(a_{ij})$ . Player $A$ chooses row $i$ with probability $p_i$ and player $B$ chooses column $j$ with probability $q_j$ ; $p$ and $q$ are distribution vectors (points of the standard simplex). The expected return to $A$ is

E_A(p,q)=\sum_{i,j}a_{ij}\,p_i\,q_j .

The game has value $v$ when $\max_p\min_q E_A=v=\min_q\max_p E_A$ , all extrema attained. In the Lean development this is IsMaxMinMinMaxValue, and the bilinear form is bilin.

In the general multi-stage game (§ 12) the state is a pair of vectors $P\in D\subseteq\mathbb R^n$ , $P'\in D'\subseteq\mathbb R^{n'}$ with norms $\|P\|=\sum_i|P_i|$ . In state $(P,P')$ , $A$ chooses $u$ in a choice domain $S(P,P')$ and $B$ chooses $v$ in $S'(P,P')$ . $A$ receives $R(u,v)$ , and play continues from the state $T(P,P';u,v)$ , $T'(P,P';u,v)$ with weight $h(P,P';u,v)$ . Mixed strategies $G$ , $G'$ are probability measures on the choice domains. The multi-stage game equation is

f(P,P')=\max_G\min_{G'}\iint\big[R(u,v)+h(P,P';u,v)\,f(T,T')\big]\,dG(u)\,dG'(v)=\min_{G'}\max_G[\ \cdots\ ].

A game of survival with integer payoffs (§ 19) has one integer state $x$ , the resources of $A$ out of a fixed total $d$ . $A$ is ruined at $x\le0$ and wins at $x\ge d$ . At each stage the players play the $2\times2$ game with matrix $\begin{pmatrix}-1&a\\c&-b\end{pmatrix}$ , whose entries are the transfers to $A$ .

Formalization targets

Goal: the extended min-max theorem (Chapter X, Theorem 7)

For real matrices $A=(a_{ij})$ , $B=(b_{ij})$ with $\sum_{i,j}b_{ij}p_iq_j\ge d>0$ for all distribution vectors $p,q$ ,

\max_p\min_q\frac{\sum_{i,j}a_{ij}p_iq_j}{\sum_{i,j}b_{ij}p_iq_j}=\min_q\max_p\frac{\sum_{i,j}a_{ij}p_iq_j}{\sum_{i,j}b_{ij}p_iq_j}.

It is the chapter's final result, and its statement involves only finite matrices.

Milestones

Eq. (3.4), von Neumann's theorem $V_A=V_B$ . It is already on the platform as AGT.zero_sum_minimax (existence of a saddle point) and enters as a reference.
Lemma 1: the value of a one-stage game moves by at most the largest change of its kernel, $|L(f)-L_1(F)|\le\max_{u,v}\,[\,|R-R_1|+|h|\,|f(T,T')-F(T,T')|\,]$ .
Theorem 1: under hypotheses (4a)–(4e), the multi-stage game equation has a unique solution among functions continuous on $D\times D'$ that vanish at the origin, and it is the uniform limit on bounded regions of the successive approximations.
Theorem 3: the successive approximations converge from any admissible initial function.
Theorem 4: stability, $|f(P,P')-F(P,P')|\le\sum_{n\ge0}\Delta(k^nc)$ .
Theorem 5: the game of survival equation with boundary values $0$ and $1$ has a unique solution with values in $[0,1]$ .

Significance

Theorem 7 gives a value for ratio games, the games in which a player maximizes a return per unit of a resource consumed. Bellman uses it to give a rationale for the play of non-zero-sum games (§ 24) and to derive the approximate equation (22.4) for non-zero-sum games of survival. Chapter XI, Theorem 5 generalizes it to Markovian decision processes. Theorem 1 is the existence and uniqueness result that justifies replacing an infinite game by its functional equation, and Theorems 3 and 4 make that equation usable for computation and perturbation. Theorem 5 is an early uniqueness theorem for a discrete stochastic game with absorbing boundaries.

None of these statements is formalized on the platform. Von Neumann's theorem is (AGT.zero_sum_minimax, and Sion's theorem as FamousTheorems.sion_minimax_theorem). Theorem 7 is a classical result: with a positive denominator the ratio is quasiconcave in $p$ and quasiconvex in $q$ . This mission asks for a machine-checked proof of the book's statement, by Bellman's route or by any other. Theorems 1, 3 and 4 need a formal theory of games whose mixed strategies are probability measures on moving compact choice domains. No such theory is on the platform yet.

Difficulty

The ratio in Theorem 7 is not bilinear, and in general it is neither concave in $p$ nor convex in $q$ , so neither von Neumann's theorem nor a concave-convex min-max theorem applies to it directly. For Theorem 1, the contraction argument needs each one-stage game to have a value and the value to depend continuously on the state. That requires a min-max theorem for continuous games on compact sets, together with continuity of the value when the choice domains move. In Theorem 5, existence follows from monotone iteration. The uniqueness step is the hard part: the operator is not a contraction in the sup norm, and a second solution must be ruled out even at states where the optimal mixed strategies are degenerate.

Formalization scope

Distribution vectors are points of stdSimplex ℝ ι for nonempty finite types. "Max-min equals min-max" always asserts attainment (IsGreatest/IsLeast) and never uses sSup/sInf, which return $0$ on empty or unbounded sets. Theorem 7 must not assume a saddle point; its only hypothesis is the bound on the denominator.
States are Fin n → ℝ with the $\ell^1$ norm of Eq. (12.1). Choice domains are nonempty compact sets (NonemptyCompacts), and mixed strategies are probability measures of full mass on them. "Vary continuously" in (4b), which the book does not define, is read as continuity in Mathlib's topology on nonempty compact sets (for a metric space, the topology of the Hausdorff distance).
The maxima $w(c)$ of (4d) and $\Delta(c)$ of Theorem 4 are expressed through majorants, which is equivalent to the book's condition. $k\ge0$ is stated explicitly. In Lemma 1 the kernels are assumed measurable and bounded on $S\times S'$ so that the integrals exist, and each game having a value is a hypothesis, as in Bellman's footnote 4.
Theorem 3's "converges" is stated as uniform convergence on bounded regions, the mode of Theorem 1, whose proof Theorem 3 repeats. Theorem 4's unspecified $c$ is any $c\ge\|P\|+\|P'\|$ . The book's p. 301 prints the first min-max of Theorem 4 with the subscripts $G$ , $G'$ interchanged; the equation used is that of Theorem 1.
Theorem 5 adds the implicit $d\ge1$ : for $d\le0$ the boundary conditions contradict each other. The state is an integer and $f:\mathbb Z\to\mathbb R$ .
Taking the choice domains constant would trivialize Theorem 1: condition (4d) would then force $R\equiv0$ on them. The choice domains therefore depend on the state.
Not included: Theorem 2 (optimal strategies of the infinite game, which needs a model of the game's plays), Theorem 6 (non-zero-sum survival; the boundary conditions (21.3) do not cover all states, see the moderation notes).

Contributions of reusable infrastructure are welcome: the min-max theorem for continuous games on compact sets (Eq. (4.2)), continuity of the value in the choice domains, and value iteration for contracting game operators.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics, 2010. DOI 10.2307/j.ctv1nxcw0f
J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100, 1928. DOI 10.1007/BF01448847
L. S. Shapley, Stochastic games, Proceedings of the National Academy of Sciences 39, 1953. DOI 10.1073/pnas.39.10.1095
M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8, 1958. DOI 10.2140/pjm.1958.8.171
I. L. Glicksberg, A further generalization of the Kakutani fixed point theorem, with application to Nash equilibrium points, Proceedings of the AMS 3, 1952. DOI 10.1090/S0002-9939-1952-0046638-5

9 thms2 active usersReviewed

Completed

Mathematical Physics Topology·Captain: Lucas

Assumptions of Physics I: Experimental Domains and Their Natural TopologyTextbook

Motivation

Assumptions of Physics by Gabriele Carcassi and Christine A. Aidala (book, v3.0, 2025) is a programme to derive the mathematical structures of physical theories from explicit physical requirements. Part II, "Physical Mathematics", begins (Chapter 1) by making precise what it means for a statement to be experimentally verifiable, and shows that a single physical requirement (only countably many tests can be run in an indefinite amount of time) is enough to force the familiar structures of point-set topology onto the space of outcomes of any experiment. This mission formalizes that chapter. It is the first mission of a series on the book; all declarations live in the namespace AssumptionsOfPhysics so that later missions can build on them.

Setting

A logical context is represented by its set $\Omega$ of possible truth assignments, and a statement (up to logical equivalence) by its truth set $s\subseteq\Omega$ . Negation, conjunction and disjunction are complement, intersection and union; the certainty is $\Omega$ and the impossibility is $\emptyset$ ; " $s_1$ is narrower than $s_2$ " means $s_1\subseteq s_2$ , and $s_1,s_2$ are compatible when $s_1\cap s_2\neq\emptyset$ .

An experimental domain $\mathcal D$ is a family of statements that contains $\Omega$ and $\emptyset$ , is closed under finite conjunction and countable disjunction, and has a countable basis $B\subseteq\mathcal D$ : every element of $\mathcal D$ is obtained from $B$ by finite conjunctions and countable disjunctions. Its theoretical domain $\bar{\mathcal D}$ is the closure of $\mathcal D$ under negation, finite conjunction and countable disjunction. A possibility is a non-impossible $x\in\bar{\mathcal D}$ that, for every $s\in\bar{\mathcal D}$ , is either narrower than $s$ or incompatible with it; $X$ denotes the set of possibilities. The verifiable set of a statement $s$ is $U(s)=\{x\in X: x\cap s\neq\emptyset\}$ , and the natural topology on $X$ is the topology generated by $\{U(s): s\in\mathcal D\}$ . A domain is decidable if it is closed under negation.

Formalization targets

Goal (Propositions 1.57, 1.61, 1.65)

\mathcal T_X = \{U(s) : s\in\mathcal D\},\qquad (X,\mathcal T_X)\ \text{is second-countable and } T_0 .

Milestones

Proposition 1.37: $\bar{\mathcal D}$ is closed under countable conjunction.
Proposition 1.46: any basis of $\mathcal D$ generates $\bar{\mathcal D}$ by negation and countable operations.
Proposition 1.48: the possibilities are exactly the non-impossible minterms of a basis.
Theorem 1.52: $|X|\le 2^{\aleph_0}$ .
Proposition 1.53: $X$ finite $\iff$ $\mathcal D$ finite $\iff$ $\mathcal D$ has a finite basis.
Proposition 1.56: $s=\bigvee_{x\in U(s)}x$ for $s\in\mathcal D$ .
Propositions 1.57, 1.60, 1.61, 1.65: the verifiable sets are exactly the open sets; $U(B)\cup\{X\}$ is a sub-basis; second countability; $T_0$ .
Proposition 1.66: $T_1$ $\iff$ every possibility is approximately verifiable.
Proposition 1.74 and Theorem 1.76: equivalent characterizations of decidable domains, and decidability $\iff$ discreteness of the natural topology.

Significance

The chapter's results identify the open sets of a topology with verifiable statements and its points with complete experimental answers (possibilities). Second countability and the $T_0$ axiom are thereby derived rather than assumed, and the cardinality bound $|X|\le 2^{\aleph_0}$ limits which mathematical objects can carry experimental meaning. Later chapters of the book (domain combination, properties and quantities, ensemble spaces) rely on these facts. The results are proved informally in the book; no machine-checked formalization of them is known to the drafters. A formalization fixes the precise hypotheses under which they hold (for instance, whether a basis must be countable in Propositions 1.46, 1.48 and 1.60) and provides a reusable library for the rest of the series.

Difficulty

The individual statements are elementary, but several of the book's proofs are informal about two points that a formal proof must handle. First, the possibilities must be shown to cover the space of assignments and to be atoms of $\bar{\mathcal D}$ ; the book argues through minterms of a countable basis, which needs a "disjunctive normal form" for countably generated families. Second, the natural topology is defined via arbitrary unions while experimental domains are only closed under countable disjunction; showing that every open set is still of the form $U(s)$ (Proposition 1.57) requires a second-countability / Lindelöf-type argument rather than direct closure.

Formalization scope

Statements are subsets s : Set Ω of an arbitrary type Ω (possibly empty); the experimental domain is the structure ExperimentalDomain Ω, whose field stmts is the family $\mathcal D$ . Generation by finite conjunction and countable disjunction (FinConjCountDisj) includes the empty conjunction $\Omega$ and the empty disjunction $\emptyset$ ; generation with negation (NegFinConjCountDisj) includes $\Omega$ . Possibilities form the type D.Possibility, which carries the natural topology as an instance; topological notions (SecondCountableTopology, T0Space, T1Space, DiscreteTopology) are Mathlib's. The primitive notion of verifiability (Axiom 1.27) is not modelled separately: membership in $\mathcal D$ is what all results of the chapter use. Statements involving "a basis" quantify over every basis (countable or not), as in the source. Contributions of reusable lemmas, in particular a disjunctive-normal-form lemma for countably generated families of sets, are welcome.

Selected references

G. Carcassi, C. A. Aidala, Assumptions of Physics, Ver. 3.0, December 31, 2025. https://assumptionsofphysics.org/book — Part II, Chapter 1 "Verifiable statements and experimental domains", pp. 101–146.

15 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

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