Famous Open Problems

Motivation

A set of integers is a Sidon set if all of its pairwise sums $a+b$ ($a\le b$) are different. Sidon, in connection with Fourier analysis, asked how dense such sets can be, and the question became one of the standard problems of additive combinatorics. Let

$$h(N)=\max\{|A| : A\subseteq\{1,\dots,N\},\ A \text{ Sidon}\}.$$

A counting argument shows $h(N)\le (1+o(1))\sqrt{2N}$, and the true order was settled early: $h(N)\sim\sqrt N$. What remains open is the size of the error term $h(N)-\sqrt N$. Erdős and Turán asked whether it is smaller than every power of $N$; Erdős offered $1000 for this problem (Erdős Problem #30), and it is also Problem 31 on Green's list of open problems and problem C9 in Guy's Unsolved Problems in Number Theory.

Timeline.

• 1938 — Singer constructs, for every prime power $q$, a set of $q+1$ residues modulo $q^2+q+1$ with all differences distinct. Combined with the density of primes this gives $h(N)\ge(1-o(1))\sqrt N$ (Singer 1938).
• 1941 — Erdős and Turán prove $h(N)\le N^{1/2}+O(N^{1/4})$ (Erdős–Turán 1941).
• 1969 — Lindström gives an alternative proof with the explicit bound $h(N)\le N^{1/2}+N^{1/4}+1$ (Lindström 1969).
• 2021 — Balogh, Füredi and Roy lower the constant: $h(N)\le N^{1/2}+0.998N^{1/4}$ for large $N$ (arXiv:2103.15850).
• 2022 — O'Bryant: $h(N)\le N^{1/2}+0.99703N^{1/4}$ for large $N$ (arXiv:2207.07800).
• 2023 — Carter, Hunter and O'Bryant: $h(N)\le N^{1/2}+0.98183N^{1/4}+O(1)$, with substantial computer assistance (arXiv:2310.20032).

No upper bound with an error exponent below $1/4$ is known, and no lower bound of the form $h(N)\ge\sqrt N-O(N^{\varepsilon})$ for every $\varepsilon>0$ is known either.

Setting

A set $A$ in an additive commutative monoid is Sidon if for all $i_1,j_1,i_2,j_2\in A$,

$$i_1+i_2=j_1+j_2\ \Longrightarrow\ (i_1=j_1\wedge i_2=j_2)\ \vee\ (i_1=j_2\wedge i_2=j_1).$$

For a finite set $X$, $\operatorname{maxSidon}(X)$ is the largest size of a Sidon subset of $X$ (the empty set is Sidon, so this is well defined), and

$$h(N)=\operatorname{maxSidon}(\{1,2,\dots,N\}),\qquad h(0)=0.$$

The first values are $h(1),\dots,h(15)=1,2,2,3,3,3,4,4,4,4,4,5,5,5,5$ (OEIS A143824).

Formalization targets

Goal (Erdős Problem #30)

$$\forall\varepsilon>0:\qquad h(N)-\sqrt N = O\!\left(N^{\varepsilon}\right)\quad(N\to\infty).$$

This is a two-sided statement: it asks both for an upper bound $h(N)\le\sqrt N+C_\varepsilon N^\varepsilon$ and for a matching lower bound $h(N)\ge\sqrt N-C_\varepsilon N^\varepsilon$ for large $N$. Erdős asked it as a yes/no question; the goal fixes the conjectured answer yes, so a disproof on the platform settles the question negatively.

Milestones (known results, weakest to strongest)

1. Singer's construction: $h(q^2+q+1)\ge q+1$ for every prime power $q$.
2. Singer's lower bound: $h(N)\ge(1-\varepsilon)\sqrt N$ for every $\varepsilon>0$ and all large $N$.
3. Erdős–Turán / Lindström: $h(N)\le\sqrt N+N^{1/4}+1$ for all $N$.
4. Balogh–Füredi–Roy: $h(N)\le\sqrt N+0.998N^{1/4}$ for all large $N$.
5. O'Bryant: $h(N)\le\sqrt N+0.99703N^{1/4}$ for all large $N$.
6. Carter–Hunter–O'Bryant: $h(N)\le\sqrt N+0.98183N^{1/4}+C$ for an absolute constant $C$.

Significance

The result itself. An affirmative answer would pin $h(N)$ down to $\sqrt N$ up to a sub-polynomial error, in both directions; Erdős even speculated that $h(N)=\sqrt N+O(1)$ might hold, while remarking that this is perhaps too optimistic. A negative answer would show that the Singer-type constructions or the counting upper bounds are off by a power of $N$. Either answer would be the first change in the exponent of the error term since 1941.

Formalizing it. The goal is open. All milestones are published theorems. The platform already contains weaker related results in other formalizations (for example the order-of-magnitude bounds $c\sqrt N\le \max|A|\le\sqrt{2N}+1$ for Sidon subsets of an initial segment, and the Erdős–Turán construction); the sharp bounds listed as milestones are not stated there for this $h$. The upper bounds of Balogh–Füredi–Roy and O'Bryant are elementary but delicate optimizations, and the Carter–Hunter–O'Bryant bound relies on a large computation, so formalizing it is a substantial verification task in its own right.

Difficulty

For the upper bound, every known argument counts differences $a-a'$ in short windows and loses at the scale $N^{1/4}$; improvements since 1941 only change the constant in front of $N^{1/4}$. For the lower bound, the constructions (Singer, Bose, Ruzsa) produce Sidon sets of size about $\sqrt p$ in a modulus $p$ of size about $N$, and the loss comes from the gap between $N$ and the nearest admissible modulus; bringing it below $N^\varepsilon$ requires either new constructions or information about primes in very short intervals that is far beyond current knowledge.

Formalization scope

Sidon sets are formalized for sets in an arbitrary additive commutative monoid, with the definition, the decidability instance and $\operatorname{maxSidon}$ transcribed from the formal-conjectures library (definitions IsSidon, Finset.maxSidonSubsetCard, and Erdos30.h in FormalConjectures/ErdosProblems/30.lean), placed in the namespace Erdos30. The value $h(N)$ is a natural number cast to $\mathbb R$; $\sqrt{\cdot}$ is the real square root and $N^{\varepsilon}$, $N^{1/4}$ are real powers of $N\ge 0$. The goal's $O(\cdot)$ is Mathlib's Asymptotics.IsBigO along atTop on $\mathbb N$. The goal is not trivialized by any junk value: $h$ is a genuine finite maximum, and the $O(\cdot)$ statement concerns all large $N$.

Useful infrastructure: basic lemmas on Sidon sets (hereditary under subsets, translation invariance, distinct differences), finite projective geometry or Bose's construction for the lower bounds, and prime gaps (Bertrand's postulate suffices for $h(N)\ge c\sqrt N$ with $c<1$; a prime number theorem in short intervals is needed for $1-o(1)$). Contributions of reusable Sidon-set lemmas are welcome.

Selected references

• J. Singer, A theorem in finite projective geometry and some applications to number theory, Trans. Amer. Math. Soc. 43 (1938), 377–385. https://doi.org/10.1090/S0002-9947-1938-1501951-4
• P. Erdős and P. Turán, On a problem of Sidon in additive number theory, and on some related problems, J. London Math. Soc. 16 (1941), 212–215. https://doi.org/10.1112/jlms/s1-16.4.212
• B. Lindström, An inequality for $B_2$-sequences, J. Combin. Theory 6 (1969), 211–212. https://doi.org/10.1016/S0021-9800(69)80124-9
• J. Balogh, Z. Füredi and S. Roy, An upper bound on the size of Sidon sets, Amer. Math. Monthly (2023). https://arxiv.org/abs/2103.15850
• K. O'Bryant, On the size of finite Sidon sets (2022). https://arxiv.org/abs/2207.07800
• D. Carter, Z. Hunter and K. O'Bryant, On the diameter of finite Sidon sets (2023). https://arxiv.org/abs/2310.20032
• K. O'Bryant, A complete annotated bibliography of work related to Sidon sequences, Electron. J. Combin. DS11 (2004). https://arxiv.org/abs/math/0407117
• T. F. Bloom, Erdős Problem #30, https://www.erdosproblems.com/30
• Google DeepMind, formal-conjectures, FormalConjectures/ErdosProblems/30.lean. https://github.com/google-deepmind/formal-conjectures

Motivation

Ramsey's theorem says that every red/blue colouring of the pairs of an infinite set has an infinite monochromatic subset. For well-ordered sets one can ask for more: the monochromatic set should have the same order type as the whole set. Erdős and Rado introduced the partition relation $\alpha \to (\beta, c)^2$ to measure exactly this, and asked which countable ordinals $\alpha$ satisfy $\alpha \to (\alpha, 3)^2$ — every colouring either has a red copy of the whole order or a blue triangle. Such ordinals are called partition ordinals. Every partition ordinal $\alpha>1$ is a power of $\omega$, so the question becomes: for which countable $\beta$ is $\omega^\beta$ a partition ordinal? This is Erdős Problem 592.

The question is a basic test case for ordinal Ramsey theory: it is the smallest nontrivial "unbalanced" relation (a whole order type against a finite clique), and progress on it has repeatedly required new combinatorial methods.

Timeline (as recorded on erdosproblems.com/592):

• 1957 — Specker. $\omega^2 \to (\omega^2,3)^2$, and $\omega^n \not\to (\omega^n,3)^2$ for every finite $n \ge 3$.
• 1972 — Chang. $\omega^\omega \to (\omega^\omega,3)^2$ (the subject of Erdős Problem 590). Milner extended this to $\omega^\omega \to (\omega^\omega,m)^2$ for all finite $m$; Larson (1973) gave a short proof.
• 1974 — Galvin and Larson. If $\beta \ge 3$ and $\omega^\beta$ is a partition ordinal then $\beta$ is additively indecomposable, so $\beta=\omega^\gamma$. They conjectured that every such $\beta\ge3$ works.
• 2010 — Schipperus. Writing $\beta=\omega^\gamma$: the relation holds when $\gamma$ is a sum of one or two indecomposable ordinals, and fails when $\gamma$ is a sum of four or more. This refutes the Galvin–Larson conjecture in general.

The case where $\gamma$ is a sum of exactly three indecomposable ordinals appears to be the remaining open case.

Setting

An ordinal $\alpha$ is identified with a well-ordered set $X_\alpha$ of order type $\alpha$. A red/blue colouring of the complete graph $K_\alpha$ on $X_\alpha$ assigns to every pair of distinct vertices exactly one of two colours; equivalently, it is a pair of complementary simple graphs (red, blue) on $X_\alpha$.

For ordinals $\alpha,\beta$ and a cardinal $c$, the partition relation $\alpha \to (\beta,c)^2$ holds when every red/blue colouring of $K_\alpha$ has

• a set $S \subseteq X_\alpha$, all of whose pairs are red, whose order type (with the order inherited from $X_\alpha$) is exactly $\beta$, or
• a set $T \subseteq X_\alpha$, all of whose pairs are blue, with $|T| = c$.

The Lean predicate is Erdos592.OrdinalCardinalRamsey α β c, following the encoding used by the Formal Conjectures project. A partition ordinal is an $\alpha$ with $\alpha \to (\alpha,3)^2$.

An ordinal is additively indecomposable if it is nonzero and $a+b<\beta$ for all $a,b<\beta$; the additively indecomposable ordinals are exactly the powers $\omega^\delta$. An ordinal $\gamma$ is the sum of $k$ indecomposable ordinals when

$$\gamma = \omega^{\delta_1}+\cdots+\omega^{\delta_k}, \qquad \delta_1 \ge \cdots \ge \delta_k,$$

i.e. its Cantor normal form has $k$ terms counted with multiplicity. The Lean predicate is Erdos592.IsSumOfIndecomposables k γ.

Formalization targets

Goal: the three-term case

$$\gamma \text{ countable},\ \gamma=\omega^{\delta_1}+\omega^{\delta_2}+\omega^{\delta_3}\ (\delta_1\ge\delta_2\ge\delta_3) \;\Longrightarrow\; \omega^{\omega^\gamma} \to \left(\omega^{\omega^\gamma}, 3\right)^2 .$$

This is the positive answer in the open case, as predicted by the Galvin–Larson conjecture. Because the truth is unknown, a formal disproof (exhibiting a countable $\gamma$ with three Cantor-normal-form terms for which the relation fails) is an equally valid resolution of the goal. Together with the milestones below, a proof of the goal gives a complete answer to Problem 592: for countable $\beta$, $\omega^\beta$ is a partition ordinal iff $\beta\le2$ or $\beta=\omega^\gamma$ with $\gamma$ a sum of at most three indecomposables.

Milestones (known results)

1. Specker: $\omega^2 \to (\omega^2,3)^2$.
2. Specker: $\omega^n \not\to (\omega^n,3)^2$ for $3 \le n < \omega$.
3. Chang: $\omega^\omega \to (\omega^\omega,3)^2$.
4. Galvin–Larson: $\beta \ge 3$ countable and $\omega^\beta \to (\omega^\beta,3)^2$ imply that $\beta$ is additively indecomposable.
5. Schipperus: $\gamma$ countable and a sum of one or two indecomposables imply $\omega^{\omega^\gamma} \to (\omega^{\omega^\gamma},3)^2$.
6. Schipperus: $\gamma$ countable and a sum of $k \ge 4$ indecomposables imply $\omega^{\omega^\gamma} \not\to (\omega^{\omega^\gamma},3)^2$.

Significance

The result itself. A resolution of the three-term case would, together with the results above, finish the classification of countable partition ordinals of the form $\omega^\beta$ asked for in Problem 592. Either answer is informative: a positive answer shows the threshold between the positive and negative cases lies between three and four terms, and a negative answer shows it lies between two and three.

Formalizing it. The drafter is not aware of any of the milestone results in Mathlib. The Formal Conjectures entry for Problem 590 links an external Lean formalization of Chang's theorem; the other results (Specker's positive and negative theorems, Galvin–Larson, Schipperus) have, to the best of the drafter's knowledge, no public machine-checked proofs. Formalizing them is a substantial project on its own, independent of the open case, and the goal itself is an open research problem.

