Number Theory

Motivation

In Esquisse d'un Programme (1984), Alexandre Grothendieck describes a discovery that reorganised his mathematical interests: a finite oriented combinatorial map drawn on a surface — a dessin d'enfant, a child's drawing — determines canonically a smooth projective algebraic curve together with a map to the projective line ramified only above $0$, $1$ and $\infty$, and that curve and map are defined over the field $\overline{\mathbb{Q}}$ of algebraic numbers (Esquisse, §3, pp. 14–16 of the French text). Consequently the absolute Galois group $\Gamma = \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ acts on these purely combinatorial objects; in the spherical case, where the structural map is a rational function $f(z) = P(z)/Q(z)$, the action of $\gamma \in \Gamma$ is obtained simply by applying $\gamma$ to the coefficients of $P$ and $Q$. Grothendieck states in §2 (p. 9) that the resulting outer action of $\Gamma$ on the profinite fundamental group $\hat{\pi}_{0,3}$ of $\mathbb{P}^1 \smallsetminus \{0,1,\infty\}$ is faithful, and in §3 that the theorem of Belyi, announced at the 1978 Helsinki congress, is what makes the dictionary between combinatorics and arithmetic exact.

Timeline of the results this mission formalizes. Belyi (1979, On Galois extensions of a maximal cyclotomic field, Izv. Akad. Nauk SSSR) proved that a smooth projective curve over $\mathbb{C}$ is defined over a number field if and only if it admits a map to $\mathbb{P}^1$ unramified outside $\{0,1,\infty\}$; the "only if" half is an explicit construction with polynomials over $\mathbb{Q}$. Grothendieck (1984) drew the consequence that $\Gamma$ acts on dessins and asserted faithfulness of the action on $\hat{\pi}_{0,3}$. Lenstra, in an appendix to L. Schneps (ed.), The Grothendieck Theory of Dessins d'Enfants (LMS Lecture Notes 200, CUP 1994), showed that the action is already faithful on the much smaller class of plane trees, equivalently on Shabat polynomials. That tree-level statement is the goal of this mission, because it is the sharpest form of faithfulness that can be stated without first building the theory of étale fundamental groups.

Setting

Work over $\overline{\mathbb{Q}}$, realized as the algebraic closure of $\mathbb{Q}$, and write $\Gamma$ for its group of field automorphisms fixing $\mathbb{Q}$ pointwise.

A nonconstant polynomial $P$ over a field $K$ is a Belyi polynomial (classically a Shabat polynomial) when every critical value of $P$ lies in $\{0,1\}$: for every $z \in K$ with $P'(z) = 0$ one has $P(z) = 0$ or $P(z) = 1$. Over an algebraically closed field of characteristic zero this says exactly that $P$, viewed as a degree-$n$ map $\mathbb{P}^1 \to \mathbb{P}^1$, is unramified outside the fibres over $0$, $1$ and $\infty$. The associated dessin is the preimage $P^{-1}([0,1])$, a plane tree with $n$ edges whose vertices are the points above $0$ and $1$, with vertex orders equal to the multiplicities of the corresponding roots of $P$ and of $P - 1$.

Two Belyi polynomials define the same dessin exactly when they are affinely equivalent: $Q = P(aX + b)$ for some $a \neq 0$ and some $b$. The target coordinate is already rigidified by the normalisation of the critical values to $\{0,1\}$; only the source coordinate remains free.

The group $\Gamma$ acts coefficientwise: $P^{\gamma}$ is the polynomial obtained from $P$ by applying $\gamma$ to each coefficient. This is exactly the action described in §3 of the Esquisse. It sends Belyi polynomials to Belyi polynomials, and it descends to an action on affine equivalence classes, i.e. on dessins.

Formalization targets

Goal — faithfulness of the Galois action on plane trees

$$\forall\, \gamma \in \Gamma,\quad \gamma \neq 1 \ \Longrightarrow\ \exists\, P \in \overline{\mathbb{Q}}[X] \text{ a Belyi polynomial with } P \not\sim_{\mathrm{aff}} P^{\gamma}.$$

Equivalently: no nontrivial element of the absolute Galois group fixes every plane tree. This is the weakest stable form of the faithfulness assertion in the Esquisse: it fixes no degree, no genus and no tree, asserting only that some dessin is moved.

Supporting targets

• Belyi's theorem, polynomial form. For every finite set $S \subseteq \overline{\mathbb{Q}}$ there is a Belyi polynomial $f \in \mathbb{Q}[X]$ with $f(S) \subseteq \{0,1\}$.
• Descent to $\overline{\mathbb{Q}}$. Every Belyi polynomial over $\mathbb{C}$ is affinely equivalent to one whose coefficients are algebraic over $\mathbb{Q}$.
• Galois equivariance and invariants. $P^{\gamma}$ is again a Belyi polynomial of the same degree, and the multiplicity of $z$ as a root of $P - c$ equals the multiplicity of $\gamma(z)$ as a root of $P^{\gamma} - \gamma(c)$: the dessin's vertex and face orders are Galois invariants.
• Finiteness of the orbit. The set of Galois conjugates of a fixed polynomial over $\overline{\mathbb{Q}}$ is finite — the "visibly finite number of conjugates" of §3.
• Finiteness in a fixed degree. For each $n$ there are only finitely many monic Belyi polynomials of degree $n$ over $\overline{\mathbb{Q}}$ with vanishing subleading coefficient.
• Separation. For every $\alpha \in \overline{\mathbb{Q}}$ there is a Belyi polynomial $P$ such that every $\gamma$ fixing the class of $P$ fixes $\alpha$. The goal follows from this by taking $\alpha$ with $\gamma(\alpha) \neq \alpha$.

Significance

The result itself. Faithfulness turns the combinatorics of finite maps into a faithful representation of $\Gamma$: every nontrivial automorphism of $\overline{\mathbb{Q}}$ is detected by a finite tree, so invariants of dessins (degree, valency lists, monodromy group, field of moduli) are in principle a complete set of tools for distinguishing Galois elements. It is also the entry point to the anabelian programme described in §3 of the Esquisse, since the same statement expresses that $\Gamma$ embeds into the outer automorphism group of $\hat{\pi}_{0,3}$.

Formalizing it. Belyi's theorem and the faithfulness of the Galois action on trees are both established results. Mathlib at the environment revision of this mission contains no declaration mentioning Belyi maps or dessins d'enfants, and no étale fundamental group, so both statements have to be built from the polynomial and Galois-theoretic libraries. What this mission produces is a formal version of the combinatorial half of the dictionary, in a form that avoids scheme theory entirely: everything is phrased with polynomials over $\overline{\mathbb{Q}}$ and $\mathbb{C}$, so the development rests only on Mathlib's existing polynomial, field theory and Galois theory libraries.

Difficulty

