What the constant is

Euler's constant $\gamma$ measures the gap between the harmonic numbers and the logarithm:

$$\gamma \;=\; \lim_{n\to\infty}\left(\sum_{k=1}^{n}\frac{1}{k} \;-\; \log n\right) \;=\; 0.5772156649\ldots$$

It appears wherever the harmonic series is compared against an integral, and it is the value at $1$ of the digamma function, $\psi(1) = -\gamma$, equivalently $\gamma = -\Gamma'(1)$. Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown.

What is being asked

For $\pi$ and $e$ the arithmetic questions were settled long ago: both are irrational and transcendental. For $\gamma$, neither is known. It is not known whether $\gamma$ is irrational, and a fortiori not whether it is transcendental, though it is universally expected to be both.

The goal theorem of this mission is transcendence,

$$\gamma \notin \overline{\mathbb{Q}},$$

with irrationality carried as a separate, weaker target — a proof of transcendence yields irrationality immediately, but not conversely, and irrationality alone would already be a landmark.

What is actually known

Progress has come in three forms, and the milestones below formalize each.

Conditional bounds on a putative denominator. If $\gamma$ were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing $\gamma$ to $30{,}000$ places by an algorithm built on modified Bessel functions, showed any denominator exceeds $10^{15000}$; a continued-fraction analysis by Papanikolaou (1997) pushed this past $10^{244663}$. These are not steps toward a proof so much as a measurement of how far brute computation can go.

Disjunctive results. The strongest unconditional statements pair $\gamma$ with the Euler–Gompertz constant

$$\delta \;=\; \int_0^{\infty} \frac{e^{-u}}{1+u}\, du \;=\; 0.5963473623\ldots$$

Aptekarev, building on work of Mahler and Shidlovskii, observed that at least one of $\gamma$ and $\delta$ is irrational. Rivoal later strengthened this to at least one of them is transcendental. Neither argument isolates which, and that is precisely the obstruction: the Padé-approximation machinery that controls the pair does not separate them.

Irrationality criteria. Sondow, adapting Beukers' treatment of Apéry's theorem for $\zeta(3)$, gave criteria equivalent to the irrationality of $\gamma$ in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it.

Timeline

• 1734 — Euler introduces the constant and computes it to six decimals.
• 1790s–1800s — Mascheroni computes further digits; the constant acquires its second name.
• 1873 — Hermite proves $e$ transcendental; 1882 — Lindemann does the same for $\pi$. The methods do not reach $\gamma$.
• 1980 — Brent and McMillan: if $\gamma = p/q$ then $q > 10^{15000}$.
• 1997 — Papanikolaou: the same denominator exceeds $10^{244663}$.
• 2009 — Aptekarev: at least one of $\gamma$, $\delta$ is irrational.
• 2012 — Rivoal: at least one of $\gamma$, $\delta$ is transcendental.
• 2010s — Murty, Saradha and others obtain transcendence results for generalized Euler–Lehmer constants, again leaving $\gamma$ itself untouched.

Formalization notes

Mathlib provides the constant as Real.eulerMascheroniConstant, defined as the limit of $\sum_{k\le n} 1/k - \log n$, together with the identifications $\psi(1) = -\gamma$ and $\gamma = -\Gamma'(1)$ and the numeric bounds $1/2 < \gamma < 2/3$. Irrational and Transcendental ℚ are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.

Egyptian fractions and the Erdős–Straus question

A unit fraction is the reciprocal of a positive integer. The Erdős–Straus conjecture asks whether the particularly simple rational number $4/n$ always admits an expansion with three such terms. Its difficulty lies in obtaining a fixed number of terms for every denominator: general algorithms for Egyptian fractions do not give this three-term guarantee.

The conjecture is open. This mission adopts the exact statement maintained as Erdős Problem 242. It aims to formalize established reductions and provide a precise frontier for further work; it does not present a proof of the universal conjecture.

The historical formulations vary. Erdős’s 1950 paper, pp. 193–195, discusses distinct unit fractions and attributes the conjecture jointly to himself and Straus. His 1961 problem I.32, p. 238, allows positive denominators without specifying distinctness, while the 1979 statement, problem 9, p. 70, explicitly orders distinct denominators. The earliest published discussion may be Obláth’s 1950 paper, submitted in 1948; it attributes the question to Erdős, as explained by Bloom–Elsholtz, pp. 238–239.

The main developments relevant here are:

• 1950: Obláth’s sufficient condition using a prime divisor of $n+1$ congruent to $3$ modulo $4$.
• 1965–1969: Yamamoto’s congruence analysis and Mordell’s exposition reduce the remaining prime cases to six classes modulo $840$.
• 1970–1971: Vaughan bounds the density of possible exceptions; Terzi develops a stronger congruence sieve modulo $120120$.
• 2013–2022: Elsholtz–Tao analyze representation counts and soluble polynomial congruences; Bloom–Elsholtz give an explicit equivalent covering formulation.
• 2025: Computational verification is reported through $10^{18}$. Pomerance–Weingartner study the more general Erdős–Straus–Schinzel problem, including quantitative dependence on a variable numerator.

The exact property

For a natural number $n$, write $\mathrm{IsErdosStraus}(n)$ for the following literal property:

$$\exists x,y,z\in\mathbb N,\qquad 1\le x<y<z,\qquad \frac4n=\frac1x+\frac1y+\frac1z.$$

Every fraction is evaluated in $\mathbb Q$. The predicate contains only these witnesses, inequalities, and equality. The required range of the conjecture is $n>2$; distinctness is part of the mathematical target. In particular, the prime $2$ cannot simply be imported from a formulation permitting repeated denominators. The boundary value $n=3$ is included, with denominators $1,4,12$.

Formalization targets

The unresolved root goal is

$$\forall n\in\mathbb N,\quad n>2\Longrightarrow\mathrm{IsErdosStraus}(n).$$

The supporting milestones concern established mathematics. Denominator clearing relates the rational equation to $4xyz=n(yz+xz+xy)$ under strict positivity. Positive scaling transports a solution for $n$ to one for $kn$ while preserving the strict order. An explicit even-number family supplies the case needed for the prime reduction.

The elementary families cover $3\mid n$, $n\equiv2\pmod3$, $n\equiv3\pmod4$, and $n\equiv5\pmod8$, with the displayed witnesses and their integrality and strict ordering recorded in separate statements. Together with the even case, they solve every $n>2$ outside $1\pmod{24}$. The useful reduction is an equivalence between the root goal and its restriction to primes $p\equiv1\pmod{24}$; the ordinary prime reduction is also stated separately. The classical scaling and residue observations are discussed in Bloom–Elsholtz, p. 239.

Obláth’s milestone says that $\mathrm{IsErdosStraus}(n)$ holds for $n>2$ whenever $n+1$ has a prime divisor $q\equiv3\pmod4$. This condition is explicitly recorded in the introduction of Pomerance–Weingartner, which identifies the original Obláth reference. The exact distinctness requirement is retained in this mission.

The Mordell–Yamamoto milestone asks for a decomposition for every prime $p>2$ satisfying

$$p\bmod840\notin\{1,121,169,289,361,529\}.$$

The actual existence claim is the theorem to prove. It has no hypothesis asserting that these classes are covered. Yamamoto’s original paper, §§3–4, pp. 42–46, supplies the congruence framework and prints this residual list. The same list appears in the current Erdős Problems record. The list printed on p. 239 of Bloom–Elsholtz instead contains $49$ and omits $529$; that discrepant list is not used here. The historical papers often permit repeated denominators, so producing distinct ordered witnesses is an explicit part of the formalization obligation.

What these results provide

The elementary infrastructure gives reusable certificates and transports for exact rational decompositions. The reductions identify a mathematically meaningful remaining domain without assuming the conjecture. Completion of the modulo-$840$ milestone would leave the prime cases in its six residual classes as the classical research frontier; those classes are not asserted to consist of counterexamples.

Later targets include Terzi’s 1971 sieve, whose publisher abstract reports 198 residual classes modulo $120120$, and Vaughan’s density theorem, bounding the exceptional count by $X\exp(-c(\log X)^{2/3})$ for a positive constant $c$. Neither is a core Lean statement in this draft. No unaudited list of 198 classes is supplied.