Difficulty

The property is not monotone in $\beta$: it holds for $\beta=2$, fails for every finite $\beta\ge3$, holds again for $\beta=\omega$, and, by Schipperus, both holds and fails for various larger $\beta=\omega^\gamma$ depending on the number of terms in the Cantor normal form of $\gamma$. So no induction on $\beta$ can settle the question, and a naive transfer of the argument for a smaller exponent to a larger one can fail. The known positive and negative results use different arguments, and the three-term case lies exactly on the boundary between the ranges they cover.

Formalization scope

• Ordinals and cardinals are Mathlib's Ordinal.{u} and Cardinal.{u} in an arbitrary universe u; "countable" is γ.card ≤ ℵ₀.
• The graph lives on α.ToType, the canonical well-ordered type of order type α; a colouring is a pair of complementary SimpleGraphs (IsCompl red blue). A red $K_\beta$ is a red clique s with typeLT s = β; a blue $K_3$ is a blue clique of cardinality exactly 3.
• IsSumOfIndecomposables k γ requires a non-increasing list of exponents of length exactly k; without the ordering requirement, "sum of $k$" would not be well defined, since for instance $\omega+\omega^2=\omega^2$.
• ω ^ ω ^ γ means $\omega^{(\omega^\gamma)}$.
• The Galvin–Larson milestone states additive indecomposability directly as $\forall a,b<\beta,\ a+b<\beta$ (for $\beta \ge 3$ this is equivalent to $\beta=\omega^\gamma$).

