Number Theory

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, $973$, 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 973,\ \textstyle\sum s = n.$$

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

How the bound arises

It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the $100\,001$ entry, and improves the density estimate:

1. Lower sieve threshold. With $z = \sqrt{s}/(\log s)^2$ the sieve gives $r(s) \le 13\,C(s)\,s/(\log s)^2$ for even $s \ge e^{100}$.
2. Weighted first moment of at least $\tfrac{43}{100}x$ for $x \ge e^{200}$.
3. Fourth moment of $C$. An Euler-product estimate gives $\sum_{s \le x,\, 2\mid s} C(s)^4 \le 400\,x$.
4. Hölder then yields $\sigma(A) \ge 1/350$ for $A = B + B$, $B = \{(p-3)/2\}$.
5. Schnirelmann's inequality with $m = 243$ (the least $m$ with $(349/350)^m < 1/2$) gives $K = 4m + 1 = 973$.

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 $973$ 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 $973$; not peer reviewed.

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Chudnovsky's bound.

Formalization target

The campaign template with the value $19.8899945$ filled in: PiIrrationality.UpperBound (19.8899945 : ℝ), i.e. $\mu(\pi) \le 19.8899945$.

Value. The bound is quoted in the literature as $19.8899944\ldots$ (e.g. Hata 1993), a truncation. This entry rounds the last digit up to $19.8899945$ so that the goal follows from the published constant.

How the bound arises

Chudnovsky determined the exact asymptotic behaviour of the Hermite-type contour integrals $\frac{1}{2\pi i}\oint \left(\frac{n!}{z(z-1)\cdots(z-n)}\right)^k e^{wz}\,dz$ behind Mahler's approximations, which sharpens the resulting exponent.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $19.8899945$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• G. V. Chudnovsky, Hermite–Padé approximations to exponential functions and elementary estimates of the measure of irrationality of $\pi$, Lecture Notes in Math. 925, Springer (1982), 299–322.
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Mignotte's bound.

Formalization target

The campaign template with the value $20.6$ filled in: PiIrrationality.UpperBound (20.6 : ℝ), i.e. $\mu(\pi) \le 20.6$.

Value. The paper's abstract states $|\pi - p/q| > q^{-20.6}$ for all $q \ge 2$, which gives $\mu(\pi) \le 20.6$ exactly as stated. The paper also proves $|\pi - p/q| > q^{-20}$ for $q \ge q_0$ (explicit), so $\mu(\pi) \le 20$ follows from the same source; this entry uses the table value $20.6$.

How the bound arises

Mignotte refined Mahler's method of explicit rational approximations to $\pi$ (Hermite's approximation formulae for the exponential and logarithm) and sharpened the estimates that turn their size and denominators into an irrationality measure.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $20.6$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• M. Mignotte, Approximations rationnelles de $\pi$ et quelques autres nombres, Mém. Soc. Math. France 37 (1974), 121–132. https://doi.org/10.24033/msmf.139
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

Motivation

Given a monic polynomial $f$ with integer coefficients, one can reduce it modulo each prime $p$ and factor it over the finite field $\mathbb F_p$. The way $f$ factors changes with $p$, and the question of how often each factorization pattern occurs has a precise answer: Chebotarëv's density theorem (1922). It is the common generalization of Dirichlet's theorem on primes in arithmetic progressions (1837) and a theorem of Frobenius (1880, published 1896), and it underlies a large part of algebraic number theory, for example the fact that a Galois extension of a number field is determined by the set of primes that split completely in it. This mission follows the elementary exposition of P. Stevenhagen and H. W. Lenstra, Jr. (Math. Intelligencer 18 (1996)), which states all three theorems over $\mathbb Q$ with a minimum of terminology.

Timeline.

• 1837 — Dirichlet: primes are equidistributed (in analytic density) over the invertible residue classes modulo $m$.
• 1880/1896 — Frobenius: the density of primes with a given decomposition type of $f$ modulo $p$ equals the proportion of Galois group elements with that cycle pattern; he conjectures the sharper statement for conjugacy classes.
• 1896 — de la Vallée-Poussin: Dirichlet's theorem for natural density.
• 1922/1925 — Chebotarëv proves Frobenius's conjecture, without class field theory.
• 1935 — Deuring's proof via Artin reciprocity, now the textbook route.

Setting