The naive attack on the goal — exhibit one tree and one Galois element moving it — does not scale: the statement quantifies over all $\gamma \neq 1$, and $\Gamma$ has no accessible presentation. The real work is the separation statement, which demands, for an arbitrary algebraic number $\alpha$, a tree whose isomorphism class remembers $\alpha$; the construction must control both the existence of a Belyi polynomial with prescribed arithmetic and the rigidity that makes affine equivalence classes finite. Belyi's theorem in polynomial form is itself an induction on the degree of the field of definition of the critical values, and each step changes the polynomial, so bookkeeping of critical values through composition is the bulk of the formal proof. The descent statement over $\mathbb{C}$ is not a formal manipulation either: it needs the finiteness of the set of Belyi polynomials of a given degree up to affine equivalence, which is where the combinatorial classification enters.

Formalization scope

Conventions fixed in the Lean development, and not to be re-litigated by solvers:

• $\overline{\mathbb{Q}}$ is AlgebraicClosure ℚ, and $\Gamma$ is its group of $\mathbb{Q}$-algebra automorphisms.
• "Belyi polynomial" means: positive degree, and every root of the formal derivative is sent to $0$ or $1$. Critical values are required to lie in $\{0,1\}$, not to be exactly $\{0,1\}$; degenerate cases such as $X^n$ (one finite critical value) are therefore included.
• Being a Belyi polynomial is stated over an arbitrary field but is only intended over algebraically closed fields ($\overline{\mathbb{Q}}$, $\mathbb{C}$), where quantifying over the field's own elements captures all critical points.
• Dessin isomorphism is modelled as affine equivalence of the source variable only; conjugating by an affine map of the target is excluded, since the target is rigidified by $\{0,1\}$.
• The Galois action is coefficientwise application of $\gamma$.

Trivialization is ruled out as follows: the goal asserts the existence of a moved Belyi polynomial for each nontrivial $\gamma$, with the nondegeneracy 0 < deg P built into the definition, so no constant or empty witness satisfies it, and no hypothesis of the goal is vacuous ($\gamma \neq 1$ is satisfiable).

A complete development needs: critical values and their behaviour under composition of polynomials; the classification of Belyi polynomials of fixed degree up to affine equivalence; Galois descent for a finite set of polynomials stable under conjugation; and, for the descent target, the identification of the coefficients of a Belyi polynomial over $\mathbb{C}$ as algebraic numbers. All of these are reusable outside this mission. Contributions of general polynomial-ramification infrastructure are welcome, as are alternative formalizations of the same statements over a general algebraically closed field of characteristic zero.

Selected references

• A. Grothendieck, Esquisse d'un Programme (1984), published in L. Schneps and P. Lochak (eds.), Geometric Galois Actions 1, LMS Lecture Note Series 242, Cambridge University Press, 1997. https://doi.org/10.1017/CBO9780511758874
• G. V. Belyi, On Galois extensions of a maximal cyclotomic field, Izv. Akad. Nauk SSSR Ser. Mat. 43 (1979), 267–276. English translation: Math. USSR-Izv. 14 (1980), 247–256. https://doi.org/10.1070/IM1980v014n02ABEH001096
• L. Schneps (ed.), The Grothendieck Theory of Dessins d'Enfants, LMS Lecture Note Series 200, Cambridge University Press, 1994. https://doi.org/10.1017/CBO9780511569302
• S. K. Lando and A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer, 2004. https://doi.org/10.1007/978-3-540-38361-1

Motivation

The Riemann hypothesis asserts that every non-trivial zero of the Riemann zeta function $\zeta$ lies on the line $\operatorname{Re} s = 1/2$; the simplicity hypothesis asserts in addition that every such zero is a simple zero of $\zeta$. Both are statements about the location and the order of a discrete set of points in the complex plane, and almost every reformulation of them stays inside analytic number theory.

Kawahira (2016) gives a reformulation of a different kind. He attaches to $\zeta$ an explicit meromorphic self-map of the Riemann sphere and shows that the Riemann hypothesis together with the simplicity hypothesis is equivalent to a statement about the local dynamics of that map: it has no attracting fixed point. The translation is elementary once the right object is in place — the holomorphic index (residue fixed point index) of a fixed point — and it turns a question about zeros into a question about stability. This mission formalizes that translation, together with the supporting propositions on indices and multipliers that make it work.

Setting

For a non-constant meromorphic $g : \mathbb{C} \to \widehat{\mathbb{C}}$, define the nu function

$$\nu_g(z) \;=\; z - \frac{g(z)}{z\,g'(z)}.$$

If $\alpha \neq 0$ is a zero of $g$ of order $m \ge 1$, then $\alpha$ is a fixed point of $\nu_g$ with multiplier

$$\lambda \;=\; \nu_g'(\alpha) \;=\; 1 - \frac{1}{m\alpha},$$

and if $\alpha$ is a pole of order $m$ the multiplier is $1 + \frac{1}{m\alpha}$. A fixed point $\alpha$ of a holomorphic map $f$ is attracting if $|f'(\alpha)| < 1$, indifferent if $|f'(\alpha)| = 1$, and repelling if $|f'(\alpha)| > 1$.

The holomorphic index of $f$ at a fixed point $\alpha$ is

$$\iota(f,\alpha) \;=\; \frac{1}{2\pi i}\oint_{C} \frac{dz}{z - f(z)},$$

the integral being over a small positively oriented circle around $\alpha$. When the multiplier $\lambda$ is not $1$ one has $\iota = \frac{1}{1-\lambda}$, and the Möbius map $\lambda \mapsto \frac{1}{1-\lambda}$ carries the unit disk onto the half-plane $\operatorname{Re}\iota > 1/2$. So a fixed point is attracting, indifferent or repelling exactly according to whether $\operatorname{Re}\iota$ is $> 1/2$, $= 1/2$ or $< 1/2$: the critical line reappears, in the index plane.

The point of the construction is that $\nu_g$ is engineered so that the index of $\nu_g$ at a simple zero $\alpha$ of $g$ is $\alpha$ itself (and $m\alpha$ at a zero of order $m$). Writing $\nu_\zeta = \nu_g$ for $g = \zeta$: a non-trivial zero $\alpha$ of order $m$ has index $m\alpha$, so $\operatorname{Re}\iota = m\operatorname{Re}\alpha$, and asking that this equal $1/2$ is asking for $m = 1$ and $\operatorname{Re}\alpha = 1/2$.

Formalization targets

Goal — Theorem 1 of the paper, conditions (a), (b), (c)

$$\Big(\text{RH} \wedge \text{simplicity}\Big) \iff \Big(\text{every non-trivial zero is an indifferent fixed point of } \nu_\zeta\Big) \iff \Big(\nu_\zeta \text{ has no attracting fixed point}\Big).$$

Supporting targets

The milestones are the paper's Propositions 3, 4, 5, 7, 8, 9, its Theorem 11 (the variant for the Riemann xi function $\xi$), and Proposition 13 of the appendix (the Newton map $N_g(z) = z - g(z)/g'(z)$, for which every zero of $g$ becomes an attracting fixed point — the contrast that explains why $\nu_g$, and not $N_g$, sees the critical line).

Significance