The goal is not trivially satisfiable: the hypotheses hold, for example, for $\gamma=3$ and $\gamma=\omega^2+\omega+1$, and the conclusion is a genuine partition relation on an infinite ordinal.

Useful reusable infrastructure includes Cantor-normal-form combinatorics for countable ordinals, order-type calculations for subsets of $\omega^\beta$, and a library of the classical colourings (Specker-type constructions). Contributions formalizing any milestone are welcome.

Selected references

• T. F. Bloom, Erdős Problem #592, erdosproblems.com. https://www.erdosproblems.com/592 (this page lists the original references [Sp57], [Ch72], [GaLa74], [Sc10] cited below).
• E. Specker, Teilmengen von Mengen mit Relationen, Comment. Math. Helv., 1957.
• C. C. Chang, A partition theorem for the complete graph on $\omega^\omega$, J. Combinatorial Theory Ser. A, 1972.
• J. A. Larson, A short proof of a partition theorem for the ordinal $\omega^\omega$, Ann. Math. Logic, 1973/74.
• F. Galvin and J. Larson, Pinning countable ordinals, Fund. Math., 1974/75.
• R. Schipperus, Countable partition ordinals, Ann. Pure Appl. Logic, 2010.
• Formal Conjectures (Google DeepMind), Erdős Problems 590–592. https://github.com/google-deepmind/formal-conjectures