Let $f\in\mathbb Z[X]$ be monic of degree $n$ with nonzero discriminant $\Delta(f)$, so that $f$ has $n$ distinct complex zeros $\alpha_1,\dots,\alpha_n$. Let $K=\mathbb Q(\alpha_1,\dots,\alpha_n)$ be its splitting field and $G=\mathrm{Gal}(K/\mathbb Q)$ its Galois group. Every $\sigma\in G$ permutes the zeros; the lengths of the cycles (including cycles of length 1) form the cycle pattern of $\sigma$, a partition of $n$.

For a prime $p\nmid\Delta(f)$, the degrees of the irreducible factors of $f \bmod p$ over $\mathbb F_p$ form the decomposition type of $f$ modulo $p$, again a partition of $n$.

A Frobenius substitution of $p$ is an element $\sigma\in G$ such that, for some prime ideal $\mathfrak Q$ of the ring of integers $\mathcal O_K$ lying over $p$,

$$\sigma(x)\equiv x^p \pmod{\mathfrak Q}\qquad\text{for all }x\in\mathcal O_K .$$

For $p\nmid\Delta(f)$ these elements form a single conjugacy class of $G$, written $\sigma_p$.

A set $S$ of primes has (analytic, or Dirichlet) density $\delta$ if

$$\frac{\sum_{p\in S}p^{-s}}{\log\frac{1}{s-1}}\longrightarrow\delta\qquad(s\downarrow 1),$$

and natural density $\delta$ if $\#\{p\le x:p\in S\}/\#\{p\le x\}\to\delta$ as $x\to\infty$.

Formalization targets

Goal: Chebotarëv's density theorem

For every conjugacy class $C$ of $G$,

$$\text{the set }\{p \text{ prime}: p\nmid\Delta(f),\ \sigma_p\in C\}\text{ has analytic density }\frac{\#C}{\#G}.$$

Milestones

1. Theorem of Dirichlet: for $m\ge1$ and $\gcd(a,m)=1$, the primes $p\equiv a \pmod m$ have density $1/\varphi(m)$.
2. A set of primes with natural density $\delta$ has analytic density $\delta$.
3. Galois theory of finite fields: for a squarefree $g\in\mathbb F_p[X]$, the cycle pattern of $x\mapsto x^p$ on the zeros of $g$ equals the decomposition type of $g$.
4. For $p\nmid\Delta(f)$, the Frobenius substitutions of $p$ form exactly one conjugacy class of $G$.
5. For $p\nmid\Delta(f)$, the cycle pattern of $\sigma_p$ equals the decomposition type of $f$ modulo $p$.
6. For $f=X^m-1$ and $p\nmid m$, $\sigma_p(\zeta)=\zeta^p$ for every primitive $m$-th root of unity $\zeta$; that is, $\sigma_p$ corresponds to $p \bmod m$ under $G\cong(\mathbb Z/m\mathbb Z)^\times$.
7. Theorem of Frobenius: the primes $p\nmid\Delta(f)$ for which $f$ has a given decomposition type $t$ have density $\#\{\sigma\in G:\text{cycle pattern }t\}/\#G$.

Significance

Chebotarëv's theorem shows that every conjugacy class of the Galois group occurs as a Frobenius class for infinitely many primes, with a predictable frequency. Its standard consequences include: the Frobenius elements are equidistributed; a Galois extension is determined by its completely split primes; if $f$ has a zero modulo almost every prime then $f$ is linear or reducible; prime ideals are equidistributed over ideal classes. The theorem is the first step in many arguments in arithmetic geometry (e.g. Serre's work on $\ell$-adic representations).

The theorem is classical and proved; this mission is about formalizing it. Mathlib contains Frobenius elements in Galois extensions of Dedekind domains and Dirichlet's theorem in the form "infinitely many primes in each coprime residue class", but, to our knowledge, neither the density form of Dirichlet's theorem nor Frobenius's or Chebotarëv's density theorem.

Difficulty