The equivalence converts the simultaneous truth of the Riemann and simplicity hypotheses into the non-existence of an attracting fixed point of one explicitly given meromorphic function. Nothing in the translation is conjectural: the content is the index computation, the symmetry $\alpha \mapsto 1 - \alpha$ of the non-trivial zeros supplied by the functional equation, and the classification of fixed points by the real part of the index. What a formalization adds is a machine-checked statement of the dictionary, and a reusable Lean development of the holomorphic index, which Mathlib does not currently contain — the index, its relation to the multiplier, and its behaviour at zeros and poles are general facts of one-variable complex dynamics, independent of this application.

Status, precisely: the Riemann hypothesis is open, and this mission does not ask anyone to settle it. Every target here is a theorem with a published proof; the work is to formalize those proofs. The goal theorem is an equivalence between two open statements, so it is provable without deciding either side.

Difficulty

The obvious route to the goal — compute $\nu_\zeta'$ at a zero, apply the classification, done — fails in one direction. From "no attracting fixed point" one gets $\operatorname{Re}(m\alpha) \le 1/2$ for each non-trivial zero $\alpha$ of order $m$, which alone excludes neither a multiple zero nor a zero to the left of the critical line. The functional equation must be used to pair $\alpha$ with $1-\alpha$, whose index is $m(1-\alpha)$; only the two inequalities together force $m = 1$ and $\operatorname{Re}\alpha = 1/2$. A complete Lean proof therefore needs, besides the local computation: that the non-trivial zeros lie in the open strip $0 < \operatorname{Re} s < 1$, that $\alpha$ and $1-\alpha$ are zeros of the same order, and that the trivial zeros and the pole at $s = 1$ give repelling fixed points.

The index milestone (Proposition 3) is a residue computation on a small circle, and the hypotheses have to be arranged so that $z - f(z)$ has exactly one zero inside; the other genuinely analytic milestone is the order-$m$ computation of $\nu_g'$, where $g'$ vanishes at the fixed point when $m \ge 2$ and the singularity is removable rather than absent.

Formalization scope

The development is over $\mathbb{C}$ with Mathlib's riemannZeta. Conventions the Lean statements commit to:

1. Non-trivial zero means: a zero of $\zeta$ that is not one of $-2, -4, -6, \dots$. Nothing about the critical strip is built into the definition; that the non-trivial zeros lie in $0 < \operatorname{Re} s < 1$ is part of the work.
2. Simplicity of a zero $\alpha$ is expressed as $\zeta'(\alpha) \neq 0$.
3. $\nu_g$ is a total function $\mathbb{C} \to \mathbb{C}$, using Lean's convention that division by zero returns zero. At a zero of $g$ this total function agrees with the genuine holomorphic extension of $\nu_g$, so multipliers there are the true ones. At a point where $g$ is non-zero and $g'$ vanishes, and at a pole of $g$, the total function takes an artefactual value; the statements about $\nu_\zeta$ therefore carry the explicit guard $\zeta(\alpha) = 0 \vee \zeta'(\alpha) \neq 0$ together with $\alpha \neq 0, 1$. The excluded points are exactly the pole of $\zeta$ (a repelling fixed point, by Proposition 7 of the paper) and the poles of $\nu_\zeta$, so the guarded statements are equivalent to the paper's, but they are guarded, and a reader should check that they consider the guards faithful.
4. The xi function is taken in Kawahira's normalization $\xi(z) = \frac{1}{2}z(1-z)\pi^{-z/2}\Gamma(z/2)\zeta(z)$, written in Lean through Mathlib's entire function $\Lambda_0$ so that the Lean $\xi$ is entire and has the correct values at $z = 0, 1$ rather than removable-singularity artefacts; the definition file carries a proved lemma identifying it with $\frac{1}{2}z(1-z)\Lambda(z)$ off $\{0,1\}$.
5. Conditions (d) and (e) of the paper's Theorems 1 and 10 — the purely topological reformulations in terms of a topological disk $D$ with $\nu_\zeta(D) \subset D$, and their homeomorphic deformations — are not part of this mission. They rest on the topological characterization of attracting fixed points (the paper's Proposition 2), whose proof uses the Riemann mapping theorem and the Schwarz–Pick lemma; the Riemann mapping theorem is not available in Mathlib, and the intended strength of the inclusion $\nu_\zeta(D) \subset D$ (compact containment) needs to be fixed before the statement can be formalized faithfully. Theorem 14 of the appendix, which is of the same topological kind, is likewise out of scope. A contribution supplying Proposition 2 in a defensible form would be welcome, as a separate mission.

Nothing here is vacuous: the goal is an equivalence of two statements each of which is satisfiable in form, and the guards exclude only points at which the Lean encoding of $\nu_\zeta$ is known not to model the meromorphic map.

Reusable beyond this mission: the holomorphic index, the multiplier classification, the general nu-function and Newton-map computations at a zero of order $m$ — all stated for an arbitrary function analytic at the point, not for $\zeta$.

Selected references

• T. Kawahira, The Riemann Hypothesis and Holomorphic Index in Complex Dynamics, Experimental Mathematics (2016). https://doi.org/10.1080/10586458.2016.1217443
• J. Milnor, Dynamics in One Complex Variable, 3rd ed., Annals of Mathematics Studies 160, Princeton University Press, 2006. (Holomorphic index: Lemma 12.2; topological characterization of fixed points: Section 8.)
• E. C. Titchmarsh, The Theory of the Riemann Zeta Function, 2nd ed., Oxford University Press, 1986. (Functional equation; trivial zeros; the xi function.)
• D. Schleicher, Newton's Method as a Dynamical System: Efficient Root Finding of Polynomials and the Riemann $\zeta$ Function, Fields Inst. Commun. 53 (2008), 213–224.

Motivation

Around 1637 Pierre de Fermat wrote, in the margin of his copy of Diophantus' Arithmetica, that no $n$-th power with $n > 2$ splits as a sum of two like powers, and that he had a proof the margin was too narrow to hold. The claim resisted every generation of number theorists that attacked it, and the machinery built during those attacks — cyclotomic fields, ideal theory, class numbers, elliptic curves, modular forms, Galois representations — became a large part of modern algebraic number theory. The statement itself is elementary enough to explain to a schoolchild; nothing about its proof is.

Timeline. Fermat himself proved the case $n = 4$ by infinite descent, as a corollary of the fact that the area of a right triangle with integer sides is never a perfect square. Euler treated $n = 3$ in his Vollständige Anleitung zur Algebra (1770), by a descent in $\mathbb{Z}[\sqrt{-3}]$ that assumed a unique-factorization property later supplied by others. Dirichlet and Legendre settled $n = 5$ between 1825 and 1830, Dirichlet added $n = 14$ in 1832, and Lamé published $n = 7$ in 1839. In 1847 Kummer made the decisive structural step: introducing ideal numbers to repair the failure of unique factorization in $\mathbb{Z}[\zeta_p]$, he proved the theorem for every regular prime exponent — those $p$ not dividing the class number of $\mathbb{Q}(\zeta_p)$, a condition he characterized by divisibility of Bernoulli numerators. Irregular primes were left open, and the elementary programme stalled there for over a century.