Motivation

The diagonal Ramsey number $R(k)$ is the least $n$ such that every red/blue colouring of the edges of the complete graph $K_n$ contains a monochromatic copy of $K_k$. Ramsey's theorem guarantees that $R(k)$ is finite; the question of how fast it grows is one of the central problems of extremal and probabilistic combinatorics. Erdős asked repeatedly ([Er88], [Er93]; see erdosproblems.com/77) for the value of

$$\lim_{k\to\infty} R(k)^{1/k}.$$

It is not even known whether this limit exists.

Timeline.

• 1935 — Erdős and Szekeres prove $R(k)\le\binom{2k-2}{k-1}$, so $R(k)\le 4^{k}$ and $\limsup_k R(k)^{1/k}\le 4$ ([ES35]).
• 1947 — Erdős proves $R(k) > 2^{k/2}$ for $k\ge 3$ by a counting (probabilistic) argument, so $\liminf_k R(k)^{1/k}\ge\sqrt2$ ([Er47]).
• 1975 — Spencer improves the lower bound by a factor of $2$: $R(k)\ge(1+o(1))\frac{\sqrt2}{e}\,k\,2^{k/2}$ ([Sp75]). The exponential base $\sqrt2$ has not been improved since.
• 2009, 2023 — Conlon ([Co09]) and then Sah ([Sa23]) obtain super-polynomial savings over $4^k$, but still with exponential base $4$.
• 2023 — Campos, Griffiths, Morris and Sahasrabudhe prove $R(k)\le(4-\varepsilon)^k$ for some constant $\varepsilon>0$ and all large $k$: the first exponential improvement on the upper bound ([CGMS23]).
• 2024 — Gupta, Ndiaye, Norin and Wei optimise the CGMS method and obtain $R(k)\le 3.8^{k+o(k)}$ ([GNNW24]). Balister et al. extend exponential improvements to the multicolour setting ([BBCGHMST24]).