Elsholtz–Tao provide counting results and a classification of polynomially soluble congruences. Bloom–Elsholtz, Theorem 1, pp. 239–240, characterize their conjecture by coverage of all primes by classes

$$-a/c\pmod{4acd-1}\quad(a,c,d\ge1),$$

or

$$-(4c^2d+1)/k\pmod{4cd}\quad(c,d,k\ge1,\ k\mid4c^2d+1).$$

Here division by $c$ denotes a modular inverse; division by $k$ is exact integer division. The authors are Bloom and Elsholtz, not Bradford and Elsholtz. This is a later formalization target: an initial core theorem is not included until the translation between that paper’s denominator convention and the present strict convention is separately formalized. Pomerance–Weingartner address growing numerators in the generalized problem; their exceptions are not counterexamples to the fixed numerator $4$ conjecture.

The remaining difficulty

Congruence identities prove infinite families only when the identities and their arithmetic hypotheses are established for arbitrary parameters. Checking finitely many representatives with a search program does not prove that all future values in an arithmetic progression work. Density estimates also allow an exceptional set and therefore do not settle the universal statement.

The current record cites Mihnea–Bogdan (2025) for computational verification through $10^{18}$. This is reported computational evidence, not a Lean-certified theorem in this mission. No universal conclusion or periodicity assertion is inferred from it.

Formalization scope

The development uses natural-number denominators, exact rational arithmetic, integer polynomial identities, divisibility, primality, and natural-number remainders. Definitions are transparent. The root is not hidden in a typeclass, structure field, certificate, or extra assumption, and its quantifier is not bounded. The existing Google DeepMind transcription is a statement reference, not an imported proof.

The draft targets Mathlib 0df444a360eaa60ab8c11dca51a86af692955474 with Lean 4.33.1. Every proposed statement has been locally elaborated and supplied with an independent read-back. Statement elaboration with sorry is not proof verification. The accompanying local proof audit distinguishes the proved supporting results from the open root and the remaining modulo-$840$ formalization task.

Selected references

• Erdős, Az … egyenlet egész számú megoldásairól, Mat. Lapok 1 (1950), 192–210; original scan.
• Erdős–Graham, Old and New Problems and Results in Combinatorial Number Theory (1980), chapter IV; author’s institutional scan.
• Obláth, Sur l’équation diophantienne $4/n=1/x_1+1/x_2+1/x_3$, Mathesis 59 (1950), 308–316; bibliographic record, also cited in Pomerance–Weingartner.
• Yamamoto, On the Diophantine Equation $4/n=1/x+1/y+1/z$, Mem. Fac. Sci. Kyushu Univ. A 19 (1965), 37–47; original paper.
• Mordell, Diophantine Equations, Academic Press (1969), chapter 30, pp. 287–290; publisher record.
• Terzi (1971), Vaughan (1970), Elsholtz–Tao (2013), Bloom–Elsholtz (2022), Mihnea–Bogdan (2025), and Pomerance–Weingartner (2025/2026): primary sources linked at their statements above.

Motivation

A unit fraction is the reciprocal $1/n$ of a positive integer. The number $1$ can be written as a sum of distinct unit fractions in infinitely many ways — $1 = \tfrac12+\tfrac13+\tfrac16$, $1 = \tfrac12+\tfrac14+\tfrac16+\tfrac1{12}$, and so on — and the combinatorics of such representations is one of the oldest recurring themes in Erdős's problem lists. Most questions in the area concern size: how many terms are needed, how small the largest denominator can be, how large the smallest one must be. Erdős Problem 287 asks instead about the shape of a representation: how tightly can the denominators be packed?

Order the denominators increasingly and look at their consecutive differences. For $1 = \tfrac12+\tfrac13+\tfrac16$ the differences are $1$ and $3$. The question is whether a difference of at least $3$ must always occur, in every representation of $1$, no matter how many terms it has. The problem is recorded in Erdős and Graham's 1980 problem book (ErGr80, p. 33) and was selected for the booklet of favourite problems prepared for the 1999 Budapest conference on Erdős's mathematics ([Va99, 1.15]). It remains open.

Timeline. The weaker statement that some difference must be at least $2$ — equivalently, that $1$ is never the sum of the reciprocals of a block of consecutive integers — is classical. Theisinger (1915) proved that the harmonic number $H_n$ is not an integer for $n \ge 2$, using Bertrand's postulate. Kürschák (1918) introduced the $2$-adic argument that proves the general block statement: for $m \le n-2$, the difference $H_n - H_m$ is not an integer. Erdős's 1932 paper [Er32], whose title translates as "A generalisation of an elementary number-theoretic theorem of Kürschák", extends the result from blocks of consecutive integers to arithmetic progressions; the erdosproblems.com entry for Problem 287 cites it for the difference-$\ge 2$ bound. Nothing stronger appears to be known: the passage from $2$ to $3$ is the open part, and no partial result is recorded in the entry beyond a conditional one, namely that the conjecture would follow for all but finitely many exceptions if it were known that for every large $N$ there is a prime $p \in [N, 2N]$ with $(p+1)/2$ also prime.

Setting

Fix an integer $k \ge 2$ and integers

$$1 < n_1 < n_2 < \cdots < n_k$$

with

$$1 \;=\; \frac{1}{n_1} + \frac{1}{n_2} + \cdots + \frac{1}{n_k},$$

the sum taken in $\mathbb{Q}$. Call such a tuple a representation of length $k$. The denominators are strictly increasing, hence distinct, and all exceed $1$: the value $n_1 = 1$ is excluded because $1/1$ already exhausts the total. The gaps of the representation are the $k-1$ consecutive differences $n_{i+1} - n_i$ for $1 \le i \le k-1$, and its maximal gap is $\max_i (n_{i+1} - n_i)$.

Representations exist for every $k \ge 3$, and for $k = 1$ only the excluded $n_1 = 1$; no representation of length $2$ exists. Examples: $(2,3,6)$ with gaps $1, 3$; $(2,4,6,12)$ with gaps $2,2,6$; $(3,4,6,10,12,15)$ with gaps $1,2,4,2,3$.

Formalization targets

Goal — Erdős Problem 287

$$\text{every representation } 1 < n_1 < \cdots < n_k \ (k \ge 2) \text{ of } 1 \text{ satisfies } \max_{1 \le i < k} (n_{i+1} - n_i) \;\ge\; 3.$$

This is the open conjecture, stated with no bound on $k$ and no restriction on the denominators beyond those in Setting. It is the weakest form that captures the question: asserting a bound for one particular $k$, or for denominators in some range, would be a different and strictly easier statement.

Milestone — the gap-two bound (Kürschák; Erdős [Er32])

$$\text{every representation satisfies } \max_{1 \le i < k}(n_{i+1} - n_i) \;\ge\; 2.$$

Equivalently: no block of two or more consecutive integers has reciprocals summing to $1$. This is closed mathematics and the natural first target.

Milestone — the classical block theorem (Kürschák)

$$\text{for } n \ge 1 \text{ and } k \ge 2, \qquad \sum_{i=0}^{k-1} \frac{1}{n+i} \notin \mathbb{Z}.$$

The gap-two bound is an immediate consequence, since a representation all of whose gaps equal $1$ is exactly a block of consecutive integers.

Milestone — sharpness

$$1 = \tfrac12+\tfrac13+\tfrac16 \text{ is a representation all of whose gaps are at most } 3.$$

So the constant $3$ in the goal is optimal and cannot be replaced by $4$.

Significance

The result itself. A positive answer would say that a representation of $1$ by unit fractions can never have all its denominators within distance $2$ of each other — a structural constraint of a kind that the size-based results in this area do not provide. The conditional route recorded on the problem page is instructive about where the difficulty sits: it reduces the conjecture, up to finitely many exceptions, to the existence of primes $p$ in $[N,2N]$ with $(p+1)/2$ prime, a statement of Bertrand-with-extra-structure type that is itself out of reach of current technology. A direct proof would therefore either bypass that route or resolve the conjecture for the remaining cases by different means.

