Number Theory

Motivation

The Langlands program proposes that the arithmetic of number fields is encoded in the representation theory of reductive groups over their adele rings. Its conjectures — reciprocity and functoriality — are stated in the survey this mission formalizes, Gelbart 1984, only after a long preparatory part on the classical results they generalize, and it is that classical part (Part II of the survey) that admits precise formal statements today.

The classical engine is a theorem of Hecke (1936): a holomorphic function on the upper half-plane, given by a Fourier expansion in $e^{2\pi i n z/h}$, transforms in a prescribed way under $z \mapsto -1/z$ exactly when the Dirichlet series built from its Fourier coefficients continues analytically and satisfies a functional equation. One side of the equivalence is a symmetry of an analytic object on the upper half-plane; the other is an analytic property of a series assembled from arithmetic data. Gelbart presents this as the prototype of the "reciprocity" that the Langlands conjectures extend to $GL_n$ and beyond.

Timeline of the material covered here.

• 1859: Riemann derives the functional equation of $\zeta(s)$ from the transformation law of the Jacobi theta function, via the Mellin transform (Gelbart, §II.B.2, p. 187).
• 1920s: Hasse and Minkowski establish the local-global principle for rational quadratic forms (Gelbart, §II.A, p. 186).
• 1936: Hecke proves the equivalence that is this mission's goal, and characterizes Euler products among Dirichlet series of automorphic forms (Gelbart, §II.B.2, Theorems 1 and 2).
• 1967: Weil extends Hecke's theorem to congruence subgroups; Langlands formulates functoriality.

Setting

Fix a sequence of complex numbers $a_0, a_1, a_2, \dots$ subject to the growth condition $a_n = O(n^c)$ for some $c > 0$, a period $h > 0$, a weight $k > 0$, and a sign $C = \pm 1$. Three objects are attached to this data.

• The form: $\displaystyle f(z) = \sum_{n \ge 0} a_n e^{2\pi i n z/h}$, holomorphic on the upper half-plane $\{z : \operatorname{Im} z > 0\}$.
• The Dirichlet series: $\displaystyle \varphi(s) = \sum_{n \ge 1} \frac{a_n}{n^s}$, absolutely convergent for $\operatorname{Re} s > c+1$.
• The completed series: $\displaystyle \Phi(s) = \left(\frac{2\pi}{h}\right)^{-s} \Gamma(s)\, \varphi(s)$.

Two conditions on this data are compared.

$$\textbf{(A)}\quad \Phi(s) + \frac{a_0}{s} + \frac{C a_0}{k-s} \ \text{extends to an entire function, bounded in every vertical strip, and}\ \Phi(k-s) = C\,\Phi(s).$$ $$\textbf{(B)}\quad f(-1/z) = C\left(\frac{z}{i}\right)^{k} f(z) \qquad (\operatorname{Im} z > 0).$$

Condition (B) says that $f$ is automorphic of weight $k$ for the group of transformations generated by $z \mapsto z + h$ and $z \mapsto -1/z$; invariance under $z \mapsto z+h$ is built into the Fourier expansion.

Formalization targets

Goal — Theorem 1 (Hecke), p. 188

$$\textbf{(A)} \iff \textbf{(B)}$$

for every coefficient sequence of polynomial growth and all $h, k > 0$, $C = \pm 1$. The goal fixes no particular group, no level and no arithmetic input: it is the general equivalence, from which the classical examples follow by specialization.

Milestones

The milestone list follows the survey: the local-global principle of §II.A, the Riemann–theta computation that motivates Hecke's proof (§II.B.2, p. 187), the Mellin representation of $\Phi$, the two implications of Theorem 1 separately, and the Euler-product criterion of Theorem 2 (p. 189).

Significance

Hecke's theorem is what makes "this $L$-function is automorphic" a checkable assertion: it converts a statement about analytic continuation and a functional equation — often the only handle one has on an arithmetically defined Dirichlet series — into the existence of an automorphic form with prescribed Fourier coefficients. Weil's converse theorem, the modularity of elliptic curves, and the automorphy criteria used throughout the Langlands program are descendants of this statement. Downstream of it sit the classical applications listed in the survey: the functional equations of $\zeta$ and of Dirichlet $L$-functions, and the identification of theta series of quadratic forms with modular forms.