So today, if the limit exists, it lies in $[\sqrt2,\,3.8]$.

Setting

For $n\in\mathbb N$ consider simple graphs $G$ on the vertex set $\{0,\dots,n-1\}$. A red/blue colouring of the edges of $K_n$ is the same as such a graph $G$ (the red edges) together with its complement $G^{c}$ (the blue edges). A $k$-clique of $G$ is a set of exactly $k$ vertices, any two of which are adjacent in $G$. Define

$$R(k)=\min\bigl\{\,n\in\mathbb N:\ \text{every graph } G \text{ on } n \text{ vertices has a } k\text{-clique in } G \text{ or in } G^{c}\,\bigr\}.$$

In the Lean development this is Erdos77.diagonalRamsey k. Small values: $R(0)=0$, $R(1)=1$, $R(2)=2$, $R(3)=6$, $R(4)=18$.

Formalization targets

Goal: existence of the limit

$$\exists\,L\in\mathbb R:\qquad R(k)^{1/k}\ \longrightarrow\ L\qquad (k\to\infty).$$

The original problem asks for the value of the limit, which is unknown; a goal with a hard-coded value cannot be stated honestly. The goal therefore asserts only that the limit exists (as a real number). Determining $L$ remains the ultimate aim; any proof of a specific value would in particular prove this goal.

Milestones (results from the literature)

1. Erdős 1947: $R(k)>2^{k/2}$ for all $k\ge 3$.
2. Spencer 1975: for every $\varepsilon>0$, eventually $R(k)\ge(1-\varepsilon)\frac{\sqrt2}{e}\,k\,2^{k/2}$.
3. Erdős–Szekeres 1935: $R(k)\le\binom{2k-2}{k-1}$ for all $k\ge1$.
4. Campos–Griffiths–Morris–Sahasrabudhe 2023: there is $\varepsilon>0$ with $R(k)\le(4-\varepsilon)^k$ for all sufficiently large $k$.
5. Gupta–Ndiaye–Norin–Wei 2024: for every $\delta>0$, eventually $R(k)\le 3.8^{(1+\delta)k}$, i.e. $R(k)\le 3.8^{k+o(k)}$.

Significance

The result itself. Existence of the limit would say that diagonal Ramsey numbers have a well-defined exponential growth rate — a regularity statement that is currently unknown in either direction. Even the bounds $\sqrt2\le\liminf$ and $\limsup\le 3.8$ are the products of decades of work, and the lower bound base $\sqrt2$ has resisted improvement since 1947.

Formalizing it. The goal is open. The milestones are proved results in the literature; the classical ones (Erdős–Szekeres, Erdős 1947) are natural first formalization targets, and the recent upper bounds (CGMS, GNNW) are substantial formalization projects in their own right. The status of existing machine-checked formalizations of these results is not asserted here.

Difficulty

There is no known sub- or super-multiplicativity for $R(k)$ that would give existence of the limit via Fekete's lemma: the natural product constructions relate $R(k\ell)$ to $R(k)$ and $R(\ell)$ only with losses that are too large, and the best lower and upper bounds come from entirely different methods (random colourings versus the book algorithm), so neither side controls the other.

Formalization scope

• $R(k)$ is defined as an infimum over $n$ of the property "every graph on $\mathrm{Fin}\,n$ has a $k$-clique in $G$ or in $G^{c}$". Lean's sInf of an empty set of naturals is $0$; the Erdős–Szekeres milestone shows the set is nonempty, so the infimum is the genuine Ramsey number.
• $R(k)^{1/k}$ is the real power of the real number $R(k)$ with exponent $1/k$; the value at $k=0$ is irrelevant for the limit.
• The limit is required to be a real number $L$; given the known bounds this loses nothing.
• Asymptotic statements ("for all sufficiently large $k$") are expressed with the atTop filter on $\mathbb N$; "$o(k)$" in GNNW is encoded as "for every $\delta>0$, eventually with exponent $(1+\delta)k$".
• Needed infrastructure: basic Ramsey theory for graphs on Fin n, binomial estimates, the probabilistic method for the lower bounds (Spencer uses the Lovász Local Lemma), and the CGMS book algorithm for the upper bounds. All of these are reusable beyond this mission.

Selected references