The route that closed the problem came from a different direction. The modularity conjecture of Taniyama (1955), refined by Shimura and given conceptual support by Weil (1967), predicted that every elliptic curve over $\mathbb{Q}$ arises from a modular form. Hellegouarch and then Frey (1985) attached to a hypothetical solution $a^p + b^p = c^p$ the curve $y^2 = x(x - a^p)(x + b^p)$, whose ramification behaviour is too tame for a curve of its conductor. Serre made this precise as the epsilon conjecture, and Ribet proved it in 1986: modularity of semistable elliptic curves over $\mathbb{Q}$ implies Fermat's Last Theorem. Wiles proved that modularity statement, with the key Hecke-algebra input supplied jointly with Taylor, in two 1995 Annals of Mathematics papers. Breuil, Conrad, Diamond and Taylor removed the semistability hypothesis in 2001.

Setting

Fix a natural number $n$ and natural numbers $a, b, c$. A Fermat triple of exponent $n$ is a triple $(a,b,c)$ of strictly positive naturals with

$$a^n + b^n = c^n.$$

For $n = 1$ such triples are everywhere, and for $n = 2$ they are the Pythagorean triples, parametrized by $(k(u^2-v^2),\, 2kuv,\, k(u^2+v^2))$. The assertion at issue is that from $n = 3$ upward there are none at all: the hypothesis $3 \le n$ and the positivity hypotheses $0 < a$, $0 < b$, $0 < c$ are exactly what is needed, since $n \le 2$ and the degenerate triples with a zero entry both produce solutions.

Two standard reductions organize any attack. First, if $(a,b,c)$ is a triple of exponent $n$ and $m \mid n$, then $(a^{n/m}, b^{n/m}, c^{n/m})$ is a triple of exponent $m$; since every $n \ge 3$ is divisible by $4$ or by an odd prime $p \ge 3$, the general statement follows from the cases $n = 4$ and $n = p$ an odd prime. Second, for a prime exponent $p$ one may assume $\gcd(a,b,c) = 1$, and the classical literature then splits on whether $p \nmid abc$ (case I) or $p \mid abc$ (case II).

Formalization targets

Goal

$$\forall\, n \ge 3,\ \forall\, a, b, c \in \mathbb{N}_{>0},\qquad a^n + b^n \ne c^n.$$

This is the mission's single goal, referenced as the published platform theorem fermat_last_theorem. It fixes no exponent, no congruence class, and no auxiliary structure: any complete argument, classical or modern, discharges it.

Significance

The result itself. As a Diophantine statement, Fermat's Last Theorem is a closed case; its value now lies in what proving it required. The proof established the modularity of semistable elliptic curves over $\mathbb{Q}$, made modularity lifting ("$R = T$") a standard technique, and turned Galois deformation theory into a working tool. Those consequences — not the non-existence of Fermat triples — are what the surrounding mathematics uses daily; the Fermat statement is the compact certificate that the machinery works.

Formalizing it. The theorem is proved but not formally verified end to end, and that gap is the mission. Machine-checked proofs exist for the small exponents and for Kummer's regular-prime case: Mathlib carries the general statement together with the cases $n = 3$ and $n = 4$, and the flt-regular project verified the regular-prime theorem in Lean 4. No formal proof of the full theorem exists in any system; Buzzard's ongoing FLT project at Imperial College is building one by reducing the statement to results known to experts by the late 1980s. Contributions here need not follow that route — a complete Lean proof of any single case not yet covered, or of any structural ingredient (level lowering, modularity lifting, the properties of the Frey curve), is a genuine advance, and the platform's sketch mechanism is the natural way to record such a reduction.

Difficulty

The naive attacks fail for identifiable reasons, and a solver should rule them out before spending time on them. Congruence and descent arguments of the kind that settle $n = 3, 4, 5, 7$ depend on the arithmetic of a specific small ring and do not generalize: the descent step needs unique factorization in $\mathbb{Z}[\zeta_n]$ or a substitute, and unique factorization fails there for all but finitely many $n$. Kummer's ideal-theoretic repair recovers the argument exactly when $p$ is regular, and no argument in that family is known to handle irregular primes; the irregular primes are moreover infinite in number, so no finite computation closes them. Parity, size, and modular-arithmetic obstructions have all been shown insufficient, since the equation has solutions modulo every prime power for suitable triples. The only known complete proof passes through modularity, which means the formal development needs elliptic curves over $\mathbb{Q}$, their Galois representations, modular forms and Hecke algebras, level-lowering, and a modularity lifting theorem — none of which is a shortcut around the difficulty, all of which is where the difficulty actually lives.

Formalization scope

The target is stated over $\mathbb{N}$, so no truncated subtraction enters the statement and no sign analysis is hidden in it; the equivalent formulations over $\mathbb{Z}$ and over $\mathbb{Q}$ follow by clearing denominators and moving terms, and a solver who prefers to work over $\mathbb{Z}$ must supply that bridge. Exponentiation is Monoid.npow on $\mathbb{N}$, and $0^0 = 1$ plays no role because $3 \le n$. The hypotheses $0 < a$, $0 < b$, $0 < c$ are all load-bearing and none of them is vacuous, so the statement admits no trivializing reading: dropping any one makes it false, and every hypothesis is satisfiable, so the conclusion cannot be reached by contradiction from the assumptions alone. Mathlib does not contain Fermat's Last Theorem, so the goal cannot be discharged by citing a library lemma.

A complete development will want: the reduction from general $n$ to $n = 4$ and odd prime exponents; the coprimality normalization; cyclotomic fields, class groups, and the regularity criterion for the Kummer line of attack; and, for the modular route, Weierstrass curves over $\mathbb{Q}$, conductors and minimal models, Galois representations attached to torsion points, modular forms and Hecke operators, and the level-lowering and modularity-lifting statements. Most of that infrastructure is reusable well beyond this mission and is welcome as separate published theorems and definitions. Partial contributions are welcome in either style: a direct proof of a single exponent, or a sketch that reduces the goal to child lemmas with statements that stand on their own.

Selected references

• Andrew Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559
• Richard Taylor and Andrew Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560
• Kenneth A. Ribet, On modular representations of $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476. https://doi.org/10.1007/BF01231195
• Christophe Breuil, Brian Conrad, Fred Diamond and Richard Taylor, On the modularity of elliptic curves over $\mathbb{Q}$: wild 3-adic exercises, Journal of the American Mathematical Society 14 (2001), 843–939. https://doi.org/10.1090/S0894-0347-01-00370-8
• Ernst Eduard Kummer, Beweis des Fermat'schen Satzes der Unmöglichkeit von $x^\lambda + y^\lambda = z^\lambda$ für eine unendliche Anzahl Primzahlen $\lambda$, Monatsberichte der Königlich Preußischen Akademie der Wissenschaften zu Berlin (1847), 132–139.
• Gerhard Frey, Links between stable elliptic curves and certain Diophantine equations, Annales Universitatis Saraviensis 1 (1986), 1–40.
• Riccardo Brasca et al., Fermat's Last Theorem for regular primes (flt-regular), Lean 4 formalization. https://github.com/leanprover-community/flt-regular
• Kevin Buzzard et al., The Fermat's Last Theorem project, Lean 4 formalization in progress. https://imperialcollegelondon.github.io/FLT/

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Klimov, Pil'tai, Sheptitskaya (1972): $115$; Riesel–Vaughan (1983): $19$ for all integers, using zero-based prime-counting estimates.
• Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's earlier values ($100\,001$ down to $241$) came from Schnirelmann's method with every constant written out. Those arguments stall near $241$ because the medium range relies only on a Chebyshev lower bound for $\pi(y)$. This entry adds the small-shift idea of Riesel and Vaughan, which removes that bottleneck without any zeta-zero input.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 159,\ \textstyle\sum s = n.$$