Formalizing it. The gap-two bound and the block theorem behind it are closed mathematics, so the honest description of that part of this mission is formalization, not research. It is nevertheless not already available: Mathlib proves Theisinger's case harmonic_not_int, that $H_n \notin \mathbb{Z}$ for $n \ge 2$, but not Kürschák's block version $H_n - H_m \notin \mathbb{Z}$, which is the form Problem 287 needs. Supplying it is a genuine strengthening of the library's existing development and is reusable for any question about reciprocal sums over intervals. The goal itself is open, and this mission does not claim otherwise: it is registered with an open proof, and the milestones are what a solver can realistically close today.

Difficulty

The obvious first idea — bound the number of terms, then check finitely many cases — fails immediately, because $k$ is unbounded: representations of $1$ exist with arbitrarily many terms, so no finite computation can settle the conjecture. The second idea, extending the $2$-adic argument that gives the gap-two bound, also fails, and instructively. That argument works because a block of consecutive integers contains exactly one element of maximal $2$-adic valuation, which leaves the total with negative valuation. Once gaps of size $2$ are permitted the denominators may be chosen to avoid that configuration — for instance all even, as in $(2,4,6,12)$ — and the valuation obstruction disappears. There is no evident replacement prime or weighting that rules out all gap-$\le 2$ configurations simultaneously, and the conditional result quoted above suggests why: the known routes pass through the distribution of primes in short intervals with a multiplicative side condition, rather than through a congruence obstruction.

Formalization scope

A representation is encoded as a function $f : \mathbb{N} \to \mathbb{N}$ together with the hypotheses ∀ i < k, 1 < f i and ∀ i j, i < j → j < k → f i < f j, and the requirement ∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1. Only the values of $f$ below $k$ are constrained; the function is not required to be monotone or bounded elsewhere, and nothing outside the window is used. The conclusion is ∃ i, i + 1 < k ∧ 3 ≤ f (i + 1) - f i, the existential form of "the maximal gap is at least $3$"; the subtraction is natural-number subtraction, which is harmless because $f$ is increasing on the window, so no truncation can occur. The sum is a rational equality, not an approximation.

The statement admits no trivializing reading. The hypothesis 1 < f i is essential and is not vacuous — dropping it would admit $f\,0 = 1$, $k = 1$; the strict monotonicity is what makes the gaps well defined and the denominators distinct; and k ≥ 2 guarantees that at least one gap exists, so the conclusion is not an empty existential. Asserting exactly $3$ rather than at least $3$ would be false, as $(2,4,6,12)$ has a gap of $6$.

Infrastructure: the block theorem is proved from Mathlib's padicNorm and padicValNat API — padicNorm.add_eq_max_of_ne, padicNorm.sum_lt', padicNorm.not_int_of_not_padic_int, pow_padicValNat_dvd and pow_succ_padicValNat_not_dvd — and needs no new definitions. That development is reusable beyond this mission and is a candidate for upstreaming to Mathlib alongside harmonic_not_int. Contributions are welcome on any milestone independently; a formalization of the conditional reduction to primes $p$ with $(p+1)/2$ prime would also be a valuable addition, and is not included as a milestone here only because the problem page states it too briefly to formalize faithfully without consulting a primary source.

Selected references