• [Er47] P. Erdős, Some remarks on the theory of graphs, Bull. Amer. Math. Soc. 53 (1947), 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-1
• [ES35] P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Math. 2 (1935), 463–470. http://www.numdam.org/item/CM_1935__2__463_0/
• [Sp75] J. Spencer, Ramsey's theorem — a new lower bound, J. Combin. Theory Ser. A 18 (1975), 108–115. https://doi.org/10.1016/0097-3165(75)90071-0
• [Co09] D. Conlon, A new upper bound for diagonal Ramsey numbers, Ann. of Math. 170 (2009), 941–960. https://doi.org/10.4007/annals.2009.170.941
• [Sa23] A. Sah, Diagonal Ramsey via effective quasirandomness, Duke Math. J. 172 (2023). https://arxiv.org/abs/2005.09251
• [CGMS23] M. Campos, S. Griffiths, R. Morris, J. Sahasrabudhe, An exponential improvement for diagonal Ramsey, arXiv:2303.09521 (2023). https://arxiv.org/abs/2303.09521
• [GNNW24] P. Gupta, N. Ndiaye, S. Norin, L. Wei, Optimizing the CGMS upper bound on Ramsey numbers, arXiv:2407.19026 (2024). https://arxiv.org/abs/2407.19026
• [BBCGHMST24] P. Balister, B. Bollobás, M. Campos, S. Griffiths, E. Hurley, R. Morris, J. Sahasrabudhe, M. Tiba, Upper bounds for multicolour Ramsey numbers, arXiv:2410.17197 (2024). https://arxiv.org/abs/2410.17197
• [Er88] P. Erdős, Problems and results in combinatorial analysis and graph theory, Discrete Math. 72 (1988), 81–92.
• [Er93] P. Erdős, Some of my favorite solved and unsolved problems in graph theory, Quaestiones Math. 16 (1993), 333–350.
• Erdős Problems, Problem #77. https://www.erdosproblems.com/77

Motivation

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

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

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

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

Timeline (as reported in the survey):

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

Setting

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

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

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

Formalization targets

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

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

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

Milestones (in the order of the survey)

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

A cellular automaton over a group $G$ with a finite alphabet $A$ is a map on configurations $x : G \to A$ that updates every cell by the same finite local rule, read off from a finite neighbourhood of that cell. Cellular automata over $\mathbb{Z}^d$ go back to von Neumann and Ulam and are a standard model in symbolic dynamics; replacing $\mathbb{Z}^d$ by an arbitrary group links the theory to geometric group theory.

In 1973 Gottschalk asked which groups $G$ have the property that every injective cellular automaton over $G$ is automatically surjective, and called such groups surjunctive. For a finite group this is the pigeonhole principle, since $A^G$ is then a finite set. For infinite groups the configuration space is an uncountable compact space and the pigeonhole principle is no longer available. Gottschalk's surjunctivity conjecture states that every group is surjunctive. It is open.

Timeline

• 1962–1963 — Moore and Myhill prove the Garden of Eden theorem for $\mathbb{Z}^2$ (and, in the same way, $\mathbb{Z}^d$): a cellular automaton is surjective if and only if it is pre-injective. In particular $\mathbb{Z}^d$ is surjunctive.
• 1969 — Hedlund (crediting Curtis and Lyndon) characterises cellular automata over $\mathbb{Z}$ as the continuous shift-commuting self-maps of $A^{\mathbb{Z}}$ (the Curtis–Hedlund–Lyndon theorem); the characterisation extends to every group.
• 1973 — Gottschalk introduces surjunctivity and states the conjecture; he records Lawton's result that residually finite groups are surjunctive.
• 1999 — Ceccherini-Silberstein, Machì and Scarabotti prove the Garden of Eden theorem for amenable groups, which implies that amenable groups are surjunctive.
• 1999–2000 — Gromov introduces what Weiss names sofic groups, and both show that sofic groups are surjunctive. Sofic groups include all residually finite groups and all amenable groups.
• Today — no group is known to be non-sofic, and no group is known to be non-surjunctive.

Setting

Fix a group $G$ and a finite nonempty set $A$ (the alphabet). A configuration is a function $x : G \to A$; the set of configurations is $A^G$. It carries the product topology, where $A$ has the discrete topology; this makes $A^G$ compact.

The left shift of $x$ by $g \in G$ is the configuration

$$(g \cdot x)(h) = x(g^{-1}h), \qquad h \in G,$$

written shift G g x in the Lean development. A map $\tau : A^G \to A^G$ is shift-equivariant (IsShiftEquivariant) if $\tau(g\cdot x) = g\cdot\tau(x)$ for all $g$ and $x$.

The group $G$ is surjunctive (IsSurjunctive) if, for every finite nonempty alphabet $A$, every map $\tau : A^G \to A^G$ that is continuous, shift-equivariant and injective is also surjective.

A map $\tau$ is a cellular automaton (IsCellularAutomaton) if there are a finite memory set $S \subseteq G$ and a local rule $\mu : A^S \to A$ with