This is the campaign template with the value $159$ filled in.

How the bound arises

Let $B = \{(p-3)/2 : p \text{ odd prime}\}$ and $A = B + B$. We show $\sigma(A) \ge 1/79$, then conclude with Mann's theorem as in the $241$ entry. Write $L = \log y$ for the scale.

1. Chebyshev constant $\log 2$. Mathlib's $\psi(x) \ge (x-1)\log 2 - \log(x+2)$ gives $\pi(x) \ge (x \log 2 - O(\log x))/\log x$, better than the constant $2/3$ used in earlier entries. On its own it covers $L \lesssim 90$ through $B \subseteq A$.
2. Small-shift range (Riesel–Vaughan 1983, Lemma 8). Fix the first $150$ odd primes $p_1$ (up to $877$) and let $R(s)$ count $s = p_1 + q$ with $q$ prime. Then $\sum_s R(s)$ needs only $\pi$, and $\sum_s R(s)^2$ needs an upper bound for prime pairs $q, q + d$ with a fixed even shift $d$. That bound is the Selberg sieve for $a(a+d)$ on an interval, whose local data are those of the existing Goldbach sieve with $s := d$. The weight sum $\sum_{p_1 \ne p_2} C(p_1 - p_2)$ over these primes is a finite computation. Cauchy–Schwarz then gives $\#\{s \le y : R(s) > 0\} \ge y/158$ for $90 \lesssim L \le 3000$.
3. Large range $L \ge 3000$: the Selberg pointwise bound $r(s) \le b\,C(s)\,s/\log^2 s$, the weighted first moment (now with constant $(\log 2)^2$), a high moment of $C(s)$, and Hölder, as in the $241$ entry, at a much higher threshold.
4. Mann's theorem turns $79\,\sigma(A) \ge 1$ into $79A = \mathbb{Z}_{\ge 0}$, so every odd $n$ beyond a small bound is a sum of $158$ odd primes plus one $3$, and small $n$ are handled with twos and threes: $K = 2 \cdot 79 + 1 = 159$.

Significance

The argument stays elementary: no prime number theorem and no zeros of $\zeta$ or $L$-functions. New reusable components:

1. Explicit Selberg upper bound for prime pairs $(q, q+d)$ with a fixed shift, uniform in $d$.
2. The Riesel–Vaughan small-shift second-moment argument.
3. Chebyshev's $\log 2$ constant from Mathlib carried into the sieve moments.

Formalization scope