• P. Erdős, Egy Kürschák-féle elemi számelméleti tétel általánosítása (A generalisation of an elementary number-theoretic theorem of Kürschák), Mat. és Phys. Lapok 39 (1932), 17–24.
• P. Erdős and R. L. Graham, Old and new problems and results in combinatorial number theory, Monographies de L'Enseignement Mathématique, Geneva, 1980, p. 33. scan
• Various, Some of Paul's favorite problems, booklet for the conference "Paul Erdős and his mathematics", Budapest, July 1999, item 1.15.
• K. Conrad, The $p$-adic growth of harmonic sums, expository notes (Theorem 2 is Kürschák's block theorem, with the $2$-adic proof). pdf
• T. F. Bloom, Erdős Problem #287, erdosproblems.com/287.

Motivation

Erdős asked, repeatedly and with a rising price tag, for an asymptotic formula for the largest subset of $\{1,\dots,N\}$ that contains no arithmetic progression of a given length. He offered 1000 dollars for it in [Er97c] and 10000 dollars in [Er81, p.4], where he called the question "probably enormously difficult"; elsewhere he described it as "probably unattackable at present". Most of modern additive combinatorics — the density increment method, the triangle removal lemma, Gowers uniformity norms, the arithmetic regularity lemma — grew out of attempts on this single question, and the answer is still unknown, even in the first non-trivial case $k=3$.

Timeline.

• 1936: Erdős and Turán conjecture that $r_k(N)=o(N)$ for every $k$.
• 1946: Behrend constructs large progression-free sets, giving $r_3(N)\ge N\exp(-c\sqrt{\log N})$.
• 1953: Roth proves $r_3(N)=o(N)$, with the quantitative form $r_3(N)\ll N/\log\log N$.
• 1961: Rankin generalises Behrend, giving $r_k(N)\ge N\exp(-c_k(\log N)^{1/(k-1)})$.
• 1969, 1975: Szemerédi proves $r_4(N)=o(N)$ and then $r_k(N)=o(N)$ for all $k$, settling Erdős–Turán.
• 1977: Furstenberg reproves Szemerédi's theorem ergodically, with no effective bound.
• 1998, 2001: Gowers introduces uniformity norms and obtains $r_k(N)\ll N(\log\log N)^{-c_k}$, the first effective bound for general $k$.
• 2017: Green and Tao obtain $r_4(N)\ll N(\log N)^{-c}$.
• 2020: Bloom and Sisask obtain $r_3(N)\ll N(\log N)^{-1-c}$, the first bound past the $N/\log N$ barrier.
• 2023: Kelley and Meka obtain $r_3(N)\le N\exp(-c(\log N)^{1/12})$.
• 2024: Leng, Sah and Sawhney obtain $r_k(N)\ll N\exp(-(\log\log N)^{c_k})$ for $k\ge5$.

Every upper bound in this list is still astronomically far from Behrend's lower bound, and no candidate asymptotic formula has been proposed for any $k\ge3$.

Setting

Fix an integer $k$. A non-trivial $k$-term arithmetic progression is a list $a,\,a+d,\,a+2d,\dots,a+(k-1)d$ of natural numbers with common difference $d>0$; the requirement $d>0$ is what "non-trivial" means, and it forces the $k$ terms to be distinct. A finite set $A\subseteq\mathbb N$ is $k$-AP-free if it contains no such progression. Write

$$r_k(N)\;=\;\max\bigl\{\,|A| \;:\; A\subseteq\{1,\dots,N\},\ A\ \text{is}\ k\text{-AP-free}\,\bigr\}.$$

The mission takes its formal definition of $r_k$ verbatim from the formal-conjectures entry for this problem, so that the goal below is literally the statement recorded there. In that development a set is called free of progressions of length $l$ when every subset of it that is an arithmetic progression of length $l$ forces $l\le1$. Progressions of length $0$ and $1$ count as trivial, so under that convention every set is free of them and $r_0(N)=r_1(N)=N$; the interesting range begins at $k\ge2$. Every statement in this mission that depends on the convention carries an explicit hypothesis on $k$.

On that range, $r_k(N)$ is non-decreasing in both $N$ and $k$, satisfies $r_k(M+N)\le r_k(M)+r_k(N)$, and hence, by Fekete's subadditivity lemma, $r_k(N)/N$ converges. Szemerédi's theorem is the statement that the limit is $0$; the whole difficulty of this mission lies in how fast it goes to $0$.

Formalization targets

Goal

$$r_k(N)\;=\;o_k\!\left(\frac{N}{\log N}\right)\qquad\text{for every }k>1 .$$

This is erdos_142.variants.lower of the formal-conjectures file for Erdős 142, reproduced binder for binder, over that file's own definition of $r_k$.

The headline theorem in that file, erdos_142, states $r_k(N)=\Theta(f)$ with the comparison function left as an answer(sorry) placeholder, and the same is true of its variants.upper and variants.three. Those are not closed propositions and cannot serve as a mission goal: the literal request of Erdős Problem #142 — "prove an asymptotic formula for $r_k(N)$" — has no known right-hand side for any $k\ge3$, which is exactly why the file leaves a hole there. variants.lower is the one formalizable target in the file, and it is also the strongest precisely-stated form the problem page attaches to #142: Erdős offered 5000 dollars for (essentially) exactly it, as recorded under Erdős Problem #3. It is known for $k=3$ — it follows from Bloom–Sisask 2020, and a fortiori from Kelley–Meka 2023 — trivial for $k=2$, where $r_2(N)=1$, and open for every $k\ge4$. It fixes no constants, so no future improvement can invalidate it.

A weaker open question

$$\frac{r_k(n)}{r_{k+1}(n)}\longrightarrow 0\qquad\text{for some }k\ge3 .$$

Erdős remarked in [Er80, p.92] that even this separation between consecutive progression lengths is not known. Here [Er80] is the erdosproblems.com bibliography key for Erdős's 1980 paper; it is a citation, not a pointer to Erdős Problem #80, which is an unrelated question about books in graphs. This statement has no counterpart in formal-conjectures: the file for #142 contains only the $\Theta$, $o$ and $O$ variants above, and the only two files in that repository that mention $r_k$ at all are the ones for #142 and #139.

Significance

Proving $r_k(N)=o_k(N/\log N)$ for all $k$ yields, by a standard summation argument, Erdős's conjecture that every $A\subseteq\mathbb N$ with $\sum_{a\in A}1/a=\infty$ contains arbitrarily long arithmetic progressions — the 5000-dollar Erdős Problem #3, of which the Green–Tao theorem on primes is the best-known special case. Below that threshold, quantitative bounds on $r_k$ control the density at which progressions must appear in any concrete set, and are the input to results on progressions in the primes, in sumsets, and in sparse random subsets of the integers.

Formalization status is uneven, and this mission is designed around that gap. Mathlib already contains the $k=3$ theory in a usable form: the predicate ThreeAPFree, the Roth number rothNumberNat, its subadditivity, and a complete formalization of Behrend's construction (Behrend.roth_lower_bound). Mathlib does not contain Roth's theorem, Szemerédi's theorem, or any of the modern upper bounds; to the best of current knowledge none of Roth, Szemerédi, Gowers, Green–Tao, Kelley–Meka or Leng–Sah–Sawhney has a machine-checked proof anywhere. The formal-conjectures entry states the problem but proves nothing: every declaration in it is a sorry. Two of this mission's targets are taken from that repository — the goal from its file for #142, and the Szemerédi milestone from its file for #139, which uses the same $r_k$; those are the only two files there that mention $r_k$. The milestones therefore split cleanly: the first six are reachable now on top of Mathlib, and the last five are open formalization projects of independent value.

Difficulty

Every known upper bound for $r_k$ runs a density increment: if $A\subseteq\{1,\dots,N\}$ of density $\delta$ has no $k$-term progression, find a long subprogression on which $A$ has density $\delta(1+c(\delta))$, and iterate. The bound this produces is governed entirely by two quantities — how large the increment $c(\delta)$ is, and how much of the interval survives one step. For $k\ge4$ the increment is extracted from an inverse theorem for the Gowers $U^{k-1}$-norm, and the best available correlation bounds there are quasipolynomial in $\delta$; iterating a quasipolynomial increment cannot do better than $N\exp(-(\log\log N)^{c})$, which is nowhere near $N/\log N$. Reaching $N/\log N$ requires an increment with polynomial dependence on $\delta$ together with a subprogression of polynomial length, and that combination is currently available only for $k=3$, through the sifting and almost-periodicity machinery of Kelley–Meka. No soft or averaging argument can substitute: Behrend's construction shows the truth at $k=3$ is $N\exp(-\Theta(\sqrt{\log N}))$, so the answer is not a power of $\log N$ and cannot be produced by any argument whose output has that shape.

Formalization scope

The mission's definition file Erdos142Basic carries two layers, and every statement in the mission is written against them.

1. The source definitions, ported verbatim. IsAPOfLengthWith, IsAPOfLength, IsAPOfLengthFree and r are the declarations of the formal-conjectures entry, transcribed unchanged into the mission's namespace: a set is an arithmetic progression of length $l$ with first term $a$ and difference $d$ when it has exactly $l$ elements and equals $\{a+nd : n<l\}$; it is free of length-$l$ progressions when every progression of length $l$ inside it forces $l\le1$; and $r_k(N)$ is the supremum of $|S|$ over subsets $S\subseteq\{1,\dots,N\}$ free of length-$k$ progressions. The ground set is Finset.Icc 1 N, and the supremum is sSup over $\mathbb N$; the file proves the two facts that make it a genuine maximum (le_r and r_le).

2. An elementary handle. HasAP k A is ∃ a d, 0 < d ∧ ∀ i < k, a + i * d ∈ A, and APFree k A its negation. This form carries no cardinality side condition in $\mathbb N\cup\{\infty\}$ and is what a solver actually wants to induct on. The first milestone is exactly the bridge between the two layers.

Two consequences of the source convention are worth stating plainly, because the prose is silent about them. Length-$0$ and length-$1$ progressions are trivial, so every set is free of them and $r_0(N)=r_1(N)=N$; monotonicity of $r_k$ in $k$ therefore holds only from $k\ge2$ onward, and the corresponding milestone carries that hypothesis. Asymptotic statements use Asymptotics.IsLittleO and Filter.atTop over $\mathbb N$ with real-valued casts, and real division is Lean's, so (N : ℝ) / Real.log N is $0$ at $N=1$; this is invisible to atTop.

A trivializing formalization is ruled out by construction: one milestone asserts $r_3(N)=$ rothNumberNat N, pinning this development against Mathlib's independently written definition of the Roth number, so a vacuous or mis-quantified notion of progression-freeness cannot survive. That milestone, the bridge milestone above it, and the monotonicity milestone have all been checked to be provable before this proposal was drafted.

A full development needs: discrete Fourier analysis on $\mathbb Z/N\mathbb Z$, Bohr sets and their regularity, the arithmetic regularity lemma, Gowers uniformity norms and the inverse theorem for them, and — for the lower bounds — sphere-counting in high-dimensional boxes (already in Mathlib via Behrend). All of this is reusable well beyond this mission. Contributions of any kind are welcome, including partial results: quantitative bounds weaker than the cited ones, the $k=3$ case of a general-$k$ milestone, and reusable Fourier-analytic infrastructure are all valuable even when they do not close a milestone.

Selected references

• Erdős Problem #142. https://www.erdosproblems.com/142
• Erdős Problem #3. https://www.erdosproblems.com/3
• Erdős Problem #139 (Szemerédi's theorem in the $r_k$ formulation), linked from #142. https://www.erdosproblems.com/139
• Google DeepMind, formal-conjectures, FormalConjectures/ErdosProblems/142.lean — the source of the goal statement and of the definition of $r_k$. https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.lean
• F. A. Behrend, On sets of integers which contain no three terms in arithmetical progression, Proc. Nat. Acad. Sci. USA 32 (1946), 331–332. https://doi.org/10.1073/pnas.32.12.331
• K. F. Roth, On certain sets of integers, J. London Math. Soc. 28 (1953), 104–109. https://doi.org/10.1112/jlms/s1-28.1.104
• R. A. Rankin, Sets of integers containing not more than a given number of terms in arithmetical progression, Proc. Roy. Soc. Edinburgh Sect. A 65 (1961), 332–344.
• E. Szemerédi, On sets of integers containing no $k$ elements in arithmetic progression, Acta Arith. 27 (1975), 199–245. https://doi.org/10.4064/aa-27-1-199-245
• W. T. Gowers, A new proof of Szemerédi's theorem, Geom. Funct. Anal. 11 (2001), 465–588. https://doi.org/10.1007/s00039-001-0332-9
• B. Green and T. Tao, New bounds for Szemerédi's theorem, III: A polylogarithmic bound for $r_4(N)$, Mathematika 63 (2017), 944–1040. https://arxiv.org/abs/1705.01703
• T. F. Bloom and O. Sisask, Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions, arXiv:2007.03528. https://arxiv.org/abs/2007.03528
• Z. Kelley and R. Meka, Strong bounds for 3-progressions, arXiv:2302.05537. https://arxiv.org/abs/2302.05537
• J. Leng, A. Sah and M. Sawhney, Improved bounds for Szemerédi's theorem, arXiv:2402.17995. https://arxiv.org/abs/2402.17995

Motivation and historical timeline

In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit (Birkhoff 1915; Liu--Salomão, Section 1.4). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics (Joung--van Koert, Introduction).

In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 (Joung--van Koert, Theorem 1.3; Hryniewicz). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for $0\leq\mu\leq 1/2$ and $2.1\leq c\leq 2.1+10^{-6}$ (Theorems 1.2 and 1.5). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to $1/2$, in fact obtaining rational open books bound by every retrograde orbit in that regime (Theorem 1.16). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem (Liu--Salomão 2026). These results leave the universal finite-mass, all-subcritical statement below as the open target.

Setting

Two primaries of masses $1-\mu$ and $\mu$, with $0<\mu<1$, are fixed in rotating coordinates at $(-\mu,0)$ and $(1-\mu,0)$. For a massless particle with phase coordinates $(q_1,q_2,p_1,p_2)$, the Hamiltonian is

$$H_\mu(q,p)=\frac{p_1^2+p_2^2}{2}+q_1p_2-q_2p_1 -\frac{1-\mu}{\sqrt{(q_1+\mu)^2+q_2^2}} -\frac{\mu}{\sqrt{(q_1-1+\mu)^2+q_2^2}}.$$

This is equation (1.1) of Joung--van Koert. Let $h_1(\mu)=H_\mu(L_1)$ be the smallest collision-free critical value, where $L_1$ lies between the primaries. The subcritical range is $H_\mu=-c<h_1(\mu)$; there are then two bounded physical components, one around each primary (Liu--Salomão, Section 4).

The mission labels the primary at $(-\mu,0)$. With complex Levi-Civita variables $z=z_1+iz_2$ and $w=w_1+iw_2$, the inverse position map is $q+\mu=2z^2$, and the regularized Hamiltonian is

$$\begin{aligned} K_{\mu,c}(z,w)={}&\frac{|w|^2}{2}+c|z|^2-\frac{1-\mu}{2} +2|z|^2(z_1w_2-z_2w_1)\\ &-\mu(z_1w_2+z_2w_1) -\frac{\mu|z|^2}{|2z^2-1|}. \end{aligned}$$

On the collision-free domain, $K_{\mu,c}=|z|^2(H_\mu+c)$, and its zero level regularizes collision with the labeled primary (Joung--van Koert, equation (2.2)). The selected component $\Sigma_{\mu,c}$ is anchored at $(z,w)=(0,\sqrt{1-\mu})$. Below $h_1$, it is a star-shaped three-sphere, invariant under the free antipodal deck map $(z,w)\mapsto(-z,-w)$, and it double-covers the corresponding Moser-regularized $\mathbb{R}P^3$ component (Joung--van Koert, Proposition 2.4).

Target

For every $0<\mu<1$, every $-c<h_1(\mu)$, and every complete flow $\varphi$ on $\Sigma_{\mu,c}$ generated by $X_{K_{\mu,c}}$ and commuting with the antipodal map, prove

$$\exists\,\delta\quad \operatorname{GeometricRetrograde}(\delta)\ \land\ \operatorname{RationalGSS}(\operatorname{DoubleLift}(\delta)).$$

Here $\delta$ consists of $x\in\Sigma_{\mu,c}$ and a quotient period $P>0$ with $\varphi_P(x)=-x$, with no earlier positive time reaching either $x$ or $-x$. Its physical projection is required to be a $q_2$-symmetric, simple, collision-free loop of winding $+1$ around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3.

The rational page is encoded by a smooth immersive disk lift $\widetilde f:D^2\to\Sigma_{\mu,c}$. Its lift is embedded, its interior is transverse to $X_{K_{\mu,c}}$, and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section (Hryniewicz, Definition 1.1).

Significance

A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences (Birkhoff 1915; Joung--van Koert, Introduction). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.

Difficulty

Existence of a $q_2$-symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every $0<\mu<1$ and every energy below $L_1(\mu)$ (Liu--Salomão, Theorem 5.1). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges (Joung--van Koert, Theorem 1.5; Liu--Salomão, Theorem 1.16).

Formalization scope

The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual Flow together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.

The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.

All theorem rows are Lean declarations ending in by sorry. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.

Selected references

• G. D. Birkhoff, The restricted problem of three bodies, Rendiconti del Circolo Matematico di Palermo 39 (1915), 265--334. DOI.
• U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859--1931. arXiv:0812.4076v8.
• C. Joung and O. van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, Nonlinearity 38 (2025), 025015. arXiv:2407.19159v3.
• L. Liu and P. A. S. Salomão, Finite energy foliations and global dynamics in the restricted three-body problem, arXiv:2506.17867v2 (25 May 2026). Preprint.
• L. Liu and P. A. S. Salomão, Birkhoff conjecture and finite energy foliations in Hill's lunar problem, arXiv:2606.12912 (2026). Preprint.

Superlinear or exact bounds for planar distinct distances

Motivation

This mission asks how restrictions on collinear and cocircular points limit the reuse of distances in the plane. Its central question is Erdős Problem 98: must the minimum number of distances grow faster than the number of points?

Setting

For each positive integer n, let h(n) be the minimum number of distinct positive Euclidean distances determined by an n-point set in the plane with no three collinear points and no four cocircular points. Write D(P) for the number of distinct positive Euclidean distances determined by P.

Target

The mission is to establish a superlinear lower bound, or determine this extremal function exactly. The superlinear target is Erdős Problem 98:

$$\lim_{n\to\infty} h(n)/n=\infty.$$

Concretely, for every real A > 0, prove that there is an integer n_A such that every general-position configuration P with |P| = n >= n_A satisfies D(P) > A n. A fixed improvement of the coefficient 1/3, or an additive sublinear improvement above n/3, does not complete this objective.

The alternative completion target is an exact determination of h(n), proved by a universal lower bound and general-position constructions attaining that bound. State the range of n explicitly. An asymptotic estimate or a counterexample to superlinearity alone must be labeled with its actual scope; neither is an exact determination of h(n).

Significance and supporting results

The current strongest internally audited prose result in this project is

$$D(P)\ge n/3+c n^{1/4}$$

for some absolute c > 0 and all sufficiently large n. Its full Lean formalization remains open. The n^(1/4), n^(1/5), and n^(1/6) theorem targets and their existing milestones are supporting results, not the mission's terminal goal. Resolving the superlinear target would establish a lower bound above every fixed linear coefficient. Determining h(n) exactly would settle the corresponding extremal problem with matching constructions.

Difficulty and research priorities

The n^(1/4) route constructs a deficiency--Newton carrier, proves pair separation, and applies one polynomial partition to obtain the curve bound D(S) >= c d^(-4/3) |S|^(4/3). Its current final calculation yields an additive n^(1/4) term. Stronger additive bounds count as intermediate progress; they must not be reported as a superlinear lower bound.

• Develop an argument that excludes D(P) <= A n for every fixed A > 0. The repository's fixed-A distance-energy gap is one sufficient route.
• Investigate additional structure of the Newton carriers and interactions between their factors, or another geometric or combinatorial route that can control the superlinear target.
• Investigate constructions and universal lower bounds together when pursuing an exact extremal determination.
• Preserve and formalize useful intermediate theorems while keeping their statements and remaining premises explicit.

Formalization scope

Configurations are finite subsets of the Euclidean plane, represented in the project by injective maps from Fin n to the plane. Both general-position hypotheses apply to the image. D(P) counts distinct positive distance values, not pairs or ordered multiplicities. The superlinear quantifier ranges over every real A > 0 and every sufficiently large general-position configuration.

The superlinear target and exact-determination target remain open here. Distinguish conjectures, conditional reductions, audited prose proofs, and kernel-checked Lean results. A completed supporting formalization does not by itself complete this mission.

Selected references

• Erdős Problem 98 — extremal question and bibliography.
• Project overview — fixed-A target and current theorem status.
• Atomic proof of the ESGK n^(1/4) additive bound, project manuscript, revised 2026-09-14.
• Full-proof audit, internal adversarial review, 2026-09-14.

The set

For a complex parameter $c$, iterate the quadratic map

$$f_c(z) = z^2 + c$$

starting at the critical point $z = 0$. The Mandelbrot set is the set of parameters for which this orbit stays bounded:

$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$

Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.

$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism

$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$

between the complement of $M$ and the exterior of the closed unit disk.

The question

MLC conjecture. $M$ is locally connected: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.

By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the pinched disk model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the density of hyperbolicity in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and zero area for $\partial M$.

MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.

Timeline

• 1982 -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
• 1984/85 -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
• 1990 -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
• 1997 -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
• 1997 -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the real quadratic family.
• 1998 -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive area remains open.
• 2005 -- Buff and Cheritat construct quadratic Julia sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
• Today -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.

What this mission asks for

The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".

The milestones are of three kinds, and are ordered accordingly:

1. Foundations provable today -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. Known theorems from the literature -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. The open companions -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.

All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.

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

$$G \;\cong\; \mathrm{Gal}(L/K),$$

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

$$\text{for every finite group } G, \qquad \exists\, L/\mathbb{Q} \text{ Galois with } \mathrm{Gal}(L/\mathbb{Q}) \cong G.$$

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

$$G \text{ cyclic} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, \qquad G \text{ abelian} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q},$$ $$\mathrm{Sym}(S),\; A_n \text{ realizable over } \mathbb{Q}, \qquad G \text{ solvable} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q},$$ $$\exists\, K,\ \mathbb{Q} \subseteq K \subseteq \mathbb{C},\ G \text{ realizable over } K,$$ $$G \text{ realizable over } \mathbb{C}(t), \qquad G \text{ realizable over } K(t) \ (K \text{ algebraically closed, char } 0),$$ $$G \text{ realizable over } \mathbb{Q}(t) \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}.$$

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.

