Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns (experimental)
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Is every odd number a sum of k primes? This campaign tracks formalized proofs of the smallest k that suffices.
Schnirelmann (1930) showed some finite k works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved k=5 unconditionally. Helfgott (2013) proved that every odd number greater than 5 is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: 27 is neither prime nor 2 + prime.
Schoolbook matrix multiplication takes n3 operations. The exponent ω is the infimum of all τ such that two n×n matrices can be multiplied in O(nτ) arithmetic operations; trivially ω≥2, and ω=2 is conjectured but open.
Strassen gave the first nontrivial bound, ω<2.81, in 1969, and introduced the laser method in 1986 to reach ω<2.48. Coppersmith and Winograd's 1990 bound of 2.376 stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached ω<2.371339 in 2025, and the current record is ω<2.371177, from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Tarcha: Braid Theory and the Artin Presentation with Explicit Half-Twist GeneratorsTextbook
## Motivation
A **braid** on $n$ strands is the everyday object it sounds like: $n$ strings hanging between two
horizontal plates, each string descending monotonically, no two strings meeting. Emil Artin turned
this picture into algebra in 1925 by showing that braids form a group under concatenation and that
this group has a finite presentation with $n-1$ generators. The braid groups sit at the crossroads
of low-dimensional topology (they are the mapping class groups of punctured discs, and closures of
braids produce every link), of algebra (they are the prototypical Artin–Tits groups, torsion-free
and orderable), and of representation theory and mathematical physics through the Burau, Lawrence–
Krammer and Temperley–Lieb representations.
This mission formalizes the braid-group development of a 2023 master's dissertation, Alexsander
Andrey Gomes Tarcha's *Um Estudo Introdutório da Teoria de Tranças* (UNESP, Rio Claro), whose
capstone is Teorema 3.15: the braid group on $n$ strands admits Artin's presentation. The
dissertation builds the group structure on equivalence classes of geometric braids (Teorema 3.9),
shows that the Artin generators generate (Teorema 3.11), derives the braid and commutation
relations (Proposição 3.14), establishes the presentation (Teorema 3.15), and closes with two
structural properties: the full twist is central (Proposição 3.16) and $B_m$ embeds in $B_n$ for
$m \le n$ (Proposição 3.17).
## Setting
Work in the plane $E^2 = \mathbb{C}$. The **ordered configuration space**
$$F_{0,n}E^2 = \{(z_1,\dots,z_n) \in \mathbb{C}^n : z_k \neq z_l \text{ for } k \neq l\}$$
carries the subspace topology of $\mathbb{C}^n$, and the symmetric group $\Sigma_n$ acts on it by
permuting coordinates. The **unordered configuration space** $B_{0,n}E^2 = F_{0,n}E^2/\Sigma_n$
carries the quotient topology; its points are the $n$-element subsets of the plane. The base
configuration is $(1,2,\dots,n)$, and $*$ denotes its class in $B_{0,n}E^2$. The **geometric braid
group** is
$$\pi_1\bigl(B_{0,n}E^2, *\bigr),$$
a loop of $n$-point configurations being exactly a geometric braid, and homotopy of loops being
exactly the equivalence by elementary moves used in the dissertation.
The **elementary half-twist** $\sigma_{i+1}$, for $0 \le i \le n-2$, is the loop that rotates the
two base points $i+1$ and $i+2$ by the angle $\pi$ about their midpoint $i + \tfrac32$, leaving the
other $n-2$ points fixed:
$$t \;\longmapsto\; \Bigl\{\, i+\tfrac32 \pm \tfrac12 e^{\pi i t} \,\Bigr\} \;\cup\;
\{\,k+1 : k \neq i,\, i+1 \,\}, \qquad t \in [0,1].$$
It returns to the base configuration at $t = 1$ with the two moving points interchanged, so it is a
loop in $B_{0,n}E^2$ and defines a class in $\pi_1(B_{0,n}E^2,*)$.
The **abstract braid group** $B_n$ is the group presented by generators $\sigma_1,\dots,\sigma_{n-1}$
subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad
\sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1} \quad (1 \le i \le n-2).$$
## Formalization targets
### Goal — Teorema 3.15, with the isomorphism pinned on generators
$$\exists\, \varphi : B_n \;\xrightarrow{\ \sim\ }\; \pi_1\bigl(B_{0,n}E^2,*\bigr), \qquad
\varphi(\sigma_{i+1}) = \bigl[\text{half-twist}_i\bigr] \ \ (0 \le i \le n-2).$$
This is the statement the dissertation actually proves: the map $\varphi$ of its proof is defined on
generators by $\varphi(x_i) = [\sigma_i]$, and the work consists in showing that it is a
well-defined homomorphism which is surjective and injective. Asking only for an abstract
isomorphism would leave the generators unconstrained; naming their images is what makes the
presentation usable downstream.
### Milestones
$$\langle\,[\text{half-twist}_i]\,\rangle = \pi_1\bigl(B_{0,n}E^2,*\bigr) \qquad \text{(Teorema 3.11)}$$
$$[\text{half-twist}_i][\text{half-twist}_j] = [\text{half-twist}_j][\text{half-twist}_i]\ (|i-j|\ge 2),
\qquad
[\text{ht}_i][\text{ht}_{i+1}][\text{ht}_i] = [\text{ht}_{i+1}][\text{ht}_i][\text{ht}_{i+1}]$$
$$\forall b \in B_2,\ \exists m \in \mathbb{Z},\ b = \sigma_1^m \qquad \text{(Proposição 3.13)}$$
$$\forall b \in B_3,\ b = \sigma_1^{a_1}\sigma_2^{b_1}\cdots\sigma_1^{a_m}\sigma_2^{b_m}
\qquad \text{(Proposição 3.14)}$$
$$(\sigma_1\sigma_2\cdots\sigma_{n-1})^n \in Z(B_n) \qquad \text{(Proposição 3.16)}$$
$$B_m \hookrightarrow B_n \ \ (m \le n) \qquad \text{(Proposição 3.17)}$$
## Significance
Artin's presentation is what makes the braid groups computable: the word problem, the Burau and
Lawrence–Krammer representations, the Markov moves on braid closures, and the Garside normal form
all start from generators and relations, while the topological side supplies the meaning of those
generators. A formalization that only exhibits an abstract isomorphism cannot be used to compute
with a given geometric braid; the version stated here transports each half-twist loop to a
generator word, which is what downstream work needs.
On the formalization side, the geometric model (configuration spaces and their fundamental groups)
and the algebraic model (a presented group) are already available on the platform in this
environment, and the abstract form of Artin's theorem is already stated there as an open problem.
What this mission adds is: the elementary half-twist as an explicit, machine-checked loop in
$B_{0,n}E^2$ — this definition is proved sorry-free here, including the injectivity of the moving
configuration at every time and the continuity of the path; the sharpened goal that fixes the
isomorphism on generators; and the dissertation's supporting results, none of which is currently
on the platform. None of the milestones or the goal has a machine-checked proof yet.
## Difficulty
Surjectivity of $\varphi$ — every braid is a product of half-twists — is a compactness-and-general-
position argument in the dissertation: cut the braid into finitely many slabs in which a single
crossing occurs. Turning that into a formal proof requires the homotopy-theoretic substitute, since
"general position" is not available for free: a loop of configurations must be subdivided and each
piece pushed to a standard crossing.
Injectivity is harder and is the step where a naive approach fails. It is not enough to check that
the relations hold; one has to know that they are *all* the relations, i.e. that a word whose braid
is null-homotopic is a consequence of the braid relations. The dissertation follows the classical
route through elementary moves on braid diagrams (its Figuras 3.22–3.26), which formalizes as a
long case analysis. The standard modern alternative is the Fadell–Neuwirth fibration together with
an induction on $n$; its inductive step needs the exact sequence of the fibration
$F_{0,n}E^2 \to F_{0,n-1}E^2$, which is itself substantial work.
## Formalization scope
The plane is $\mathbb{C}$; configurations are injective tuples indexed by `Fin n`; the unordered
configuration space is the quotient by the coordinate-permutation action with the quotient
topology; the base configuration is $(1,2,\dots,n)$ (not $(0,1,\dots,n-1)$). Braid generators are
indexed by `Fin (n-1)`, the index $i$ standing for the book generator $\sigma_{i+1}$; truncated
natural subtraction means the degenerate values $n = 0, 1$ give the trivial group, and the
statements are asserted for all $n$ including those cases. The abstract braid group is the
presented group on `Fin (n-1)` modulo the normal closure of the commutation and braid relators.
The half-twist rotates counterclockwise. The mirror symmetry $z \mapsto \bar z$ fixes the base
configuration and exchanges the two orientations, so the goal statement does not depend on this
choice; a solver may use either convention internally.
The goal cannot be satisfied trivially: it asks for a group isomorphism whose values on the
generators are the prescribed classes of explicit loops, so neither the identity on a presented
group nor an abstract counting argument suffices.
Contributions welcome beyond the milestones: the Fadell–Neuwirth exact sequence for the plane, the
pure braid group as the kernel of the map to $\Sigma_n$, the exponent-sum homomorphism, and
torsion-freeness of $B_n$. The half-twist definition published with this mission is reusable for
any further work on braids in this environment.
## Selected references
- Alexsander Andrey Gomes Tarcha, *Um Estudo Introdutório da Teoria de Tranças*, master's
dissertation, UNESP Rio Claro, 2023. https://repositorio.unesp.br/items/9d2ffbf0-8bd2-4ec7-9e45-e2cee8a1b202
- Emil Artin, *Theorie der Zöpfe*, Abhandlungen aus dem Mathematischen Seminar der Universität
Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
- Joan S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82,
Princeton University Press, 1974. https://doi.org/10.1515/9781400881420
- Edward Fadell and Lee Neuwirth, *Configuration spaces*, Mathematica Scandinavica 10 (1962),
111–118. https://doi.org/10.7146/math.scand.a-10517
Kriz–Nordentoft: Horizontal p-adic L-functionsResearch Paper
## Motivation
Central values of twists of elliptic-curve and modular-form $L$-functions govern arithmetic questions ranging from Mordell--Weil ranks to the distribution of nonvanishing twists. Classical Iwasawa theory organizes twists whose conductors grow vertically through powers of one prime. Kriz and Nordentoft introduce a horizontal analogue in which the order of the character is fixed while its conductor acquires new prime factors. Their paper [*Horizontal p-adic L-functions*](https://arxiv.org/abs/2310.20678) constructs measures encoding these twists and proves a structure theorem that forces quantitative nonvanishing.
The mission formalizes the paper's common mechanism behind its nonvanishing theorems: Fourier theory of horizontal measures, norm-compatible modular-symbol theta elements, interpolation of central values, and propagation from nonzero measures to logarithmic-power lower bounds. The elliptic-curve statements in Theorems 1.1 and 1.2 are obtained in the paper by specializing this mechanism to weight-two newforms and adding the stated Galois-representation hypotheses.
## Setting
Fix a prime $p$. The **digit group** is the compact product
$$G_p=\prod_{n\ge 0}\mathbf Z/p\mathbf Z.$$
A continuous character of $G_p$ has finite image and factors through a finite product. For a complete algebraically closed nonarchimedean field $K$ of residue characteristic $p$, a **horizontal measure** is represented in Lean by a continuous $K$-linear functional on the Banach space $C(G_p,K)$. Its Fourier transform is
$$\widehat\nu(\chi)=\int_{G_p}\chi\,d\nu.$$
The integral measures arising from the digit Iwasawa algebra have Fourier norms in a discrete geometric lattice. This is recorded explicitly by `HasDiscreteFourierNorm`; it is the norm-language counterpart of the discrete valuation hypothesis used in Corollary 2.9.
On the arithmetic side, modular symbols produce theta elements at finite squarefree conductors. Their projection maps do not initially form a compatible inverse system: an Euler factor appears each time a prime is removed. At an orderly prime this factor is a unit, so normalization produces a compatible system and hence a horizontal $p$-adic $L$-function. Evaluation at a character gives the modified central $L$-value of the corresponding twist.
## Formalization targets
### Finite-correction structure and interpolation
For every nonzero integral horizontal measure $\nu$, there is a finite set $M_\nu$ of characters and a constant $c>0$ such that
$$
\lvert\widehat\nu(\chi\chi_0)\rvert_p=c
$$
for some $\chi_0\in M_\nu$, for every continuous character $\chi$. If $\nu$ interpolates modified central values, these corrected values are nonzero and have optimal $p$-adic size. This is Theorem 1.6, equivalently the digit-algebra case of Corollary 2.9, combined with Corollary 5.4.
### Elliptic-curve specialization
For a modular elliptic curve over $\mathbf Q$, the normalized theta system is assembled into the horizontal $p$-adic $L$-function of Definition 5.3 and shown to satisfy Corollary 5.4. The final milestones then specialize the structure and propagation theorems to prove Theorems 1.1 and 1.2 (assuming modularity), retaining the three alternative hypotheses of Theorem 1.1 and the jointly-good hypothesis for simultaneous nonvanishing in Theorem 1.2.
### Quantitative propagation
If a fixed-order family has counting function bounded below by $X/(\log X)^{1-\alpha}$ and every character is related to a nonvanishing one by one of finitely many conductor-bounded corrections, the same lower bound holds for the nonvanishing subfamily. This isolates the formal content of Theorem 5.9 used in the applications of Section 5.4.
## Significance
The structure theorem replaces one-variable Weierstrass preparation in an infinite-dimensional, non-noetherian Iwasawa algebra. It shows that the zero set of a nonzero horizontal measure is rigid enough that finitely many translations detect an optimal Fourier value everywhere. Through interpolation, this converts a single nonzero horizontal $p$-adic $L$-function into infinitely many nonzero complex central values with a quantitative lower bound.
A formal proof will add reusable infrastructure for nonarchimedean Fourier analysis on profinite products, finite group rings, inverse systems of theta elements, and character-counting asymptotics. None of these results currently has a machine-checked proof in Mathlib. The development is arranged so the analytic structure theorem and the modular-symbol construction can be attacked independently.
## Difficulty
The central obstacle is that the horizontal Iwasawa algebra is neither noetherian nor reduced. A direct compactness or finite-generation argument on its spectrum is unavailable. At finite level, Fourier inversion introduces the group order into the valuation estimates; globally, one must control compatible finite quotients while keeping the exceptional correcting set finite. The arithmetic half has a separate normalization problem: raw theta elements satisfy norm relations only up to Euler factors, and interpolation must track imprimitive characters and the removed Euler factors exactly.
## Formalization scope
The first version works with the exponent-$p$ digit group $G_p$, which is the setting of Theorem 1.6. Characters take values in the unit group of a complete algebraically closed ultrametric field $K$. Measures are continuous linear functionals on $C(G_p,K)$, and discreteness of integral Fourier values is an explicit hypothesis. The definition does not assume the finite-correction conclusion.
The modular-form layer is exposed through `RawThetaSystem`, `ThetaSystem`, and `InterpolationDatum`. Milestones must construct these data from genuine modular symbols and prove their norm and interpolation fields; merely postulating the desired nonvanishing values does not satisfy the goal. The quantitative statement uses an explicit eventual lower bound rather than asymptotic notation hidden behind an uninterpreted predicate.
## Selected references
- Daniel Kriz and Asbjørn Christian Nordentoft, *Horizontal p-adic L-functions*, arXiv:2310.20678v3, 2025. https://arxiv.org/abs/2310.20678
- Yuri Manin, *Periods of parabolic forms and p-adic Hecke series*, Mathematics of the USSR-Sbornik 21 (1973). https://doi.org/10.1070/SM1973v021n03ABEH002016
- Glenn Stevens, *The cuspidal group and special values of L-functions*, Transactions of the AMS 291 (1985). https://doi.org/10.1090/S0002-9947-1985-0797057-3
### Current proof decomposition
The new definition node isolates the horizontal Iwasawa algebra and the interpolation interface. The first new milestone constructs a nonzero horizontal $2$-adic $L$-function $\nu_E$. The second milestone assumes such a pair $(\nu_E,\nu_E\ne0)$ and combines the horizontal-measure structure theorem, the Friedberg--Hoffstein quadratic seed, Corollary 5.10, and fixed-order character counting to obtain the lower bound in Theorem 1.1(1). The mission goal then follows immediately by applying the existence milestone and passing its witness to the implication milestone.
Long-Wagner Conjecture 5.1: cube-free subsets of Z/2^nZ have density at most 5/8Open Problem
Call $A \subseteq \mathbb{Z}/2^n\mathbb{Z}$ *cube-free* if no triple $x, y, z$ has all seven of $x$, $y$, $z$, $x+y$, $y+z$, $z+x$, $x+y+z$ inside $A$. The triple is unconstrained, so a degenerate one counts. Write $f(n)$ for the largest size of a cube-free subset.
**The conjecture.** $f(n) \le \frac{5}{8} 2^n$ for every $n$.
This is Conjecture 5.1 of Jason Long and Adam Zsolt Wagner, *The largest projective cube-free subsets of $\mathbb{Z}_{2^n}$*, [arXiv:1810.01225](https://arxiv.org/abs/1810.01225). It has been open since October 2018, and a 2026 journal paper still names it as conjectured: Yuchen Meng, *On Cube-Free Problems*, Electron. J. Combin. 33(1) (2026) #P1.16.
## The constant is attained
The bound is sharp, and the extremal set is explicit: $A = \{v : v \bmod 8 \in \{1,3,4,5,7\}\}$, the odd residues together with those congruent to 4 mod 8. Its size is $2^{n-1} + 2^{n-3} = \frac{5}{8} 2^n$. In the layer language of Long and Wagner this is $C_3 = L_1 \cup L_3$.
## What is known
The conjecture holds for unions of layers. That is Long-Wagner Theorem 1.10 at $d = 3$, and it is the largest class on which the conjectured constant is proved.
For arbitrary sets the best published unconditional bound is $f(n) < \frac{2}{3} 2^n$. Meng calls this bound "quite trivial" and gives it in one paragraph for every cyclic group, so it should not be read as progress toward $5/8$. The residual gap is exactly $\frac{2}{3} - \frac{5}{8} = \frac{1}{24}$, that is $2^n/24$ elements.
Small values are $f(1) = 1$, $f(2) = 2$, $f(3) = 5$, $f(4) = 10$, $f(5) = 20$, $f(6) = 40$, $f(7) = 80$, matching $2^{n-1} + 2^{n-3}$ from $n = 3$ on.
**State those values honestly.** They come from solver searches, Gurobi in Long and Wagner for $n \le 7$ and an independent SAT reproduction. The SAT half that matters, the unsatisfiability of "a cube-free set of size 81 exists at $n = 7$", is a solver claim with no proof certificate checked and no kernel check behind it. The witness half is verified: a set of exactly 80 elements was produced and re-checked cube-free. So $f(7) \ge 80$ is solid and $f(7) \le 80$ is not certified. Nothing in this mission rests on either.
## What the items are
The goal item is the conjecture itself, for $n \ge 4$, and it is open. Every other item is a milestone that is proved mathematics, and the two closed instances $n = 4$ and $n = 5$ are stated separately because they are the only cases of the goal that a proof assistant has actually settled here.
The chain runs: the base case mod 8 by exhaustion, monotonicity under subsets, the bridge between the membership form and the `Finset` form of the forbidden configuration, sharpness, the odd-residue tight case, the layer-union theorem, the two-thirds bound, and then $n = 4$ and $n = 5$.
## Notes on the formalization
Six definitions live in one definition item, `Def_Z2nCubeFreeLayers`: `HasCube`, `CubeFree`, `config`, `ConfigFree`, `layerIdx` and `IsLayerUnion`. `layerIdx` is written through the 2-adic valuation rather than through a congruence, because the congruence form leaves $0$ in no layer at all and needs the last layer special-cased.
`CubeFree` and `ConfigFree` are two encodings of the same condition and they are not definitionally equal, because `config` collapses duplicates on a degenerate triple. Their equivalence is a milestone rather than an assumption.
Formal Conjectures Portfolio: Bateman-Horn and CompanionsOpen Problem
## 1. Motivation
Wikipedia's pages on open problems are, for many mathematicians, the first contact with a
conjecture: a one-paragraph statement, a short history, a list of partial results. The
[Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) library (Google
DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the
conjectures can be attacked — and, just as importantly, *stated unambiguously* — by machine.
This mission ports a coherent slice of that material to Prove2Me. It is deliberately a
**portfolio mission**: the goal theorem is the Bateman–Horn conjecture, the strongest single
statement in the collection, and the milestone list gathers the other conjectures and the
landmark theorems that surround them. Some milestones are genuine steps toward the goal (the
Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems
from other fields, grouped here because they share a source, a level of difficulty, and a need
for faithful formal statements. **A reader should not assume that proving a milestone advances
the goal theorem.** The mission's value is that every statement in it has been written against
the same Mathlib revision, checked to compile, and documented well enough to be attacked.
A rough timeline of the collection's landmarks:
- 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
- 1962 — Radó: the busy beaver function outgrows every computable function.
- 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$.
- 1978 — Apéry: $\zeta(3)$ is irrational.
- 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant
subspace.
- 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
- 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
- 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
- 2021 — Gardam: Kaplansky's *unit* conjecture is false (its zero-divisor and idempotent
companions remain open).
- 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$.
- 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$.
## 2. Setting
The goal theorem concerns prime values of polynomials. Fix a finite set
$S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the
**Bunyakovsky condition** if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is
irreducible over $\mathbb{Z}$; say that $S$ satisfies the **Schinzel condition** if for every
prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides
the product at every argument.
For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some
$f_i$ vanishes, let $D=\prod_i \deg f_i$, and let
$$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$
The **Bateman–Horn constant** is the (conditionally convergent) Euler product
$$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$
The other groups use their own vocabulary, each fixed in a definition item of this mission:
Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property
$\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial
self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of
a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its
maximum-shifts function $\mathrm{BB}$.
## 3. Target
The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses,
$C$ exists and is positive and
$$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$
Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's
conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The
remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine
equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality
(New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants
(Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$,
Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample),
group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry
(the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta
values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the
$1/3$–$2/3$ conjecture), and computability (Radó's theorem).
## 4. Significance
*The results themselves.* Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it
contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky
as special cases, and it is the standard heuristic behind prime-counting predictions. The other
targets are each the headline question of their area: whether every bounded Hilbert-space
operator has an invariant subspace; whether group algebras of torsion-free groups are domains;
whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir,
Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library
contributions in their own right.
*Formalizing them.* None of the open statements is expected to fall here; the concrete deliverable
is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones,
most of which are not in Mathlib today. Several are realistically in reach: the finite-field
Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$
cannot both be algebraic, and Radó's diagonal argument.
## 5. Difficulty
For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound
$\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes,
but the parity problem blocks every known sieve from producing a single prime value of an
irreducible quadratic. The conditional convergence of the Euler product is a second, smaller
trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered
infinite product changes the statement.
Each other group has its own obstruction, and they do not transfer: the parity problem says
nothing about Kakeya, where the difficulty is that dimension is not stable under the natural
compactness arguments, nor about the invariant subspace problem, where the known counterexamples
on $\ell^1$ show that no soft argument can work.
## 6. Formalization scope
Conventions this mission commits to, all fixed in the definition items:
- Polynomials are elements of `ℤ[X]`; primality of a polynomial value is primality of its
absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$.
- The Bateman–Horn constant is the limit of the *ordered* partial products over $p<N$, not an
unordered infinite product.
- Kakeya sets carry no compactness or measurability hypothesis, matching the source; the
conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$.
- Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$.
- Torsion-freeness of a group is spelled out as "every element of finite order is the identity",
which is the hypothesis the source intends (it is weaker than Mathlib's `IsMulTorsionFree`).
- Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities
are quotients of set cardinalities in $\mathbb{Q}$.
- The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean
tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition
included, and $\mathrm{BB}(0)=0$.
- Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me
statements must be definite, so each such question is recorded in its **affirmative** form
(e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one
question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth
theorem rather than guessed at.
- Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya
sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).
Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful
statements from the same source library, which contains far more than fits in one mission.
## 7. Selected references
- P. T. Bateman and R. A. Horn, *A heuristic asymptotic formula concerning the distribution of
prime numbers*, Math. Comp. 16 (1962), 363–367.
[DOI](https://doi.org/10.1090/S0025-5718-1962-0148632-7)
- T. Radó, *On non-computable functions*, Bell System Tech. J. 41 (1962), 877–884.
[DOI](https://doi.org/10.1002/j.1538-7305.1962.tb00480.x)
- R. O. Davies, *Some remarks on the Kakeya problem*, Math. Proc. Cambridge Philos. Soc. 69
(1971), 417–421. [DOI](https://doi.org/10.1017/S0305004100046867)
- C. J. Read, *A solution to the invariant subspace problem on the space $\ell_1$*, Bull. London
Math. Soc. 17 (1985), 305–317. [DOI](https://doi.org/10.1112/blms/17.4.305)
- K. Falconer, *On the Hausdorff dimensions of distance sets*, Mathematika 32 (1985), 206–212.
[DOI](https://doi.org/10.1112/S0025579300010998)
- W. Zudilin, *One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational*, Russian
Math. Surveys 56 (2001), 774–776. [DOI](https://doi.org/10.1070/RM2001v056n04ABEH000427)
- P. Mihăilescu, *Primary cyclotomic units and a proof of Catalan's conjecture*, J. reine angew.
Math. 572 (2004), 167–195. [DOI](https://doi.org/10.1515/crll.2004.048)
- Z. Dvir, *On the size of Kakeya sets in finite fields*, J. Amer. Math. Soc. 22 (2009),
1093–1097. [DOI](https://doi.org/10.1090/S0894-0347-08-00607-3)
- B. Bukh and T.-W. Chao, *Sharp density bounds on the finite field Kakeya problem*, Discrete
Analysis 26 (2021). [DOI](https://doi.org/10.19086/da.30071)
- G. Gardam, *A counterexample to the unit conjecture for group rings*, Ann. of Math. 194 (2021),
967–979. [DOI](https://doi.org/10.4007/annals.2021.194.3.9)
- K. Saito, *Mills' constant is irrational*, Mathematika 71 (2025), e70027.
[arXiv:2404.19461](https://arxiv.org/abs/2404.19461)
- H. Wang and J. Zahl, *Volume estimates for unions of convex sets, and the Kakeya set conjecture
in three dimensions*, [arXiv:2502.17655](https://arxiv.org/abs/2502.17655)
- Google DeepMind, *Formal Conjectures*, Apache-2.0,
[github.com/google-deepmind/formal-conjectures](https://github.com/google-deepmind/formal-conjectures)
---
*Provenance note.* The Lean statements in this mission are adaptations of the Formal Conjectures
library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition
items, and checked to compile against the platform's Mathlib revision. Each draft item carries a
read-back; **those read-backs are non-blind** — they were written by the same agent that drafted
the statements, and each says so in its first line. They are documentation, not independent
testimony.
## Motivation
Almost every classical transcendence theorem is a statement about the interaction between the additive structure of $\mathbb{C}$ and the exponential function. Hermite proved in 1873 that $e$ is transcendental, Lindemann in 1882 that $e^{\alpha}$ is transcendental for every nonzero algebraic $\alpha$ — hence that $\pi$ is transcendental and the circle cannot be squared — and Weierstrass in 1885 extended this to the linear independence of $e^{\alpha_1},\dots,e^{\alpha_n}$ over $\overline{\mathbb{Q}}$ for distinct algebraic $\alpha_i$. Gelfond and Schneider settled Hilbert's seventh problem in 1934, and Baker's 1966 theorem on linear forms in logarithms made the subject effective.
**Schanuel's conjecture**, formulated by Stephen Schanuel in the 1960s and first published by Lang (*Introduction to Transcendental Numbers*, Addison–Wesley, 1966, Chapter III), is a single statement that contains all of these as special cases, together with a large number of statements that remain open — for instance that $e$ and $\pi$ are algebraically independent, or that $e + \pi$ is irrational. No case of it is known beyond those already covered by the Lindemann–Weierstrass theorem or by Baker's theorem.
Timeline, with the hypotheses each result actually assumes:
- 1882, Lindemann: $e^{\alpha}$ is transcendental for algebraic $\alpha \neq 0$.
- 1885, Weierstrass: for pairwise distinct algebraic $\alpha_1,\dots,\alpha_n$, the values $e^{\alpha_1},\dots,e^{\alpha_n}$ are linearly independent over $\overline{\mathbb{Q}}$.
- 1934, Gelfond and Schneider, independently: if $\lambda \neq 0$ is a logarithm of an algebraic number and $\beta$ is algebraic and irrational, then $e^{\beta\lambda}$ is transcendental.
- 1960s, Siegel, Lang and Ramachandra: the six exponentials theorem, unconditional; the analogous four exponentials statement is still open.
- 1966, Baker: if logarithms $\lambda_1,\dots,\lambda_n$ of algebraic numbers are linearly independent over $\mathbb{Q}$, then $1,\lambda_1,\dots,\lambda_n$ are linearly independent over $\overline{\mathbb{Q}}$.
- 1971, Ax: the function-field analogue of Schanuel's conjecture, for formal power series and, more generally, differential fields of characteristic zero.
## Setting
Write $\exp$ for the complex exponential function. A tuple $z_1,\dots,z_n$ of complex numbers is **linearly independent over $\mathbb{Q}$** when the only rationals $q_1,\dots,q_n$ with $\sum_i q_i z_i = 0$ are $q_1 = \dots = q_n = 0$; here $\mathbb{C}$ is viewed as a vector space over $\mathbb{Q}$.
For a subset $S \subseteq \mathbb{C}$, let $\mathbb{Q}(S)$ denote the subfield of $\mathbb{C}$ generated by $S$ over $\mathbb{Q}$. The **transcendence degree** $\operatorname{trdeg}_{\mathbb{Q}} \mathbb{Q}(S)$ is the cardinality of a transcendence basis of $\mathbb{Q}(S)$ over $\mathbb{Q}$: the largest number of elements of $\mathbb{Q}(S)$ that are algebraically independent over $\mathbb{Q}$. A number $x$ is **transcendental** over $\mathbb{Q}$ when no nonzero polynomial with rational coefficients vanishes at $x$, and numbers $x_1,\dots,x_m$ are **algebraically independent** over $\mathbb{Q}$ when no nonzero polynomial in $m$ variables with rational coefficients vanishes at $(x_1,\dots,x_m)$.
## Formalization targets
### Goal
$$z_1,\dots,z_n \text{ linearly independent over } \mathbb{Q} \;\Longrightarrow\; \operatorname{trdeg}_{\mathbb{Q}} \mathbb{Q}\bigl(z_1,\dots,z_n,\,e^{z_1},\dots,e^{z_n}\bigr) \;\ge\; n .$$
The goal fixes no numerical constant and no special shape for the $z_i$: it asserts only the inequality, for every $n$ and every $\mathbb{Q}$-linearly independent tuple. The case $n = 0$ is vacuous and the conclusion is a bound on a cardinal, so nothing is hidden in a degenerate convention.
### Milestones
The milestone list consists of the landmark unconditional theorems that Schanuel's conjecture generalizes, the known function-field analogue, and one conditional corollary that records what the conjecture buys:
- Hermite–Lindemann (1882): $\alpha$ algebraic and nonzero $\Rightarrow$ $e^{\alpha}$ transcendental.
- Lindemann–Weierstrass (1885): $\sum_i \beta_i e^{\alpha_i} \neq 0$ for distinct algebraic $\alpha_i$ and algebraic $\beta_i$ not all zero.
- Gelfond–Schneider (1934): $\lambda \neq 0$ a logarithm of an algebraic number, $\beta$ algebraic irrational $\Rightarrow$ $e^{\beta\lambda}$ transcendental.
- Six exponentials theorem: $x_1,x_2$ and $y_1,y_2,y_3$ each $\mathbb{Q}$-linearly independent $\Rightarrow$ at least one of the six numbers $e^{x_i y_j}$ is transcendental.
- Baker (1966): $\mathbb{Q}$-linearly independent logarithms of algebraic numbers, together with $1$, are linearly independent over $\overline{\mathbb{Q}}$.
- Ax (1971), power series form: $\operatorname{trdeg}_{\mathbb{C}} \mathbb{C}(f_1,\dots,f_n,g_1,\dots,g_n) \ge n+1$ when $g_i' = f_i' g_i$, the $g_i$ are units, and no nontrivial $\mathbb{Q}$-linear combination of the $f_i$ is constant.
- Conditional corollary: Schanuel's conjecture implies that $e$ and $\pi$ are algebraically independent over $\mathbb{Q}$.
## Significance
Schanuel's conjecture decides, in one stroke, a long list of questions that are individually open: the algebraic independence of $e$ and $\pi$, the irrationality of $e+\pi$ and of $e\pi$, the transcendence of $e^{e}$ and $\pi^{\pi}$, the four exponentials conjecture, and — combined with work of Macintyre and Wilkie — the decidability of the first-order theory of the real exponential field. Its restriction to algebraic $z_i$ is exactly the Lindemann–Weierstrass theorem, and its restriction to $z_i$ whose exponentials are algebraic is exactly Baker's theorem, so the conjecture is a common generalization of the two main unconditional pillars of the subject.
On the formalization side, the state of the art in Lean's mathematical library is modest relative to this history: the analytic core of the Lindemann–Weierstrass argument is present, but the Hermite–Lindemann theorem, the Lindemann–Weierstrass theorem, the transcendence of $\pi$, the Gelfond–Schneider theorem, the six exponentials theorem and Baker's theorem are not available as usable statements in the pinned environment. Each milestone here is therefore a genuine formalization project with a known mathematical proof, and none of them is a restatement of an existing library result. The goal theorem itself is open mathematically; the realistic contributions to it are reductions — implications between the goal and other statements — and closing the milestones that the conjecture generalizes.
## Difficulty
The obvious approach to any single case — build an auxiliary function with many zeros, bound its derivatives, and derive a contradiction from an integrality argument — is the method behind every result on the milestone list, and it is exactly what fails for the conjecture in general. Those proofs need the exponentials, or the arguments, to be algebraic somewhere, so that heights and denominators can be controlled; for a general $\mathbb{Q}$-linearly independent tuple there is no arithmetic input at all, and no known construction produces the required auxiliary function. Ax's theorem shows that the differential-algebraic shadow of the statement is true, but its proof uses the derivation on the function field and has no arithmetic counterpart. A solver should not expect the conjecture itself to fall to a variation of the classical method.
## Formalization scope
All statements are over $\mathbb{C}$, with the complex exponential. Tuples are indexed by `Fin n`, `ℚ`-linear independence is Mathlib's `LinearIndependent ℚ`, transcendence degree is Mathlib's `Algebra.trdeg`, the generated field is `IntermediateField.adjoin`, and the inequality is between cardinals, so the goal reads `(n : Cardinal) ≤ Algebra.trdeg ℚ (adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z)))`. Algebraicity is `IsAlgebraic ℚ`, transcendence is `Transcendental ℚ`, and algebraic independence is `AlgebraicIndependent ℚ`.
There is no trivializing formalization here: the hypothesis `LinearIndependent ℚ z` is satisfiable for every $n$, so the goal is not vacuous, and the conclusion is an inequality of cardinals rather than a statement about a definition introduced for this mission.
The Ax milestone is stated for formal power series in one variable over $\mathbb{C}$: the exponential relation is expressed as the differential equation $g_i' = f_i' g_i$ with `PowerSeries.derivative`, and the conclusion bounds `Algebra.trdeg ℂ` of the `ℂ`-subalgebra generated by the $f_i$ and the $g_i$. The conditional corollary takes the full statement of Schanuel's conjecture as an explicit hypothesis, so it is provable unconditionally as stated.
Infrastructure that a complete development needs, and that is reusable well beyond this mission: Siegel's lemma and height machinery for algebraic numbers, the standard auxiliary-function construction with derivative bounds, and interface lemmas relating `Algebra.trdeg`, `AlgebraicIndependent` and `Transcendental`. Reductions between the milestones — for example deriving Hermite–Lindemann from Lindemann–Weierstrass, or the six exponentials theorem from a general Baker-type statement — are welcome as sketches.
## Selected references
- S. Lang, *Introduction to Transcendental Numbers*, Addison–Wesley, 1966. (Schanuel's conjecture is stated in Chapter III.)
- A. Baker, *Linear forms in the logarithms of algebraic numbers I*, Mathematika 13 (1966), 204–216. https://doi.org/10.1112/S0025579300003971
- J. Ax, *On Schanuel's conjectures*, Annals of Mathematics 93 (1971), 252–268. https://doi.org/10.2307/1970774
- A. Macintyre and A. J. Wilkie, *On the decidability of the real exponential field*, in Kreiseliana, A K Peters, 1996, 441–467.
- M. Waldschmidt, *Diophantine Approximation on Linear Algebraic Groups*, Springer, 2000.
- Wikipedia, *Schanuel's conjecture*. https://en.wikipedia.org/wiki/Schanuel%27s_conjecture
## 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$:
$$
\begin{array}{llllllll}
2 & 3 & 5 & 7 & 11 & 13 & 17 & \dots\\
1 & 2 & 2 & 4 & 2 & 4 & \dots\\
1 & 0 & 2 & 2 & 2 & \dots\\
1 & 2 & 0 & 0 & \dots\\
1 & 2 & 0 & \dots
\end{array}
$$
**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](https://doi.org/10.1090/S0025-5718-1959-0105398-3)).
- 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](https://doi.org/10.1090/S0025-5718-1993-1192979-9)).
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
$$
d^0(n) = p_n, \qquad d^{k+1}(n) = \bigl| d^{k}(n+1) - d^{k}(n) \bigr| \quad (k, n \ge 0).
$$
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
$$
\forall k \ge 1,\qquad d^{k}(0) = 1 .
$$
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
4-to-1 Games with Perfect CompletenessResearch Paper
## Motivation
Many approximation problems resist the standard PCP toolkit: the best known NP-hardness
factors for **Max-Cut**, **Vertex-Cover** and **approximate graph colouring** are far from
the best known polynomial-time algorithms. To explain this gap, Khot (CCC 2002) proposed the
**Unique-Games Conjecture** and the family of **$d$-to-1 Games Conjectures**. The
$d$-to-1 conjectures assert *perfect completeness*: the hard instances are either fully
satisfiable, or satisfiable only to a vanishing extent. Perfect completeness is what makes
these conjectures usable for colouring problems, where a "yes" instance must be genuinely
$3$-colourable rather than almost so.
A line of work culminating in Khot–Minzer–Safra and Dinur–Khot–Kindler–Minzer–Safra
established the *almost*-perfect completeness version for $2$-to-1 games: for every
$\varepsilon>0$ there is an alphabet bound $r$ such that distinguishing value
$\ge 1-\varepsilon$ from value $\le\varepsilon$ is NP-hard. Their route goes through
Håstad's hardness for linear equations, which cannot have perfect completeness, so the loss
is intrinsic to the technique. The source paper of this mission removes that loss for
$d = 4$.
## Setting
A **label-cover instance** $\Psi$ (Definition 1.1 of the source) consists of a bipartite
graph $G = (L \sqcup R, E)$, two finite alphabets $\Sigma_L, \Sigma_R$, and for each edge
$e = (u,v)$ a constraint $\Phi_e \subseteq \Sigma_L \times \Sigma_R$. The constraint is a
**projection constraint** if there is $\varphi_e : \Sigma_L \to \Sigma_R$ with
$\Phi_e = \{(\sigma, \varphi_e(\sigma))\}$, and a **$d$-to-1 constraint** if in addition
$|\varphi_e^{-1}(\sigma)| = d$ for every $\sigma \in \Sigma_R$. Given assignments
$A_L : L \to \Sigma_L$ and $A_R : R \to \Sigma_R$, the fraction of satisfied edges is
$\mathrm{val}_\Psi(A_L, A_R)$, and
$$\mathrm{val}(\Psi) \;=\; \max_{A_L, A_R} \mathrm{val}_\Psi(A_L, A_R).$$
An instance all of whose constraints are $d$-to-1 is a **$d$-to-1 game**.
For $0 < s < c \le 1$, $\mathrm{Gap\text{-}}d\mathrm{\text{-}to\text{-}}1_r(c,s)$ is the
promise problem: given a $d$-to-1 game with both alphabets of size at most $r$, distinguish
$\mathrm{val}(\Psi) \ge c$ from $\mathrm{val}(\Psi) \le s$. Writing
$\mathrm{GapPLC}_r(c,s)$ for the same promise problem over all projection instances, the
PCP theorem together with the parallel repetition theorem gives that
$\mathrm{GapPLC}_{r}(1,\varepsilon)$ is NP-hard for a suitable $r = r(\varepsilon)$
(Theorem 1.2 of the source); this mission takes that statement as an external input.
## Formalization targets
### Goal — Theorem 1.6 of the source
$$\forall \varepsilon > 0 \ \exists r \in \mathbb{N}^{+} : \quad
\mathrm{Gap\text{-}4\text{-}to\text{-}1}_r(1,\varepsilon) \text{ is NP-hard.}$$
In Lean this is stated as a **polynomial-time gap-preserving reduction**: for every
$\varepsilon > 0$ there is a soundness threshold $s \in (0,1)$ such that for every source
alphabet bound $r_0$ there is a target alphabet bound $r$ and a polynomial-time computable
map sending projection label-cover instances with alphabets of size at most $r_0$ and value
$1$ to $4$-to-1 games with alphabets of size at most $r$ and value $1$, and instances of
value at most $s$ to $4$-to-1 games of value at most $\varepsilon$. Combined with the
NP-hardness of $\mathrm{GapPLC}_{r_0}(1,s)$, this is exactly Theorem 1.6.
### Supporting targets
The milestone list follows the source's own numbering: the hardness of approximate colouring
of $3$-uniform hypergraphs that starts the construction (Theorem 3.1), the two Grassmann
decoding theorems the inner PCP rests on (Theorems 3.2 and 3.3), the sunflower bound on
zoom-outs (Lemma 3.8), and the linear-algebraic layer connecting NAE-satisfying bilinear
forms with their tensor decompositions (Propositions 4.13, 4.14 and Corollary 4.15).
## Significance
Theorem 1.6 confirms the $4$-to-1 Games Conjecture, the first of Khot's $d$-to-1 conjectures
to be settled with perfect completeness. Via known reductions it yields: for every $k$, it is
NP-hard to $k$-colour a $3$-colourable graph (previously known for $k = 5$); for every
$\delta>0$, it is NP-hard to find an independent set of relative size $\delta$ in a
$2$-colourable $3$-uniform hypergraph; and hardness results for low-rank matrix completion.
None of this material is formalized today. Mathlib has no label cover, no PCP machinery, no
Grassmann graph and no complexity classes beyond the computability layer. A complete
development therefore contributes reusable infrastructure — finite two-prover games and their
value, gap-preserving reductions, the Grassmann graph over $\mathbb{F}_2$ and its agreement
tests — well beyond this single theorem.
## Difficulty
The obvious attempt is to redo the $2$-to-1 construction with a perfectly complete outer PCP,
namely hardness of systems of *quadratic* equations over $\mathbb{F}_2$ in place of linear
ones. This fails at composition: the Grassmann agreement test, the only known device that
produces $d$-to-1 constraints, is a test for *linear* functions and cannot certify quadratic
constraints. Linearizing the quadratic equations by a low-rank test destroys the **covering
property** of the outer PCP, which is what makes the composed soundness analysis work. The
source paper's answer is a three-layer construction (outer, middle and inner PCP) with a lazy
parallel repetition in the middle layer and an inner PCP based on a tensor of the standard
Grassmann encoding with Golowich's low-rank variant.
## Formalization scope
All objects are finite and explicit. A label-cover instance carries left vertices
$\{0,\dots,n_L-1\}$, right vertices $\{0,\dots,n_R-1\}$, alphabets
$\{0,\dots,|\Sigma_L|-1\}$ and $\{0,\dots,|\Sigma_R|-1\}$, a finite edge set, and a
projection map for every pair of vertices; only projection instances are representable, as in
Definition 1.1. The value is the supremum over all pairs of assignments of the fraction of
satisfied edges, taken in $\mathbb{R}$; when there are no edges, or no assignments at all,
the convention gives value $0$. A tripled set (Definition 4.1) is modelled as
$\iota \times \{0,1,2\}$, with the triple indexed by $i$ being
$\{(i,0),(i,1),(i,2)\}$. The Grassmann objects live in $\mathbb{F}_2^n$ modelled as
$\mathrm{Fin}\,n \to \mathbb{Z}/2$, and all probabilities are ratios of cardinalities of
finite sets of subspaces, with the convention that an empty denominator gives $0$.
Hardness is **not** stated as "NP-hard" — no notion of NP is available — but as the existence
of a reduction. This matters: a reduction required only to preserve the gap, with no
computability condition, would be trivially satisfiable by a map that inspects the value of
its input and returns one of two fixed instances. The formalization therefore requires the
reduction map to be computed by a Turing machine within a polynomial time bound, using
Mathlib's `Turing.TM2ComputableInPolyTime` together with an explicit binary encoding of
instances. The NP-hardness of the source problem $\mathrm{GapPLC}_{r_0}(1,s)$ (Theorem 1.2,
i.e. the PCP theorem plus parallel repetition) is an external input and is not part of this
mission.
Contributions of intermediate infrastructure are welcome: the games of Sections 4–6 (Game1a,
Game1b, Game2a, Game2b, Game2c, Game3) and their completeness and soundness lemmas are the
natural next layer of milestones, as are the covering properties of Appendix C and the
list-decoding bounds of Appendix E.
## Selected references
- Yumou Fei, Dor Minzer, Shuo Wang, *On the Hardness of 4-to-1 Games with Perfect
Completeness*, ECCC TR26-179 (2026),
[https://eccc.weizmann.ac.il/report/2026/179/](https://eccc.weizmann.ac.il/report/2026/179/)
- Subhash Khot, *On the power of unique 2-prover 1-round games*, STOC 2002,
[https://doi.org/10.1145/509907.509985](https://doi.org/10.1145/509907.509985)
- Irit Dinur, Subhash Khot, Guy Kindler, Dor Minzer, Muli Safra, *Towards a proof of the
2-to-1 games conjecture?*, STOC 2018,
[https://doi.org/10.1145/3188745.3188804](https://doi.org/10.1145/3188745.3188804)
- Subhash Khot, Dor Minzer, Muli Safra, *Pseudorandom sets in Grassmann graph have
near-perfect expansion*, FOCS 2018,
[https://doi.org/10.1109/FOCS.2018.00062](https://doi.org/10.1109/FOCS.2018.00062)
- Louis Golowich, *New Explicit Constant-Degree Lossless Expanders*, FOCS 2023,
[https://arxiv.org/abs/2306.07551](https://arxiv.org/abs/2306.07551)
Grothendieck-Teichmüller: the graded Lie algebra grt_1 and the Deligne-Drinfeld-Ihara conjectureOpen Problem
## 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](https://doi.org/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](https://doi.org/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](https://doi.org/10.1007/s00222-014-0528-x).
Faithfulness of the Burau representation of B4Research Paper
## Motivation
In 1935 Werner Burau attached to every braid on $n$ strands a matrix over the ring of Laurent polynomials $\mathbb{Z}[t,t^{-1}]$. The resulting homomorphism $\rho_n : B_n \to \mathrm{GL}_n(\mathbb{Z}[t,t^{-1}])$ is the oldest and most studied linear representation of the braid group, and whether it is *faithful* — whether a nontrivial braid can act as the identity matrix — became one of the best known questions about braid groups.
The history is short and sharp:
* **1969** — Magnus and Peluso prove that $\rho_3$ is faithful, by a direct algebraic computation.
* **1991** — Moody proves $\rho_n$ is **not** faithful for $n \ge 9$.
* **1993** — Long and Paton improve this to $n \ge 6$.
* **1999** — Bigelow settles $n = 5$: $\rho_5$ is not faithful.
* This left exactly one open case, $n = 4$, which appears as Question 3.1 in Margalit's problem list for mapping class groups.
* **2026** — Bharathram, Birman and Brendle prove that $\rho_4$ **is** faithful ([arXiv:2607.05283](https://arxiv.org/abs/2607.05283)), closing the last case.
## Setting
Let $n \ge 1$. The braid group $B_n$ is taken here in Artin's presentation: generators $\sigma_1,\dots,\sigma_{n-1}$ subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad \sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1}.$$
Let $R = \mathbb{Z}[t,t^{-1}]$. The **unreduced Burau representation** is the homomorphism
$$\rho_n : B_n \longrightarrow \mathrm{GL}_n(R), \qquad \sigma_i \longmapsto I_{i-1} \oplus \begin{pmatrix} 1-t & t \\ 1 & 0\end{pmatrix} \oplus I_{n-i-1},$$
i.e. the identity matrix altered only in the two rows and columns $i$, $i+1$. That these matrices satisfy the two families of braid relations — so that $\rho_n$ is well defined — is proved in the mission's definition file, together with the invertibility of each generator matrix (its inverse is the identity altered by the block $\begin{pmatrix} 0 & 1 \\ t^{-1} & 1-t^{-1}\end{pmatrix}$).
Equivalently, $\rho_n$ is the action of the mapping class group of the $n$-punctured disk $D_n$ on the relative homology $H_1(\widetilde{D_n}, \{\tilde p_*\})$ of the infinite cyclic cover determined by total winding number; this is the description used throughout the source paper.
A representation is **faithful** when it is injective.
## Target
The goal of the mission is the Main Theorem of the paper:
$$\rho_4 : B_4 \longrightarrow \mathrm{GL}_4(\mathbb{Z}[t,t^{-1}]) \ \text{ is injective.}$$
The milestones are three supporting results, each of which can be attacked independently:
1. **Theorem 4.1 (Magnus–Peluso).** $\rho_3$ is injective. The paper gives a new topological proof of this classical statement, and the same argument is the model for the four-strand case.
2. **Observation 2.1.** If a braid $\Phi \in B_n$ satisfies $\rho_n(\Phi) = I$, then its image under the standard inclusion $B_n \hookrightarrow B_{n+1}$ (add one unbraided strand) satisfies $\rho_{n+1}(\iota(\Phi)) = I$. The paper uses this to move a four-strand braid into $B_5$, where a parity obstruction can be applied.
3. **Long's criterion** ([Long 1986, Theorem 2.2], quoted in Section 1 of the paper). If $N \trianglelefteq B_n$ is nontrivial and not contained in the centre, and $\rho_n$ is injective on $N$, then $\rho_n$ is injective. This is what reduces the Main Theorem to faithfulness on the Brunnian subgroup $\mathrm{Brun}_4$.
## Significance
Faithfulness of $\rho_4$ closes the classification of the faithful Burau representations: $\rho_n$ is faithful exactly for $n \le 4$. It immediately gives faithfulness of the Jones representation of $B_4$ (Corollary 1.1 of the paper), since the Jones representation contains the reduced Burau representation as a summand. Beyond the statement itself, the kernel and the image of $\rho_n$ for $n \ge 5$ remain poorly understood, and the paper's disk-sequence and parity technology is proposed by its authors as a tool for that problem.
For formalization, essentially nothing of this is machine-checked today: Mathlib has neither braid groups nor the Burau representation. This mission puts in place a checked definition of $\rho_n$ over $\mathbb{Z}[t,t^{-1}]$ (including well-definedness and invertibility), and then asks for the mathematics. Even the three-strand case — Magnus–Peluso, known since 1969 — is not formalized anywhere, and it is the natural first target.
## Difficulty
The obvious approach fails in both directions. One cannot simply compute: a braid in the kernel would have to be found or excluded among infinitely many words, and no normal form for $B_4$ turns injectivity of $\rho_4$ into a finite check. Nor can one argue by a free-subgroup / ping-pong pattern, which is how *non*-faithfulness is proved for $n \ge 5$.
The source argument is topological. To a braid $\Phi$ one associates the arc $\beta = (\beta_*^3)\Phi$ and the sequence of punctured disks cut out by its intersections with a fixed arc $\alpha$; the Moody polynomial $M(\alpha,\beta) \in \mathbb{Z}[t,t^{-1}]$ then obstructs membership in the kernel provided no cancellation occurs among its monomials. Three-strand braids always satisfy the relevant parity condition; four-strand braids do not, and the paper repairs this by pushing a point-pushing braid $\Phi \in K_4$ into $B_5$ and applying Moody's theorem there. A complete formalization therefore needs curves on punctured disks, minimal position, and the Birman exact sequence — none of which exist in Mathlib. Contributions that build any of that infrastructure are as welcome as contributions to the statements themselves.
## Formalization scope
Conventions fixed by the Lean development:
1. $B_n$ is the abstract group given by Artin's presentation, with generators indexed by $\mathrm{Fin}(n-1)$ using truncated subtraction; the generator of index $i$ is $\sigma_{i+1}$. This is the already-published definition reused by the mission, so results proved here interoperate with other braid-group missions.
2. The representation is the **unreduced** Burau representation, of size $n \times n$, not the reduced $(n-1)$-dimensional one; the variable is written $t$ and the coefficient ring is $\mathbb{Z}[t,t^{-1}]$.
3. Faithfulness is stated as injectivity of the group homomorphism, not as triviality of the kernel on some subgroup, and it is the genuine homomorphism out of the presented group: the braid relations are verified for the Burau matrices in the definition file, so no statement here is vacuous or conditional on well-definedness.
4. Long's criterion is stated for all $n$; for $n \le 2$ its noncentrality hypothesis cannot be satisfied, so its content is the case $n \ge 3$ that the paper uses.
A complete development will additionally need: point-pushing subgroups and the Brunnian group $\mathrm{Brun}_4$, the Moody polynomial of a pair of arcs, and winding-number sequences. These are not yet formalized and are deliberately not part of the current statements; proposals for faithful formalizations of them are welcome in the mission discussion.
## Selected references
* V. Bharathram, J. S. Birman, T. E. Brendle, *The Burau representation is faithful for n = 4*, 2026, [arXiv:2607.05283](https://arxiv.org/abs/2607.05283).
* W. Magnus, A. Peluso, *On a theorem of V. I. Arnold*, Comm. Pure Appl. Math. 22 (1969), 683–692, [DOI:10.1002/cpa.3160220508](https://doi.org/10.1002/cpa.3160220508).
* D. D. Long, *A note on the normal subgroups of mapping class groups*, Math. Proc. Cambridge Philos. Soc. 99 (1986), 79–87, [DOI:10.1017/S0305004100063969](https://doi.org/10.1017/S0305004100063969).
* J. A. Moody, *The Burau representation of the braid group $B_n$ is unfaithful for large $n$*, Bull. Amer. Math. Soc. 25 (1991), 379–384, [DOI:10.1090/S0273-0979-1991-16080-5](https://doi.org/10.1090/S0273-0979-1991-16080-5).
* D. D. Long, M. Paton, *The Burau representation is not faithful for $n \ge 6$*, Topology 32 (1993), 439–447, [DOI:10.1016/0040-9383(93)90030-Y](https://doi.org/10.1016/0040-9383(93)90030-Y).
* S. Bigelow, *The Burau representation is not faithful for $n = 5$*, Geom. Topol. 3 (1999), 397–404, [DOI:10.2140/gt.1999.3.397](https://doi.org/10.2140/gt.1999.3.397).
Braids, Links and Mapping Class Groups I: Artin's Presentation of the Braid GroupTextbook
## Motivation
The **braid group** is one of the places where group theory, low-dimensional topology and
knot theory meet. Artin introduced it in 1925 (E. Artin, *Theorie der Zöpfe*, Abh. Math. Sem.
Univ. Hamburg 4 (1925), 47–72) and returned to it in 1947; since then it has become standard
equipment in the study of links (closed braids and Markov's theorem), of mapping class groups
of punctured surfaces, and of configuration spaces. Birman's *Braids, Links, and Mapping Class
Groups* (Annals of Mathematics Studies 82, Princeton University Press, 1974) is the classical
reference that develops all three subjects from the braid group outwards, and its Chapter 1
is the foundation on which the rest of the book rests.
The chapter's structure is itself the reason to formalize it first: everything later in the
book — the closed-braid picture of links, Markov's theorem, the Magnus representations, the
mapping class group of the punctured sphere — is phrased in terms of the group
$\pi_1 B_{0,n}E^2$ and of the presentation established here. A mission that fixes faithful Lean
definitions of the configuration spaces and of the abstract braid group therefore fixes the
vocabulary for the whole series.
Timeline of the results collected here: Artin (1925) gave the presentation and the
characterization of braid automorphisms of a free group; Chow (1948) determined the centre;
Fadell–Neuwirth (1962) introduced the configuration-space fibrations, and Fadell–Van Buskirk
(1962) used them to give the proof of the presentation reproduced by Birman.
## Setting
Write $E^2$ for the Euclidean plane, identified throughout with the complex numbers $\mathbb{C}$.
For $n \ge 0$ let
$$F_{0,n}E^2 = \{\,(z_1,\dots,z_n) \in \mathbb{C}^n : z_i \neq z_j \text{ for } i \neq j\,\}$$
be the **ordered configuration space** of $n$ points in the plane, topologized as a subspace of
$\mathbb{C}^n$. The symmetric group $\Sigma_n$ acts on it by permuting coordinates; the quotient
$$B_{0,n}E^2 = F_{0,n}E^2 / \Sigma_n,$$
with the quotient topology, is the **unordered configuration space**. A point of $B_{0,n}E^2$ is
an unordered set of $n$ distinct points of the plane. The base configuration is
$\bar z^{\,0} = (1,2,\dots,n)$, and all fundamental groups below are taken at $\bar z^{\,0}$ or at
its image.
The **braid group of the plane** is $\pi_1 B_{0,n}E^2$: a loop is a motion of $n$ points of the
plane returning to the same set of points, and homotopy classes of such motions compose as
braids. The **pure braid group** is $P_n = \pi_1 F_{0,n}E^2$, the subgroup of motions returning
each point to its own starting position.
Separately, let $B_n$ denote the abstract group given by generators $\sigma_1,\dots,\sigma_{n-1}$
subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad
\sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1} \quad (1 \le i \le n-2).$$
These are equations (1-1) and (1-2) of the book (p. 11). Geometrically $\sigma_i$ interchanges the
$i$-th and $(i+1)$-st points along a semicircle.
## Formalization targets
### Goal — Theorem 1.8 (Artin, 1925; Birman p. 18)
$$B_n \;\cong\; \pi_1 B_{0,n} E^2 .$$
The group of motions of $n$ points of the plane is the group with generators
$\sigma_1,\dots,\sigma_{n-1}$ and the two families of relations above: the relations are not only
valid but *defining*.
### Milestones
The milestone list follows the chapter: the covering-space description of the projection
$F_{0,n}E^2 \to B_{0,n}E^2$ (Proposition 1.1, p. 11), the Fadell–Neuwirth exact sequence
(Theorem 1.4, p. 14), the semidirect-product decomposition of the pure braid group
(Corollary 1.8.1, p. 24), the faithful representation of $B_n$ by automorphisms of a free group
(Corollary 1.8.3, p. 25), the centre of $B_n$ (Corollary 1.8.4, p. 28, due to Chow), and Artin's
algebraic characterization of the braid automorphisms (Theorem 1.9, p. 30).
## Significance
Theorem 1.8 is what makes the braid group *computable*: with defining relations in hand one can
combine braids into the normal form of Corollary 1.8.2 and solve the word problem, represent
braids by automorphisms of a free group, and pass to the link-theoretic material of Chapters 2
and 5 where braid words, not motions, are the objects manipulated. Corollary 1.8.3 turns braids
into concrete data — a braid is determined by what it does to the generators of a free group —
and Theorem 1.9 says exactly which endomorphisms arise this way; both are the algebraic engine
behind the conjugacy-problem and Magnus-representation chapters.
For formalization the state of play is that Mathlib has free groups, presented groups, the
fundamental groupoid and fundamental group, covering maps and fibre bundles, but no braid
groups and no configuration spaces: nothing here can be assembled from existing declarations.
The mission therefore produces reusable infrastructure — configuration spaces of the plane, the
symmetric-group quotient, the Artin presentation, the Artin action on a free group — as well as
machine-checked proofs of results that are classical but, as far as the mission's search of the
library showed, not yet formalized in Mathlib.
## Difficulty
The generators and relations are easy to write down and easy to verify *in* $\pi_1 B_{0,n}E^2$;
what is hard is completeness, i.e. that no further relations are needed. The naive route —
draw the braid, push it into a normal form by hand — is exactly what a formal proof cannot do.
The Fadell–Van Buskirk argument reproduced by Birman instead runs an induction on $n$ driven by
the fibration $F_{0,n}E^2 \to F_{0,n-1}E^2$: its homotopy exact sequence gives a split extension
of $P_{n-1}$ by a free group, presentations are assembled along the extension, and finally the
covering $F_{0,n}E^2 \to B_{0,n}E^2$ with deck group $\Sigma_n$ transfers the answer from the pure
braid group to the full braid group. Each of those steps needs genuine algebraic topology —
local triviality of the projection, exactness of the homotopy sequence, freeness of
$\pi_1$ of a punctured plane — which is where the formalization work actually lies.
## Formalization scope
The plane is $\mathbb{C}$. $F_{0,n}E^2$ is the subtype of injective functions
$\mathrm{Fin}\,n \to \mathbb{C}$; $B_{0,n}E^2$ is its quotient by the equivalence "differ by
precomposition with a permutation", with the quotient topology. Base point: the configuration
$i \mapsto i+1$, i.e. $(1,2,\dots,n)$, and its image. Fundamental groups are Mathlib's
`FundamentalGroup` at those base points. Braid generators are indexed by $\mathrm{Fin}(n-1)$
with $0$-based indices ($i$ stands for $\sigma_{i+1}$), and free-group generators by
$\mathrm{Fin}\,n$; the abstract braid group is a `PresentedGroup` on that index set. Truncated
subtraction makes the generator set empty for $n \le 1$, so $B_0$ and $B_1$ are trivial, as
intended. Two milestones are stated with the shift $n \mapsto n+1$ (i.e. for the projection
$F_{0,n+1}E^2 \to F_{0,n}E^2$) to avoid truncated subtraction in the maps.
Two conventions are worth flagging because they weaken what the Lean text asserts relative to
the prose. First, the goal asserts the existence of *some* isomorphism $B_n \cong \pi_1B_{0,n}E^2$;
it does not pin the isomorphism down on the geometric generators of Figure 2, since those loops
are not part of the formal development. Second, Artin's representation is formalized as the
existence of a homomorphism $\xi$ from $B_n$ to the automorphism group of the free group whose
value on each $\sigma_i$ is the explicit endomorphism of equation (1-14), together with its
injectivity; Theorem 1.9 is then stated for an arbitrary such $\xi$, given as a hypothesis, and
is non-vacuous precisely because Corollary 1.8.3 supplies one.
No trivializing formalization is available: the goal is an isomorphism statement between two
groups that are both defined independently of it, and the degenerate cases $n \le 1$ (both sides
trivial) are genuine special cases of it, not the content.
Infrastructure a complete development needs, all reusable: freeness of $\pi_1$ of a punctured
plane, local triviality of the Fadell–Neuwirth projection, the homotopy exact sequence of a
fibration in the range needed, presentations of split extensions, and the transfer of a
presentation along a regular covering. Contributions of any of these as standalone lemmas are
welcome, as is a formalization of the geometric generators (1-9) that would let the goal be
strengthened to pin the isomorphism on $\sigma_i$.
## Selected references
- E. Artin, *Theorie der Zöpfe*, Abhandlungen aus dem Mathematischen Seminar der Universität
Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
- E. Artin, *Theory of braids*, Annals of Mathematics 48 (1947), 101–126.
https://doi.org/10.2307/1969218
- W.-L. Chow, *On the algebraical braid group*, Annals of Mathematics 49 (1948), 654–658.
https://doi.org/10.2307/1969333
- E. Fadell, L. Neuwirth, *Configuration spaces*, Mathematica Scandinavica 10 (1962), 111–118.
https://doi.org/10.7146/math.scand.a-10517
- E. Fadell, J. Van Buskirk, *The braid groups of $E^2$ and $S^2$*, Duke Mathematical Journal 29
(1962), 243–257. https://doi.org/10.1215/S0012-7094-62-02925-3
- J. S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82,
Princeton University Press, 1974. https://doi.org/10.1515/9781400881420
Gribov Ambiguity: no continuous gauge fixing (Singer 1978)Research Paper
## Motivation
In the Feynman path-integral approach to a non-abelian gauge theory one wants to integrate a
gauge-invariant weight over the space $\mathfrak{A}$ of vector potentials (connections) of a
principal bundle. The integrand is constant on the orbits of the group $\mathcal{G}$ of gauge
transformations, so the integral over $\mathfrak{A}$ diverges and one is supposed to integrate
instead over the orbit space $\mathfrak{R} = \mathfrak{A}/\mathcal{G}$. The Faddeev–Popov
procedure realizes this by *fixing a gauge*: choosing, continuously in the orbit, exactly one
vector potential on each orbit, and correcting by a Jacobian determinant.
V. N. Gribov (SLAC Translation 176, 1977) observed that for $SU(2)$ potentials on
$\mathbb{R}^3$ (or $\mathbb{R}^4$) with suitable conditions at infinity, the Coulomb gauge
condition does not do this: the Coulomb slice through the zero potential meets the orbit of the
zero potential again, far from the origin. These extra intersections are the **Gribov copies**;
R. Jackiw, I. Muzinich and C. Rebbi (Phys. Rev. D 17 (1978) 1576) analyzed them in detail.
I. M. Singer, *Some Remarks on the Gribov Ambiguity* (Commun. Math. Phys. **60** (1978) 7–12),
showed that the phenomenon is not a defect of the Coulomb gauge. If the conditions at infinity
are those of Gribov — gauge transformations extending to the one-point compactification with
value $I$ at infinity, so that the base manifold is $M = S^3$ or $M = S^4$ — then **no**
continuous gauge fixing exists at all, in any gauge. The obstruction is topological: the space
of irreducible connections is weakly contractible, while the gauge group is not, and a
weakly contractible principal bundle admits no global continuous section.
## Setting
Fix $N \ge 2$ and take the structure group $SU(N)$, the group of $N \times N$ complex matrices
$U$ with $U^\ast U = I$ and $\det U = 1$, topologized as a subspace of matrices. Let
$S^r$ denote the unit sphere of $\mathbb{R}^{r+1}$, with base point $m$ the north pole.
For the trivial $SU(N)$-bundle over a space $M$, a gauge transformation is a map
$\varphi : M \to SU(N)$, and the **gauge group** is
$$\mathcal{G}(M,N) \;=\; C\bigl(M, SU(N)\bigr),$$
continuous maps with pointwise multiplication and the compact-open topology. Two subobjects
matter. The **based gauge group** $\mathcal{G}_m = \{\varphi : \varphi(m) = I\}$ is the subgroup
of transformations that are the identity at the base point. The constant transformations with
value in the centre $Z_N = \{e^{2\pi i k/N} I\}$ of $SU(N)$ form a normal subgroup, and the
**reduced gauge group** is the quotient
$$\overline{\mathcal{G}}(M,N) \;=\; \mathcal{G}(M,N)/Z_N$$
with the quotient topology. The centre acts trivially on vector potentials, so
$\overline{\mathcal{G}}$ is the group that acts effectively.
A group $G$ acting continuously on a space $\mathfrak{A}$ has orbit space
$\mathfrak{A}/G$ with the quotient topology, and a **gauge fixing** is a continuous map
$s : \mathfrak{A}/G \to \mathfrak{A}$ with $p \circ s = \mathrm{id}$, where
$p : \mathfrak{A} \to \mathfrak{A}/G$ is the projection: a continuous choice of exactly one point
on each orbit. The action is **principal** when it is free and the division map, which sends a
pair of points on one orbit to a group element carrying the second to the first, can be chosen
continuously; this is the topological content of "$p$ is a principal $G$-bundle". The space
$\mathfrak{A}$ is **weakly contractible** when it is nonempty and all its homotopy groups vanish.
In the paper, $\mathfrak{A}$ is the affine space of connections, $\mathfrak{R}$ its set of
irreducible members, and Theorems 1 and 2 say exactly that $\mathfrak{R}$ is a weakly
contractible principal $\overline{\mathcal{G}}$-space.
## Formalization targets
### Goal — Corollary 4 (no gauge fixing)
For $r \in \{3,4\}$, $N \ge 2$, and every weakly contractible principal
$\overline{\mathcal{G}}(S^r,N)$-space $A$:
$$\nexists\, s : A/\overline{\mathcal{G}}(S^r,N) \longrightarrow A \quad\text{continuous with}\quad p \circ s = \mathrm{id}.$$
By Theorems 1 and 2 of the paper the space of irreducible connections over $S^3$ or $S^4$ is such
an $A$, so the goal contains Singer's Corollary 4 for that space; it leaves the analytic
construction of the space of connections unfixed, which is what makes it statable today.
### Milestone level — Theorem 3
$$\exists\, j \ge 1: \quad \pi_j\bigl(\overline{\mathcal{G}}(S^r,N)\bigr) \neq 0, \qquad r \in \{3,4\},\ N \ge 2 .$$
### Milestone level — Theorem 5 and its homotopy inputs
$$\pi_j\bigl(\mathcal{G}_m(S^r,N)\bigr) \;\cong\; \pi_{j+r}\bigl(SU(N)\bigr), \qquad
\pi_3(SU(N)) \cong \mathbb{Z}, \qquad \pi_4(SU(N)) = 0 \ (N\ge 3), \qquad \pi_4(SU(2)) \cong \mathbb{Z}/2 .$$
## Significance
The result rules out the existence of a global gauge in the topological sense: every gauge
condition used in practice is at best a local slice, and the Faddeev–Popov construction has to be
read as a local statement, patched with a partition of unity over the orbit space (as the last
section of the paper proposes). It is the mathematical reason why the Gribov ambiguity cannot be
repaired by a cleverer gauge condition, and it is the origin of the Gribov–Zwanziger restriction
of the functional integral to a fundamental domain.
Formalizing it adds a machine-checked version of an argument that is quoted far more often than
it is checked, and it forces into Lean a piece of infrastructure that Mathlib currently lacks:
homotopy groups of mapping spaces, the long exact sequence of a fibration in the form needed for
$0 \to \mathcal{G}_m \to \mathcal{G} \to SU(N) \to 0$, and the classical computations
$\pi_3(SU(N)) \cong \mathbb{Z}$, $\pi_4(SU(N)) = 0$ for $N \ge 3$, $\pi_4(SU(2)) \cong \mathbb{Z}/2$.
Singer's results are proved mathematics; none of them is formalized, and Mathlib as of the pinned
revision contains homotopy groups as a definition together with their group structure, but
essentially no computation of them.
## Difficulty
The naive approach to the goal — build a section by hand, or average over the group — fails
because $\overline{\mathcal{G}}$ is neither compact nor contractible and the obstruction is
global: locally, slices do exist (that is the content of the generalized Coulomb gauge), so no
local argument can produce a contradiction. The proof has to convert a section into a
homotopy-theoretic statement: a section of a principal bundle trivializes it, exhibiting the
group as a retract of the total space, so all homotopy groups of the group would vanish; the work
is then to show that some homotopy group of the reduced gauge group does not vanish, which needs
the identification of the based gauge group with a mapping space, the exact sequences relating
$\mathcal{G}_m$, $\mathcal{G}$ and $\overline{\mathcal{G}}$, and non-trivial homotopy groups of
$SU(N)$ — including $\pi_6(S^3) \cong \mathbb{Z}/12$ for the $SU(2)$ case of Theorem 3.
## Formalization scope
The formalization commits to the following conventions, all of them visible in the definitions of
this mission.
- The bundle is the **trivial** $SU(N)$-bundle, so gauge transformations are literally maps
$M \to SU(N)$. This is the case of Gribov's original setting over $S^3$; over $S^4$ the paper
also treats bundles of nonzero Pontrjagin index, which are out of scope here.
- Gauge transformations are **continuous**, not smooth, with the compact-open topology; Singer's
Theorem 5 uses smoothing homotopies to pass between the two, and the homotopy-theoretic content
is the same.
- $SU(N)$ is the special unitary group of complex $N \times N$ matrices, with its subspace
topology; $S^r$ is the unit sphere of $\mathbb{R}^{r+1}$ with its subspace topology.
- Homotopy groups are Mathlib's `HomotopyGroup`, based at the identity element.
- The **space of connections is not constructed**: Mathlib has no space of connections on a
principal bundle, and building one is a mission of its own. The goal therefore quantifies over
an arbitrary topological space carrying a weakly contractible principal action of the reduced
gauge group — exactly the properties Theorems 1 and 2 establish for the irreducible
connections.
- This quantification is not vacuous: such spaces exist (the total space of a universal
$\overline{\mathcal{G}}$-bundle is one), so the goal is a genuine non-existence statement and
not a statement about an empty class. Conversely it is not trivially true: the hypotheses do
not mention any homotopy invariant of the gauge group, and refuting a section requires
Theorem 3.
- The paper's analytic statements — Theorem 1 (openness and density of the irreducible
connections, principal bundle structure), Theorem 2 (weak contractibility), Theorem 6
($\pi_1$ of the irreducible orbit space), Theorem 7 (no flat connection), Theorem 8 (tangency
of orbits to the Coulomb slice) and Theorem 9 (the canonical connection and its curvature) —
are out of scope until a space of connections exists in Lean. Contributions that build one, in
reusable form, are welcome and would let this mission be extended to them.
## Selected references
- V. N. Gribov, *Instability of non-abelian gauge theories and impossibility of choice of Coulomb
gauge*, SLAC Translation 176 (1977); Nucl. Phys. B **139** (1978) 1–19,
[doi:10.1016/0550-3213(78)90175-X](https://doi.org/10.1016/0550-3213(78)90175-X).
- I. M. Singer, *Some Remarks on the Gribov Ambiguity*, Commun. Math. Phys. **60** (1978) 7–12,
[doi:10.1007/BF01609471](https://doi.org/10.1007/BF01609471).
- R. Jackiw, I. Muzinich, C. Rebbi, *Coulomb gauge description of large Yang-Mills fields*,
Phys. Rev. D **17** (1978) 1576, [doi:10.1103/PhysRevD.17.1576](https://doi.org/10.1103/PhysRevD.17.1576).
- H. Toda, *Composition methods in homotopy groups of spheres*, Annals of Mathematics Studies 49,
Princeton University Press (1962).
The de Bruijn–Newman Constant is Non-negativeResearch Paper
## Motivation
The **Riemann hypothesis** asserts that all nontrivial zeros of the Riemann zeta function lie on the critical line. A classical way to measure how far the hypothesis is from failing runs through a one-parameter deformation of the Riemann $\xi$ function by the **backward heat flow**. De Bruijn (1950) introduced a family of entire functions $H_t$, $t \in \mathbb{R}$, with $H_0$ essentially the $\xi$ function, and showed that $H_t$ has only real zeros for $t \ge 1/2$. Newman (1976) proved that there is a finite constant $\Lambda$, now called the **de Bruijn–Newman constant**, such that $H_t$ has only real zeros precisely when $t \ge \Lambda$. The Riemann hypothesis is exactly the statement $\Lambda \le 0$, and Newman conjectured the complementary bound $\Lambda \ge 0$ — in his phrase, that if the Riemann hypothesis is true, then it is only barely so.
Timeline of lower bounds on $\Lambda$, all obtained before 2018 by exhibiting **Lehmer pairs**, that is, pairs of adjacent zeros of $\zeta$ that are unusually close together: $\Lambda > -\infty$ (Newman 1976), $\Lambda \ge -50$ (Csordas–Norfolk–Varga 1988), $\Lambda \ge -5$ (te Riele 1991), $\Lambda \ge -0.385$ (Norfolk–Ruttan–Varga 1992), $\Lambda \ge -0.0991$ (Csordas–Ruttan–Varga 1991), $\Lambda \ge -4.379 \times 10^{-6}$ (Csordas–Smith–Varga 1994), $\Lambda \ge -5.895 \times 10^{-9}$ (Csordas–Odlyzko–Smith–Varga 1993), $\Lambda \ge -2.63 \times 10^{-9}$ (Odlyzko 2000), $\Lambda \ge -1.15 \times 10^{-11}$ (Saouter–Gourdon–Demichel 2011). Rodgers and Tao closed the gap in 2020 by proving $\Lambda \ge 0$. In the other direction, de Bruijn's bound $\Lambda \le 1/2$ was sharpened to $\Lambda < 1/2$ by Ki–Kim–Lee (2009) and to $\Lambda \le 0.22$ by the Polymath 15 project (2019).
## Setting
For a real number $u$ put
$$\Phi(u) := \sum_{n=1}^{\infty}\bigl(2\pi^2 n^4 e^{9u} - 3\pi n^2 e^{5u}\bigr)\exp\bigl(-\pi n^2 e^{4u}\bigr),$$
a function that decays super-exponentially as $|u| \to \infty$ and satisfies $\Phi(u) = \Phi(-u)$. For each $t \in \mathbb{R}$ define the entire function
$$H_t(z) := \int_0^{\infty} e^{t u^2}\,\Phi(u)\,\cos(z u)\,du .$$
Each $H_t$ is even and satisfies $H_t(\bar z) = \overline{H_t(z)}$; the function $H_0$ is $\tfrac18 \xi\bigl(\tfrac12 + \tfrac{iz}{2}\bigr)$, so the Riemann hypothesis says exactly that every zero of $H_0$ is real. Write
$$S := \{\, t \in \mathbb{R} : \text{every zero of } H_t \text{ is real} \,\},\qquad \Lambda := \inf S .$$
By Pólya and Newman, $S$ is the ray $[\Lambda, \infty)$ with $-\infty < \Lambda \le 1/2$.
When $\Lambda < t \le 0$ the zeros of $H_t$ are real, simple, symmetric about the origin and avoid the origin, so they can be listed as $(x_j(t))_{j \in \mathbb{Z}^*}$, indexed by the nonzero integers, with $0 < x_1(t) < x_2(t) < \cdots$ and $x_{-j}(t) = -x_j(t)$. The **classical locations** $\xi_j$ are defined for $j \ge 1$ by $\Psi(\xi_j) = j$ with
$$\Psi(T) := \frac{T}{4\pi}\log\frac{T}{4\pi} - \frac{T}{4\pi},$$
extended by $\xi_{-j} = -\xi_j$; they are the positions the zeros would occupy if the Riemann–von Mangoldt counting formula were exact. Throughout, $\log_+ x := \log(2 + |x|)$.
## Formalization targets
### Goal — Newman's conjecture
$$\Lambda \ge 0, \qquad\text{equivalently}\qquad \text{every } t \text{ with } H_t \text{ having only real zeros satisfies } t \ge 0 .$$
The goal is stated in both forms simultaneously, so that it does not depend on any convention for the infimum of a set that might be empty or unbounded below.
### Milestones
The milestone list follows the architecture of Rodgers–Tao, which is a proof by contradiction: every milestone is stated under the standing hypothesis $\Lambda < 0$ of that paper, in the time ranges the paper uses ($\Lambda < t \le 0$, then $\Lambda/2 \le t \le 0$, then $\Lambda/4 \le t \le 0$). In order: an upper bound for $H_t$ near the real axis (Lemma 4); Riemann–von Mangoldt type counting formulae for the zeros of $H_t$ (Theorem 9); the resulting macroscopic description of the zeros (Corollary 10); the equations of motion $\partial_t x_k = 2\sum_{j \ne k} (x_k - x_j)^{-1}$ (Theorem 11); a quantitative lower bound on gaps between zeros (Proposition 13); a bound on the time-integrated renormalized energy (Theorem 17); and a bound on that energy at time $t = 0$ (Proposition 26). The last of these says that at time zero the zeros are, on average, locally in the equilibrium configuration of an arithmetic progression, which contradicts known results on the local distribution of zeros of $\zeta$.
## Significance
$\Lambda \ge 0$ settles Newman's conjecture, and together with the Riemann hypothesis it would force $\Lambda = 0$. Unconditionally, it says that the zeros of $\xi$ are not in local equilibrium: infinitely often, gaps between consecutive zeros deviate from the mean spacing, which is what makes the pair correlation phenomenology of Montgomery and of Conrey–Ghosh–Goldston–Gonek–Heath-Brown incompatible with $\Lambda < 0$. Any proof of the Riemann hypothesis must therefore be compatible with the hypothesis being tight in this sense.
The theorem has a complete published proof (Rodgers–Tao, *Forum of Mathematics, Pi*, 2020); it is not an open problem. What is missing is a machine-checked proof. To the extent the material has been formalized at all, the underlying objects — the $\xi$ function, the heat flow $H_t$, the counting function for zeros, the zero dynamics, the renormalized energies — are not available in Mathlib, so the mission produces reusable analytic infrastructure: bounds for a Fourier–Laplace type integral by the saddle point method, a Riemann–von Mangoldt counting argument via the argument principle, and a gradient-flow monotonicity framework for an infinite particle system with logarithmic interaction.
## Difficulty
The obvious route to $\Lambda \ge 0$ is the one used for every previous lower bound: exhibit Lehmer pairs of ever higher quality, since if $\Lambda$ were very negative the zeros of $H_0$ would repel each other and unusually close pairs of zeta zeros could not exist. Producing an infinite sequence of Lehmer pairs of arbitrarily high quality is possible under the GUE hypothesis, but the known unconditional upper bounds for small gaps between zeta zeros are too weak, even assuming the Riemann hypothesis. The proof instead upgrades repulsion to relaxation to local equilibrium: it must control the zeros of $H_t$ uniformly for $\Lambda < t \le 0$ at length scales as fine as $\log T$, with only the weaker counting formulae available for negative $t$ (an error term $O(\log_+^2 T)$ rather than $O(\log_+ T)$), and must make sense of a Hamiltonian and an energy that are given by divergent series, which requires truncation, renormalization, and careful control of all the resulting boundary terms.
## Formalization scope
The Lean development commits to the following conventions. $\Phi$ is a `tsum` over the positive integers and $H_t(z)$ is the Bochner integral over $(0, \infty)$ of $e^{tu^2}\Phi(u)\cos(zu)$; no convergence or entireness statement is built into the definition. $\Lambda$ is `sInf` of the set of admissible times, and the goal theorem also states the quantifier form "every admissible $t$ is nonnegative", so it cannot be satisfied by a junk value of the infimum. The zero families $(x_j(t))$ and the classical locations $(\xi_j)$ are not defined by choice functions: they enter the milestones as universally quantified functions $\mathbb{Z} \to \mathbb{R}$ subject to explicit predicates saying exactly which sequences they are, so a milestone asserts something about every valid enumeration. Asymptotic notation is unfolded: $O(\cdot)$ becomes an explicit existential constant, $o_{T \to \infty}(\cdot)$ an explicit $\varepsilon$–$T_0$ statement, and a principal value sum a limit of symmetric partial sums. Where a statement asserts the value of a time integral, absolute integrability is part of the conclusion, so the statement cannot be satisfied by the convention that a non-integrable function has integral zero.
One degeneracy is inherent to the source and is stated here explicitly: since the paper argues by contradiction, each milestone carries the hypothesis $\Lambda < 0$ (directly, or through a time range such as $\Lambda < t \le 0$). Once the goal theorem is proved, those hypotheses are unsatisfiable and the milestones become vacuously true. They are the intended attack path on the goal, not independent targets, and a solver who derives one of them from the goal theorem contributes nothing.
Contributions welcome: the analytic estimates for $H_t$ (Lemma 4) and the counting formulae (Theorem 9) are independent of the dynamical part and are the natural entry points; Mathlib-level infrastructure on the argument principle, the saddle point method, and Stirling asymptotics for $\Gamma$ in vertical strips is reusable well beyond this mission.
## Selected references
- B. Rodgers and T. Tao, *The de Bruijn–Newman constant is non-negative*, Forum of Mathematics, Pi 8 (2020), e6. https://doi.org/10.1017/fmp.2020.6
- N. G. de Bruijn, *The roots of trigonometric integrals*, Duke Math. J. 17 (1950), 197–226. https://doi.org/10.1215/S0012-7094-50-01720-0
- C. M. Newman, *Fourier transforms with only real zeros*, Proc. Amer. Math. Soc. 61 (1976), 246–251. https://doi.org/10.1090/S0002-9939-1976-0434982-5
- G. Csordas, W. Smith and R. S. Varga, *Lehmer pairs of zeros, the de Bruijn–Newman constant $\Lambda$, and the Riemann hypothesis*, Constr. Approx. 10 (1994), 107–129. https://doi.org/10.1007/BF01205170
- H. L. Montgomery, *The pair correlation of zeros of the zeta function*, Proc. Sympos. Pure Math. XXIV (1973), 181–193. https://doi.org/10.1090/pspum/024
- J. B. Conrey, A. Ghosh, D. Goldston, S. M. Gonek and D. R. Heath-Brown, *On the distribution of gaps between zeros of the zeta-function*, Q. J. Math. 36 (1985), 43–51. https://doi.org/10.1093/qmath/36.1.43
- D. H. J. Polymath, *Effective approximation of heat flow evolution of the Riemann $\xi$ function, and a new upper bound for the de Bruijn–Newman constant*, Res. Math. Sci. 6 (2019), 31. https://doi.org/10.1007/s40687-019-0193-1
Algebraicity of Weil classes on abelian sixfolds of discriminant -1Research Paper
## Motivation
The Hodge conjecture predicts that on a non-singular complex projective variety $X$ every rational cohomology class of type $(p,p)$ is a rational linear combination of the classes of algebraic subvarieties of $X$. Abelian varieties are the oldest testing ground for the conjecture, and the hardest known classes on them were isolated by A. Weil. A $2n$-dimensional complex abelian variety $A$ is **of Weil type** for an imaginary quadratic field $K=\mathbb{Q}(\sqrt{-d})$ if $K$ embeds into $\mathrm{End}_{\mathbb{Q}}(A)$ in such a way that both eigenspaces of $\eta(\sqrt{-d})$ meet $H^{1,0}(A)$ in an $n$-dimensional subspace. Such an $A$ carries a distinguished two-dimensional space of rational $(n,n)$-classes, the **Weil classes**, which for a generic $A$ of Weil type does not lie in the subring generated by divisor classes. Weil classes are therefore the standard obstruction to the Hodge conjecture in low dimension: for abelian fourfolds the conjecture reduces to their algebraicity.
Timeline of the unconditional results on algebraicity of Weil classes:
- A. Weil (1977) constructed the classes and showed that the generic abelian variety of Weil type has a three-dimensional space of rational $(n,n)$-classes, spanned by $h^n$ and the two-dimensional Weil plane.
- C. Schoen (Compositio Math. 65 (1988) and its 1998 Addendum, Compositio Math. 114) proved algebraicity for fourfolds of Weil type with $K=\mathbb{Q}(\sqrt{-3})$ and arbitrary discriminant, for sixfolds with $K=\mathbb{Q}(\sqrt{-3})$ and trivial discriminant, and for fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$; a second proof of the last case is in B. van Geemen's survey (1994).
- K. Koike (Canad. Math. Bull. 47 (2004)) proved algebraicity for sixfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$, which yields fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and arbitrary discriminant.
- E. Markman (JEMS 25 (2023)) proved algebraicity for fourfolds, arbitrary $K$, and discriminant $1$.
- E. Markman, [arXiv:2502.03415](https://arxiv.org/abs/2502.03415), proves algebraicity for **sixfolds of discriminant $-1$ and every imaginary quadratic $K$**, and deduces the Hodge conjecture for all abelian fourfolds.
## Setting
Fix $g$ and present a $g$-dimensional complex torus by its first homology: a complex structure $J$ on $H_1(A,\mathbb{R})=\mathbb{R}^{2g}$ with $J^2=-1$, the lattice being $\mathbb{Z}^{2g}\subset\mathbb{R}^{2g}$. A **polarization** is a rational alternating form $E$ on $H_1(A,\mathbb{Q})=\mathbb{Q}^{2g}$ satisfying the Riemann relations $E(Jx,Jy)=E(x,y)$ and $E(x,Jx)>0$ for $x\neq 0$. Cohomology is $H^k(A,\mathbb{C})=\wedge^k H^1(A,\mathbb{C})$, realized as the alternating $\mathbb{C}$-multilinear forms on $H_1(A,\mathbb{C})=\mathbb{C}^{2g}$; a class is **rational** if its values on rational vectors are rational, and it has **type** $(p,q)$ if it is multiplied by $z^p\bar z^{q}$ under the scaling action $v\mapsto (\mathrm{Re}\,z)v+(\mathrm{Im}\,z)Jv$ of $z\in\mathbb{C}$. A **Hodge class** of degree $2p$ is a rational class of type $(p,p)$.
Let $g=2n$ and $K=\mathbb{Q}(\sqrt{-d})$ with $d>0$. A **polarized abelian $2n$-fold of Weil type** is such an $(A,E)$ together with a rational endomorphism $M=\eta(\sqrt{-d})$ of $H_1(A,\mathbb{Q})$ with
$$M^2=-d,\qquad MJ=JM,\qquad E(Mx,My)=d\,E(x,y),$$
the last condition saying that $\eta(k)$ multiplies the polarization class by the norm $\mathrm{Nm}(k)$, and such that each of the two eigenspaces $W,\overline{W}\subset H_1(A,\mathbb{C})$ of $M$ meets the $i$-eigenspace of $J$ in an $n$-dimensional subspace. The **Hodge–Weil classes** are the rational classes in
$$\widehat{HW}\;=\;\big(\wedge^{2n}W\;\oplus\;\wedge^{2n}\overline{W}\big)\cap H^{2n}(A,\mathbb{Q}),$$
equivalently the rational degree-$2n$ classes that vanish on every tuple of vectors containing both a vector of $W$ and a vector of $\overline{W}$.
The form $H(x,y)=E(Mx,y)+\sqrt{-d}\,E(x,y)$ is $K$-valued and hermitian on $H_1(A,\mathbb{Q})$, viewed as a $K$-vector space through $\eta$. The determinant of its Gram matrix in a $K$-basis lies in $\mathbb{Q}^{\times}$, and its class in $\mathbb{Q}^{\times}/\mathrm{Nm}(K^{\times})$ is the **discriminant** $\det H$ of $(A,\eta,h)$. Discriminant $-1$ means that this determinant equals $-(a^2+dc^2)$ for some rationals $a,c$ not both zero.
**Algebraicity** is not modelled abstractly. An abelian variety is tied to a genuine non-singular projective variety $X\subseteq\mathbb{P}^N$ by a *projective realization*: a smooth, $\mathbb{Z}^{2g}$-periodic immersion $u:\mathbb{R}^{2g}\to X$, surjective onto $X$ and injective modulo the lattice, whose differential intertwines $J$ with the complex structure of $\mathbb{P}^N$. A class $w\in H^{2p}(A,\mathbb{C})$ is algebraic when some de Rham class of $X$ whose periods over the $2p$-cycles swept out by rational vectors $\lambda_1,\dots,\lambda_{2p}$ equal $w(\lambda_1,\dots,\lambda_{2p})$ is a rational combination of cycle classes $\mathrm{cl}(Z)$ of irreducible subvarieties $Z\subseteq X$ of dimension $g-p$. Cycle classes, de Rham cohomology of a projective variety, $(p,q)$-types and Hodge classes are taken from the platform's `HodgeConjecture` bundle, which formalizes §1 of Deligne's Clay problem description.
## Formalization targets
### Goal — Theorem 1.5.1 of arXiv:2502.03415
$$\text{For every } d>0:\ \text{the Hodge–Weil classes of a polarized abelian sixfold of Weil type with CM by }\mathbb{Q}(\sqrt{-d})\text{ and discriminant }-1\text{ are algebraic.}$$
The statement fixes neither the field $K$ nor the sixfold: it quantifies over every $d>0$, every polarized abelian sixfold of Weil type of discriminant $-1$, and every projective realization of it.
### Milestone — Weil's plane of Hodge–Weil classes (§1.1)
$$\widehat{HW}\ \text{is a two-dimensional }\mathbb{Q}\text{-space, and each of its elements has type }(n,n).$$
### Milestone — Schoen's degeneration step (§1.6)
$$\text{Goal for all sixfolds of discriminant }-1\ \Longrightarrow\ \text{Hodge–Weil classes of every abelian fourfold of Weil type are algebraic,}$$
for every imaginary quadratic $K$ and every discriminant; this is the use made of Schoen's Proposition 10 (Compositio Math. 114 (1998)) in the paper.
### Milestone — Corollary 1.6.1
$$\text{The Hodge conjecture holds for abelian fourfolds.}$$
### Milestone — Lefschetz $(1,1)$
Divisor classes: every Hodge class in $H^2$ of a non-singular projective variety is algebraic. This is an already published platform statement, imported here as a reference, since the reduction in Corollary 1.6.1 uses the algebraicity of divisor classes.
## Significance
Weil classes are, by the results of Moonen–Zarhin (Duke Math. J. 77 (1995), Math. Ann. 315 (1999)), the only obstruction left in dimension four: for a simple abelian fourfold $H^{2,2}(A,\mathbb{Q})$ is spanned by quadratic expressions in divisor classes and by Weil classes, and the non-simple cases reduce to products treated by Ramón Marí (Collect. Math. 59 (2008)) and Moonen–Zarhin. The goal theorem therefore closes the Hodge conjecture for abelian fourfolds, the first dimension in which the conjecture for abelian varieties was open.
Formalizing it produces, first, a reusable Lean model of polarized abelian varieties, of complex multiplication of Weil type, of the Hodge–Weil plane and of the discriminant, tied to an honest notion of algebraic cohomology class through projective realizations. None of these objects exists in Mathlib today. The result itself is proved in the source preprint and has no machine-checked proof; the milestones below are equally unformalized, including the classical statements of Weil and Schoen that the paper's Corollary depends on.
## Difficulty
The naive attack — write down subvarieties whose classes span $\widehat{HW}$ — fails because Weil classes are not expressible through divisors: for a generic abelian variety of Weil type the Néron–Severi group is cyclic while $H^{n,n}(A,\mathbb{Q})$ is three-dimensional, so no product of divisor classes reaches the Weil plane. The source constructs instead a reflexive sheaf $\mathcal{E}$ on $X\times\hat X$, for $X$ the Jacobian of a genus-$3$ curve, whose characteristic class $\kappa(\mathcal{E})$ remains of Hodge type along all deformations of $(X\times\hat X,\eta,h)$ as a polarized abelian sixfold of Weil type, and deforms the pair over that moduli space using a semiregularity theorem for twisted sheaves. Each of these steps — Orlov's derived equivalence, spinor geometry of the Mukai lattice, semiregularity — is itself missing from Mathlib, which is why the milestone list stays on the Hodge-theoretic side of the argument rather than transcribing the sheaf-theoretic core.
## Formalization scope
Conventions the Lean development commits to:
1. Complex tori are presented by $(J,E)$ on $\mathbb{R}^{2g}$ with the lattice $\mathbb{Z}^{2g}$; the polarization form is rational rather than integral, which is the isogeny-invariant form of the Riemann relations.
2. Cohomology is the space of alternating multilinear forms on $H_1(A,\mathbb{C})$, i.e. invariant forms on the torus; a period over a lattice cube is used to compare it with the de Rham cohomology of a projective realization.
3. The Weil condition is imposed symmetrically on both eigenspaces of $\eta(\sqrt{-d})$, so it does not depend on the choice of convention for $H^{1,0}$ versus $H^{0,1}$.
4. Discriminant $-1$ is stated as the existence of a $K$-basis in which the Gram determinant of $H$ is $-\mathrm{Nm}(k)$; changing the basis multiplies the determinant by a norm, so the condition is basis-independent.
5. Algebraicity always refers to cycle classes of subvarieties of an actual projective variety, in the sense of Deligne's formulation, never to an abstract subspace of "algebraic" classes; in particular the goal cannot be satisfied by exhibiting a formal object, and the hypotheses are satisfiable — abelian varieties of Weil type of discriminant $-1$ exist for every $K$, and abelian varieties admit projective realizations.
A complete development needs, beyond what is drafted here: the spin representation of the Mukai lattice of an abelian $n$-fold, pure spinors and $K$-secant lines, Orlov's equivalence, Atiyah classes and semiregularity for twisted sheaves. Contributions establishing any of these, or proving the Hodge-theoretic milestones, are welcome.
## Selected references
- E. Markman, *Cycles on abelian $2n$-folds of Weil type from secant sheaves on abelian $n$-folds*, arXiv:2502.03415. https://arxiv.org/abs/2502.03415
- A. Weil, *Abelian varieties and the Hodge ring*, Collected Papers III, Springer 1980, 421–429.
- C. Schoen, *Hodge classes on self-products of a variety with an automorphism*, Compositio Math. 65 (1988), 3–32; *Addendum*, Compositio Math. 114 (1998), 329–336. https://eudml.org/doc/89880
- B. van Geemen, *An introduction to the Hodge conjecture for abelian varieties*, Lecture Notes in Math. 1594, Springer 1994, 233–252. https://doi.org/10.1007/BFb0094425
- K. Koike, *Algebraicity of some Weil Hodge classes*, Canad. Math. Bull. 47 (2004), 566–572. https://doi.org/10.4153/CMB-2004-055-3
- B. Moonen, Y. Zarhin, *Hodge classes and Tate classes on simple abelian fourfolds*, Duke Math. J. 77 (1995), 553–581. https://doi.org/10.1215/S0012-7094-95-07717-5
- B. Moonen, Y. Zarhin, *Hodge classes on abelian varieties of low dimension*, Math. Ann. 315 (1999), 711–733. https://doi.org/10.1007/s002080050333
- J. Ramón Marí, *On the Hodge conjecture for products of certain surfaces*, Collect. Math. 59 (2008), 1–26. https://doi.org/10.1007/BF03191179
- E. Markman, *The monodromy of generalized Kummer varieties and algebraic cycles on their intermediate Jacobians*, J. Eur. Math. Soc. 25 (2023), 231–321. https://doi.org/10.4171/JEMS/1199
- P. Deligne, *The Hodge conjecture*, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/hodge.pdf
## 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](https://doi.org/10.4064/aa-4-3-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](https://doi.org/10.1090/S0025-5718-1962-0148632-7)).
- **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](https://doi.org/10.4064/aa-4-3-185-208)
- 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](https://doi.org/10.1090/S0025-5718-1962-0148632-7)
- H. Iwaniec, *Almost-primes represented by quadratic polynomials*, Inventiones Mathematicae 47
(1978), 171–188. [DOI](https://doi.org/10.1007/BF01578070)
- B. Green and T. Tao, *The primes contain arbitrarily long arithmetic progressions*, Annals of
Mathematics 167 (2008), 481–547. [arXiv:math/0404188](https://arxiv.org/abs/math/0404188)
- J. Maynard, *Small gaps between primes*, Annals of Mathematics 181 (2015), 383–413.
[arXiv:1311.4600](https://arxiv.org/abs/1311.4600)
## 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](https://en.wikipedia.org/wiki/Inverse_Galois_problem).
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](https://arxiv.org/abs/2411.07857)) 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
Local Connectivity of the Mandelbrot Set (MLC)Open Problem
## 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.
Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper
## Motivation
Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical $\Phi^4_3$ model $\partial_t u = \Delta u - u^3 + \xi$ on the three-dimensional torus, the KPZ equation $\partial_t h = \partial_x^2 h + (\partial_x h)^2 - \infty + \xi$, and the parabolic Anderson model $\partial_t u = \Delta u + u\,\xi$ all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's *A theory of regularity structures* (Invent. Math. 198 (2014) 269–504, [arXiv:1303.5113](https://arxiv.org/abs/1303.5113)) develops a calculus in which such products, and the resulting fixed-point problems, become well posed.
The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on $\mathbb{R}^d$ with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper.
## Setting
Fix a dimension $d$ and a **scaling** $s = (s_1,\dots,s_d)$ of positive integers, with $|s| = \sum_i s_i$, and put $\|x\|_s = \max_i |x_i|^{1/s_i}$. For $\delta > 0$, a point $x \in \mathbb{R}^d$ and a test function $\varphi$, the **rescaled test function** is
$$ (S^{\delta}_{s,x}\varphi)(y) = \delta^{-|s|}\,\varphi\!\left(\frac{y_1-x_1}{\delta^{s_1}},\dots,\frac{y_d-x_d}{\delta^{s_d}}\right). $$
Write $\mathcal{B}^r_{s,0}$ for the set of test functions supported in $\{\|y\|_s \le 1\}$ whose derivatives up to order $r$ are bounded by $1$. For $\alpha<0$, a distribution $\xi$ belongs to the Hölder–Besov space $\mathcal{C}^\alpha_s$ if, on every compact set $K$, $|\langle \xi, S^{\delta}_{s,x}\eta\rangle| \le C\delta^{\alpha}$ uniformly over $x\in K$, $\delta \in (0,1]$ and $\eta \in \mathcal{B}^r_{s,0}$ with $r=-\lfloor\alpha\rfloor$.
A **regularity structure** $(A,T,G)$ consists of an index set $A \subseteq \mathbb{R}$ containing $0$, bounded below and locally finite; a graded vector space $T = \bigoplus_{\alpha\in A} T_\alpha$ with $T_0 \cong \mathbb{R}$ spanned by a unit $\mathbf{1}$; and a group $G$ of linear operators on $T$ with $\Gamma a - a \in \bigoplus_{\beta<\alpha}T_\beta$ for $a \in T_\alpha$, and $\Gamma\mathbf{1} = \mathbf{1}$. Elements of $T_\alpha$ are "homogeneous of order $\alpha$": they are placeholders for objects whose size at scale $\varepsilon$ is $\varepsilon^{\alpha}$.
A **model** $(\Pi,\Gamma)$ assigns to each point $x$ a linear map $\Pi_x : T \to \mathcal{D}'(\mathbb{R}^d)$ and to each pair $(x,y)$ an element $\Gamma_{xy}\in G$, subject to $\Gamma_{xx}=\mathrm{id}$, $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$, $\Pi_y = \Pi_x\circ\Gamma_{xy}$ and, locally uniformly, the analytic bounds
$$ |(\Pi_x a)(S^{\delta}_{s,x}\varphi)| \lesssim \|a\|_\ell\,\delta^{\ell}, \qquad \|\Gamma_{xy}a\|_m \lesssim \|a\|_\ell\,\|x-y\|_s^{\ell-m}, \qquad a \in T_\ell,\; m<\ell. $$
A **modelled distribution** of order $\gamma$ is a function $f : \mathbb{R}^d \to T_{<\gamma}$ such that on every compact $K$
$$ |||f|||_{\gamma;K} = \sup_{x\in K,\ \beta<\gamma}\|f(x)\|_\beta + \sup_{\substack{x,y \in K,\ \|x-y\|_s\le 1 \\ \beta<\gamma}} \frac{\|f(x)-\Gamma_{xy}f(y)\|_\beta}{\|x-y\|_s^{\gamma-\beta}} < \infty; $$
the space of these is $\mathcal{D}^\gamma$, and $\mathcal{D}^\gamma(V)$ if $f$ takes values in a **sector** $V$, that is, a graded $G$-invariant subspace vanishing in degrees below its regularity.
## Formalization targets
### Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$
With $\alpha = \min A < 0$ and $r$ the order attached to $A$, for every $f \in \mathcal{D}^\gamma$ with $\gamma>0$ there is a **unique** distribution $\mathcal{R}f \in \mathcal{C}^\alpha_s$ with
$$ \big|(\mathcal{R}f - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \lesssim \delta^{\gamma} \qquad (x \in K,\ \delta\in(0,1],\ \eta\in\mathcal{B}^r_{s,0}). $$
The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants.
### Milestone level — the calculus around the reconstruction operator
The uniqueness clause of Theorem 3.10 in isolation; the existence of a *linear* reconstruction operator for arbitrary $\gamma \in \mathbb{R}$ (for $\gamma\le 0$ the bound no longer pins it down); Corollary 3.16, improving the regularity of $\mathcal{R}f$ to $\mathcal{C}^\beta_s$ when $f$ takes values in a sector of regularity $\beta$; Proposition 3.31, that for $\nu>0$ the action of $\Pi$ on $T_\nu$ is determined by $\Gamma$ and by $\Pi$ in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of $f_1 \in \mathcal{D}^{\gamma_1}(V)$ and $f_2\in\mathcal{D}^{\gamma_2}(W)$ lies in $\mathcal{D}^{\gamma}$ with $\gamma = (\gamma_1+\alpha_2)\wedge(\gamma_2+\alpha_1)$.
## Significance
The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces $\mathcal{D}^\gamma$ carry no information about actual distributions.
Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces $\mathcal{C}^\alpha_s$ that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the $\Phi^4_3$ and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one.
## Difficulty
The naive construction fails: setting $\mathcal{R}f := \Pi_x f(x)$ for a fixed $x$ is wrong away from $x$, and the pointwise limit $\lim_{\delta\to0}$ of localisations of $\Pi_x f(x)$ around each $x$ does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling $s$: one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the $\mathcal{D}^\gamma$ bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for $\gamma>0$ is by contrast short, and is listed as a separate milestone.
## Formalization scope
The development commits to the following conventions, fixed in the mission's definition files. Points of $\mathbb{R}^d$ are `Fin d → ℝ`. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by $0$ to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's $\mathcal{B}^r_{s,0}$ consists of $C^r$ functions; here it consists of smooth ones, which defines the same spaces $\mathcal{C}^\alpha_s$. The model space is the algebraic direct sum $\bigoplus_{a\in A} T_a$ over the index set, each $T_a$ a real normed space, with $Q_a$ the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces $V_a \subseteq T_a$; Hairer's requirement that each $V_a$ admit a complement is automatic in this algebraic setting. The integer $r$ appearing in the model bounds is the smallest one with $\ell > -r$ for all $\ell \in A$, which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in $\mathcal{C}^\alpha_s$, and uniqueness simultaneously.
Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on $\mathbb{R}^d$, the elementary theory of $\mathcal{C}^\alpha_s$ (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates.
## Selected references
- M. Hairer, *A theory of regularity structures*, Inventiones Mathematicae 198 (2014) 269–504. [arXiv:1303.5113](https://arxiv.org/abs/1303.5113), [DOI:10.1007/s00222-014-0505-4](https://doi.org/10.1007/s00222-014-0505-4)
- T. Lyons, *Differential equations driven by rough signals*, Revista Matemática Iberoamericana 14 (1998) 215–310. [DOI:10.4171/RMI/240](https://doi.org/10.4171/RMI/240)
- M. Gubinelli, *Controlling rough paths*, Journal of Functional Analysis 216 (2004) 86–140. [arXiv:math/0306433](https://arxiv.org/abs/math/0306433)
- M. Gubinelli, P. Imkeller, N. Perkowski, *Paracontrolled distributions and singular PDEs*, Forum of Mathematics Pi 3 (2015) e6. [arXiv:1210.2684](https://arxiv.org/abs/1210.2684)
- Y. Bruned, M. Hairer, L. Zambotti, *Algebraic renormalisation of regularity structures*, Inventiones Mathematicae 215 (2019) 1039–1156. [arXiv:1610.08468](https://arxiv.org/abs/1610.08468)
Superlinear or exact bounds for planar distinct distancesOpen Problem
# 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](https://www.erdosproblems.com/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](https://github.com/flound1129/esgk-on3/blob/main/docs/results/esgk-n14-atomic-proof-2026-09-13.md) 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](https://www.erdosproblems.com/98) — extremal question and
bibliography.
- [Project overview](https://github.com/flound1129/esgk-on3/blob/main/README.md)
— fixed-A target and current theorem status.
- [Atomic proof of the ESGK n^(1/4) additive bound](https://github.com/flound1129/esgk-on3/blob/main/docs/results/esgk-n14-atomic-proof-2026-09-13.md),
project manuscript, revised 2026-09-14.
- [Full-proof audit](https://github.com/flound1129/esgk-on3/blob/main/docs/audits/esgk-n14-strengthened-full-audit-2026-09-14.md),
internal adversarial review, 2026-09-14.
Birkhoff's Retrograde Global-Section Conjecture in the Planar Circular Restricted Three-Body ProblemOpen Problem
## 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](https://doi.org/10.1007/BF03015982); [Liu--Salomão, Section 1.4](https://arxiv.org/abs/2506.17867v2)). 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](https://arxiv.org/abs/2407.19159v3)).
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](https://arxiv.org/abs/2407.19159v3); [Hryniewicz](https://arxiv.org/abs/0812.4076v8)). 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](https://arxiv.org/abs/2407.19159v3)). 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](https://arxiv.org/abs/2506.17867v2)). 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](https://arxiv.org/abs/2606.12912)). 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](https://arxiv.org/abs/2407.19159v3). 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](https://arxiv.org/abs/2506.17867v2)).
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)](https://arxiv.org/abs/2407.19159v3)). 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](https://arxiv.org/abs/2407.19159v3)).
## 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](https://arxiv.org/abs/2407.19159v3).
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](https://arxiv.org/abs/0812.4076v8)).
## 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](https://doi.org/10.1007/BF03015982); [Joung--van Koert, Introduction](https://arxiv.org/abs/2407.19159v3)). 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](https://arxiv.org/abs/2506.17867v2)). 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](https://arxiv.org/abs/2407.19159v3); [Liu--Salomão, Theorem 1.16](https://arxiv.org/abs/2506.17867v2)).
## 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](https://doi.org/10.1007/BF03015982).
- U. Hryniewicz, *Fast finite-energy planes in symplectizations and applications*, Trans. Amer. Math. Soc. 364 (2012), 1859--1931. [arXiv:0812.4076v8](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/2506.17867v2).
- L. Liu and P. A. S. Salomão, *Birkhoff conjecture and finite energy foliations in Hill's lunar problem*, arXiv:2606.12912 (2026). [Preprint](https://arxiv.org/abs/2606.12912).
Circle packing in a square: exact constantsTextbook
## Motivation
Packing congruent circles into a square is a classical problem in discrete geometry: for each natural number $n$, choose a common radius as large as possible while keeping all disks inside the square and preventing overlap. Every exact value requires two logically distinct achievements: an explicit configuration attaining the proposed radius and a proof that no configuration can do better.
The character of those proofs changes sharply with $n$. The first cases admit short geometric arguments; later cases use contact-graph analysis, specialized case divisions, or computer-assisted global optimization with interval arithmetic. Formalizing the resulting constants therefore provides a growing benchmark for extremal geometry, real algebra, finite configurations, and verified computation in Lean.
This is an **open-ended formalization mission**. It begins with the exact constants currently represented by theorem-backed milestones, but it is not restricted to a fixed terminal value of $n$. Further milestones may be added whenever an exact packing value and its rigorous optimality argument are identified and stated precisely enough for formalization.
## Setting
A point is a pair of real coordinates. For points $p=(x,y)$ and $q=(x',y')$, squared Euclidean distance is
$$
\operatorname{sqDist}(p,q)=(x-x')^2+(y-y')^2.
$$
For a real radius $r$, a point lies in the inner square when both coordinates belong to the closed interval $[r,1-r]$. This is exactly the coordinate condition saying that a closed disk of radius $r$, centered at that point, is contained in the unit square.
The predicate $\operatorname{Packable}(n,r)$ requires $0\le r\le \tfrac12$ and a family of $n$ centers in the inner square such that the squared distance between every two distinctly indexed centers is at least $(2r)^2$. Equality is allowed, so tangent disks are admitted. Radius zero is also admitted.
Define
$$
r_n=\sup\{r\in\mathbb R:\operatorname{Packable}(n,r)\}
$$
and define the optimal covered-area fraction by
$$
c_n=n\pi r_n^2.
$$
It is often convenient to use the equivalent point-separation constant $d_n$, the greatest possible minimum pairwise distance among $n$ points in the unit square. The conversion is
$$
r_n=\frac{d_n}{2(1+d_n)},
\qquad
c_n=n\pi\left(\frac{d_n}{2(1+d_n)}\right)^2.
$$
The Lean definitions use a supremum rather than assuming in advance that an optimal packing is attained.
## Current exact-value milestones
The mission currently contains theorem-backed milestones for the following values:
| $n$ | Exact separation or area value | Proof character in the supplied notes |
|---:|---|---|
| $2$ | $d_2=\sqrt2$, hence $c_2=\pi(3-2\sqrt2)$ | diagonal bound |
| $3$ | $d_3=\sqrt6-\sqrt2$ | minimum enclosing square of a triangle |
| $4$ | $d_4=1$, hence $c_4=\pi/4$ | convex hull and perimeter |
| $5$ | $d_5=1/\sqrt2$ | four-cell pigeonhole argument |
| $6$ | $d_6=\sqrt{13}/6$ | case-specific geometric proof |
| $7$ | $d_7=4-2\sqrt3$ | hand proof and later computer verification |
| $8$ | $d_8=\sqrt{2-\sqrt3}$ | case-specific geometric proof |
| $9$ | $d_9=1/2$, hence $c_9=\pi/4$ | classical geometric proof |
| $16$ | $d_{16}=1/3$, hence $c_{16}=\pi/4$ | theoretical grid-optimality proof |
| $25$ | $d_{25}=1/4$, hence $c_{25}=\pi/4$ | theoretical grid-optimality proof |
| $36$ | $d_{36}=1/5$, hence $c_{36}=\pi/4$ | theoretical grid-optimality proof |
For rows stated using $d_n$, the corresponding milestone for $c_n$ uses the conversion formula above. The equalities are claims about the supremum-defined packing constants, not merely about the displayed candidate configurations.
## An extensible mission
The milestone list is intended to grow. The supplied survey notes classify $n=2,\ldots,33$ and $n=36$ as rigorously solved in the cited literature, while distinguishing $n=34$ and $n=35$ as not rigorously closed in the cited 2021 account. Many of the computer-assisted cases do not have a simple radical expression in the supplied notes. Before such a case is linked to a Lean theorem, its primary source must provide a precise candidate value, algebraic characterization, certified enclosure, or optimal-configuration certificate that can be stated faithfully.
A new milestone should identify:
1. the precise value or exact characterization being formalized;
2. an attaining configuration or a certified existence argument;
3. a universal upper bound or global-optimality certificate;
4. the primary source and exact theorem, equation, or certificate location;
5. any trusted computational artifact and the arithmetic guarantees it requires.
Numerical evidence and strong bounds are valuable, but they must be labeled as bounds rather than exact-value milestones. Conversely, newly published exact results for larger $n$ may be added without changing the underlying definitions.
## Proof obligations
Every exact-value milestone must connect the proposed value to `Packable`, `r_n`, and `c_n`. Constructing a configuration establishes only a lower bound. An upper-bound argument without attainability also does not establish equality. A complete proof must bridge both directions through the supremum definition.
The proof methods may include:
- elementary diameter, pigeonhole, convexity, or enclosing-shape arguments;
- normalization between disk centers and point-separation configurations;
- contact-graph and boundary-constraint analysis;
- finite case decompositions;
- interval arithmetic and formally checked branch-and-bound certificates;
- exact algebraic identities needed to convert $d_n$ into $r_n$ and $c_n$.
Shortcuts that redefine $r_n$, $d_n$, or $c_n$ to equal a desired answer are excluded. The constants must remain consequences of the common geometric model.
## Mission structure
The root theorem `CirclePackingConstants.c_all` is the conjunction of the eleven exact-value milestones currently in the mission, covering $n=2,3,4,5,6,7,8,9,16,25,36$. Its proof sketch reduces the root directly to those milestone theorems, so the mission remains open until every current exact value is proved.
The milestone theorems remain separately reusable and independently auditable. When further exact values are added, a successor aggregate theorem can extend the conjunction and become the new root without replacing the shared definitions or invalidating earlier results.
This structure allows elementary cases, historical hand proofs, and computer-assisted certificates to progress independently while remaining part of one cumulative library of exact circle-packing constants.
## Formalization scope
The Lean model uses `ℝ × ℝ` for points and an explicit coordinate formula for squared Euclidean distance. Disk containment is represented by inclusive coordinate inequalities. Nonoverlap is represented by a weak squared-distance inequality, so tangency is permitted. The indexing type is `Fin n`, and the definitions apply to every natural number, including zero.
The definition bundle contains only `Point`, `sqDist`, `InInnerSquare`, `Packable`, `r_n`, and `c_n`. Solvers may introduce normalization maps, separation bounds, explicit configurations, supremum lemmas, contact structures, certificate checkers, and radical or polynomial identities as auxiliary declarations.
## Selected references
- User-supplied notes, *Circles in squares: constants, proofs, and what is actually known*, supplied September 12, 2026. The notes summarize the exact small-$n$ formulas, grid cases, historical proof taxonomy, and computer-assisted frontier used to organize this mission.
- J. Schaer and A. Meir, “On a geometric extremum problem,” *Canadian Mathematical Bulletin* 8 (1965), 21–27.
- J. Schaer, “The densest packing of nine circles in a square,” *Canadian Mathematical Bulletin* 8 (1965), 273–277.
- B. L. Schwartz, “Separating points in a square,” *Journal of Recreational Mathematics* 3 (1970), 195–204.
- J. B. M. Melissen, “Densest packing of six equal circles in a square,” *Elemente der Mathematik* 49 (1994), 27–31.
- M. C. Markot, “Improved interval methods for solving circle packing problems in the unit square,” *Journal of Global Optimization* 81 (2021), 773–803.
- Erich Friedman, *Circles in Squares*, Erich's Packing Center, for background tables and diagrams of candidate packings.
Erdős Problem 142: Asymptotics for Sets Free of k-Term Arithmetic ProgressionsOpen Problem
## 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](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.lean) 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](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/142.lean), 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>
# Proofs from THE BOOK: verified results and open formalization tasks
This Textbook project develops a reusable Lean library around Martin Aigner and Günter M. Ziegler's *Proofs from THE BOOK*. It combines results imported from the existing `proof_in_the_book` repository with precise contribution targets from the sixth edition (2018). The aim is to preserve mathematical meaning, reuse existing proofs, and make the remaining work accessible to other contributors.
## What is already verified
The original import contains 156 distinct platform-accepted results. Euclid, the original main theorem, is retained as a completed milestone when the project goal moves to the sixth-edition extension. Every one of the repository's 40 chapter topics has accepted results. Each result certifies its actual Lean statement, including its hypotheses; this does not certify every argument or every theorem in a chapter. Some proofs reuse Mathlib, while others were developed in the repository. Their source and proof notes retain that distinction.
The imported source snapshot is `873d52e0c88cd351f594221e70c3c5b3559777a9`. Imported results use Lean 4.30.0 and Mathlib `c5ea00351c28e24afc9f0f84379aa41082b1188f`. Immutable public source links are used only where the linked source matches the verified artifact. Compatibility changes, unsuccessful attempts, and verification evidence are retained in the integration project.
The live goal is the explicit conjunction of the 21 linked sixth-edition extension targets. Its reduction connects these targets to the goal, so proving the remaining children advances the project. This goal is deliberately narrower than “every theorem and every proof in the book”; the unlinked topology tasks below are additional formalization work.
## Sixth-edition contribution targets
New milestones explicitly marked **6th ed.** cover Chapters 7 (spectral theorem and determinants), 15 (round circles and links), 35 (finite Kakeya), 37 (permanents and entropy), and 45 (probabilistic counting). They include the precise definitions and boundary conditions needed to state the results. Compiled Open targets are requests for proofs, not proved results. The spectral theorem has a direct Mathlib proof; community results are reused under their actual statements and with attribution.
Two Chapter 15 tasks intentionally remain unlinked mathematical milestones: the full non-equivalence assertion for the depicted Borromean, Tait, and trivial links, and the Fox-coloring invariance bridge for equivalent link diagrams. These invite formalization of the diagrams and the topology bridge as well as proof. The separate modular Fox calculations do not by themselves establish ambient non-equivalence.
The crossing-lemma target is the universal good-drawing form: actual injective edge arcs and exact finite intersection records appear in its interface. It does not assume the desired crossing bound. The Ramsey target preserves the real exponent for odd k. The related public Erdős–Ramsey result with a rounded exponent is identified as a supporting result, not as proof of that full target.
## Chapter numbering and statement scope
Older milestones use the repository's chapter labels. Repository Chapters 1–21 match the bundled fourth edition; Chapter 22 inserts Van der Waerden's permanent theorem, and Chapters 23–40 correspond to fourth-edition Chapters 22–39. The sixth edition has 45 chapters, so these organizational labels are not sixth-edition chapter numbers. New milestones give sixth-edition numbers and printed source pages explicitly.
Some existing formalizations preserve narrower statements or additional premises. Examples include repository Chapter 13's dihedral-angle conclusion, Chapter 28's Dilworth lower-bound result, and the geometric premises in Chapter 36. Read the actual linked theorem and its description before reusing it. A chapter title or the former Euclid main theorem is not a completion certificate for the collection.
## How to contribute
Choose an Open linked theorem and inspect its definitions, exact binders, Mathlib revision, and prior attempts. Reuse a compatible existing result when it proves that statement; preserve the original contributor's attribution. Submit a matching proof for verification. For an unlinked milestone, first formalize and review the source statement and its definitions. These are known textbook results awaiting formalization or proof in this project, rather than claims of new unresolved mathematics.
Source repository: https://github.com/xiangyazi24/proof_in_the_book
Book: Aigner and Ziegler, *Proofs from THE BOOK*, Sixth Edition (2018), https://doi.org/10.1007/978-3-662-57265-8
Erdős Problem 287: Gaps Between Unit-Fraction DenominatorsOpen Problem
## 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](https://mathweb.ucsd.edu/~ronspubs/80_11_number_theory.pdf)) 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](https://www.erdosproblems.com/287).
**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](https://mathweb.ucsd.edu/~ronspubs/80_11_number_theory.pdf)
- 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](https://kconrad.math.uconn.edu/blurbs/gradnumthy/padicharmonicsum.pdf)
- T. F. Bloom, *Erdős Problem #287*, [erdosproblems.com/287](https://www.erdosproblems.com/287).
The Erdős–Straus Conjecture (Erdős Problem 242)Open Problem
## 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](https://www.erdosproblems.com/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](https://www.renyi.hu/~p_erdos/1950-02.pdf), discusses distinct unit fractions and attributes the conjecture jointly to himself and Straus. [His 1961 problem I.32, p. 238](https://www.renyi.hu/~p_erdos/1961-22.pdf), allows positive denominators without specifying distinctness, while [the 1979 statement, problem 9, p. 70](https://www.renyi.hu/~p_erdos/1979-22.pdf), 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](https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf).
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](https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf).
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](https://math.dartmouth.edu/~carlp/ESS-ExceptionsV9.pdf), 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](https://www.jstage.jst.go.jp/article/kyushumfs/19/1/19_1_37/_pdf/-char/en), 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](https://doi.org/10.1007/BF01934370), whose publisher abstract reports 198 residual classes modulo $120120$, and [Vaughan’s density theorem](https://doi.org/10.1112/S0025579300002886), 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](https://arxiv.org/abs/1107.1010) provide counting results and a classification of polynomially soluble congruences. [Bloom–Elsholtz, Theorem 1, pp. 239–240](https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf), 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](https://math.dartmouth.edu/~carlp/ESS-ExceptionsV9.pdf) 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)](https://arxiv.org/abs/2509.00128) 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](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/242.lean) 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](https://www.renyi.hu/~p_erdos/1950-02.pdf).
- Erdős–Graham, *Old and New Problems and Results in Combinatorial Number Theory* (1980), chapter IV; [author’s institutional scan](https://mathweb.ucsd.edu/~ronspubs/80_11_number_theory.pdf).
- Obláth, *Sur l’équation diophantienne $4/n=1/x_1+1/x_2+1/x_3$*, Mathesis **59** (1950), 308–316; [bibliographic record](https://www.erdosproblems.com/bibs/Ob50), 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](https://doi.org/10.2206/kyushumfs.19.37).
- Mordell, *Diophantine Equations*, Academic Press (1969), chapter 30, pp. 287–290; [publisher record](https://shop.elsevier.com/books/diophantine-equations/mordell/978-0-12-506250-3).
- 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.
Irrationality and transcendence of Euler's constantOpen Problem
## 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.