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

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$,

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

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)

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

A set $A$ of positive integers is pairwise coprime if $\gcd(a,b)=1$ for all distinct $a,b\in A$. The primes are the model example, and a recurring theme in Erdős's combinatorial number theory is that pairwise coprime sets cannot do much better than the primes on natural additive or harmonic statistics. Erdős Problem 1210 asks for a sharp version of this principle for the harmonic weight $1/(n-a)$, which measures how densely a coprime set can crowd the point $n$ from below.

Timeline.

• 1977. In [Er77c, p.64] Erdős posed a question about the primes $q_1<\dots<q_k$ in an interval $(n,m]$: is $\sum_i 1/(q_i-n)<\sum_{p<m-n}1/p+O(1)$?
• 1980. In [Er80, p.112] he wrote that he had "not stated [this] quite correctly" in [Er77c] and posed the question for arbitrary pairwise coprime sets $A\subseteq[1,n)$, which is the form recorded as Problem 1210.
• 2026. On the erdosproblems.com forum, a reduction to a counting bound for $A\cap[n-x,n)$ was suggested; it was then observed that this counting bound would itself imply an open inequality of the type $\pi(x+y)\le\pi(x)+\pi(y)+O(y/(\log y)^2)$ (compare Problem 855). The problem remains open.

Setting

Fix a natural number $n$. Consider finite sets $A$ of integers with $1\le a<n$ for every $a\in A$, and with $\gcd(a,b)=1$ for all distinct $a,b\in A$. For such a set define the reciprocal gap sum

Every term is at most $1$, and the element $a=n-d$ contributes $1/d$. Write $\sum_{p<n}1/p$ for the sum of reciprocals of the primes below $n$; by Mertens' theorem it equals $\log\log n+O(1)$. Throughout, $\pi(x)$ denotes the number of primes $p\le x$.

Target

The goal of the mission is the affirmative answer to Problem 1210: there is an absolute constant $C$ such that

for every $n$ and every pairwise coprime $A\subseteq[1,n)$. A negative answer is equally welcome and is recorded by disproving the goal statement.

The milestones are:

1. Small prime factors. For pairwise coprime $A$, at most $\pi(x)$ elements of $A\cap[n-x,n)$ have a prime factor $\le x$.
2. Partial summation reduction. If $|A\cap[n-x,n)|\le\pi(x)+O(x/(\log x)^2)$ uniformly, then the goal holds.
3. The [Er77c] variant. For the primes $q_i$ in $(n,m]$, $\sum_i 1/(q_i-n)<\sum_{p<m-n}1/p+O(1)$.

Significance

The result itself. An affirmative answer would say that, for the weight $1/(n-a)$, no pairwise coprime set beats the primes by more than a constant, and would give a quantitative form of the heuristic that coprime sets behave like sets of primes near a point. A negative answer would exhibit coprime sets that concentrate near $n$ more efficiently than the primes do in the harmonic sense. The [Er77c] variant concerns only primes, and relates the distribution of primes just above $n$ to the primes below the interval length $m-n$.

Formalizing it. Neither the goal nor the [Er77c] variant is known. The mission produces Lean statements checked against the source, a reduction (milestone 2), to be verified in Lean, that isolates exactly which counting estimate would suffice, and the elementary coprimality lemma (milestone 1). These pin down what a proof or disproof must supply.

Difficulty

The natural first attempt splits $A\cap[n-x,n)$ into elements with a prime factor $\le x$, of which there are at most $\pi(x)$, and $x$-rough elements, and then hopes that sieve bounds make the rough part $O(x/(\log x)^2)$. The obstruction is that $A$ may contain many primes in $[n-x,n)$. Bounding the number of primes in a short interval $[n-x,n)$ by $\pi(x)+O(x/(\log x)^2)$ is a form of the second Hardy–Littlewood conjecture $\pi(x+y)\le\pi(x)+\pi(y)$, which is open and known to be incompatible, in its exact form, with the prime $k$-tuples conjecture. So the counting route in milestone 2 needs input on primes in short intervals beyond current knowledge, and any proof of the goal must either supply such input or avoid pointwise counting.