The statements cannot be satisfied vacuously: IsRealizable K G asserts the existence of data, so a solver must exhibit an extension; and the hypotheses of the milestones (cyclic, abelian, solvable, or none at all) are all satisfiable, so no milestone is empty. The one conditional milestone, Hilbert descent, is stated with realizability over $\mathbb{Q}(t)$ as an explicit hypothesis.

Infrastructure a complete development needs, most of it reusable well beyond this mission: transport of a Galois realization along an isomorphism of groups and along an isomorphism of base fields; the fixed-field construction and the fundamental theorem in the form "$\mathrm{Gal}(L/L^H) \cong H$"; Galois groups of cyclotomic fields; Dirichlet's theorem on primes in arithmetic progressions (already in Mathlib); Hilbert's irreducibility theorem (not in Mathlib). Contributions of any of these as reusable platform definitions or lemmas are welcome, as are decompositions of the harder milestones into sketches.

Selected references

• Inverse Galois problem, Wikipedia. https://en.wikipedia.org/wiki/Inverse_Galois_problem
• I. R. Shafarevich, The imbedding problem for splitting extensions, Dokl. Akad. Nauk SSSR 120 (1958), 1217–1219.
• C. U. Jensen, A. Ledet, N. Yui, Generic Polynomials: Constructive Aspects of the Inverse Galois Problem, MSRI Publications 45, Cambridge University Press, 2002. http://library.msri.org/books/Book45/files/book45.pdf
• G. Malle, B. H. Matzat, Inverse Galois Theory, Springer Monographs in Mathematics, 1999.
• R. van Bommel, E. Costa, N. D. Elkies, T. Keller, S. Schiavone, J. Voight, 17T7 is a Galois group over the rationals, arXiv:2411.07857, 2024. https://arxiv.org/abs/2411.07857