The Lean statement is the campaign template verbatim with $159$ in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev bounds (Chebyshev.psi_ge', Chebyshev.theta_le_log4_mul_x) and the Λ² sieve framework (Mathlib.NumberTheory.SelbergSieve).

Selected references

• H. Riesel, R. C. Vaughan, On sums of primes, Ark. Mat. 21 (1983), 45–74.
• P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
• Explicit improvement of the $241$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $159$; not peer reviewed.

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Klimov, Pil'tai, Sheptitskaya (1972): $115$; Riesel–Vaughan (1983): $19$ for all integers, using zero-based prime-counting estimates.
• Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's earlier values ($100\,001$ down to $241$) came from Schnirelmann's method with every constant written out. Those arguments stall near $241$ because the medium range relies only on a Chebyshev lower bound for $\pi(y)$. This entry adds the small-shift idea of Riesel and Vaughan, which removes that bottleneck without any zeta-zero input.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 151,\ \textstyle\sum s = n.$$

This is the campaign template with the value $151$ filled in.

How the bound arises

Let $B = \{(p-3)/2 : p \text{ odd prime}\}$ and $A = B + B$. We show $\sigma(A) \ge 1/75$, then conclude with Mann's theorem as in the $241$ entry. Write $L = \log y$ for the scale.

1. Chebyshev constant $\log 2$. Mathlib's $\psi(x) \ge (x-1)\log 2 - \log(x+2)$ gives $\pi(x) \ge (x \log 2 - O(\log x))/\log x$, better than the constant $2/3$ used in earlier entries. On its own it covers $L \lesssim 90$ through $B \subseteq A$.
2. Small-shift range (Riesel–Vaughan 1983, Lemma 8). Fix the first $500$ odd primes $p_1$ (up to $3581$) and let $R(s)$ count $s = p_1 + q$ with $q$ prime. Then $\sum_s R(s)$ needs only $\pi$, and $\sum_s R(s)^2$ needs an upper bound for prime pairs $q, q + d$ with a fixed even shift $d$. That bound is the Selberg sieve for $a(a+d)$ on an interval, whose local data are those of the existing Goldbach sieve with $s := d$. The weight sum $\sum_{p_1 \ne p_2} C(p_1 - p_2)$ over these primes is a finite computation. Cauchy–Schwarz then gives $\#\{s \le y : R(s) > 0\} \ge y/150$ for $90 \lesssim L \le 10^4$.
3. Large range $L \ge 10^4$: the Selberg pointwise bound $r(s) \le b\,C(s)\,s/\log^2 s$, the weighted first moment (now with constant $(\log 2)^2$), a high moment of $C(s)$, and Hölder, as in the $241$ entry, at a much higher threshold.
4. Mann's theorem turns $75\,\sigma(A) \ge 1$ into $75A = \mathbb{Z}_{\ge 0}$, so every odd $n$ beyond a small bound is a sum of $150$ odd primes plus one $3$, and small $n$ are handled with twos and threes: $K = 2 \cdot 75 + 1 = 151$.

Significance

The argument stays elementary: no prime number theorem and no zeros of $\zeta$ or $L$-functions. New reusable components:

1. Explicit Selberg upper bound for prime pairs $(q, q+d)$ with a fixed shift, uniform in $d$.
2. The Riesel–Vaughan small-shift second-moment argument.
3. Chebyshev's $\log 2$ constant from Mathlib carried into the sieve moments.

Formalization scope

The Lean statement is the campaign template verbatim with $151$ in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev bounds (Chebyshev.psi_ge', Chebyshev.theta_le_log4_mul_x) and the Λ² sieve framework (Mathlib.NumberTheory.SelbergSieve).

Selected references

• H. Riesel, R. C. Vaughan, On sums of primes, Ark. Mat. 21 (1983), 45–74.
• P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
• Explicit improvement of the $241$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $151$; not peer reviewed.

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
• Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$, came from Schnirelmann's method with every constant written out. This entry records a sharper value, $241$, from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 241,\ \textstyle\sum s = n.$$

This is the campaign template with the value $241$ filled in. The argument proves the stronger statement that every odd $n \ge 483$ is a sum of exactly $241$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It follows the companion $351$ entry, with every parameter pushed to the limit of the same tools. Let $B = \{(p-3)/2 : p \text{ odd prime}\}$ and $A = B + B$. We show $\sigma(A) \ge 1/120$:

1. Sieve at a low threshold. The explicit Selberg inequality with $z = \sqrt{s}/(\log s)^2$ gives $r(s) \le \tfrac{45}{4}\,C(s)\,s/(\log s)^2$ for even $s \ge e^{130}$, where $r(s)$ counts representations $s = p + q$ by odd primes and $C(s) = \prod_{p \mid s}\bigl(1 + p/(p-1)^2\bigr)$.
2. Weighted first moment. $\sum_{e^{130} < s \le x} r(s)\,(\log s)^2/s \ge 0.439\,x$ for $x \ge e^{159}$.
3. Sixteenth moment of $C$. Expanding $C(s)^{16}$ over squarefree divisors, treating the primes up to $31$ exactly and bounding the tail in one step, gives $\sum_{s \le x,\, 2 \mid s} C(s)^{16} \le 9.44 \cdot 10^{12}\, x$.
4. Hölder with exponent $16$ then gives $\#\{s \le x : r(s) > 0\} \ge x/238$ for $x \ge e^{159}$. Below that scale, Chebyshev's bound $\pi(y) - 1 \ge 2y/(3 \log y)$ and $B \subseteq A$ suffice, so $\sigma(A) \ge 1/120$ at every scale.
5. Mann's theorem, $\sigma(D + E) \ge \min\{1, \sigma(D) + \sigma(E)\}$ for sets containing $0$, gives $120A = \mathbb{Z}_{\ge 0}$, so $240B = \mathbb{Z}_{\ge 0}$. For odd $n \ge 3K = 723$, write $(n - 3K)/2$ as a sum of $240$ elements of $B$ and add one more $3$. For $483 \le n < 723$, use $n - 2K$ threes and $3K - n$ twos. This gives $K = 241$.

About $241$ is the floor of this method: the medium range relies on the Chebyshev constant $2/3$, which forces the sieve threshold below $e^{4k/3}$ and so inflates the sieve coefficient.

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$, but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization. Reusable components:

1. Explicit Chebyshev-type lower bound for $\pi(y)$.
2. Explicit Selberg upper-bound sieve for $r(s)$ at an arbitrary threshold.
3. High moments $\sum_{s \le x} C(s)^{q}$ of the singular-series factor.
4. Mann's theorem ($\alpha\beta$ theorem) on Schnirelmann density.

Formalization scope

The Lean statement is the campaign template verbatim with $241$ in place of the value. All the ingredients above except the moment bound and the final assembly are already proved on the platform (Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density).

Selected references

• P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
• Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026), extending the $351$ entry. Source of the constant $241$; not peer reviewed.

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
• Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$, came from Schnirelmann's method with every constant written out. This entry records a sharper value, $6101$, from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 6101,\ \textstyle\sum s = n.$$

This is the campaign template with the value $6101$ filled in. The source proves the stronger statement that every odd $n \ge 12\,203$ is a sum of exactly $6101$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It keeps the explicit Selberg sieve, Cauchy–Schwarz and Schnirelmann's original sumset inequality from the $100\,001$ entry, and improves the first moment:

1. Whole-triangle count. Counting all pairs with $p + q \le x$ gives $\sum_{s \le x} r(s) \ge 2(x-2000)^2/(9(\log x)^2)$ for $x \ge 2000$.
2. Weighting. Weighting $r(s)$ by $(\log s)^2/s$ cancels the varying factor in the sieve bound $r(s) \le 9\,C(s)\,s/(\log s)^2$, giving a weighted first moment of at least $\tfrac{44}{100}x$.
3. Second moment of $C$. With $\sum_{s \le x,\, 2\mid s} C(s)^2 \le \tfrac{21}{2}x$, Cauchy–Schwarz yields $\sigma(A) \ge 1/2200$ for $A = B + B$, $B = \{(p-3)/2\}$.
4. Schnirelmann's inequality with $m = 1525$ (the least $m$ with $(1 - 1/2200)^m < 1/2$) gives $K = 4m + 1 = 6101$.

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$, but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from $100\,001$. Reusable components:

1. Explicit Chebyshev-type lower bound for $\pi(y)$.
2. Explicit Selberg upper-bound sieve for $r(s)$.
3. Moment bounds for the singular-series factor $C(s)$.
4. Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$.

Formalization scope

The Lean statement is the campaign template verbatim with $6101$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

• P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
• Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $6101$; not peer reviewed.

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
• Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$, came from Schnirelmann's method with every constant written out. This entry records a sharper value, $97\,041$, from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 97\,041,\ \textstyle\sum s = n.$$

This is the campaign template with the value $97\,041$ filled in. The source proves the stronger statement that every odd $n \ge 194\,083$ is a sum of exactly $97\,041$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It is the argument behind the $100\,001$ entry, unchanged up to the last step: the explicit Selberg sieve and Cauchy–Schwarz give $\sigma(A) \ge 1/35\,000$ for $A = B + B$, $B = \{(p-3)/2 : p \text{ odd prime}\}$. The only change is to take the smallest admissible $m$ in Schnirelmann's inequality: $(1 - 1/35\,000)^{m} < 1/2$ first holds at $m = 24\,260$ (rather than the rounded $25\,000$), so $2mA = \mathbb{Z}_{\ge 0}$ and $K = 4m + 1 = 97\,041$.

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$, but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from $100\,001$. Reusable components:

1. Explicit Chebyshev-type lower bound for $\pi(y)$.
2. Explicit Selberg upper-bound sieve for $r(s)$.
3. Moment bounds for the singular-series factor $C(s)$.
4. Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$.

Formalization scope

The Lean statement is the campaign template verbatim with $97\,041$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

• P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
• Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $97\,041$; not peer reviewed.

Motivation

Goldbach's problem asks whether every integer greater than $1$ can be written as a sum of a small number of primes. The first unconditional result of this kind was obtained by Schnirelmann around 1930: there is an absolute constant $k$ such that every integer $n > 1$ is a sum of at most $k$ primes. His argument is elementary. It uses an upper-bound sieve and Chebyshev-type prime estimates, together with a notion of additive density, and it does not need the prime number theorem or complex analysis.

The constant has since been reduced by much deeper methods. A short timeline for odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Vinogradov (1937): every sufficiently large odd integer is a sum of three primes, with an ineffective threshold in the original argument.
• Ramaré (1995): every even integer is a sum of at most six primes, which gives at most seven primes for every odd $n > 1$. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): every odd $n > 1$ is a sum of at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes (the ternary Goldbach conjecture). (arXiv:1312.7748)

This mission targets a much weaker constant than any of these, $k = 100\,001$. It does so because the constant comes from Schnirelmann's elementary method with every estimate made explicit, and that proof is short enough to be a realistic target for a complete formalization.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset $s$ of natural numbers such that every element of $s$ is prime, the elements of $s$ sum to $n$, and $s$ has at most $k$ elements counted with multiplicity. Repetitions are allowed and order is irrelevant.

The number $1$ is not a sum of primes, so the question concerns odd $n \ge 3$. Even numbers are excluded from the campaign statement.