Formalization scope

All objects are elementary: $A$ is a Finset ℕ, coprimality is Nat.Coprime, primes are Nat.Prime, $\pi$ is Nat.primeCounting, and the sums are real-valued. The source's $O(1)$ is encoded as an existentially quantified real constant $C$ chosen before $n$ and $A$. The source asks a yes/no question; each statement is posed in its affirmative form, and a disproof (a proof of the negation) settles the negative answer. The standing hypothesis $1\le a<n$ means every denominator $n-a$ is at least $1$, so no division-by-zero default can make the statement trivial. The window $[n-x,n)$ is written as $a\ge n-x$ with truncated natural subtraction together with $a<n$.

No new definitions are required. Useful reusable contributions include Mertens-type estimates for $\sum_{p<n}1/p$, partial summation lemmas for finite sums over $\mathbb N$, and upper bounds for primes in short intervals.

Selected references

• P. Erdős, Problems and results on combinatorial number theory. III, Number Theory Day (Proc. Conf., Rockefeller Univ., New York, 1976), (1977), 43–72. [Er77c]
• P. Erdős, A survey of problems in combinatorial number theory, Ann. Discrete Math. (1980), 89–115. [Er80]
• T. F. Bloom, Erdős Problem #1210, https://www.erdosproblems.com/1210 , and discussion thread https://www.erdosproblems.com/forum/thread/1210
• Formal Conjectures project, ErdosProblems/1210.lean, https://github.com/google-deepmind/formal-conjectures

Motivation

Addition and multiplication interact in rigid ways: a finite set of numbers that is highly structured with respect to one operation (an arithmetic progression, say) tends to be unstructured with respect to the other (a geometric progression). The sum–product problem asks for the sharp quantitative form of this principle. It was posed by Erdős and Szemerédi in 1983 (Erdős Problem 52) and has since become a central question of additive combinatorics, with applications in incidence geometry, exponential sum estimates, expanders and randomness extraction.

Timeline.

• 1983 — Erdős and Szemerédi show that $\max(|A+A|,|AA|)\ge c|A|^{1+\delta}$ for some absolute $\delta>0$ and every finite set of integers $A$, and conjecture exponent $2-\varepsilon$.
• 1997 — Nathanson obtains the explicit exponent $1+\tfrac1{31}$; Ford (1998) improves it to $1+\tfrac1{15}$.
• 1997 — Elekes, using the Szemerédi–Trotter incidence theorem, proves $|A+A|\,|AA|\gg|A|^{5/2}$ for finite sets of reals, hence exponent $5/4$.
• 2009 — Solymosi proves $|A+A|^2|AA|\gg |A|^4/\log|A|$ for finite sets of positive reals, hence exponent $4/3$ up to a logarithmic factor.
• 2015–2022 — Konyagin and Shkredov first break the $4/3$ barrier (exponent $4/3+c$ for a small explicit $c>0$); after several improvements, Rudnev and Stevens reach $4/3+2/1167$ up to logarithmic factors.

The conjecture itself remains open.

Setting

For a finite set $A\subset\mathbb Z$ define the sumset and product set

For nonempty $A$ both contain at least $|A|$ elements and at most $\binom{|A|+1}{2}$. The quantity of interest is $\max(|A+A|,|AA|)$ as a function of $|A|$.

Formalization targets

Goal (Erdős–Szemerédi conjecture)

For every $0<\varepsilon<1$ there is $C_\varepsilon>0$ such that for every finite set $A\subset\mathbb Z$,

Known lower bounds (milestones, weakest to strongest)

Sharpness

The $\varepsilon$ cannot be removed: there is no $C>0$ with $\max(|A+A|,|AA|)\ge C|A|^2$ for all $A$ (take $A=\{1,\dots,n\}$; the multiplication table $|AA|$ is $o(n^2)$ by Erdős).