Status. Hecke's theorem is a classical, fully proved result (Hecke 1936; a textbook treatment is Ogg, Modular forms and Dirichlet series, Ch. 1). Hasse–Minkowski is likewise classical. Neither has a formalization in Mathlib at the pinned revision: Mathlib supplies the completed Riemann zeta function and its functional equation, the Jacobi theta transformation law, LSeries and its abscissa theory, the Gamma function and the Mellin transform, and modular forms with SlashAction, but no converse theorem and no local-global principle for quadratic forms. What this mission produces is therefore new formal mathematics on top of an old result, not a re-derivation of something already machine-checked.

Difficulty

The forward implication (B) $\Rightarrow$ (A) is Riemann's argument: split $\int_0^\infty (f(iy) - a_0) y^{s-1}\,dy$ at $y = 1$, substitute $y \mapsto 1/y$ in the lower piece, and use (B). The obstacle is not the algebra but the analysis that licenses it: exchanging the sum defining $f$ with the integral, controlling $f(iy) - a_0$ as $y \to 0^{+}$, where the naive termwise bound diverges, and showing the result is entire and bounded on vertical strips rather than merely holomorphic on a half-plane.

The reverse implication (A) $\Rightarrow$ (B) is harder, and it is where the first idea fails: one cannot simply run the computation backwards, because the Mellin inversion integral $\frac{1}{2\pi i}\int_{(\sigma)} \Phi(s) y^{-s}\,ds$ converges only once boundedness in vertical strips is combined with Stirling decay of $\Gamma$, and the contour shift that produces the $a_0$ terms needs both. Mathlib has the Mellin transform and an inversion theorem, under hypotheses that are not met verbatim here; supplying that bridge is the main work.

Formalization scope

Conventions committed to in Lean, all of them invisible in the prose.

• $f$ is defined as an unconditional tsum over $n \ge 0$, so it takes the junk value $0$ where the series fails to converge; every statement about $f$ is guarded by $\operatorname{Im} z > 0$, and a separate item asserts summability there.
• $\varphi$ is Mathlib's LSeries, whose $n = 0$ term is $0$ by definition, so $a_0$ never enters the Dirichlet series — only the correction terms $a_0/s$ and $C a_0/(k-s)$.
• "Entire" is rendered as differentiability on all of $\mathbb{C}$; "bounded in every vertical strip" as: for all reals $\sigma_1, \sigma_2$ there is an $M$ bounding the function on $\sigma_1 \le \operatorname{Re} s \le \sigma_2$.
• The functional equation is imposed on the continued function $F$ as $F(k-s) = C\,F(s)$; for $C = \pm 1$ this is equivalent to $\Phi(k-s) = C\,\Phi(s)$ on the half-plane of convergence.
• Complex powers $(2\pi/h)^{-s}$, $(z/i)^{k}$ and $y^{s-1}$ are principal-branch cpow; on the upper half-plane $z/i$ has positive real part, so no branch ambiguity arises.
• The growth hypothesis is $\lVert a_n \rVert \le K n^{c}$ for $n \ge 1$ with $c > 0$, and the abscissa used throughout is $\sigma = c+1$.
• The printed source reads $\Phi(s) + a_0/s + C/(k-s)$; the term $C a_0/(k-s)$ used here is the standard form of the correction (see Ogg, Ch. 1), and the two agree when $a_0 = 0$.

No trivializing reading is available: condition (A) requires the entire function to agree with $\Phi(s) + a_0/s + C a_0/(k-s)$ on $\operatorname{Re} s > c+1$, where $\Phi$ is genuinely defined, so it is not satisfied by an arbitrary entire function; and the hypotheses of the goal are satisfiable — the Jacobi theta coefficients with $h = 2$, $k = 1/2$, $C = 1$ are an instance, recorded as its own item.

A complete development needs: summability and holomorphy of $q$-expansions of polynomial growth; the Mellin transform of an exponentially decaying series; entirety and strip-boundedness of the continued $\Phi$; Mellin inversion with Stirling control of $\Gamma$; and, for the Euler-product item, the passage from multiplicativity to an Euler product for LSeries. All of these are reusable beyond this mission. Contributions to any single item are welcome; the two implications of the goal are independently valuable and are listed as separate milestones for that reason.

Selected references