The Schnirelmann density of a set $A \subseteq \mathbb{Z}_{\ge 0}$ is

$$\sigma(A) = \inf_{N \ge 1} \frac{|A \cap \{1, \dots, N\}|}{N}.$$

This notion is the additive tool behind the elementary approach. Mathlib provides it as schnirelmannDensity.

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 100\,001,\ \textstyle\sum s = n.$$

This is the campaign template of Odd numbers as sums of primes with the value $100\,001$ filled in. A stronger explicit form in the source is that every odd $n \ge 200\,003$ is a sum of exactly $100\,001$ primes; the at-most form for all odd $n > 1$ follows from it immediately.

Significance

The result itself. The bound $100\,001$ is far from the best known constants; five (Tao) and three (Helfgott) are both known on paper. Its value is that it rests on an elementary argument with every constant written out. There is no "sufficiently large" threshold and no appeal to the prime number theorem, zero-density estimates, or large-scale computation.

Formalizing it. No finite bound in this problem has a machine-checked proof on this platform yet. A proof of this goal would be the campaign's first proved value. The components are reusable beyond this mission:

1. Explicit Chebyshev-type bounds for $\pi(y)$.
2. An explicit Selberg upper-bound sieve for the number of representations of an even number as a sum of two odd primes.
3. An averaged bound for the associated singular-series factor.
4. Schnirelmann's density inequality $\sigma(D + E) \ge \sigma(D) + \sigma(E) - \sigma(D)\sigma(E)$.

Difficulty

The only substantial step is an upper bound for

$$r(s) = \#\{(p, q) : p, q \text{ odd primes},\ p + q = s\}$$

that is sharp up to a constant factor, namely of order $s/(\log s)^2$ times an arithmetic factor depending on the prime divisors of $s$, with an explicit constant. The trivial bound $r(s) \le \pi(s)$ is weaker by a factor of $\log s$. That loss makes the density of sums of two primes appear to be zero, so the additive argument cannot start. Everything after the sieve bound is short and explicit.

Formalization scope

The Lean statement is the campaign template verbatim with $100\,001$ in place of the value. It uses Multiset ℕ, Nat.Prime, and Odd n ∧ 1 < n. The statement is fixed by the campaign, and it has no vacuous hypotheses: every odd $n > 1$ is covered.

Mathlib already contains schnirelmannDensity and the fact that $\sigma(A) + \sigma(B) \ge 1$ with $0 \in A \cap B$ implies $A + B = \mathbb{N}$. It also contains the Λ² setup of the Selberg sieve (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial-coefficient bounds. Missing, and welcome as contributions:

1. The explicit sieve bound for $r(s)$.
2. The mean-square bound for the arithmetic factor.
3. Schnirelmann's inequality for $\sigma(D + E)$.
4. The explicit lower bound for $\pi(y)$ in the form needed here.

Selected references

• P. Pollack, Not Always Buried Deep: A Second Course in Elementary Number Theory, AMS, 2009. Chapter 6, §6, "An application to the Goldbach problem", pp. 196–201. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa Cl. Sci. (4) 22 (1995), 645–706. http://www.numdam.org/item/ASNSP_1995_4_22_4_645_0/
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014), 997–1038. https://arxiv.org/abs/1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
• An explicit elementary constant for sums of primes, unpublished note, September 2026, Theorem 1. Source of the constant $100\,001$ (with $c_1 = 1/9$, $c_2 = 860$, $x_0 = e^{2000}$, $\sigma(A) \ge 1/35\,000$, $m = 25\,000$).

Motivation

The representation function $r_{2}(n)=\#\{(a,b)\in\mathbb Z^{2}:a^{2}+b^{2}=n\}$ is one of the oldest objects in number theory. Fermat characterised the integers with $r_{2}(n)>0$ — those in which every prime congruent to $3$ modulo $4$ occurs to an even power — and Euler's proof supplied the closed form $r_{2}(n)=4\,(d_{1}(n)-d_{3}(n))$, where $d_{j}(n)$ counts divisors congruent to $j$ modulo $4$ (sum of two squares theorem).

That description counts representations but does not relate them to one another. The integers carrying several essentially different representations,

$$50=1^{2}+7^{2}=5^{2}+5^{2},\qquad 65=1^{2}+8^{2}=4^{2}+7^{2},$$

are exactly the integers that produce quadruples $(a,b,c,d)$ with

$$a^{2}+b^{2}=c^{2}+d^{2}$$

whose two sides are not identified by swapping the two entries or changing their signs. Three reasons make this relation worth a formal development rather than a passing remark.

• Energy counts. Counting solutions of the equation inside a box is the additive energy of the set of sums of two squares, the quantity controlling mean-square errors for $r_{2}$; it is a genuinely different problem from determining $r_{2}(n)$ for a single $n$, and every estimate for it starts from a description of the solution set.
• Composition of representations. The Brahmagupta–Fibonacci identity

$$(p^{2}+q^{2})(r^{2}+s^{2})=(pr+qs)^{2}+(ps-qr)^{2}=(pr-qs)^{2}+(ps+qr)^{2}$$

takes two representations and produces a third. Known to Brahmagupta and stated by Fibonacci in Liber Quadratorum (1225), it is the multiplicativity of the norm in the Gaussian integers, and it is the engine behind every statement below.

• Geometry. Over a field, the locus $a^{2}+b^{2}=c^{2}+d^{2}$ in projective three-space is the split quadric, isomorphic to $\mathbb P^{1}\times\mathbb P^{1}$ under the Segre embedding; the four parameters introduced below are Segre coordinates in this sense. The arithmetic content of the equation is precisely the integrality that this geometry ignores.

The parametrisation targeted here is classical. Nothing in this mission claims new mathematics; the aim is a machine-checked development in which every hypothesis is explicit.

Setting

Fix integers. A solution is a quadruple $(a,b,c,d)\in\mathbb Z^{4}$ with $a^{2}+b^{2}=c^{2}+d^{2}$. It is trivial if the multisets $\{a^{2},b^{2}\}$ and $\{c^{2},d^{2}\}$ coincide, i.e. if $(c,d)$ equals $\pm(a,b)$ or $\pm(b,a)$; if entries are allowed to vanish, the least value carried by a non-trivial solution is $25=0^{2}+5^{2}=3^{2}+4^{2}$, and requiring all four entries to be positive raises that value to $50$. A solution is primitive when the four entries have greatest common divisor $1$, and positive when all four entries are positive and pairwise distinct — the case in which nothing about the relation is explained by signs, zeros or coincidences.

Two constructions produce solutions. The four-parameter family associates to integers $p,q,r,s$ the quadruple

$$a=pr+qs,\qquad b=ps-qr,\qquad c=pr-qs,\qquad d=ps+qr,$$

which solves the equation because both sides equal $(p^{2}+q^{2})(r^{2}+s^{2})$ by the identity above. Substituting particular parameters is unrevealing, so a genuine supply comes instead from the elementary one-parameter family

$$1^{2}+(n^{2}-n+1)^{2}=(2n-1)^{2}+(n^{2}-n-1)^{2},$$