Significance

A proof of the goal would settle the sharp form of the sum–product phenomenon over $\mathbb Z$. Sum–product estimates are an input to incidence bounds, to Bourgain–Katz–Tao-type results over finite fields, and to explicit constructions in theoretical computer science; improvements of the exponent over $\mathbb R$ have come together with new incidence-geometric tools.

Formalization status: the milestones are published theorems (Erdős–Szemerédi, Elekes, Solymosi, Rudnev–Stevens, Erdős's multiplication table bound), but their proofs are not known to be formalized in Lean/Mathlib. The Szemerédi–Trotter theorem, multiplicative energy, and the Elekes and Solymosi arguments are reusable infrastructure. The goal itself is an open problem.

Difficulty

Incidence-geometric methods (Szemerédi–Trotter and its descendants) naturally produce exponents near $4/3$, and passing beyond $4/3$ has required intricate higher-energy arguments yielding only small gains. None of the existing approaches is known to reach exponents close to $2$; even over $\mathbb Z$, where arithmetic structure is available, the best general bounds are the real-number ones.

Formalization scope

Sets are Finset ℤ; $A+A$ and $AA$ are Mathlib's pointwise sumset and product set (open scoped Pointwise), and cardinalities are cast to $\mathbb R$. Powers are real powers (Real.rpow). The empty set is allowed; the hypothesis $\varepsilon<1$ keeps every exponent positive, so the empty set contributes the trivial inequality $0\ge 0$ rather than a junk value $0^0=1$. The constant $C$ may depend on $\varepsilon$ but not on $A$. The Solymosi milestone is stated for $|A|\ge2$ so that $\log|A|>0$.

The statements are for integer sets only; results proved over $\mathbb R$ specialise to them. Contributions of general-purpose infrastructure (Szemerédi–Trotter over $\mathbb R$, multiplicative energy, bounds for the multiplication table) are welcome.

Selected references

• P. Erdős, E. Szemerédi, On sums and products of integers, Studies in Pure Mathematics, Birkhäuser, 1983, 213–218.
• M. B. Nathanson, On sums and products of integers, Proc. Amer. Math. Soc. 125 (1997), 9–16.
• K. Ford, Sums and products from a finite set of real numbers, Ramanujan J. 2 (1998), 59–66.
• G. Elekes, On the number of sums and products, Acta Arith. 81 (1997), 365–367.
• J. Solymosi, Bounding multiplicative energy by the sumset, Adv. Math. 222 (2009), 402–408. https://arxiv.org/abs/0806.1040
• S. V. Konyagin, I. D. Shkredov, On sum sets of sets having small product set, Proc. Steklov Inst. Math. 290 (2015), 288–299. https://arxiv.org/abs/1503.05771
• M. Rudnev, S. Stevens, An update on the sum-product problem, Math. Proc. Cambridge Philos. Soc. 173 (2022), 411–430. https://arxiv.org/abs/2005.11145
• Erdős Problem 52, https://www.erdosproblems.com/52

Erdős Problem 68: Irrationality of sum 1/(n! - 1)

Problem Statement & Context

Erdős Problem 68 asks whether the infinite series 184987\sum_{n=2}^{\infty} rac{1}{n! - 1}184987 is irrational.

Paul Erdős proved in 1948 that \sum_{n=1}^{\infty} rac{1}{2^n - 1} is irrational, but the problem for factorial denominators ! - 1$ remains open.

Main Target Theorem

Motivation

Write the primes in increasing order, take the absolute differences of consecutive entries, take the absolute differences of the resulting row, and repeat. Every row produced this way appears to begin with $1$:

Gilbreath's conjecture asserts that this never fails. The observation is due to Norman L. Gilbreath (1958), who rediscovered a statement already published by François Proth in 1878 together with an argument that is not accepted as a proof. It is attractive because it is elementary to state and because it is one of the few statements about the primes whose difficulty is not visibly analytic: it concerns the combinatorics of iterated differences rather than the distribution of primes directly.

Timeline.

• 1878 — Proth states the property and publishes a proof that is now regarded as erroneous.
• 1958 — Gilbreath rediscovers the pattern; it circulates as a conjecture.
• 1959 — Killgrove and Ralston verify the leading entry for the first $63{,}418$ rows (MTAC 13 (1959), 121–122).
• 1993 — Odlyzko reports a verification of the leading entry for all rows of index at most $\pi(10^{13}) \approx 3.4 \times 10^{11}$, using an argument that propagates a long block of entries lying in $\{0,2\}$ downwards through the triangle (Math. Comp. 61 (1993), 373–380).

No proof is known.

Setting

Let $p_0 = 2 < p_1 = 3 < p_2 = 5 < \dots$ be the increasing enumeration of the prime numbers, indexed from $0$. Define the rows of the Gilbreath triangle by

Thus $d^k$ is an infinite sequence of natural numbers for every $k$, row $0$ is the sequence of primes, row $1$ is the sequence of prime gaps $p_{n+1}-p_n$, and each later row is the sequence of absolute differences of consecutive entries of the row above it. Only the leading entry $d^k(0)$ of each row is at issue.

More generally, for an arbitrary sequence $a : \mathbb{N} \to \mathbb{N}$ write $(\Delta a)(n) = |a(n+1) - a(n)|$ and $\Delta^j a$ for the $j$-fold iterate, so that $d^k = \Delta^k p$.

Formalization targets

Goal

This is the conjecture in its standard form: every row after the row of primes begins with $1$. It fixes no constants and no ranges, so no computational advance can invalidate it.

Milestones

The milestone list collects the statements that a proof, or a further computational verification, would be built from: the two low-level structural facts about the triangle (row $1$ is the gap sequence; from row $1$ on, the leading entry is odd and all later entries are even), a finite verification of the first rows, and the two statements underlying Odlyzko's method — the propagation lemma for an arbitrary sequence beginning $1$ and continuing in $\{0,2\}$, and the reduction of the conjecture to the existence, for each row index, of an earlier row with a long enough block of entries in $\{0,2\}$.

Significance

The result itself. The conjecture is not known to imply other open statements about the primes, and its interest lies elsewhere: it is a test case for how much of the fine structure of the prime sequence is forced by coarse information. The propagation mechanism shows that the conjecture for a given row index follows from purely local data about an earlier row, and that mechanism is what every verification to date has relied on. A proof would have to show that such blocks of entries in $\{0,2\}$ always appear early enough, which is a statement about the density of small prime gaps in disguise.

Formalizing it. Nothing here is currently formalized: Mathlib has the prime enumeration $n \mapsto p_n$ (Nat.nth Nat.Prime) and the basic facts about it, but not the iterated-difference triangle nor any of its properties. This mission contributes the definition of the triangle, the structural facts about its rows, and a machine-checked version of the reduction step that all computational work on the problem uses. The goal theorem itself is open — the milestones are known mathematics, and each is provable with current tools, while the goal is not.

Difficulty

The obvious attack is induction on the row index: to see that $d^{k+1}(0) = 1$ it suffices to know that $d^{k}(0) = 1$ and $d^{k}(1) \in \{0,2\}$. But controlling $d^{k}(1)$ requires controlling $d^{k-1}(1)$ and $d^{k-1}(2)$, and so on: the invariant that closes is not "the row begins with $1$" but "the row begins with $1$ and its next $m$ entries lie in $\{0,2\}$", and each application of the difference operator consumes one entry of that block. So a finite block of good entries only carries the conclusion a finite number of rows further down, and the conjecture needs such blocks to keep reappearing forever, arbitrarily far down the triangle. Nothing is known that produces them.

A second warning, due to Hallard Croft: the property is not specific to the primes. Sequences that start with $2$, continue with odd numbers, and have gaps that are not too large empirically exhibit the same behaviour, so any proof that uses only such coarse features would prove a much more general statement — and conversely, an argument exploiting deep properties of primes is likely to be proving the wrong thing.

Formalization scope

Rows are total functions $\mathbb{N} \to \mathbb{N}$, defined for every index, and the whole triangle is a single family indexed by the row number. Differences are taken as Int.natAbs of a difference computed in $\mathbb{Z}$, so truncated natural subtraction never occurs; the one place where $\mathbb{N}$-subtraction does appear is the milestone identifying row $1$ with the gap sequence, where the subtraction is justified by monotonicity of $n \mapsto p_n$.

Primes are indexed from $0$ via Mathlib's Nat.nth Nat.Prime, so $p_0 = 2$; rows are indexed with row $0$ the primes, and the goal quantifies over all $k \ge 1$ in the form d (k + 1) 0 = 1, with no upper bound and no extra hypothesis, so no vacuous or finitely-truncated reading of the goal is available. The general difference operator is stated for arbitrary sequences $\mathbb{N} \to \mathbb{N}$, which is what makes the propagation lemma usable as a black box, and reusable beyond this mission.

A complete development needs no analytic input for the milestones: Mathlib's Nat.nth, Nat.prime_nth_prime, Nat.nth_prime_zero_eq_two and the strict monotonicity of the prime enumeration suffice. Contributions that would extend the mission beyond its current list: a formal version of a concrete computational verification (checking that the leading entries of the first $N$ rows are $1$ for an $N$ well beyond the hand-checkable range), and formalizations of the general statement for non-prime sequences of the Croft type.

Selected references

• N. L. Gilbreath, as reported in R. B. Killgrove and K. E. Ralston, On a conjecture concerning the primes, Mathematical Tables and Other Aids to Computation 13 (1959), 121–122. https://doi.org/10.1090/S0025-5718-1959-0105398-3
• A. M. Odlyzko, Iterated absolute values of differences of consecutive primes, Mathematics of Computation 61 (1993), 373–380. https://doi.org/10.1090/S0025-5718-1993-1192979-9
• Gilbreath's conjecture, Wikipedia. https://en.wikipedia.org/wiki/Gilbreath%27s_conjecture

Motivation

Galois theory attaches to every finite Galois extension $L/K$ a finite group $\mathrm{Gal}(L/K)$, the group of field automorphisms of $L$ fixing $K$ pointwise, and the fundamental theorem of Galois theory turns the subfield structure of $L/K$ into the subgroup structure of that group. The inverse Galois problem asks whether this correspondence is surjective over the rationals: given an arbitrary finite group $G$, is there a Galois extension $L/\mathbb{Q}$ with $\mathrm{Gal}(L/\mathbb{Q}) \cong G$? The question was posed in the early nineteenth century and is unsolved.

What makes it a live research question rather than a curiosity is that the known positive results come from genuinely different sources, and none of them covers all finite groups.

• Cyclic and, more generally, finite abelian groups are realizable over $\mathbb{Q}$ by an explicit cyclotomic construction resting on Dirichlet's theorem on primes in arithmetic progressions.
• Symmetric and alternating groups are realizable over $\mathbb{Q}$; this is due to Hilbert, who realized them first over the rational function field $\mathbb{Q}(t)$ and then specialized $t$ using his irreducibility theorem.
• Every finite solvable group is realizable over $\mathbb{Q}$; this is Shafarevich's theorem (I. R. Shafarevich, The imbedding problem for splitting extensions, Dokl. Akad. Nauk SSSR 120 (1958), 1217–1219), obtained by solving embedding problems.
• Over $\mathbb{C}(t)$ — and over $K(t)$ for any algebraically closed $K$ of characteristic zero — every finite group is realizable, by the Riemann existence theorem. The obstruction to the goal is not the group theory; it is descending the field of constants to $\mathbb{Q}$.
• Case-by-case work covers large finite lists: all transitive permutation groups of degree at most $23$, and every sporadic simple group, are known to be realizable over $\mathbb{Q}$.

Setting

Fix a field $K$ and a group $G$. A Galois realization of $G$ over $K$ is a field $L$ equipped with a $K$-algebra structure such that the extension $L/K$ is Galois — normal and separable — together with a group isomorphism

where $\mathrm{Gal}(L/K)$ denotes the group of $K$-algebra automorphisms of $L$ under composition. The group $G$ is realizable over $K$, written IsRealizable K G, when at least one Galois realization of $G$ over $K$ exists. No finiteness of $L/K$ is imposed in the definition; it is automatic once $G$ is finite, because an infinite Galois extension has infinite automorphism group.

Two base fields beyond $\mathbb{Q}$ appear throughout. $K(t)$ denotes the field of rational functions in one variable over $K$, written RatFunc K; and for the statement that a group is realizable over some number field, the base field ranges over the intermediate fields of $\mathbb{C}/\mathbb{Q}$.

Formalization targets

Goal — the inverse Galois problem

The goal fixes no degree, no polynomial and no construction: it asserts only the shape of the truth, so no later refinement of the known constructions can invalidate it.

Milestones — the known partial results

The last milestone is the Hilbert-irreducibility descent step; together with the geometric milestones it makes precise which half of the classical programme is missing.

Significance

The result itself would settle a two-century-old question and, with it, the surjectivity of the Galois correspondence over $\mathbb{Q}$: every abstract finite group would be known to arise from an explicit arithmetic object, a polynomial with rational coefficients. Its absence is felt in practice — constructing a single new Galois group over $\mathbb{Q}$ is publishable work, as the recent additions of the degree-$17$ group $17T7$ (van Bommel–Costa–Elkies–Keller–Schiavone–Voight, 2024) and of the Mathieu group $M_{23}$ show.

Formalizing it produces something available today independently of the goal: a machine-checked library of the known realizability results. Mathlib has the fundamental theorem of Galois theory, cyclotomic extensions, the Kronecker–Weber theorem, solvability of groups and symmetric/alternating group theory, but it does not have a predicate for "$G$ is a Galois group over $K$", nor any of the milestones above. Every milestone here is a proved theorem of classical number theory and an unformalized one; the cyclic and abelian cases are within reach of current Mathlib, while the Shafarevich and Riemann-existence milestones are substantial formalization projects in their own right.

Difficulty

The obvious strategy fails at a well-understood point. Over $\mathbb{C}(t)$ the problem is solved: by the Riemann existence theorem every finite group occurs as the deck-transformation group of a branched cover of the projective line. Hilbert's irreducibility theorem then descends realizability from $\mathbb{Q}(t)$ to $\mathbb{Q}$. What is missing is the step in between: producing the cover over $\mathbb{Q}$ rather than over $\mathbb{C}$, i.e. showing that the geometric solution can be chosen with rational field of constants. The rigidity method makes this work for many groups, but there is no known argument covering all of them; an approach that only produces realizability over some number field is not enough, and that weaker statement is included as a milestone precisely to mark the line.

A second, purely formal difficulty: the milestones are classical but their published proofs are long. Shafarevich's theorem rests on a delicate analysis of embedding problems, and the Riemann existence theorem is analytic input that Mathlib does not currently have in the required form.

Formalization scope

The mission fixes one definition file, published first, carrying the structure GaloisRealization and the one-field class IsRealizable. Conventions it commits to:

• IsGalois K L is Mathlib's Galois condition (normal and separable); finiteness of the extension is not assumed.
• The isomorphism is with the full automorphism group $L \simeq_{\mathrm{alg}[K]} L$, not with a quotient or a subgroup of it.
• The carrier $L$ of a realization is required to live in the same universe as $K$. This costs no generality for the statements of the mission — for finite $G$ a realization is a finite extension of $K$ — and keeps every statement universe-monomorphic.
• $\mathrm{Sym}(S)$ is Equiv.Perm S for a finite type $S$, and $A_n$ is alternatingGroup (Fin n); degenerate small cases are included rather than excluded.
• Solvability is Group.IsSolvable.