• S. Gelbart, An elementary introduction to the Langlands program, Bull. Amer. Math. Soc. (N.S.) 10 (1984), 177–219. https://doi.org/10.1090/S0273-0979-1984-15237-6
• E. Hecke, Über die Bestimmung Dirichletscher Reihen durch ihre Funktionalgleichung, Math. Ann. 112 (1936), 664–699. https://doi.org/10.1007/BF01565437
• A. Ogg, Modular forms and Dirichlet series, W. A. Benjamin, 1969.
• R. P. Langlands, Problems in the theory of automorphic forms, Lectures in Modern Analysis and Applications III, Lecture Notes in Math. 170 (1970), 18–61. https://doi.org/10.1007/BFb0079065
• J.-P. Serre, A course in arithmetic, Springer GTM 7, 1973 (Ch. IV: Hasse–Minkowski).

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

The value $L(1,\chi)$ of a Dirichlet $L$-function at $s=1$ controls class numbers of quadratic fields, the least quadratic non-residue, and the distribution of primes in arithmetic progressions. For a real character $\chi$ modulo $q$ the size of $L(1,\chi)$ is governed by the zeros of $L(s,\chi)$ near $s=1$: a real zero close to $1$ (a Siegel zero) would make $L(1,\chi)$ abnormally small, and no unconditional argument rules this out effectively.

Littlewood's bound (1928) states that under the generalized Riemann hypothesis for $L(s,\chi)$,

$$L(1,\chi)\gg\frac{1}{\log\log q},$$

which is optimal up to the constant. Explicit constants under GRH were given by Lamzouri, Li and Soundararajan (2015).

The mission The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s) > 7/8 formalizes a preprint (OpenAI, 30 September 2026) claiming that every Dirichlet $L$-function is zero-free in $\Re s>7/8$. That claim is not yet verified. This mission asks what a zero-free half-plane would give: an explicit Littlewood-type lower bound for $L(1,\chi)$ under the hypothesis $\Re s>7/8\Rightarrow L(s,\chi)\neq0$ for the single character concerned.

Timeline.

• 1928. Littlewood proves $L(1,\chi)\gg1/\log\log q$ under GRH.
• 1959. Rademacher gives explicit Phragmén–Lindelöf convexity bounds for Dirichlet $L$-functions.
• 2003. Granville and Soundararajan describe the distribution of $L(1,\chi_d)$.
• 2004. Ji and Lu give an explicit lower bound $L(1,\chi)>1/(7.7388\log q)$ when no real zero lies in a narrow interval below $1$.
• 2010. Dusart publishes explicit estimates for sums over primes, including $\sum_{p\le x}1/p$.
• 2015. Lamzouri, Li and Soundararajan give explicit Littlewood constants under GRH.
• 2026. The 7/8 preprint appears, and Daugherty, Ryan and Ward prove explicit Littlewood bounds under a zero-free half-plane $\Re s>a$ for one character.

Setting

A Dirichlet character $\chi$ modulo $q\ge1$ is a multiplicative function $\mathbb Z/q\mathbb Z\to\mathbb C$ that vanishes off the units. It is primitive if its conductor equals $q$, and real if all its values are real (they then lie in $\{-1,0,1\}$). Its $L$-function is

$$L(s,\chi)=\sum_{n\ge1}\chi(n)\,n^{-s}\qquad(\Re s>1),$$

continued meromorphically to $\mathbb C$, with a pole only for the trivial character. For a primitive character modulo $q\ge3$ the continuation is entire and $L(1,\chi)\neq0$.

The hypothesis used throughout is

$$H_{7/8}(\chi):\qquad L(s,\chi)\neq0\quad\text{for all } s \text{ with } \Re s>7/8.$$

It concerns one character, not a family, and the half-plane is open. For primitive $\chi$, GRH for $L(s,\chi)$ implies $H_{7/8}(\chi)$.

Formalization targets

Goal: a Littlewood lower bound under $H_{7/8}$

There are constants $c>0$ and $q_0$ such that for every primitive real character $\chi$ modulo $q\ge q_0$ satisfying $H_{7/8}(\chi)$,

$$L(1,\chi)\ \ge\ \frac{c}{\log\log q}.$$

Milestone: explicit constant

For $q\ge10^{100}$ the constant $c=0.0617$ is admissible:

$$H_{7/8}(\chi)\ \Longrightarrow\ L(1,\chi)\ \ge\ \frac{0.0617}{\log\log q}.$$

Milestone: explicit two-sided bound

For the same $\chi$ and $q\ge10^{100}$,

$$|\log L(1,\chi)|\ \le\ \log\log\log q+3.2914 .$$

Milestone: Dusart's bound for $\sum 1/p$