Motivation

Almost every classical question about prime values of polynomials is a special case of one statement. Are there infinitely many twin primes? Infinitely many primes of the form $n^2+1$? Infinitely many Sophie Germain primes $p$ with $2p+1$ prime? Each asks whether a fixed finite list of integer polynomials takes prime values simultaneously infinitely often. Schinzel's Hypothesis H (A. Schinzel and W. Sierpiński, 1958) is the single conjecture that predicts "yes" in all these cases, subject to the two obvious obstructions: a polynomial that factors cannot be prime infinitely often, and neither can a family whose product is always divisible by some fixed prime.

Timeline.

• 1837 — Dirichlet proves the degree-one, single-polynomial case: if $\gcd(a,b)=1$ and $a>0$, then $an+b$ is prime for infinitely many $n$.
• 1857 — Bunyakovsky states the single-polynomial case for arbitrary degree. It is open for every fixed polynomial of degree $\ge 2$; not one instance, not even $n^2+1$, is known.
• 1904 — Dickson states the case of arbitrarily many linear polynomials.
• 1958 — Schinzel and Sierpiński state Hypothesis H in the generality used here (Acta Arith. 4 (1958), 185–208).
• 1962 — Bateman and Horn give the conjectural asymptotic count of such $n \le N$, refining Hypothesis H to a quantitative form (Math. Comp. 16 (1962), 363–367).
• 1978 — Iwaniec proves that $n^2+1$ has at most two prime factors infinitely often; the sieve barrier that blocks "exactly one" has not been broken.
• 2004 — Green and Tao prove the analogous simultaneous-prime statement for systems of linear forms of finite complexity, which yields arbitrarily long arithmetic progressions of primes but does not cover Dickson's conjecture in full (the pair $n$, $n+2$ has infinite complexity).
• 2013 — Zhang, and then Maynard and Tao, establish bounded gaps between primes, i.e. that some admissible pair $\{n+h_1, n+h_2\}$ is simultaneously prime infinitely often — but the method does not identify which pair.

Hypothesis H itself remains open in every case that is not covered by Dirichlet's theorem.

Setting

Work in the ring $\mathbb{Z}[X]$ of polynomials with integer coefficients. Fix a finite set $\mathcal{F} \subseteq \mathbb{Z}[X]$ of polynomials $f$, each subject to the Bunyakovsky condition:

• $\deg f \ge 1$;
• the leading coefficient of $f$ is positive;
• $f$ is irreducible in $\mathbb{Z}[X]$.

Irreducibility in $\mathbb{Z}[X]$ is strictly stronger than irreducibility in $\mathbb{Q}[X]$: it also forces the content of $f$ to be $1$, ruling out $2X^2+2$.

Even an irreducible family can be blocked by congruences. The polynomial $X^2+X+2$ is irreducible with positive leading coefficient, yet $n^2+n+2$ is even for every integer $n$, so it is prime only when it equals $2$. The family $\mathcal{F}$ therefore also has to satisfy the Schinzel condition: for every prime $p$ there exists an integer $n$ with

$$p \nmid \prod_{f \in \mathcal{F}} f(n).$$

Equivalently, no prime is a fixed divisor of the product $\prod_{f\in\mathcal{F}} f$. A family satisfying both conditions is called admissible.

Target

For an admissible family $\mathcal{F}$, write

$$S(\mathcal{F}) \;=\; \{\, n \in \mathbb{N} \;:\; |f(n)| \text{ is prime for every } f \in \mathcal{F} \,\}.$$

The goal of the mission is Hypothesis H:

$$\mathcal{F} \text{ admissible} \;\Longrightarrow\; S(\mathcal{F}) \text{ is infinite.}$$

The milestones are, in order: the linear one-polynomial case (Dirichlet); the reduction of the Schinzel condition to the finitely many primes $p \le \sum_{f\in\mathcal F}\deg f$; the necessity of the Schinzel condition; and three specializations of the goal — Bunyakovsky's conjecture, the twin prime conjecture, and Landau's problem on $n^2+1$ — each stated as an implication from the goal statement, so that they can be proved before the goal itself is.

Significance