$$\tau(x)(g) = \mu\big(s \mapsto x(gs)\big) \qquad \text{for all } x \in A^G,\ g \in G.$$

Three classes of groups appear in the milestones:

1. $G$ is residually finite (IsResiduallyFinite) if every $g \neq 1$ lies outside some normal subgroup of finite index.
2. $G$ is amenable if there is a finitely additive, left-invariant probability measure defined on all subsets of $G$ (the existing platform definition Garrido.IsAmenable).
3. $G$ is sofic (IsSofic) if for every finite $K \subseteq G$ and every $\varepsilon > 0$ there are a finite nonempty set $X$ and a map $\sigma : G \to \mathrm{Sym}(X)$ such that $\sigma_{gh}(x) = \sigma_g(\sigma_h(x))$ for at least a $(1-\varepsilon)$ fraction of the points $x \in X$ whenever $g, h \in K$, and $\sigma_g(x) \neq x$ for at least a $(1-\varepsilon)$ fraction of the points whenever $g \in K \setminus \{1\}$.

Formalization targets

Goal: Gottschalk's conjecture

$$\forall\, G \text{ group}: \quad G \text{ is surjunctive.}$$

Milestones

1. Curtis–Hedlund–Lyndon: for finite $A$, a map $\tau : A^G \to A^G$ is continuous and shift-equivariant if and only if it is a cellular automaton.
2. Subgroups: every subgroup of a surjunctive group is surjunctive.
3. Local character: if every finitely generated subgroup of $G$ is surjunctive, then $G$ is surjunctive.
4. Finite groups are surjunctive.
5. Residually finite groups are surjunctive (Lawton).
6. Amenable groups are surjunctive (Ceccherini-Silberstein–Machì–Scarabotti).
7. Sofic groups are surjunctive (Gromov; Weiss).

Significance

The result itself. A positive answer would make the implication "injective $\Rightarrow$ surjective" for cellular automata hold unconditionally, extending the pigeonhole principle from finite sets to all shift spaces $A^G$. Surjunctivity is also tied to Kaplansky's direct finiteness conjecture: for a surjunctive group $G$ and any finite field $K$, the group ring $K[G]$ is directly finite ($ab = 1 \Rightarrow ba = 1$). A counterexample would be the first known non-sofic group, since sofic groups are surjunctive.

Formalizing it. Milestones 4–7 are proved results in the literature; milestones 1–3 are standard facts of the theory. At the time of writing, none of milestones 1–3 and 5–7 is known to exist as a machine-checked proof on this platform. Formalizing them requires building the basic theory of cellular automata over groups (memory sets, local rules, induced automata on subgroups), which can be reused by other work in symbolic dynamics. The goal theorem itself is open.

Difficulty

For infinite $G$ the space $A^G$ is infinite, so no counting argument applies directly. All known proofs approximate $G$ by finite objects: finite quotients (residually finite case), Følner sets with an entropy count (amenable case), or approximate finite permutation models (sofic case). No such approximation is known to exist for every group, and it is not known whether every group is sofic. A proof of the full conjecture therefore needs either a proof that every group is sofic or an argument that does not go through finite approximations.

Formalization scope

• Groups $G$ and alphabets $A$ live in Type (universe $0$). Alphabets are finite (Fintype) and nonempty; their topology is an arbitrary topology assumed to be discrete, and $A^G$ carries Lean's product topology.
• The shift is a plain function shift, not a MulAction instance, to avoid a clash with Mathlib's pointwise action on function types.
• Amenability is taken from the existing platform definition Garrido.IsAmenable (finitely additive invariant probability measure on all subsets). Residual finiteness and soficity are defined in GottschalkSurjunctivity_Defs.
• Soficity is stated with a normalised count of points; the conditions are required for every $\varepsilon > 0$, so small $\varepsilon$ is where the content lies.
• Surjunctivity is not trivialised by the nonemptiness assumption: for a nonempty group and a nonempty alphabet, $A^G$ is nonempty and, when $G$ is infinite, uncountable.

Contributions welcome: the Curtis–Hedlund–Lyndon theorem, restriction and induction of cellular automata along subgroups, and the residually finite case are natural first steps.

Selected references