With $B=\gamma+\sum_p\big(\log(1-1/p)+1/p\big)$ (Mertens' constant), for every real $x\ge10372$,

$$\sum_{p\le x}\frac1p-\log\log x-B\ \le\ \frac{1}{10\log^2x}+\frac{4}{15\log^3x}.$$

Milestone: Rademacher's convexity bound

For every primitive character $\chi$ modulo $q\ge3$ and every $s$ with $-\tfrac12\le\Re s\le\tfrac32$,

$$|L(s,\chi)|\ \le\ \zeta(\tfrac32)\left(\frac{q\,|1+s|}{2\pi}\right)^{(3/2-\Re s)/2}.$$

Significance

The result. A zero-free half-plane at a fixed distance from $\Re s=1$ makes the Littlewood bound effective with explicit constants. Through the class number formula it gives explicit lower bounds for class numbers of quadratic fields of large discriminant, and it excludes Siegel zeros for the character concerned. The hypothesis is weaker than GRH, and, if the 7/8 preprint is correct, it holds for every primitive character. In that case the goal and the explicit milestones become unconditional explicit theorems.

Formalizing it. The explicit bounds are proved in the preprint by Daugherty, Ryan and Ward (doi:10.5281/zenodo.23400116, Theorem 2), with constants certified in interval arithmetic. None of the statements here has a machine-checked proof. A formalization would give an independently checked conditional result that composes directly with a Lean proof of the zero-free half-plane. It would also add explicit analytic number theory to Mathlib: the convexity bound, explicit prime-sum estimates, and logarithms of $L$-functions on zero-free regions.

Difficulty

The classical proof of Littlewood's bound under GRH uses the zeros' location on the critical line to bound $\log L(s,\chi)$ just to the left of $s=1$. Under the weaker hypothesis $H_{7/8}$ only a fixed strip next to $\Re s=1$ is zero-free, and $\log L$ grows like $\log q$ there. The control must be strong enough that an exponentially smoothed prime sum of length $(\log q)^{\nu}$ dominates, with every constant explicit and uniform in $q$. The prime sums in turn need explicit, not asymptotic, estimates for $\sum_{p\le x}1/p$.

Formalization scope

The $L$-function is Mathlib's DirichletCharacter.LFunction, primitivity is DirichletCharacter.IsPrimitive, and "real" is stated as $\operatorname{Im}\chi(a)=0$ for every $a\in\mathbb Z/q\mathbb Z$. The value $L(1,\chi)$ is compared through its real part, and the two-sided milestone uses the principal complex logarithm. Mertens' constant is written out as $\gamma+\sum_p(\log(1-1/p)+1/p)$ with Mathlib's tsum over primes. The hypothesis $H_{7/8}(\chi)$ is a hypothesis on the single character in each statement, never a family-wide assumption. It is satisfiable, for example under GRH, so the conditional statements are not vacuous.

A complete development needs:

• holomorphic logarithms of $L(s,\chi)$ on zero-free half-planes;
• Mellin inversion for $e^{-y}$;
• an explicit Phragmén–Lindelöf convexity bound;
• explicit estimates for sums over primes;
• rational certificates for the numerical constants.

The convexity bound and the prime-sum estimates are reusable well beyond this mission. Contributions toward any of these are welcome.

Selected references

• J. E. Littlewood, On the class-number of the corpus $P(\sqrt{-k})$, Proc. London Math. Soc. (2) 27 (1928), 358–372.
• H. Rademacher, On the Phragmén–Lindelöf theorem and some applications, Math. Z. 72 (1959/60), 192–204.
• A. Granville and K. Soundararajan, The distribution of values of $L(1,\chi_d)$, Geom. Funct. Anal. 13 (2003), 992–1028.
• C.-G. Ji and H.-W. Lu, Lower bound of real primitive $L$-function at $s=1$, Acta Arith. 111 (2004), 405–409. https://doi.org/10.4064/aa111-4-2
• P. Dusart, Estimates of some functions over primes without R.H., preprint (2010), Theorem 6.10. https://arxiv.org/abs/1002.0442
• Y. Lamzouri, X. Li and K. Soundararajan, Conditional bounds for the least quadratic non-residue and related problems, Math. Comp. 84 (2015), 2391–2412; corrigendum, Math. Comp. 86 (2017), 2551–2554. https://arxiv.org/abs/1309.3595
• OpenAI, The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane $\Re s>7/8$, preprint, 30 September 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/paper.pdf
• B. W. Daugherty, S. Ryan and G. Ward, Certified harmonic-measure barriers and explicit Littlewood bounds from zero-free regions, preprint (2026). https://doi.org/10.5281/zenodo.23400116