The result itself. Hypothesis H implies the twin prime conjecture, the Sophie Germain prime conjecture, Landau's conjecture that $n^2+1$ is prime infinitely often, the infinitude of primes in every admissible constellation, and Dickson's conjecture; with Bateman–Horn it also predicts the density of such $n$. Nothing beyond the degree-one case is known, and the conjecture is the standard yardstick against which sieve-theoretic progress on prime values of polynomials is measured.

Formalizing it. The goal is open, so the mission's deliverable is not a proof of it but a formal, audited statement of it together with a supporting environment: the admissibility predicates, the classical reductions, and machine-checked derivations of the famous corollaries from the goal. Dirichlet's theorem on primes in arithmetic progressions is already formalized in Mathlib, so the linear milestone is a matter of connecting that result to this mission's formulation rather than of new mathematics. The three "H implies …" milestones are provable now, unconditionally, because they are implications; they are also the sharpest available check that the goal statement has been formalized faithfully, since a mis-stated goal will usually fail to yield twin primes.

Difficulty

The obvious first idea — sieve the values $\prod_{f} f(n)$ for $n \le N$ and count survivors — is exactly the idea that fails. Sieve methods lose a constant factor (the parity problem): they can show that $\prod_f f(n)$ has few prime factors infinitely often, but they cannot distinguish "one prime factor" from "two", which is why Iwaniec's $n^2+1$ result stops at $P_2$. The analytic input that works for degree one — the nonvanishing of Dirichlet $L$-functions on $\Re s = 1$ — has no known analogue for a polynomial of degree $\ge 2$, because the relevant counting problem is not governed by characters of a finite abelian group. Milestones 1–3 are elementary or already available in Mathlib; the goal itself is not expected to be resolved here.

Formalization scope

Conventions fixed by the Lean development, and deliberately so:

• The family is a finite set of polynomials, so repeated polynomials collapse, and it is allowed to be empty (the goal is then a statement about all of $\mathbb{N}$, and true).
• Primality is asserted of the absolute value $|f(n)|$ as a natural number. Since the leading coefficient is positive and $\deg f \ge 1$, the values are eventually positive, so this is equivalent to asking for a positive prime value at all large $n$.
• The variable $n$ ranges over $\mathbb{N}$, not $\mathbb{Z}$, and "infinitely often" means that the set of such $n$ is infinite.
• Irreducibility is irreducibility in $\mathbb{Z}[X]$ (so primitivity is included), and the degree hypothesis is $\deg f \ge 1$ in the sense of the natural-number degree.
• The Schinzel condition is stated as a condition on the product over the family, quantified over all primes $p$ — not over $p$ up to a bound; milestone 2 is what reduces it to a finite check.

The statement admits no trivializing reading: the hypotheses are satisfiable (for example $\{X, X+2\}$ and $\{X^2+1\}$ are admissible, as milestones 5 and 6 require one to verify), so the goal is not vacuous, and the conclusion asserts infinitude rather than the existence of a single $n$.

A complete development needs the admissibility predicates (supplied as the mission's definition bundle), Mathlib's polynomial and modular-arithmetic APIs for the fixed-divisor arguments, and Mathlib's Dirichlet theorem for milestone 1. The definition bundle and milestones 2–3 are reusable for any future mission on Bateman–Horn, Dickson's conjecture, or prime constellations. Contributions of further conditional consequences of the goal (Sophie Germain primes, prime $k$-tuples, cousin primes) are welcome as additions to the tree.

Selected references

• A. Schinzel and W. Sierpiński, Sur certaines hypothèses concernant les nombres premiers, Acta Arithmetica 4 (1958), 185–208. DOI
• P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Mathematics of Computation 16 (1962), 363–367. DOI
• H. Iwaniec, Almost-primes represented by quadratic polynomials, Inventiones Mathematicae 47 (1978), 171–188. DOI
• B. Green and T. Tao, The primes contain arbitrarily long arithmetic progressions, Annals of Mathematics 167 (2008), 481–547. arXiv:math/0404188
• J. Maynard, Small gaps between primes, Annals of Mathematics 181 (2015), 383–413. arXiv:1311.4600

Motivation

The Grothendieck-Teichmüller group organises a family of symmetries that act on braided monoidal categories, on quantised universal enveloping algebras, on the little-discs operad, and on the ring of periods of the projective line minus three points. Three versions exist: a profinite one $\widehat{GT}$, introduced by Grothendieck and Drinfeld and containing the absolute Galois group $\mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q)$; a pro-$\ell$ one; and a pro-unipotent one $GT$, together with its graded companion $GRT$. This mission is about the graded, pro-unipotent side, which is the version that governs the homological-algebra and deformation-quantisation applications, and which is closest to a concrete, computable object: a Lie algebra of Lie polynomials in two variables, cut out by three explicit equations.

Its Lie algebra $\mathfrak{grt}_1$ carries a distinguished family of elements $\sigma_3, \sigma_5, \sigma_7, \dots$, one in each odd degree at least $3$, produced from the Knizhnik-Zamolodchikov associator. Deligne, Drinfeld and Ihara conjectured that $\mathfrak{grt}_1$ is the free Lie algebra on such a family. A timeline of what is actually known:

• 1990 - V. Drinfeld, On quasitriangular quasi-Hopf algebras and a group closely connected with $\mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q)$, introduces $GT$, $GRT$, associators, and the defining equations of $\mathfrak{grt}_1$; the Knizhnik-Zamolodchikov associator shows the set of associators is non-empty, hence $\sigma_3, \sigma_5, \dots$ exist and are non-zero.
• 2012 - F. Brown, Mixed Tate motives over $\mathbb Z$ (Annals of Mathematics 175, 949-976, doi:10.4007/annals.2012.175.2.10), proves that the $\zeta^{\mathfrak f}(r_1,\dots,r_n)$ with $r_j \in \{2,3\}$ form a basis of the algebra of motivic multiple zeta values. One half of the conjecture follows: the Lie subalgebra of $\mathfrak{grt}_1$ generated by the $\sigma_{2p+1}$ is free on them.
• The converse half - that these elements generate all of $\mathfrak{grt}_1$ - is open.

Setting

Let $\mathbb{F}(x,y)$ be the free Lie algebra over $\mathbb Q$ on two generators $x$ and $y$, graded by total word length. For a Lie algebra $A$ over $\mathbb Q$ and $a, b \in A$, write $\psi(a,b)$ for the image of $\psi \in \mathbb{F}(x,y)$ under the unique Lie algebra morphism sending $x \mapsto a$ and $y \mapsto b$.

For $n \ge 1$, the Drinfeld-Kohno Lie algebra $\mathfrak t_n$ is generated over $\mathbb Q$ by symbols $t_{ij}$, $1 \le i, j \le n$, subject to

$$t_{ii} = 0, \qquad t_{ij} = t_{ji}, \qquad [t_{ij}, t_{kl}] = 0, \qquad [t_{ij}, t_{ik} + t_{jk}] = 0,$$

the third relation for $i,j,k,l$ pairwise distinct and the fourth for $i,j,k$ pairwise distinct. It is the Lie algebra of infinitesimal braid relations: the associated graded of the pure braid Lie algebra, and the coefficient algebra of the Knizhnik-Zamolodchikov connection.

The graded Grothendieck-Teichmüller Lie algebra $\mathfrak{grt}_1$ is the set of $\psi \in \mathbb{F}(x,y)$ satisfying three equations:

$$\psi(x,y) = -\psi(y,x),$$ $$\psi(x,y) + \psi(y,z) + \psi(z,x) = 0 \quad \text{where } x + y + z = 0,$$ $$\psi(t_{12},t_{23}) - \psi(t_{12},t_{23}+t_{24}) + \psi(t_{12}+t_{13},t_{24}+t_{34}) - \psi(t_{13}+t_{23},t_{34}) + \psi(t_{23},t_{34}) = 0 \ \text{ in } \mathfrak t_4 .$$

All three are linear in $\psi$ and degree preserving, so $\mathfrak{grt}_1$ is a graded $\mathbb Q$-subspace.

$\mathfrak{grt}_1$ is not closed under the bracket of $\mathbb{F}(x,y)$; it is closed under the Ihara (Poisson) bracket