The Galois-theoretic parts (milestones 3–6) are standard but require connecting Frobenius elements in $\mathcal O_K$ with factorization of $f$ modulo $p$, including the fact that $p\nmid\Delta(f)$ forces $p$ to be unramified in $K$. The analytic core is harder: one needs Dedekind zeta functions and $L$-functions of number fields and their behaviour at $s=1$. The reduction of the general case to the cyclotomic case (Chebotarëv's "crossing" with cyclotomic extensions) needs the density statement over an arbitrary number field as base, not only over $\mathbb Q$; in particular, the statement over $\mathbb Q$ alone cannot be proved by induction on itself.

Formalization scope

All declarations live in the namespace ChebotarevDensity and share one definition file.

• $K$ is Mathlib's SplittingField of $f$ viewed in $\mathbb Q[X]$; $G$ is Polynomial.Gal; $\Delta(f)$ is Mathlib's Polynomial.discr.
• A Frobenius substitution is expressed with Mathlib's IsArithFrobAt at some prime ideal of $\mathcal O_K$ containing $p$; "$\sigma_p\in C$" means that some Frobenius substitution of $p$ lies in $C$ (for $p\nmid\Delta(f)$ this is equivalent to all of them lying in $C$, by milestone 4).
• The cycle pattern is Equiv.Perm.partition of the permutation induced on the complex zeros of $f$; it includes fixed points.
• The decomposition type is the multiset of degrees of the normalized (monic) irreducible factors of $f \bmod p$.
• Analytic density uses $\sum' p^{-s}$ over the primes of $S$ and the limit $s\to1^+$ within $(1,\infty)$; natural density compares prime counts up to $x\in\mathbb N$.
• The hypotheses $\Delta(f)\neq0$ and "$f$ monic" are those of the source; the theorems are not vacuous, since e.g. $f=X^m-1$ satisfies them.

Welcome contributions: Dedekind zeta functions and Hecke $L$-functions at $s=1$, the density form of Dirichlet's theorem, unramifiedness of primes not dividing the discriminant, and the general number-field version of the theorem.

Selected references

• P. Stevenhagen, H. W. Lenstra, Jr., Chebotarëv and his density theorem, Math. Intelligencer 18 (1996), no. 2, 26–37. doi:10.1007/BF03027290
• N. Tschebotareff, Die Bestimmung der Dichtigkeit einer Menge von Primzahlen, welche zu einer gegebenen Substitutionsklasse gehören, Math. Ann. 95 (1925), 191–228. doi:10.1007/BF01206606
• S. Lang, Algebraic Number Theory, Addison-Wesley, 1970, Chap. VIII.
• J. Neukirch, Class Field Theory, Springer, 1986, Chap. V.
• Chebotarev density theorem, Wikipedia. link

Motivation

The discrete logarithm problem modulo a prime asks, given a prime $p$, a generator $g$ of the multiplicative group modulo $p$, and a nonzero residue $x$, for the exponent $r$ with $g^r\equiv x \pmod p$. Its presumed classical hardness underlies Diffie–Hellman key exchange, ElGamal encryption and the Digital Signature Algorithm. The best classical algorithm known when Shor wrote, Gordon's adaptation of the number field sieve, runs in time $\exp(O((\log p)^{1/3}(\log\log p)^{2/3}))$.

In §6 of Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (SIAM J. Comput. 26(5), 1997; doi:10.1137/S0097539795293172, arXiv:quant-ph/9508027), Shor gave a quantum algorithm that uses two modular exponentiations and two quantum Fourier transforms and outputs, with constant probability, a pair from which $r$ can be computed. The quantitative core of that analysis is a single number: the circuit produces a "good" output with probability at least $1/480$. This mission formalizes that bound and the three estimates it is assembled from.

Setting

Let $p$ be a prime and $g$ a generator of $(\mathbb Z/p\mathbb Z)^\times$, so that $1,g,\dots,g^{p-2}$ are all the nonzero residues. Fix the unknown $r$ with $0\le r<p-1$ and put $x=g^r$. Let $q=2^l$ be the power of $2$ with $p<q<2p$.

The Fourier matrix $A_q$ is the $q\times q$ matrix with entries $(A_q)_{a,c}=q^{-1/2}\exp(2\pi i\,ac/q)$ for $0\le a,c<q$ (§4, eq. (4.1)). Rows index input basis vectors and columns output basis vectors.

The algorithm uses three registers: two holding numbers $0\le a,b<q$ and one holding a nonzero residue modulo $p$. It starts from the state

$$\frac{1}{p-1}\sum_{a=0}^{p-2}\sum_{b=0}^{p-2}|a,b,g^ax^{-b}\ (\mathrm{mod}\ p)\rangle \qquad (6.1)$$

(preFourierState), applies $A_q$ to each of the first two registers (finalState), and measures all three registers. The probability of observing $|c,d,y\rangle$ is the squared modulus of its amplitude (outcomeProb).

For integers $z$ and $q>0$, the symmetric residue $\{z\}_q$ is the residue of $z$ modulo $q$ in $(-q/2,q/2]$ (symmRes). Put

$$T=rc+d-\frac{r}{p-1}\{c(p-1)\}_q .$$

An observed state $|c,d,y\rangle$ is good (IsGood) when

$$|\{T\}_q|\le\tfrac12 \quad (6.10) \qquad\text{and}\qquad |\{c(p-1)\}_q|\le q/12 \quad (6.11).$$

Goodness depends only on $(c,d)$.

Formalization targets

Goal: a good output with probability at least $1/480$ (§6, p. 1504)

$$\sum_{\substack{0\le c,d<q\\ (c,d)\ \text{good}}}\ \sum_{y\in(\mathbb Z/p)^\times}\Pr[c,d,y]\ \ge\ \frac1{480}.$$

The constant is the one the page carries forward. The goal fixes no threshold on $p$: it is stated for every prime $p$ that admits a power of two strictly between $p$ and $2p$.

Milestones

1. The output distribution, eq. (6.4). For $0\le k<p-1$,

$$\Pr[c,d,g^k]=\left|\frac{1}{(p-1)q}\sum_{\substack{0\le a,b\le p-2\\ a-rb\equiv k\ (p-1)}}\exp\Bigl(\frac{2\pi i}{q}(ac+bd)\Bigr)\right|^2 .$$

2. Each good state is likely, eq. (6.17). If $(c,d)$ is good, then $\Pr[c,d,y]\ge 1/(20q^2)$ for every $y$.
3. Many good pairs (p. 1504). At least $q/12$ pairs $(c,d)$ are good.
4. Each good $c$ is likely (p. 1504). If $(c,d)$ is good for some $d$, then $\sum_{d',y}\Pr[c,d',y]\ge(p-1)/(20q^2)\ge1/(40q)$.

Significance

The result. The bound $1/480$ is what turns the circuit into an algorithm. Repeating the circuit $O(1)$ times in expectation yields a good output, and from a good pair $(c,d)$ one reads off an equation that determines $r$ modulo divisors of $p-1$ (§6, eqs. (6.18)–(6.20)). Together with the quantum Fourier transform circuit and reversible modular exponentiation, this places the discrete logarithm modulo a prime in quantum polynomial time. Every later analysis of quantum attacks on discrete-logarithm cryptography starts from this success probability or a sharpened version of it.

Formalizing it. The result has been proved since 1994–1997 and is textbook material; it is not open. As far as is known, no machine-checked proof of Shor's discrete-logarithm analysis exists. The paper's proof of eq. (6.17) replaces a sum by an integral with an error term $O(W/(pq))$ whose constant is not given, yet states $1/(20q^2)$ for every prime. A formal proof must therefore either control that error explicitly or find another argument, and so settles a point the paper leaves informal. Numerically, the smallest value of $q^2\Pr[c,d,y]$ over good states is about $0.49$ for all primes $p<90$, so the unconditional claim is not in doubt for small $p$. The page also contains two small slips, recorded under Formalization scope; a complete development pins down exactly what is true.

Difficulty

The exponential sum (6.4) runs over pairs $(a,b)$ satisfying a congruence modulo $p-1$, while the phases are taken modulo $q$. The two moduli are unrelated: $q$ is a power of two and $p-1$ is arbitrary. Eliminating $a$ through the congruence introduces a floor function $\lfloor(br+k)/(p-1)\rfloor$, and the resulting phase is not linear in $b$. The obvious estimate treats the sum as a geometric series in $b$ and bounds it by its first-order phase; this fails because the floor term perturbs every phase by an amount of size up to $|\{c(p-1)\}_q|$. Condition (6.11) only keeps this perturbation within $\pi/6$ of the main phase; it does not remove it. The per-state bound must survive this perturbation uniformly in $p$, $r$ and $k$, including small primes where the paper's integral approximation gives no explicit control.

The count of good pairs needs a separate argument about how often a multiple $c(p-1)$ lies within $q/12$ of a multiple of $q$ when $\gcd(p-1,q)$ is large.

Formalization scope

• States are functions Fin q × Fin q × (ZMod p)ˣ → ℂ. The first two registers range over $\{0,\dots,q-1\}$; the third over the units modulo $p$.
• Matrix convention. Following §2, rows are inputs, so the amplitude of $|c,d,y\rangle$ after the transforms is $\sum_{a,b}\psi(a,b,y)(A_q)_{a,c}(A_q)_{b,d}$. finalState is defined this way from (6.1) and $A_q$. It is not typed in as the closed form (6.3) or (6.4). A formalization that defined the final state by (6.4) directly would make milestone 1 trivial, and is ruled out.
• Probability of a basis state is the squared norm of its amplitude, with no normalization hypothesis.
• Parameters. $p$ is prime (Fact p.Prime). The generator is encoded as orderOf g = p - 1. $r<p-1$ is a parameter, with $x=g^r$. $q$ is given by q = 2 ^ l together with $p<q<2p$. No large-$p$ threshold is added anywhere.
• Arithmetic. $x^{-b}$ is x⁻¹ ^ b in the unit group. $p-1$ is computed in $\mathbb Z$ and $\mathbb R$ inside $T$ and the congruences, and as natural-number subtraction only where $p\ge2$ makes it exact. $T$ is real.
• Condition (6.10) is stated as "some integer $j$ has $|T-jq|\le\frac12$". Because $q\ge4$, this is equivalent to the page's form with $j$ the closest integer to $T/q$.
• Not formalized. The preparation of (6.1) by testing and restarting is not formalized; the state (6.1) is taken as displayed. The printed test "whether the number is less than $p$" should read $p-1$, as the sums in (6.1) show. Also out of scope: the recovery of $r$ (eqs. (6.18)–(6.20)), the repetition count "$480t$", and all running-time claims.
• Printed slips.
  • The page asserts that for each $c$ there is exactly one $d$ satisfying (6.10). At a tie $\{T\}_q=\pm\frac12$ there can be two such $d$. Milestone 3 states only the count, which needs at least one.
  • The page's intermediate bound "at least $p/(240q)$" should be $(p-1)/(240q)$. The conclusion $1/480$ is unaffected, since $q$ and $2p$ are both even and so $q\le 2(p-1)$. Only $1/480$ is stated.

Needed infrastructure: finite exponential sums and their modulus, the symmetric residue and its basic properties, and counting multiples in residue classes of $\mathbb Z/q$. The exponential-sum estimates of milestones 1 and 2 are reusable in the order-finding analysis of §5 of the same paper. Proofs of any milestone, of the normalization $\sum\Pr=1$, and of auxiliary lemmas about symmRes are welcome.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172 (preprint: https://arxiv.org/abs/quant-ph/9508027)
• D. M. Gordon, Discrete logarithms in GF(p) using the number field sieve, SIAM J. Discrete Math. 6(1):124–138, 1993. https://doi.org/10.1137/0406010
• W. Diffie and M. E. Hellman, New directions in cryptography, IEEE Trans. Inform. Theory 22(6):644–654, 1976. https://doi.org/10.1109/TIT.1976.1055638
• M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511976667

Motivation

Shor's 1997 paper (SIAM J. Comput. 26(5), arXiv:quant-ph/9508027) gives a polynomial-time quantum algorithm for factoring integers. The quantum computer does not factor directly: it finds the multiplicative order of an element modulo $n$. The step from order finding to factoring is classical and randomized, and goes back to Miller's 1976 work on primality testing (G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13 (1976)). Every account of Shor's algorithm, and every resource estimate for breaking RSA with a quantum computer, depends on this reduction succeeding with a constant probability per trial. This mission formalizes that probability bound as Shor states it on p. 1498 of the published paper.

Setting

Let $n > 1$ be an odd integer with prime factorization

$$n = \prod_{i=1}^{k} p_i^{\alpha_i},$$

so $k$ is the number of distinct prime factors of $n$, all odd. The unit group $(\mathbb{Z}/n\mathbb{Z})^\times$ consists of the residues coprime to $n$; it has $\varphi(n)$ elements, where $\varphi$ is Euler's totient function.

For a unit $x$ the order $r = \operatorname{ord}_n(x)$ is the least positive integer with $x^r \equiv 1 \pmod n$. For each $i$ the local order $r_i$ is the order of $x \bmod p_i^{\alpha_i}$, taken modulo the full prime power, not modulo $p_i$. For a positive integer $m$, $\nu_2(m)$ denotes the exponent of the largest power of $2$ dividing $m$.

The reduction is: choose $x$ uniformly at random from $(\mathbb{Z}/n\mathbb{Z})^\times$, obtain its order $r$ (from the quantum subroutine), and compute

$$g(x) = \gcd\bigl(x^{r/2} - 1,\ n\bigr).$$

The procedure yields a nontrivial factor at $x$ when $r$ is even and $1 < g(x) < n$. In Lean this event is ShorAlgorithms.Reduction.successEvent n u for u : (ZMod n)ˣ, and $r_i$ is localOrder n u p for p ∈ n.primeFactors.

Formalization targets

Goal: the success probability

$$\Pr_{x \in (\mathbb{Z}/n)^\times}\bigl[r \text{ even and } 1 < \gcd(x^{r/2}-1, n) < n\bigr] \;\ge\; 1 - \frac{1}{2^{k-1}}.$$

It is stated for every odd $n > 1$. For a prime power ($k = 1$) the bound is $0$, so the statement says nothing there; it is informative exactly when $n$ is not a prime power, as the paper remarks. The constant is sharp: for $n = 21$ exactly $6$ of the $12$ units succeed, so $1 - 1/2^{k}$ in place of $1 - 1/2^{k-1}$ would be false.

Milestones, in the order the page uses them

1. Success criterion. If $r$ is even and $x^{r/2} \not\equiv -1 \pmod n$, then $1 < \gcd(x^{r/2}-1, n) < n$.
2. Order is the lcm. $r = \operatorname{lcm}(r_1, \dots, r_k)$.
3. Failure forces agreement. For odd $n$, if the procedure fails at $x$, then $\nu_2(r_1) = \cdots = \nu_2(r_k)$.
4. At most half per odd prime power. For an odd prime $p$ and $\alpha \ge 1$, at most $\varphi(p^\alpha)/2$ units modulo $p^\alpha$ have order with a prescribed 2-adic valuation.
5. All agree rarely. The units for which $\nu_2(r_1) = \cdots = \nu_2(r_k)$ number at most $\varphi(n)/2^{k-1}$.

Significance

The result. The bound turns an order-finding oracle into a factoring algorithm: when $n$ is odd and not a prime power, each trial succeeds with probability at least $1/2$, so $t$ independent trials all fail with probability at most $2^{-t}$. Even numbers and prime powers are split classically, as the paper notes, so the bound completes the reduction from factoring to order finding. The same criterion — a square root of $1$ other than $\pm 1$ splits $n$ — underlies the Miller–Rabin test and several classical factoring methods.

Formalizing it. The mathematics is classical and proved; the paper gives a sketch of one paragraph. This mission writes out the sketch as machine-checked statements over Mathlib's ZMod, including the probabilistic step, which in the paper is an informal appeal to the Chinese remainder theorem and "50% probability of agreeing with the previous ones". Mathlib already has the needed ingredients (cyclicity of $(\mathbb{Z}/p^\alpha)^\times$ for odd $p$, ZMod.chineseRemainder, ZMod.card_units_eq_totient), but not the reduction or its probability bound.

Difficulty

The success criterion (milestone 1) is elementary. The substance is the counting. The obvious route — treating the $\nu_2(r_i)$ as independent and each "equal to the previous one with probability $1/2$" — needs both a precise product decomposition of the unit group modulo $n$ into the unit groups modulo $p_i^{\alpha_i}$, compatible with the local orders, and the count in a cyclic group of even order of the elements whose order has a given 2-adic valuation. The informal phrase "at most a 50% probability of agreeing with the previous ones" hides a conditioning argument over $k - 1$ coordinates that has to be done by an explicit cardinality bound. A second pitfall is milestone 3: its converse direction and its forward direction use oddness of $n$ in different places, and modulo a power of $2$ the argument breaks because $-1 \equiv 1 \pmod 2$.

Formalization scope

• Sample space. Uniform on (ZMod n)ˣ; probabilities are stated in cleared-denominator form, $(1 - 2^{-(k-1)})\,\varphi(n) \le \#\{\text{successes}\}$ in $\mathbb{R}$, with the count as Nat.card of a subtype. Non-units have no multiplicative order and are not sampled.
• The gcd. $x^{r/2}$ is represented by its least nonnegative residue .val, which is at least $1$ for a unit when $n > 1$, so the natural-number subtraction in val - 1 never truncates. $r/2$ is natural-number division, used only under Even r.
• $k$. n.primeFactors.card, at least $1$ for $n > 1$, so k - 1 does not truncate. Since $n$ is odd this equals the page's "number of distinct odd prime factors".
• Local orders. The order of the image of $x$ in ZMod (p ^ n.factorization p) under the reduction homomorphism.
• Hypotheses. The goal assumes exactly $n$ odd and $n > 1$. It does not assume "not a prime power": that clause in the paper describes when the bound is useful. Milestones 1 and 2 do not assume $n$ odd, because they do not need it; milestones 3 and 5 do.
• No trivialization. Counting over all of ZMod n instead of the units would put non-units (with junk order $0$) into the denominator; the goal counts over (ZMod n)ˣ and divides by $\varphi(n)$. The goal's constant is the paper's $1 - 1/2^{k-1}$, which is attained, so it cannot be weakened into a triviality without changing the theorem.
• Welcome contributions. A reusable counting lemma for elements of prescribed 2-adic order in a finite cyclic group; the transfer of ZMod.chineseRemainder to unit groups and to local orders; and proofs of the milestones in any order.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172 (preprint arXiv:quant-ph/9508027, https://arxiv.org/abs/quant-ph/9508027)
• G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13(3):300–317, 1976. https://doi.org/10.1016/S0022-0000(76)80043-8
• D. E. Knuth, The Art of Computer Programming, Vol. 2: Seminumerical Algorithms, 2nd ed., Addison-Wesley, 1981.
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 5th ed., Oxford University Press, 1979 (Theorem 121, Chinese remainder theorem).

Motivation

Rings of arithmetic power series — power series with integer coefficients that converge on a disc of radius close to $1$ — sit between algebra and analysis: an element has both archimedean zeros, in the complex disc, and non-archimedean ones, at $p$-adic points. Harbater (Convergent arithmetic power series, Amer. J. Math. 106 (1984), 801–846, DOI 10.2307/2374325) showed that a well-chosen ring of such series is a principal ideal domain and identified its prime ideals; the same ring is the arithmetic model of the closed disc of radius $r$ in the adic space $\mathrm{Spa}(\mathbb{Z}[[T]])$.

The result was put to work in Clausen–Scholze's Lectures on Analytic Geometry (Lecture VII), where $\mathbb{Z}((T))_{>r}$ supplies a two-term presentation of the real numbers as a condensed abelian group: for $0 < r' < r < 1$ there is an exact sequence $0 \to \mathbb{Z}((T))_r \xrightarrow{f_{r'}} \mathbb{Z}((T))_r \to \mathbb{R} \to 0$, whose existence rests on the principality of the kernel of evaluation at $r'$. The quantitative refinement of that sequence (Propositions 7.2 and 7.3 of the notes) is what produces the $\ell^p$-norms in the analytic ring structure on $\mathbb{R}$.

Setting

Fix a real number $r$ with $0 < r < 1$. An integral Laurent series is a family of integers $(a_n)_{n \in \mathbb{Z}}$ whose support is bounded below, written $f = \sum_{n \gg -\infty} a_n T^n$; these form the ring $\mathbb{Z}((T))$ under coefficientwise addition and the Cauchy product.

Define

$$\mathbb{Z}((T))_{>r} \;=\; \Big\{\, \sum_{n \gg -\infty} a_n T^n \;\Big|\; \exists\, s > r,\ |a_n|\, s^{\,n} \xrightarrow[n \to \infty]{} 0 \,\Big\} \;\subseteq\; \mathbb{Z}((T)).$$

Concretely, $f$ lies in $\mathbb{Z}((T))_{>r}$ when the associated Laurent expansion converges on some punctured disc $\{0 < |y| < s\}$ with $s > r$ strictly larger than $r$ — an overconvergence condition. For $x$ a real or complex number, $f(x) = \sum_{n} a_n x^{\,n}$ denotes the evaluation, whenever the family is summable.

Two features distinguish this ring from the classical Tate algebra. The coefficients are integers, not elements of a complete field, so reduction modulo a prime $p$ is available and produces $\mathbb{F}_p((T))$. And the condition is an overconvergence condition: the radius $s$ is required to be strictly larger than $r$, which is what makes the ring behave like the ring of functions on a closed disc rather than an open one.

Formalization targets

Goal

$$0 < r < 1 \;\Longrightarrow\; \mathbb{Z}((T))_{>r} \text{ is a principal ideal domain.}$$

The ring is a subring of the domain $\mathbb{Z}((T))$, so integrality is automatic and the content of the goal is that every ideal is generated by one element.

The prime ideals (context, not a formalization target here)

Theorem 7.1 of the source also classifies the nonzero primes: kernels of evaluation at a complex $x$ with $0 < |x| \le r$ (up to conjugation); the ideals $(p)$ for $p$ prime; and kernels of evaluation at a topologically nilpotent unit $x$ of a finite extension of $\mathbb{Q}_p$ (up to Galois conjugacy). The milestones below formalize the parts of the classification that the principality proof actually consumes — surjectivity of the three evaluation maps, and principality of the archimedean kernels — and leave the full classification statement for a later mission in this series.

Significance

The result itself. Principality gives, for each point of the closed disc, a single equation cutting it out; that is exactly what the presentation $0 \to \mathbb{Z}((T))_r \to \mathbb{Z}((T))_r \to \mathbb{R} \to 0$ needs. Downstream, that presentation is the input to the computation of measures on $\mathbb{R}$ in the analytic-ring formalism, and the reason $\ell^p$-spaces with $p < 1$ appear there at all. Without it, one has no finite free resolution of $\mathbb{R}$ by rings of arithmetic functions, and the structure results of Lectures VI–VII of the source lose their computational base.

Formalizing it. The mathematics is classical and fully proved; nothing here is open. What is missing is a machine-checked version. Mathlib has Hahn series, Laurent series, complex analysis on discs, and the $p$-adic numbers, but nothing about arithmetic overconvergent series: not the ring itself, not the greedy expansions that make real evaluation surjective, not the invertibility criterion. Each milestone below is a self-contained piece of that missing theory, reusable outside this mission.

Difficulty

The obvious approach — Weierstrass preparation, as for the Tate algebra $K\langle T\rangle$ over a complete field $K$ — does not apply: the coefficient ring $\mathbb{Z}$ is not a field, and no single valuation controls it. An element of $\mathbb{Z}((T))_{>r}$ must be divided simultaneously by archimedean generators (complex zeros in the disc) and $p$-adic ones, with the quotient required to stay integral and still overconvergent. Two steps carry the weight and fail for naive reasons:

• Producing an integral generator for the kernel of evaluation at a real or complex $x$: one first needs a real polynomial $g \in 1 + T^n\mathbb{R}[T]$ with $x$ as its only zero in $\{0 < |y| \le r\}$, then a correction series $h$ with small coefficients such that $gh$ has integer coefficients. Neither factor alone is integral.
• Showing that an element of $1 + T\mathbb{Z}[[T]]$ with no zero in the closed disc of radius $r$ is invertible in the ring: the inverse is integral for formal reasons, but its overconvergence is an analytic statement about the absence of zeros.

Finiteness — that a nonzero element lies in only finitely many of the listed maximal ideals — mixes the identity theorem for holomorphic functions with a $p$-adic Weierstrass argument, which is why the reduction and $p$-adic surjectivity milestones are prerequisites rather than side remarks.

Formalization scope

The ambient ring is Mathlib's LaurentSeries ℤ (Hahn series over $\mathbb{Z}$ indexed by $\mathbb{Z}$), and $\mathbb{Z}((T))_{>r}$ is given as a set of such series, cut out by the decay condition $|a_n| s^{\,n} \to 0$ as $n \to +\infty$ for some $s > r$. Evaluations are unordered sums over $\mathbb{Z}$; where a statement asserts a value of an evaluation, summability is asserted alongside it, so the junk value of a divergent sum cannot be exploited.

Because the carrier is a set, the goal theorem is stated for an arbitrary subring of $\mathbb{Z}((T))$ whose underlying set is $\mathbb{Z}((T))_{>r}$. That form would be vacuous if no such subring existed, which is precisely why the first milestone asserts its existence; the two together carry the intended content, and the mission is not considered advanced by the goal alone.

Milestone 6 formalizes only the case $K = \mathbb{Q}_p$ of part (3) of the source theorem (topologically nilpotent units of proper finite extensions of $\mathbb{Q}_p$ are out of scope, since Mathlib lacks the ambient theory of such extensions). Milestone 3 drops the "with multiplicity one" clause of the source and asserts only that the zero set in the punctured closed disc is $\{x\}$.

A complete development will need: closure of the decay condition under the Cauchy product; summability of evaluations on the closed disc; the identity theorem for the induced holomorphic functions; greedy $x$-adic expansions of real numbers with bounded integer digits; and $p$-adic expansions in the lattice generated by a topologically nilpotent unit. Contributions of any of these, as standalone lemmas, are welcome.

Selected references

• D. Harbater, Convergent arithmetic power series, American Journal of Mathematics 106 (1984), 801–846. DOI 10.2307/2374325
• P. Scholze (joint with D. Clausen), Lectures on Analytic Geometry, Bonn, 2019/20; Lecture VII, Theorem 7.1. PDF
• P. Scholze (joint with D. Clausen), Lectures on Condensed Mathematics, Bonn, 2019. PDF

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