• W. H. Gottschalk, Some general dynamical notions, Recent Advances in Topological Dynamics, Lecture Notes in Math. 318, Springer, 1973, pp. 120–125. https://doi.org/10.1007/BFb0061728
• G. A. Hedlund, Endomorphisms and automorphisms of the shift dynamical system, Math. Systems Theory 3 (1969), 320–375. https://doi.org/10.1007/BF01691062
• T. Ceccherini-Silberstein, A. Machì, F. Scarabotti, Amenable groups and cellular automata, Ann. Inst. Fourier 49 (1999), 673–685. https://doi.org/10.5802/aif.1686
• M. Gromov, Endomorphisms of symbolic algebraic varieties, J. Eur. Math. Soc. 1 (1999), 109–197. https://doi.org/10.1007/PL00011162
• B. Weiss, Sofic groups and dynamical systems, Sankhyā Ser. A 62 (2000), 350–359.
• T. Ceccherini-Silberstein, M. Coornaert, Cellular Automata and Groups, Springer Monographs in Mathematics, 2010. https://doi.org/10.1007/978-3-642-14034-1
• Wikipedia, Surjunctive group. https://en.wikipedia.org/wiki/Surjunctive_group

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

Motivation

For $n \ge 1$ let $p_n$ denote the $n$-th prime. Brocard's conjecture, named after Henri Brocard, asserts that for every $n \ge 2$ there are at least four primes strictly between $p_n^2$ and $p_{n+1}^2$ (Wikipedia). It belongs to the family of "primes between consecutive squares" problems together with Legendre's conjecture, and it is a concrete, elementary-looking question about short-interval prime distribution that remains open.

Timeline

• Early 20th century — Brocard states the conjecture.
• 2023 — L. A. Ferreira (arXiv:2307.08725) proves that the conjecture holds for all sufficiently large $n$.

Setting

Primes are listed in increasing order. In the Lean development the list is 0-indexed: Nat.nth Nat.Prime k is the $k$-th prime counting from $0$, so nth 0 = 2, nth 1 = 3, nth 2 = 5, and so on. For an index $n$ write $\mathrm{prev} =$ n.nth Nat.Prime and $\mathrm{next} =$ (n+1).nth Nat.Prime, two consecutive primes. The quantity of interest is

$$\#\{\, q \text{ prime} : \mathrm{prev}^2 < q < \mathrm{next}^2 \,\}.$$

Target

Milestone (Ferreira): for all sufficiently large indices $n$,

$$4 \le \#\{\, q \text{ prime} : \mathrm{prev}^2 < q < \mathrm{next}^2 \,\}.$$

Goal (Brocard's conjecture): the same inequality for every 0-indexed $n \ge 1$, i.e. for every pair of consecutive primes starting from $(3,5)$.

Significance

A proof of the goal settles Brocard's conjecture outright. Given Ferreira's asymptotic result, the remaining work splits into making the threshold effective and closing the finite range below it, both of which would be new formal content; the milestone itself (formalizing Ferreira's analytic argument) is a substantial analytic-number-theory formalization project.

Difficulty

Unconditional results on primes in short intervals $[x, x + x^{\theta}]$ only reach exponents $\theta$ well above $1/2$, while the interval $(p_n^2, p_{n+1}^2)$ has length about $2 p_n g_n$ where $g_n = p_{n+1} - p_n$ can be small (e.g. twin primes), i.e. length on the order of the square root of its endpoint. Standard short-interval theorems therefore do not apply uniformly, and Legendre's conjecture — which would only give two primes here — is itself open.

Formalization scope

Everything is stated with Mathlib's Nat.nth Nat.Prime, Finset.Ioo (open interval, endpoints excluded) and Finset.filter Nat.Prime, followed by Finset.card. The hypothesis 1 ≤ n in the goal is the 0-indexed form of the source's "$n \ge 2$"; it is necessary, since for index $0$ (primes $2, 3$) the interval $(4, 9)$ contains only the two primes $5, 7$. The milestone uses Filter.atTop ("for all sufficiently large $n$"), with no explicit threshold. No custom definitions are required.

Selected references

• Brocard's conjecture, Wikipedia. https://en.wikipedia.org/wiki/Brocard%27s_conjecture
• L. A. Ferreira, Real exponential sums over primes and prime gaps, arXiv:2307.08725 (2023). https://arxiv.org/abs/2307.08725
• Statement adapted from the Formal Conjectures project (Apache-2.0), file BrocardConjecture.lean.

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 have not survived.

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), and it remains open as of 2026.

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 is open. A proof of this statement proves the conjecture; a disproof shows that $F$ is amenable, and settles the question the other way.

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, a proof of the goal proves it, and a disproof of it disproves the goal. 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
• N. Monod, Some comments on piecewise-projective groups of the line, Groups Geom. Dyn. 19 (2025) 459–476. doi:10.4171/ggd/883

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)

1. Smale's inequality with $K = 4$.
2. 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.
3. Tischler's optimal inequality for polynomials with only real roots, and for polynomials whose roots all have the same absolute value.
4. The Conte–Fujikawa–Lakic bound $K \le 4\frac{d-1}{d+1}$.
5. Crane's bound $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$.
6. 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