$$\{f,g\} = [f,g] + D_f g - D_g f,$$

where $D_f$ is the derivation of $\mathbb{F}(x,y)$ determined by $D_f x = 0$ and $D_f y = [y,f]$. Writing $\mathrm{Der}$ for the Lie algebra of derivations of $\mathbb{F}(x,y)$ under the commutator, the assignment $f \mapsto D_f$ satisfies $[D_f, D_g] = D_{\{f,g\}}$, and it is injective on $\mathfrak{grt}_1$; this is the form in which the Lie structure of $\mathfrak{grt}_1$ is expressed in the formal statements below.

Finally, for $n_1 \ge 2$ and $n_2,\dots,n_k \ge 1$ the multiple zeta value is

$$\zeta(n_1,\dots,n_k) = \sum_{j_1 > j_2 > \cdots > j_k \ge 1} \frac{1}{j_1^{n_1} j_2^{n_2} \cdots j_k^{n_k}} .$$

These numbers are the coefficients of the Knizhnik-Zamolodchikov associator, which is why they enter a mission about $\mathfrak{grt}_1$; they satisfy the stuffle and shuffle relations, whose common refinement (the double shuffle relations) is the arithmetic side of the same story.

Formalization targets

Goal - Deligne-Drinfeld-Ihara

$$\exists\, \sigma_0, \sigma_1, \sigma_2, \dots \in \mathfrak{grt}_1, \quad \deg \sigma_p = 2p+3, \quad \text{such that } \mathfrak{grt}_1 \text{ is the free Lie algebra} \text{ on } (\sigma_p)_{p \ge 0} \text{ for } \{\,,\}.$$

Concretely: the Lie algebra morphism from the free Lie algebra on countably many generators to $\mathrm{Der}$ sending the $p$-th generator to $D_{\sigma_p}$ is injective, and its image is exactly $D(\mathfrak{grt}_1)$. The statement fixes the degrees of the generators but not the generators themselves, which is the weakest form that still carries the content of the conjecture.

Milestone level - Brown's half

The same family exists with the morphism merely injective: the $\sigma_{2p+1}$ generate a free Lie subalgebra. This is a theorem (Brown 2012); the open part of the goal is surjectivity.

Supporting levels

The Ihara bracket is a Lie bracket; $\mathfrak{grt}_1$ is closed under it; the degree-$3$ element $[x+y,[x,y]]$ lies in $\mathfrak{grt}_1$; every odd degree $\ge 3$ contains a non-zero element of $\mathfrak{grt}_1$; multiple zeta values satisfy the stuffle and shuffle relations; and $\zeta(2,1) = \zeta(3)$.

Significance

A positive answer would determine $\mathfrak{grt}_1$ completely and, through the $GT$-$GRT$-associator torsor, describe the pro-unipotent Grothendieck-Teichmüller group by generators without relations. Downstream it would pin down the homotopy automorphisms of the rationalised little-discs operad and the Lie algebra of the motivic Galois group of mixed Tate motives over $\mathbb Z$ up to the same freeness statement. Without it, even the dimension of $\mathfrak{grt}_1$ in a given degree is only known to be bounded above by the Broadhurst-Kreimer style count, with equality unproved.

Formalizing this mission produces a machine-checked definition of $\mathfrak t_n$, $\mathfrak{grt}_1$ and the Ihara bracket - objects that have no Mathlib counterpart at present - and machine-checked proofs of the Lie-theoretic facts around them. Brown's theorem itself is proved in the literature but not formalized; the goal statement is genuinely open, and no part of this mission is closed by an existing Lean development known to the proposal.

Difficulty

The obvious approach to the goal - exhibit the generators and count dimensions degree by degree - fails in both directions. Upwards, no closed formula for $\sigma_{2p+1}$ is known: they are extracted from the Knizhnik-Zamolodchikov associator, whose coefficients are regularised iterated integrals, and only their leading coefficients are controlled. Downwards, freeness of the subalgebra they generate is not an algebraic manipulation of the three defining equations: Brown derives it from the motivic theory of multiple zeta values, where the missing input is a basis theorem for a period algebra, not an identity in $\mathbb{F}(x,y)$. Even the milestone "$\mathfrak{grt}_1$ is closed under the Ihara bracket" is not a formality: the pentagon equation lives in $\mathfrak t_4$ and must be transported through substitutions into a quotient Lie algebra.

Formalization scope

The formalization commits to the following conventions, all visible in the definition files.

1. The base field is $\mathbb Q$. The source works over a field $K$ of characteristic zero; every statement here is over $\mathbb Q$.
2. $\mathfrak{grt}_1$ is modelled inside the free Lie algebra FreeLieAlgebra ℚ (Fin 2), i.e. by Lie polynomials, not the completed Lie algebra $\widehat{\mathbb{F}}(x,y)$ of the source. The three defining equations are homogeneous, so the graded object determines the completed one; solvers should be aware that no topology or completion appears anywhere.
3. $\mathfrak t_n$ is the quotient of the free Lie algebra on ordered pairs of indices in Fin n by the Lie ideal generated by the four relation families above, so dkGen i j is $t_{i+1,j+1}$ under the shift Fin 4 = {0,1,2,3} versus indices $1,2,3,4$.
4. Homogeneity is expressed by the rescaling characterisation: $\psi$ has degree $n$ if $\psi(cx,cy) = c^n \psi(x,y)$ for all $c \in \mathbb Q$. Over an infinite field this is equivalent to homogeneity for the word-length grading.
5. The Ihara derivation uses $D_f x = 0$. The source writes $D_f x = x$ in Remark 4.4 and in Section 7.3, but that convention contradicts Lemma 7.2 of the same notes and the computation $\{x,y\} = [x,y] + [y,x] = 0$ in Remark 7.2; $D_f x = 0$ is the convention under which both hold, and is the standard one.
6. The Lie structure on $\mathfrak{grt}_1$ is carried by the injection $f \mapsto D_f$ into LieDerivation ℚ (FreeLieAlgebra ℚ (Fin 2)) (FreeLieAlgebra ℚ (Fin 2)), so that freeness can be stated as injectivity of a morphism out of a free Lie algebra without first installing a new Lie algebra structure. Note $f \mapsto D_f$ is injective on $\mathfrak{grt}_1$ but not on all of $\mathbb{F}(x,y)$, where $D_y = 0$; a supporting item records the injectivity actually used.
7. Multiple zeta values are real numbers defined by an iterated tsum; for non-admissible words the series diverges and the definition returns Mathlib's junk value. Every statement about them therefore carries an admissibility hypothesis: all letters $\ge 1$ and first letter $\ge 2$. The stuffle and shuffle products are multisets of words, so no free module on words is needed.
8. Nothing here is vacuous by construction: the defining equations of $\mathfrak{grt}_1$ are linear conditions on a non-zero graded space, $\mathfrak t_4 \ne 0$, and the milestone $[x+y,[x,y]] \in \mathfrak{grt}_1$, $[x+y,[x,y]] \ne 0$ exhibits a non-zero element.

Contributions welcome: the Lie-theoretic milestones (Lemma 7.2, Corollary 7.1, closure of $\mathfrak{grt}_1$, the degree-$3$ element) are self-contained and need no motivic input; the multiple zeta milestones need summability infrastructure for iterated series; Brown's theorem and the goal need a substantial development that does not yet exist in Lean.

Selected references

• V. G. Drinfeld, On quasitriangular quasi-Hopf algebras and a group closely connected with $\mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q)$, Leningrad Math. J. 2 (1991), 829-860.
• F. Brown, Mixed Tate motives over $\mathbb Z$, Annals of Mathematics 175 (2012), 949-976, doi:10.4007/annals.2012.175.2.10.
• T. Willwacher, The Grothendieck-Teichmüller Group, ETH Zürich lecture notes, 27 February 2014 (the source text for this mission).
• T. Willwacher, M. Kontsevich's graph complex and the Grothendieck-Teichmüller Lie algebra, Invent. Math. 200 (2015), 671-760, doi:10.1007/s00222-014-0528-x.