whose four entries $1$, $n^{2}-n+1$, $2n-1$, $n^{2}-n-1$ are strictly increasing — hence positive and pairwise distinct — as soon as $n\ge 4$. The bound is sharp: at $n=3$ the two entries $2n-1$ and $n^{2}-n-1$ are equal.

In the reverse direction, rewrite the equation as $(a+c)(a-c)=(d+b)(d-b)$ and set

$$X=(a+c)/2,\quad Y=(a-c)/2,\qquad U=(b+d)/2,\quad V=(d-b)/2 .$$

The halves are integers exactly when $a$ and $c$ share a parity and so do $b$ and $d$, and in that case the equation becomes

$$XY=UV .$$

The development is organised in the namespace TwoSquares, with node names matching the roles above (four_param_identity, explicit_family_chain, sum_sq_eq_halves, four_factor_param, complete_parametrization).

Formalization targets

Goal — completeness of the four-parameter family

For all integers $a,b,c,d$ with $a^{2}+b^{2}=c^{2}+d^{2}$, there are integers $p,q,r,s$ with

$$a=pr+qs,\quad b=ps-qr,\quad c=pr-qs,\quad d=ps+qr,$$

possibly after interchanging $c$ and $d$. The goal asserts only the existence of integral parameters and the necessity of at most one swap; it does not assert uniqueness of $(p,q,r,s)$, which is false, and it says nothing about how many solutions lie in a given box.

The four-parameter identity

The identity itself, over an arbitrary commutative ring, together with the two forms of the Brahmagupta–Fibonacci identity that imply it — so that the reason it holds, rather than the expansion, is what is recorded.

An explicit infinite family

For every integer $n\ge 4$ the displayed family is a positive pairwise distinct solution; the parametrisation $n\mapsto(1,\,n^{2}-n+1,\,2n-1,\,n^{2}-n-1)$ is injective; the set of quadruples it produces is infinite; and no member is a nontrivial integer multiple of another, each member being primitive.

From the sum-of-squares equation to $XY=UV$

The equivalence of $a^{2}+b^{2}=c^{2}+d^{2}$ with $(a+c)(a-c)=(d+b)(d-b)$; the parity statement that matching entries share a parity after at most one swap; and the resulting existence of the half-sum variables satisfying $XY=UV$.

Parametrizing $XY=UV$

For all integers $X,Y,U,V$ with $XY=UV$ there are integers $p,q,r,s$ with $X=pr$, $Y=qs$, $U=ps$, $V=qr$ — the coordinate form of the statement that a rank-one $2\times2$ matrix factors through the integers.

Significance

The result. Taken together, the reverse chain converts the Diophantine equation $a^{2}+b^{2}=c^{2}+d^{2}$ into four free integer parameters, at the cost of one possible swap. In that form every question about the solution set becomes a question about four independent variables, which is what makes energy estimates, density statements and searches for primitive solutions tractable. The chain also isolates where integrality enters: over a field the parametrisation of $XY=UV$ is formal, so the content is carried entirely by the parity step and by divisibility over $\mathbb Z$.

Formalizing it. None of the mathematics is new, and that is the point: the value here is a development in which each link is a reusable statement with explicit hypotheses. Three conventions make the nodes reusable rather than bespoke. The algebraic identity is proved over a general commutative ring, not over $\mathbb Z$. The positivity and distinctness of a family are packaged as one strict chain rather than as a list of inequalities, since later arguments use the ordering, not merely the disequalities. The parity issue is isolated into a single node stating a disjunction, instead of being discharged by case splits buried inside a later proof. Conversely, the shape of the final theorem records honestly what is not claimed: parameters are not unique, and no normal form is asserted.

As difficulty, the early nodes have short proofs, while completeness requires the full chain and is the substantial part of the mission.

Difficulty

The obvious first idea is to use the Gaussian integers: $a+bi$ and $c+di$ have the same norm, so factor both and compare. It fails. Equal norm does not make two Gaussian integers associates or divisors of one another — $1+8i$ and $4+7i$ both have norm $65$ and are related by no divisibility — because uniqueness of factorisation regroups prime factors in ways that the norm alone cannot distinguish. The correct route recovers the four parameters from the product equation instead, and there the friction is entirely arithmetic:

Clearing halves. The substitution $X=(a+c)/2$ is not available for arbitrary solutions: $a^{2}+b^{2}=c^{2}+d^{2}$ forces only that the multiset of parities of $(a,b)$ matches that of $(c,d)$, so $(a,c)$ may have different parities and no integer $X$ may exist. The example $a=1,b=0,c=0,d=1$ shows this is not vacuous, and it is why the goal carries a swap.

Factoring $XY=UV$. Taking $p=\gcd(X,U)$ yields $X=pr$, $U=ps$ with $\gcd(r,s)=1$, and Euclid's lemma then forces $s\mid Y$ and $r\mid V$. The degenerate case $X=U=0$ — where the gcd vanishes and no cancellation is possible — must be handled separately, and because the variables range over $\mathbb Z$ rather than $\mathbb N$, every divisibility step must be tracked with signs. Working over a ring where division is available would delete both issues and with them the entire content of the statement.

Formalization scope

• All nodes are stated over $\mathbb Z$, except the Brahmagupta–Fibonacci identity and the four-parameter identity, which are proved over an arbitrary commutative ring. No node is stated over $\mathbb N$; transporting the prime-level statements is out of scope.
• Gaussian integers are deliberately unused. Mathlib carries them, but nothing here needs them, and a development depending on them would obscure the arithmetic that actually carries the proof.
• No quotient types, no permutation machinery: the possible swap of $c$ and $d$ is expressed as a disjunction, and the parity statement as a disjunction over Even.
• Trivializing formalizations are excluded. Over a field the parametrisation of $XY=UV$ holds trivially (take $p=X$, $r=1$, $s=U/X$), so the quarter-ring version carries no information; likewise, a completeness statement whose hypotheses already postulate the existence of the parameters would be vacuous. Both are explicitly not what is asked for.
• Expected to be reusable beyond this mission: the two forms of the Brahmagupta–Fibonacci identity; the strict-chain packaging of positivity and distinctness for a family given by polynomials; and the integer parametrisation of $XY=UV$, which is the Segre parametrization.
• Contributions are welcome for any node, and especially for the integer factoring lemma, for which several proofs are available. Explicitly out of scope: uniqueness or normal forms for $(p,q,r,s)$, counting asymptotics for solutions in a box, the Gaussian-integer reformulation, and all $\mathbb N$-level variants.

Selected references

• Sum of two squares theorem — Fermat's characterisation and Euler's divisor formula for $r_{2}$.
• Brahmagupta–Fibonacci identity — the two-square composition identity, its history, and its interpretation through norms.
• Leonardo Pisano (Fibonacci), Liber Quadratorum, 1225. English translation: L. E. Sigler, The Book of Squares, Academic Press, 1987.
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008 — Chapter XX on representations by two squares.
• Segre embedding — the identification of the rank-one quadric in $\mathbb P^{3}$ with $\mathbb P^{1}\times\mathbb P^{1}$.