Number Theory

Motivation

An additive question about the primes asks how many of them are needed to represent every integer. Shnirelman's constant is the least $k$ such that every natural number greater than $1$ is a sum of at most $k$ primes; that such a $k$ exists at all is Shnirelman's theorem (1930). The even Goldbach conjecture would give $k = 3$, and is close to equivalent to that claim, but Goldbach is open, so every bound on $k$ has come from the circle method together with explicit numerical input.

The history is a sequence of shrinking bounds, each one effective and each one resting on a numerical verification available at the time:

• 1937. Vinogradov proves that every sufficiently large odd integer is a sum of three primes, with no effective threshold (Vinogradov's theorem).
• 1956. Borozdkin makes the threshold effective; later work reduces it, and Liu and Wang bring it to $\exp(3100)$ (Liu–Wang, 2002).
• 1995. Ramaré proves that every even natural number is a sum of at most six primes, giving Shnirelman's constant $k \le 7$ (Ramaré).
• 1995. Kaniecki obtains "at most five primes" under the Riemann hypothesis (Kaniecki).
• 2012. Tao removes the hypothesis: every odd number greater than $1$ is a sum of at most five primes, unconditionally, lowering Shnirelman's constant to $k \le 6$ (arXiv:1201.6656). This mission's goal.
• 2013. Helfgott proves the ternary Goldbach conjecture outright — every odd $n > 5$ is a sum of three primes — which supersedes the statement above (arXiv:1312.7748). Neither result is formalized.

Setting

For a real number $\theta$ write $e(\theta) = \exp(2\pi i\theta)$. The von Mangoldt function $\Lambda(n)$ equals $\log p$ when $n = p^m$ is a prime power and $0$ otherwise; it is Mathlib's ArithmeticFunction.vonMangoldt.

The paper does not work with the sharp-cutoff exponential sum $S(x,\alpha) = \sum_{n \le x} \Lambda(n)e(\alpha n)$ but with a smoothed variant. For a piecewise smooth $\eta : \mathbb{R} \to \mathbb{C}$ and a modulus $q_0$, set

$$S_{\eta,q_0}(x,\alpha) \;:=\; \sum_{n} \Lambda(n)\,e(\alpha n)\, \mathbf{1}_{(n,q_0)=1}\,\eta(n/x).$$

The modulus $q_0$ is a technical device: taking $q_0 = 2$ restricts the sum to odd $n$ and saves a factor of two in the explicit constants. Because of that restriction it is $4\alpha$, not $\alpha$, that gets approximated by a rational $a/q$.

Two explicit cutoffs are fixed. The Lipschitz cutoff

$$\eta_0(t) := 4\big(\log 2 - |\log 2t|\big)_+$$

has unit mass and is supported on $[1/4, 1]$; it is chosen because it factorises the Type II sums. The $L^2$-normalised cutoff

$$\eta_1(t) := \big(1 - 10\,\mathrm{dist}(t,[0.2,0.8])\big)_+$$

is supported on $[0.1,0.9]$ and symmetric, $\eta_1(1-t) = \eta_1(t)$.

Throughout, $O^*(Y)$ denotes a quantity of magnitude at most $Y$ — an explicit bound, not an asymptotic one. Two numerical constants are fixed once and for all: $T_0 := 3.29\times 10^9$ and $N_0 := 4\times 10^{14}$.

Formalization targets

Goal (Theorem 1.4)

$$\forall n \text{ odd},\ n > 1 \;\Longrightarrow\; \exists\, p_1,\dots,p_k \text{ prime},\ k \le 5,\ n = p_1 + \cdots + p_k.$$

The goal fixes no constants and no thresholds, so no later improvement can invalidate it.

The milestone list is the paper's own attack path, in its numbering: the two numerical verifications (Theorems 1.5, 1.6) and the short-interval prime bound (Theorem 8.1) that together settle $n \le 8.7\times10^{36}$; the $L^2$ apparatus (Lemma 4.4, Proposition 4.10) and Vaughan-type identity (Lemma 4.11) feeding the minor-arc bound (Theorem 5.1) and hence the main exponential sum estimate (Theorem 1.3); the major-arc analysis (Proposition 7.2); and the circle-method core (Theorem 8.2).

Significance

The result itself. Theorem 1.4 lowers Shnirelman's constant from $7$ to $6$ and removes the Riemann hypothesis from Kaniecki's conditional "five primes". Its durable content, however, is not the headline but the explicit exponential sum estimate of Theorem 1.3: a bound on $|S_{\eta_0,q_0}(x,\alpha)|$ with constants small enough to be useful for $x$ between $10^{30}$ and $10^{1300}$, a range where the asymptotically superior estimates of Vinogradov, Chen–Daboussi and Ramaré carry constants too large or too ineffective to apply. That estimate is the reusable object; it has been improved since (Helfgott–Platt) but not superseded in method.

Formalizing it. Status honesty matters here. Theorem 1.4 is closed mathematics, and as a statement it was superseded within a year by Helfgott's ternary Goldbach theorem, which gives three primes for every odd $n > 5$ and hence five a fortiori. Neither Tao's theorem nor Helfgott's is formalized anywhere, and this mission does not claim to be attacking an open problem: the work is formalizing a known, fully explicit proof. That proof happens to be an unusually good formalization target, because every constant in it is written down.

The platform already hosts the surrounding infrastructure. The CircleMethod namespace carries a large verified development of Hardy–Littlewood apparatus following Vaughan, and the ThreePrimes namespace carries a machine-checked proof of Vinogradov's three primes theorem conditional on Siegel–Walfisz. This mission sits directly downstream of both and should import from them rather than rebuild.

Difficulty

The obvious route — deduce five primes from three primes — fails on the range where it is needed. Vinogradov's theorem is asymptotic, and the best effective threshold is $\exp(3100)$; below it the theorem says nothing, and $\exp(3100)$ is far beyond any possible exhaustive check. So the entire difficulty lives in the window $8.7\times10^{36} \le x \le \exp(3100)$, which must be handled by a circle-method argument carrying explicit constants at every step.

Within that window the specific obstruction is the minor arc $T_0/x \ll \|\alpha\|_{\mathbb{R}/\mathbb{Z}} \ll 1/N_0$. A direct Plancherel bound on the $L^2$ side costs a factor of $\log x$, which is more than the argument can afford; Montgomery's uncertainty principle cuts the loss to roughly $2\log x/\log N_0$, and only a large-sieve estimate on prime pairs brings it down to a bounded factor of $8$. On the $L^\infty$ side, Theorem 1.3 must be non-trivial across the whole window, which is why the refinements (1.10)–(1.12) for $q$ near $1$ and near $x$ exist at all. Neither bound alone suffices; the proof closes only because both are pushed to explicit constants simultaneously.

Formalization scope

The goal is stated over $\mathbb{N}$ as a Multiset ℕ of cardinality at most $5$ whose members are all Nat.Prime and whose sum is $n$. A multiset, not a list or a finset: repetition is essential ($9 = 3+3+3$) and order is not. "At most five" is not "exactly five" — $3$ is a sum of one prime and cannot be a sum of five, since the least sum of five primes is $10$. A formalization asserting exactly five primes is false, not merely weaker.

The goal admits no trivializing reading: the empty multiset has sum $0 \ne n$, and the cardinality bound is on the multiset itself, so no prime can be counted with multiplicity zero to evade it.

Everything else in the mission is stated with explicit constants and $O^*(\cdot)$ bounds rather than asymptotic notation, matching the paper: $X = O^*(Y)$ becomes $\|X\| \le Y$ outright. Sums over $n$ are unrestricted sums against a compactly supported cutoff, not sums over Finset.range. Real powers are Real.rpow. The two cutoffs $\eta_0,\eta_1$ and the sum $S_{\eta,q_0}$ are published as mission definitions; solvers should use them verbatim rather than re-deriving equivalent forms.

Three of the milestones are honest dead weight for a solver to attempt directly, and are listed so the dependency graph is truthful rather than because they are tractable. Theorem 1.5 (all zeroes of $\zeta$ up to height $3.29\times10^9$ lie on the critical line) and Theorem 1.6 (every even number up to $4\times10^{14}$ is a sum of two primes) are finite, decidable statements that Lean can express and that are true, but each represents a verified computation of a scale no current proof assistant can replay — Theorem 1.6 alone is $2\times10^{14}$ cases. Theorem 8.1 is quoted from Ramaré–Saouter and itself depends on Theorem 1.5. They are leaves that will stay open; a solver's effort is far better spent on the analytic milestones, and the circle-method core (Theorem 8.2) can be closed independently of them.

A complete development additionally needs the smoothed Vaughan identity bookkeeping, the large sieve in Siebert's form, the von Mangoldt explicit formula with a zero sum (Proposition 7.1), and Bourgain's trick of taking one of the three summands of size $x/K$. The exponential sum machinery is reusable well beyond this mission — it is the standard input to every explicit Goldbach-type result. Contributions to any milestone are welcome independently, and a formalization of Helfgott's theorem that closes the goal by a different route would be an entirely acceptable solution.

Selected references

• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Mathematics of Computation 83 (2014), 997–1038. arXiv:1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. arXiv:1312.7748
• H. A. Helfgott and D. Platt, Numerical verification of the ternary Goldbach conjecture up to $8.875\cdot10^{30}$, 2013. arXiv:1305.3062
• O. Ramaré, On Shnirel'man's constant, Ann. Scuola Norm. Sup. Pisa 22 (1995), 645–706. numdam
• L. Kaniecki, On Shnirelman's constant under the Riemann hypothesis, Acta Arithmetica 72 (1995), 361–374. doi:10.4064/aa-72-4-361-374
• J. Richstein, Verifying the Goldbach conjecture up to $4\cdot10^{14}$, Mathematics of Computation 70 (2001), 1745–1749. doi:10.1090/S0025-5718-00-01290-4
• O. Ramaré and Y. Saouter, Short effective intervals containing primes, Journal of Number Theory 98 (2003), 10–33. doi:10.1016/S0022-314X(02)00029-X
• M. C. Liu and T. Z. Wang, On the Vinogradov bound in the three primes Goldbach conjecture, Acta Arithmetica 105 (2002), 133–175. doi:10.4064/aa105-2-3
• H. L. Montgomery, The analytic principle of the large sieve, Bulletin of the AMS 84 (1978), 547–567. doi:10.1090/S0002-9904-1978-14497-8
• R. C. Vaughan, The Hardy–Littlewood Method, 2nd ed., Cambridge University Press, 1997. doi:10.1017/CBO9780511470929

Motivation

This mission seeks a Lean proof that every odd natural number greater than 1 is the sum of at most three primes. It follows from Helfgott's ternary Goldbach theorem for odd numbers greater than 5, together with the small cases 3 and 5, each of which is itself prime.

Setting and goal

For every natural number n with Odd n and 1 < n, construct a multiset of at most three prime natural numbers whose sum is n. Repetition is allowed and order is irrelevant. Examples include 3 = 3, 5 = 5, 7 = 2 + 2 + 3, and 9 = 3 + 3 + 3. The primes need not all be odd.

Relationship to the five-primes mission

The goal uses the same Multiset ℕ representation and the same hypothesis 1 < n as Every Odd Number Greater Than 1 is the Sum of at Most Five Primes. The cardinality bound changes from s.card ≤ 5 to s.card ≤ 3. No custom definitions are needed.

Formalization scope

The target is unconditional and covers every odd natural number greater than 1. At most three is essential: 3 and 5 cannot be sums of exactly three primes. All summands must satisfy Nat.Prime, and multiplicities count toward the cardinality bound. The initial proposal contains the goal with an open proof, ready for formalization.

Proof approach

A proof may combine a formalization of Helfgott's theorem, which supplies exactly three primes for odd n > 5, with singleton multisets for n = 3 and n = 5. Establishing Helfgott's result requires verified proofs of the analytic and computational ingredients of the chosen argument.

Reference

H. A. Helfgott, The ternary Goldbach conjecture is true, 2013, revised 2014. The mission's at-most-three formulation also includes the elementary cases n = 3 and n = 5.

Motivation

A number field $\mathbb{K}$ has a unit group $E = \mathcal{O}(\mathbb{K})^\times$ which, by Dirichlet's unit theorem, is free of $\mathbb{Z}$-rank $r_1 + r_2 - 1$ modulo roots of unity. Fix a prime $p$ and embed the units diagonally into the units of the completions of $\mathbb{K}$ at the primes above $p$. The topological closure of the image is a finite free a $\mathbb{Z}_p$-module modulo roots of unity, and its $\mathbb{Z}_p$-rank can in principle be smaller than $r_1 + r_2 - 1$: units that are independent over $\mathbb{Z}$ may become dependent $p$-adically. Leopoldt's conjecture asserts that this never happens.

The conjecture controls how many independent $\mathbb{Z}_p$-extensions a number field has. Iwasawa showed that if $\Omega(\mathbb{K})$ is the maximal $p$-abelian $p$-ramified extension of $\mathbb{K}$, then $\mathrm{Gal}(\Omega(\mathbb{K})/\mathbb{K}) \cong \mathbb{Z}_p^{\,r_2 + 1 + \mathcal{D}_L(\mathbb{K})}$, where $\mathcal{D}_L(\mathbb{K})$ is the defect defined below. So a positive defect means extra $\mathbb{Z}_p$-extensions beyond the ones accounted for by the archimedean places, and for a totally real field it means a non-cyclotomic $\mathbb{Z}_p$-extension exists. Non-vanishing of the $p$-adic regulator is also what makes $p$-adic $L$-functions and $p$-adic class number formulas behave as their complex analogues do.

Timeline of what is actually proved, under which hypotheses:

• 1962 — Leopoldt conjectures non-vanishing of the $p$-adic regulator for abelian fields (H. Leopoldt, Zur Arithmetik in Abelschen Zahlkörpern, J. reine angew. Math. 209).
• 1965–1967 — Ax reduces the abelian case to a $p$-adic analogue of Baker's theorem on linear forms in logarithms; Baker proves the archimedean version; Brumer adapts it $p$-adically and proves the conjecture for abelian extensions of $\mathbb{Q}$ (A. Brumer, On the units of algebraic number fields, Mathematika 14, 1967).
• 1976 — Greenberg relates the conjecture to a case of his own conjecture: Leopoldt for totally real fields implies the $T$-part of the relevant Iwasawa module is finite.
• 1981 — Waldschmidt proves the general bound $\mathcal{D}_L(\mathbb{K}) \le r/2$, where $r$ is the $\mathbb{Z}$-rank of the units: at least half of the expected $p$-adic rank is always attained.
• 1984, 1987–2007 — Emsalem–Kisilevsky–Wales settle some small non-abelian Galois groups by representation theory plus Baker theory; Jaulent handles fields of small discriminant.
• 2011–2016 — Mihăilescu posts a claimed proof for all CM fields at odd $p$ (arXiv:1105.4544). It is currently an unpublished preprint, and its proof invokes a separate preprint asserting the vanishing of Iwasawa's $\mu$-invariant for cyclotomic $\mathbb{Z}_p$-extensions of CM fields, with an appendix that is said to avoid that assumption.

Beyond the abelian case the conjecture is open. This mission takes the CM claim as its target.

Setting

Let $p$ be a prime and $\mathbb{K}$ a number field with ring of integers $\mathcal{O}(\mathbb{K})$ and units $E = \mathcal{O}(\mathbb{K})^\times$.

Let $P = \{\wp \subset \mathcal{O}(\mathbb{K}) : (p) \subset \wp\}$ be the set of primes above $p$, a finite set. For $\wp \in P$ write $\mathbb{K}_\wp$ for the completion and $\mathcal{O}_\wp$ for its valuation ring. Set

$$U \;=\; \prod_{\wp \in P} \mathcal{O}_\wp^{\times},$$

the group of semilocal units at $p$, and let

$$\iota : E \longrightarrow U$$

be the diagonal embedding, whose $\wp$-component is the completion map. Define the $p$-adic closure of the global units

$$\bar{E} \;=\; \bigcap_{n > 0} \iota(E) \cdot U^{p^n} \;\subseteq\; U ,$$

where $U^{p^n} = \{u^{p^n} : u \in U\}$ and the product of the two subgroups is taken inside the abelian group $U$. Finally, the Leopoldt defect of $\mathbb{K}$ at $p$ is

$$\mathcal{D}_L(\mathbb{K}) \;=\; \mathbb{Z}\text{-rk}(E) \;-\; \mathbb{Z}_p\text{-rk}(\bar{E}),$$

the difference between Dirichlet's unit rank $r_1 + r_2 - 1$ and the free $\mathbb{Z}_p$-rank of $\bar{E}$. The defect is always non-negative, and it is positive exactly when units that are independent over $\mathbb{Z}$ satisfy a $p$-adic relation after the diagonal embedding.

A number field $\mathbb{K}$ is CM when it is a totally complex quadratic extension of its maximal real subfield $\mathbb{K}^+$. For CM fields a positive defect is equivalent to the vanishing of the $p$-adic regulator of $\mathbb{K}$.

Formalization targets

Goal — Leopoldt's conjecture for CM fields at odd $p$

$$p \text{ odd prime}, \quad \mathbb{K}/\mathbb{Q} \text{ CM} \quad \Longrightarrow \quad \mathcal{D}_L(\mathbb{K}) = 0 .$$

This is Theorem 1 of arXiv:1105.4544. It fixes no constants and no auxiliary choices, so it is stable under any later improvement of the argument.

Supporting targets

$$\mathcal{D}_L(\mathbb{K}) = 0 \quad \text{for } \mathbb{K}/\mathbb{Q} \text{ abelian} \qquad \text{(Brumer, 1967)}$$ $$\mathcal{D}_L(\mathbb{K}) \le r/2, \quad r = \mathbb{Z}\text{-rk}(E) \qquad \text{(Waldschmidt, 1981)}$$ $$\mathcal{D}_L(\mathbb{F}) > 0 \quad \Longrightarrow \quad \mathcal{D}_L(\mathbb{K}) > 0 \quad \text{for every finite } \mathbb{K}/\mathbb{F}$$

The last is Remark 1.A of the source, attributed there to Laurent: a defect is inherited by finite extensions, because the $p$-adic relations among $\mathbb{Z}$-generators of the units are preserved under the embedding of unit groups.

Significance

The result itself. Leopoldt's conjecture for CM fields would pin down $\mathrm{Gal}(\Omega(\mathbb{K})/\mathbb{K}) \cong \mathbb{Z}_p^{\,r_2+1}$ for every CM field and, via the totally real subfield, would rule out non-cyclotomic $\mathbb{Z}_p$-extensions of the totally real fields underlying them. It would remove a standing hypothesis from results in Iwasawa theory and $p$-adic $L$-functions that are currently stated conditionally on Leopoldt. Without it, the $\mathbb{Z}_p$-rank of the $p$-ramified Galois group is only known to lie in a range.

Formalizing it. Nothing in this area is formalized today. Mathlib has Dirichlet's unit theorem, the archimedean regulator, CM fields, and the completions of a number field at its finite places, but no $p$-adic regulator, no $p$-adic logarithm, and no Iwasawa theory. This mission first pins down a machine-checked statement of the conjecture itself — which is where the mathematical content of Theorem 1 sits, since the theorem is one sentence long — and then attacks it. Because the target is an unrefereed argument, a serious attempt to formalize it is also a test of it: a step that cannot be closed localizes a gap, and a milestone that turns out to be unprovable is itself the finding.

Difficulty

The obvious approach is transcendence theory, and it is the one that works in the abelian case: a $p$-adic relation among units is a vanishing linear form in $p$-adic logarithms of algebraic numbers, and Baker-type lower bounds forbid it. This is exactly Ax's reduction and Brumer's theorem. It stalls immediately beyond abelian fields, because the argument needs units whose Galois structure is explicit — for abelian fields the cyclotomic units supply them, and in general nothing does. Waldschmidt's $\mathcal{D}_L \le r/2$ is the limit of what the transcendence route has delivered in general, and it has not been improved by that route. The source therefore abandons transcendence entirely and argues in Iwasawa theory, constructing a CM $\mathbb{Z}_p$-extension of a field where the conjecture is assumed to fail and deriving a contradiction from the classes of primes that split completely in it. That route needs the structure theory of $\Lambda$-modules, $\mu$- and $\lambda$-invariants, Tate cohomology of class group limits, and the vanishing of $\mu$ — none of which exists in Lean.

Formalization scope

The development commits to the following conventions, all of them visible in the definition file.

$P$ is the subtype of height-one primes $\wp$ of $\mathcal{O}(\mathbb{K})$ with $p \in \wp$, and carries a Finite instance. $U$ is the dependent product over $P$ of the unit groups of the valuation rings adicCompletionIntegers, so it is a commutative topological group. $\bar{E}$ is defined by the intersection displayed above rather than as a topological closure: the source gives both descriptions, and the intersection is the one that needs no choice of topology on $\prod_\wp \mathbb{K}_\wp$. The two can differ by a finite subgroup, which does not affect the $\mathbb{Z}_p$-rank.

$\mathbb{Z}_p\text{-rk}(\bar{E})$ is defined as the largest $n \le [\mathbb{K}:\mathbb{Q}]$ for which $\mathbb{Z}_p^n$ admits a continuous injective homomorphism into $\bar{E}$. Continuity is not decoration: as abstract groups $\mathbb{Z}_p^n$ embeds into $\mathbb{Z}_p$ for every $n$, so the topological requirement is what makes the rank the intended one; and since $\mathbb{Z}_p^n$ is compact and $U$ is Hausdorff, such an injection is automatically a closed embedding. For a closed subgroup of $U$, which is isomorphic to a finite group times $\mathbb{Z}_p^d$, such injections exist exactly for $n \le d$. The cut-off at $[\mathbb{K}:\mathbb{Q}]$ is carried only so that the supremum ranges over a visibly bounded set of naturals rather than falling back on a junk value; since the $\mathbb{Z}_p$-rank of the whole semilocal unit group $U$ is already $[\mathbb{K}:\mathbb{Q}]$, it never binds.

The defect subtracts in $\mathbb{N}$, hence truncates. Since the $\mathbb{Z}_p$-rank never exceeds the $\mathbb{Z}$-rank, truncation is never triggered and $\mathcal{D}_L(\mathbb{K}) = 0$ is equivalent to the two ranks being equal.

One trivializing formalization is worth ruling out. The goal is not vacuous: it is neither provable nor refutable by unfolding the definitions, and it has genuine content whenever $\mathbb{Z}\text{-rk}(E) > 0$, that is for every CM field other than the imaginary quadratic ones, where Dirichlet's rank is $0$ and the statement is trivially true.

A complete development needs, beyond what Mathlib supplies: the $p$-adic logarithm on the units of a local field and the resulting $p$-adic regulator; the Iwasawa algebra acting on inverse limits of $p$-class groups along a $\mathbb{Z}_p$-extension, with $\mu$- and $\lambda$-invariants and the decomposition of Definition 1 of the source; CM $\mathbb{Z}_p$-extensions; and Tate cohomology of these modules. All of that is reusable well beyond this mission — it is the missing foundation of Iwasawa theory in Lean. Contributions of any of these pieces as definitions, and of the three supporting targets as theorems, are welcome independently of the goal.

Selected references

• P. Mihăilescu, On CM $\mathbb{Z}_p$-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544 (2011–2016). https://arxiv.org/abs/1105.4544
• H. Leopoldt, Zur Arithmetik in Abelschen Zahlkörpern, J. reine angew. Math. 209 (1962), 54–71. https://doi.org/10.1515/crll.1962.209.54
• A. Brumer, On the units of algebraic number fields, Mathematika 14 (1967), 121–124. https://doi.org/10.1112/S0025579300003703
• J. Ax, On the units of an algebraic number field, Illinois J. Math. 9 (1965), 584–589. https://doi.org/10.1215/ijm/1256059299
• A. Baker, Linear forms in the logarithms of algebraic numbers I, II, III, Mathematika 13–14 (1966–67).
• M. Waldschmidt, Transcendance et exponentielles en plusieurs variables, Invent. Math. 63 (1981), 97–127. https://doi.org/10.1007/BF01389194
• M. Emsalem, H. Kisilevsky, D. Wales, Indépendance linéaire sur $\overline{\mathbb{Q}}$ de logarithmes $p$-adiques de nombres algébriques et rang $p$-adique du groupe des unités d'un corps de nombres, J. Number Theory 19 (1984), 384–391. https://doi.org/10.1016/0022-314X(84)90040-1
• R. Greenberg, On the Iwasawa invariants of totally real fields, Amer. J. Math. 98 (1976), 263–284. https://doi.org/10.2307/2373625
• K. Iwasawa, On $\mathbb{Z}_\ell$-extensions of number fields, Ann. of Math. 98 (1973), 246–326. https://doi.org/10.2307/1970784
• M. Laurent, Rang $p$-adique d'unités et action de groupes, J. reine angew. Math. 399 (1989), 81–108. https://doi.org/10.1515/crll.1989.399.81

Motivation and history

The Collatz conjecture, also called the $3x+1$ problem, asks whether one elementary iteration rule has the same long-term behavior for every positive integer. It belongs to number theory and discrete dynamical systems: the rule is deterministic and trivial to compute for any fixed input, but no argument is known that controls every orbit. The problem has served as a test case for methods involving congruences, stopping times, probabilistic models, computation, and arithmetic dynamics. Jeffrey Lagarias's survey, The $3x+1$ Problem and Its Generalizations, organized much of the classical theory and explains why strong results about large classes of starting values do not settle the universal statement (Lagarias 1985).

The problem has a long record of partial results. By 1985, the literature already included results on stopping-time densities, possible cycles, and divergent trajectories, summarized by Lagarias. In 2019, Terence Tao proved that for every function $f(N)$ tending to infinity, the minimum value attained by the orbit of $N$ is at most $f(N)$ for almost all positive integers $N$, where “almost all” is measured using logarithmic density (Tao 2019). This is a strong statement about typical orbits, but it does not cover every starting value. Computational verification has also been pushed to very large finite ranges; David Barina describes algorithms and verification methods for this task in Convergence Verification of the Collatz Problem (Barina 2021). A finite verification bound, regardless of size, leaves all larger starting values outside its scope.

Setting

For a natural number $n$, define the Collatz step $C(n)$ by

$$C(n)= \begin{cases} n/2, & \text{if } n \text{ is even},\\ 3n+1, & \text{if } n \text{ is odd}. \end{cases}$$

Write $C^m(n)$ for the result of applying $C$ exactly $m$ times, with $C^0(n)=n$. The forward orbit of $n$ is therefore

$$n,\ C(n),\ C^2(n),\ C^3(n),\ldots.$$

The familiar orbit beginning at $6$, for example, starts $6,3,10,5,16,8,4,2,1$. Reaching $1$ is the relevant event; after that point the usual map continues around the cycle $1,4,2,1$.

Formalization target

The mission goal is the universal assertion

$$\forall n\in\mathbb N,\quad n>0\Longrightarrow \exists m\in\mathbb N,\quad C^m(n)=1.$$

The existential index $m$ may be zero, so the case $n=1$ is included directly. The hypothesis $n>0$ excludes $0$, whose behavior under the total natural-number definition of $C$ is irrelevant to the conjecture.

The goal is the existing public prove2.me theorem collatz_conjecture, rather than a new copy. Its statement follows the Collatz declaration in the Formal Conjectures collection.

Significance

A proof would classify every positive-integer orbit with respect to reaching $1$. It would simultaneously rule out an orbit that escapes forever without visiting $1$ and any nontrivial cycle disjoint from $1$. Partial density results and finite computations establish neither universal exclusion.

The formalization goal is to make the universal quantifiers, parity split, finite iteration, and boundary cases explicit in Lean 4. Supporting contributions can isolate reusable facts about iterates, stopping times, accelerated odd-only maps, residue classes, and finite certificates. Such components may also support formal work on related piecewise-affine integer dynamical systems, while every contribution remains tied to a precisely stated theorem.

Difficulty

Individual trajectories can be computed, and many families of inputs can be reduced by elementary parity arguments, but the map combines contraction and expansion. Even steps halve the current value, while odd steps replace it by the larger value $3n+1$. Local information about a bounded initial segment of an orbit does not supply a uniform bound on all later values or on the time required to reach $1$.

Statistical control of most inputs also leaves exceptional inputs unresolved. Likewise, excluding cycles up to a finite length does not exclude longer cycles, and checking all inputs below a finite threshold does not constrain every larger input. The mission therefore requires statements whose quantifiers genuinely cover all positive natural numbers; a large finite computation or an almost-everywhere theorem cannot by itself close the goal.

Formalization scope

The existing Lean statement works over ℕ. Its local collatzStep definition branches on the proposition that $n$ is even, uses natural-number division by $2$ on the even branch, and uses $3n+1$ on the odd branch. Iteration is represented by the standard finite function iterate notation. The theorem quantifies over a positive starting value $n$ and asserts the existence of a finite iterate index $m$ at which the value is exactly $1$.

The positivity hypothesis is essential: the total function sends $0$ to $0$, so including $0$ would make the universal statement false. The mission does not replace the universal quantifier by a fixed numerical bound, and it does not encode a predetermined stopping-time limit. A complete solution must account for every positive starting value.

Useful supporting formalizations include exact relations between the classical and accelerated maps, composition laws for finite iteration, stopping-time predicates, cycle exclusion statements, descent criteria, and checked finite ranges. Each supporting theorem should state its own hypotheses and trust boundary explicitly. Computational artifacts are welcome when their finite scope is stated precisely and their result is connected to a Lean consumer through a checked certificate or another accepted verification boundary.

Selected references

• Jeffrey C. Lagarias, The $3x+1$ Problem and Its Generalizations, American Mathematical Monthly 92 (1985), 3–23. https://websites.umich.edu/~lagarias/3x%2B1.html
• Terence Tao, Almost All Orbits of the Collatz Map Attain Almost Bounded Values, 2019; published in Forum of Mathematics, Pi 10 (2022). https://arxiv.org/abs/1909.03562
• David Barina, Convergence Verification of the Collatz Problem, The Journal of Supercomputing 77 (2021), 2681–2688. https://doi.org/10.1007/s11227-020-03368-x
• Google DeepMind, Formal Conjectures: Collatz Conjecture, Lean 4 statement. https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/CollatzConjecture.lean

Motivation

A positive integer is perfect when it equals the sum of its proper divisors: $6 = 1 + 2 + 3$, $28 = 1 + 2 + 4 + 7 + 14$, then $496$, $8128$, and so on. Every perfect number anyone has ever exhibited is even. Whether an odd one exists is one of the oldest unsettled questions in mathematics, and it is unsettled in a strong sense: there is no heuristic consensus that odd perfect numbers should be absent for a structural reason, only an accumulating list of conditions any example would have to meet.

The even side of the question is completely resolved. Euclid (Elements IX.36) showed that if $2^p - 1$ is prime then $2^{p-1}(2^p - 1)$ is perfect; Euler proved the converse, so even perfect numbers correspond exactly to Mersenne primes. Nothing comparable is known on the odd side, and the literature instead consists of increasingly severe necessary conditions.

A timeline of what is actually proved about a hypothetical odd perfect number $N$:

• Euler (published posthumously in 1849): $N = p^k m^2$ with $p$ prime, $p \equiv k \equiv 1 \pmod 4$, and $p \nmid m$. In particular $N$ is not a perfect square.
• Servais (1887), Sylvester (1888): lower bounds on the number $\omega(N)$ of distinct prime divisors; Sylvester obtained $\omega(N) \ge 5$, and $\omega(N) \ge 8$ when $3 \nmid N$.
• Touchard (1953): $N \equiv 1 \pmod{12}$ or $N \equiv 9 \pmod{36}$. Shorter proofs were later given by Satyanarayana (1959) and Holdener (2002).
• Chein (1979) and Hagis (1980), independently: $\omega(N) \ge 8$; Nielsen (2007): $\omega(N) \ge 9$; Nielsen (2015): $\omega(N) \ge 10$.
• Nielsen (2003): an upper bound in terms of $\omega$, namely $N < 2^{4^{\omega(N)}}$ — the first bound of its kind, later sharpened by Nielsen himself.
• Ochem–Rao (2012): $N > 10^{1500}$; Ochem–Rao (2014): $N$ has at least $101$ prime factors counted with multiplicity.

None of these results, alone or together, rules out an odd perfect number.

Setting

For $n \ge 1$ write $\sigma(n) = \sum_{d \mid n} d$ for the sum of all positive divisors of $n$. Then $n$ is perfect exactly when

$$\sigma(n) = 2n,$$

equivalently when the divisors of $n$ other than $n$ itself sum to $n$. The function $\sigma$ is multiplicative: $\sigma(ab) = \sigma(a)\sigma(b)$ whenever $\gcd(a,b) = 1$, and $\sigma(p^a) = 1 + p + \cdots + p^a$ for a prime power. The quantity $\sigma(n)/n$ is the abundancy index of $n$, so a perfect number is one of abundancy index exactly $2$.

Write $\omega(n)$ for the number of distinct prime divisors of $n$. In Lean, $\omega(n)$ is n.primeFactors.card, and perfection is Mathlib's Nat.Perfect n, which unfolds to ∑ i ∈ n.properDivisors, i = n ∧ 0 < n — the positivity clause is part of the definition, so $n = 0$ is not perfect.

Formalization targets

Goal

$$\forall n \in \mathbb{N}, \quad \sigma(n) = 2n \ \Longrightarrow\ 2 \mid n.$$

Every perfect number is even; equivalently, no odd perfect number exists. This is the weakest statement that settles the question, and it fixes no constants, so no future numerical improvement can invalidate it.

Milestones

The milestones are the unconditional theorems of the literature listed above, each stated for a hypothetical odd perfect number $N$:

$$N = p^k m^2, \quad p \text{ prime}, \quad p \equiv k \equiv 1 \ (\mathrm{mod}\ 4), \quad p \nmid m \qquad \text{(Euler)}$$ $$N \text{ is not a perfect square} \qquad \text{(Euler)}$$ $$\omega(N) \ge 3, \qquad \omega(N) \ge 5 \qquad \text{(Servais, Sylvester)}$$ $$N \equiv 1 \ (\mathrm{mod}\ 12) \quad \text{or} \quad N \equiv 9 \ (\mathrm{mod}\ 36) \qquad \text{(Touchard)}$$ $$N < 2^{4^{\omega(N)}} \qquad \text{(Nielsen)}$$

Significance

The result itself. A proof of the goal would complete the classification of perfect numbers begun by Euclid: together with the Euclid–Euler theorem, every perfect number would be $2^{p-1}(2^p-1)$ for a Mersenne prime $2^p - 1$. A disproof — an explicit odd perfect number — would be an object with at least ten distinct prime factors and more than $1500$ decimal digits, and would immediately settle a long list of dependent questions about the abundancy index, about the distribution of the values of $\sigma$, and about the multiperfect numbers.

Formalizing it. Only the even half of the theory is currently formalized: the Euclid–Euler theorem is available in Mathlib's Archive (Archive/Wiedijk100Theorems/PerfectNumbers.lean, as Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect and Theorems.perfect_iff_even_and_mersenne), and the main library carries the divisor-sum API around Nat.Perfect in Mathlib/NumberTheory/Divisors.lean, but nothing about the odd case. None of the milestones above is in Mathlib; formalizing them builds the missing $\sigma$-arithmetic infrastructure — factor chains, abundancy estimates, and the parity analysis of $\sigma$ on odd numbers — that any attack on the goal, or any future formalization of the computational bounds, will need.

Difficulty

The obvious approach — take Euler's form $N = p^k m^2$ and push the congruence conditions until they conflict — does not terminate. There is no known local obstruction: the equation $\sigma(N) = 2N$ has no contradiction modulo any fixed integer, so no congruence argument can close the problem. The known results are all of a different type: they exclude configurations of the prime factorization by finite case analysis on factor chains, and each analysis leaves infinitely many admissible configurations. Increasing $\omega$ weakens the constraints rather than strengthening them, which is why the lower bounds on $\omega$ have advanced by one prime factor per decade at very high computational cost. The upper bound $N < 2^{4^{\omega(N)}}$ makes the search space finite for each fixed $\omega$, but astronomically so.

Formalization scope

The development is stated over ℕ with Mathlib's Nat.Perfect, so positivity is built into the hypothesis and no separate 0 < n assumption appears. Oddness is Odd n, the number of distinct prime divisors is n.primeFactors.card, and Euler's form is stated with explicit residues p % 4 = 1, k % 4 = 1, together with ¬ p ∣ m and n = p ^ k * m ^ 2. No custom definitions are introduced; everything rests on Mathlib's Nat.sigma / Nat.Perfect API.

One caution on the shape of the milestones. Each is stated conditionally, for an $n$ assumed both perfect and odd, so each would follow trivially from the goal theorem. The point of the milestones is precisely that they are proved unconditionally in the literature: a submission is expected to reproduce (or improve on) the published argument, not to derive the statement from an unproved conjecture. Since the goal is itself open on the platform, no admissible proof can take that shortcut.

Contributions welcome: any of the milestones, the supporting multiplicativity and abundancy lemmas needed for them, and reusable infrastructure for $\sigma$ on odd numbers. Sharper published bounds — larger values of $\omega$, the improved Nielsen bound $N < 2^{4^{\omega(N)} - 2^{\omega(N)}}$, the Ochem–Rao size bound — are also in scope and are strictly stronger than the milestones listed.

Selected references

• L. Euler, De numeris amicabilibus, Commentationes arithmeticae 2 (1849), 627–636.
• J. J. Sylvester, Sur les nombres parfaits, Comptes Rendus de l'Académie des Sciences CVI (1888), 403–405.
• J. Touchard, On prime numbers and perfect numbers, Scripta Mathematica 19 (1953), 35–39.
• J. A. Holdener, A theorem of Touchard on the form of odd perfect numbers, American Mathematical Monthly 109 (2002), 661–663.
• P. P. Nielsen, An upper bound for odd perfect numbers, INTEGERS: Electronic Journal of Combinatorial Number Theory 3 (2003), #A14.
• P. P. Nielsen, Odd perfect numbers have at least nine distinct prime factors, Mathematics of Computation 76 (2007), 2109–2126.
• P. P. Nielsen, Odd perfect numbers, Diophantine equations, and upper bounds, Mathematics of Computation 84 (2015), 2549–2567.
• P. Ochem and M. Rao, Odd perfect numbers are greater than $10^{1500}$, Mathematics of Computation 81 (2012), 1869–1877.
• P. Ochem and M. Rao, On the number of prime factors of an odd perfect number, Mathematics of Computation 83 (2014), 2435–2439.
• Overview and further pointers: https://en.wikipedia.org/wiki/Perfect_number

1. Motivation

Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, stated unambiguously — by machine.

This mission ports a coherent slice of that material to Prove2Me. It is deliberately a portfolio mission: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. A reader should not assume that proving a milestone advances the goal theorem. The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked.

A rough timeline of the collection's landmarks:

• 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
• 1962 — Radó: the busy beaver function outgrows every computable function.
• 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$.
• 1978 — Apéry: $\zeta(3)$ is irrational.
• 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant subspace.
• 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
• 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
• 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
• 2021 — Gardam: Kaplansky's unit conjecture is false (its zero-divisor and idempotent companions remain open).
• 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$.
• 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$.

2. Setting

The goal theorem concerns prime values of polynomials. Fix a finite set $S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the Bunyakovsky condition if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is irreducible over $\mathbb{Z}$; say that $S$ satisfies the Schinzel condition if for every prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides the product at every argument.

For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some $f_i$ vanishes, let $D=\prod_i \deg f_i$, and let

$$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$

The Bateman–Horn constant is the (conditionally convergent) Euler product

$$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$

The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property $\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function $\mathrm{BB}$.

3. Target

The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, $C$ exists and is positive and

$$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$

Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$, Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the $1/3$–$2/3$ conjecture), and computability (Radó's theorem).

4. Significance

The results themselves. Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right.

Formalizing them. None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$ cannot both be algebraic, and Radó's diagonal argument.

5. Difficulty

For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound $\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered infinite product changes the statement.

Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on $\ell^1$ show that no soft argument can work.

6. Formalization scope

Conventions this mission commits to, all fixed in the definition items:

• Polynomials are elements of ℤ[X]; primality of a polynomial value is primality of its absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$.
• The Bateman–Horn constant is the limit of the ordered partial products over $p<N$, not an unordered infinite product.
• Kakeya sets carry no compactness or measurability hypothesis, matching the source; the conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$.
• Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$.
• Torsion-freeness of a group is spelled out as "every element of finite order is the identity", which is the hypothesis the source intends (it is weaker than Mathlib's IsMulTorsionFree).
• Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities are quotients of set cardinalities in $\mathbb{Q}$.
• The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition included, and $\mathrm{BB}(0)=0$.
• Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me statements must be definite, so each such question is recorded in its affirmative form (e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth theorem rather than guessed at.
• Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).

Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission.

7. Selected references

• P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Math. Comp. 16 (1962), 363–367. DOI
• T. Radó, On non-computable functions, Bell System Tech. J. 41 (1962), 877–884. DOI
• R. O. Davies, Some remarks on the Kakeya problem, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. DOI
• C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$, Bull. London Math. Soc. 17 (1985), 305–317. DOI
• K. Falconer, On the Hausdorff dimensions of distance sets, Mathematika 32 (1985), 206–212. DOI
• W. Zudilin, One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational, Russian Math. Surveys 56 (2001), 774–776. DOI
• P. Mihăilescu, Primary cyclotomic units and a proof of Catalan's conjecture, J. reine angew. Math. 572 (2004), 167–195. DOI
• Z. Dvir, On the size of Kakeya sets in finite fields, J. Amer. Math. Soc. 22 (2009), 1093–1097. DOI
• B. Bukh and T.-W. Chao, Sharp density bounds on the finite field Kakeya problem, Discrete Analysis 26 (2021). DOI
• G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021), 967–979. DOI
• K. Saito, Mills' constant is irrational, Mathematika 71 (2025), e70027. arXiv:2404.19461
• H. Wang and J. Zahl, Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions, arXiv:2502.17655
• Google DeepMind, Formal Conjectures, Apache-2.0, github.com/google-deepmind/formal-conjectures

---

Provenance note. The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; those read-backs are non-blind — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.

What the constant is

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

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

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

What is being asked

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

The goal theorem of this mission is transcendence,

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

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

What is actually known

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

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

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

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

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

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

Timeline

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

Formalization notes

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

Motivation

A polynomial $f \in \mathbb{Q}[x]$ is split if $\deg f \ge 1$ and $f(x) = a\prod_{i=1}^{n}(x - r_i)$ for some $a \in \mathbb{Q}^\times$ and $r_1,\dots,r_n \in \mathbb{Q}$. Split polynomials are the simplest non-constant maps defined over $\mathbb{Q}$ that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into $\mathbb{Q}$.

Say $\alpha$ is $k$-collapsible if there are split $f_1,\dots,f_k$ with $(f_k \circ \cdots \circ f_1)(\alpha) \in \mathbb{Q}$, collapsible if it is $1$-collapsible, and eventually collapsible if it is $k$-collapsible for some $k \ge 1$. Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree $3$: Jordi Ribes settled the cubic case of eventual collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is $\deg\alpha \ge 4$. For the one-step notion the picture is different — degrees $1$ and $2$ are settled, and degree $3$ is open. That one-step cubic case is this mission's goal.

Setting

Let $\alpha$ be an algebraic number with $[\mathbb{Q}(\alpha):\mathbb{Q}] = 3$. After an affine change of variable over $\mathbb{Q}$ one may assume $\alpha$ is a root of a depressed cubic

$$m(x) = x^3 + d\,x + e, \qquad d, e \in \mathbb{Q},$$

with discriminant $\Delta = \operatorname{disc}(m) = -4d^3 - 27e^2$. When $\Delta > 0$ the cubic is totally real (three real roots); when $\Delta < 0$ it has one real root and a complex-conjugate pair. In the latter case write the roots as

$$\alpha_1 = -2u, \qquad \alpha_{2,3} = u \pm iv, \qquad d = v^2 - 3u^2, \quad e = 2u(u^2 + v^2),$$

and set $\psi = \arctan(3u/v)$, the parameter that controls the archimedean obstruction below. Scaling $\alpha \mapsto w\alpha$ sends $(d,e) \mapsto (w^2 d, w^3 e)$, so the single rational invariant

$$\tau = e^2/d^3$$

determines the problem up to scaling: the search space is one rational parameter, not two.

Formalization targets

Goal — every cubic algebraic number is collapsible

$$\forall\, \alpha \in \mathbb{C}, \quad [\mathbb{Q}(\alpha):\mathbb{Q}] = 3 \ \Longrightarrow\ \exists\, f \text{ split with } f(\alpha) \in \mathbb{Q}.$$

This is the weakest statement that settles the case: it fixes no bound on $\deg f$, and asserts only that some split $f$ exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.

Supporting targets

The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:

1. the product criterion — $\alpha$ is collapsible iff $\prod_i(\alpha - r_i) \in \mathbb{Q}$ for some nonempty finite multiset of rationals, which turns collapsibility into a multiplicative relation in $K^\times/\mathbb{Q}^\times$;
2. affine invariance, and the completeness of $\tau$ as an invariant of the scaling action, which together justify the reduction to one parameter;
3. two sufficient conditions: square discriminant, and the power-family condition subsuming it;
4. three obstructions: gap parity in the totally real case; the archimedean degree bound when $\Delta < 0$; and the extension of that bound beyond cubics, to any algebraic number possessing both a real and a non-real conjugate.

The mission also carries, as a plain theorem rather than a milestone, the single open instance $x^3 + 6x + 1$ — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.

Significance

A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree $3$. A disproof would be at least as informative: a single cubic $\alpha$ admitting no split $f$ with $f(\alpha) \in \mathbb{Q}$ would separate $1$-collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.

The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing $\deg f \to \infty$, and it is what rules out a uniform-degree approach.

Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are not proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance $x^3 + 6x + 1$ and the goal itself are open.

Difficulty

The obvious approach is to write down a split $f$ with rational roots and force $f(\alpha) \in \mathbb{Q}$ by solving for the roots. This works when $\Delta$ is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.

Suppose $\Delta < 0$ and $f = a\prod_i(x - r_i)$ is split with $f(\alpha) \in \mathbb{Q}$. Irreducibility of $m$ forces $f - c$ to be divisible by $m$, hence $f(\alpha_1) = f(\alpha_2) \ne 0$, hence $\prod_i \frac{\alpha_1 - r_i}{\alpha_2 - r_i} = 1$. Each factor lies on a fixed circle through $0$ and $1$ determined by $\psi$, and a convexity argument on $\log\cos$ then forces

$$\deg f \ \ge\ \pi/\psi.$$

As $\tau \to 0^+$ one has $\psi \to 0$, so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For $x^3 + 6x + 1$ the bound already gives $\deg f \ge 32$, which is why that cubic resists the searches that settle its neighbours.

Only one step of this argument is special to cubics: the identification of the circle parameter as $3u/v$. For an algebraic number of any degree with a real conjugate $\alpha_1$ and a non-real conjugate $\alpha_2$, irreducibility gives the same relation $\prod_i (\alpha_1 - r_i)/(\alpha_2 - r_i) = 1$, the images again lie on a circle through $0$ and $1$, and the parameter is $\lambda = (\operatorname{Re}\alpha_2 - \alpha_1)/\operatorname{Im}\alpha_2$, which specialises to $3u/v$ in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.

In the totally real case ($\Delta > 0$) the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto $\widehat{\mathbb{R}}$ — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of $f$. Whether degrees stay bounded there is itself unsettled.

Formalization scope

Representation. IsSplit f says $0 < \deg f$ and $f = C\,a \cdot \prod_{r \in rs}(X - r)$ for a nonzero rational $a$ and a multiset $rs$ of rationals; multiplicities are therefore allowed and the roots need not be distinct. Collapsible α is stated for $\alpha$ in an arbitrary field $K$ carrying a $\mathbb{Q}$-algebra structure, not only for $K = \mathbb{C}$, so the results apply verbatim to a root in $\mathbb{R}$, in $\mathbb{C}$, or in $\mathbb{Q}[x]/(m)$. The goal theorem is stated over $\mathbb{C}$, with "cubic" expressed as $\deg(\operatorname{minpoly}_{\mathbb{Q}}\alpha) = 3$.

Ruling out a trivialisation. Collapsible places no lower bound on $\deg f$ and does not require the value $c = f(\alpha)$ to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: $c = 0$ would make $m \mid f$, impossible for an irreducible cubic $m$ dividing a polynomial that splits over $\mathbb{Q}$. Constant $f$ is excluded by $0 < \deg f$. Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.

Conventions in the archimedean milestones. In the cubic bound the parameters $u, v$ enter as real numbers satisfying the factorisation identity, with the normalisation $0 < uv$; this is not a restriction, since $v$ is determined only up to sign and the sign may be chosen. Under it $\psi = \arctan(3u/v) \in (0, \pi/2)$, and the conclusion is $\pi/\psi \le \deg f$ with $\deg f$ the natural-number degree.

In the general bound the corresponding normalisation is $0 < (\operatorname{Re}\alpha_2 - \alpha_1)\operatorname{Im}\alpha_2$. It forces $\operatorname{Im}\alpha_2 \neq 0$, so $\alpha_2$ is genuinely non-real and $\lambda > 0$, hence $\psi \in (0,\pi/2)$ and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of $\alpha_2$ flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when $\operatorname{Re}\alpha_2 = \alpha_1$, which the hypothesis excludes and which cannot occur for a depressed cubic with $\Delta<0$. No degree hypothesis on $m$ is needed: possessing both a real and a non-real root already forces $\deg m \ge 3$.

Infrastructure. A complete development needs Polynomial, Multiset, minpoly, and for the archimedean bound Real.arctan, Complex.arg, and strict concavity of $\log\cos$ on $(-\pi/2, \pi/2)$. The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of $x^3 + 6x + 1$ of any degree.

Selected references

• Griffin Macris, List of open problems, Problem 3. https://sites.google.com/view/griffinmacris/open-problems
• Miles, Collapsible algebraic numbers, 2026. https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ — source of the definitions of split, $k$-collapsible, collapsible and eventually collapsible used above, of Ribes's cubic result for eventual collapsibility, and of the statement that the degree-$3$ case of one-step collapsibility is open.

Motivation

An elliptic curve over $\mathbb{Q}$ is a smooth cubic curve with a rational point. Its rational points form a finitely generated abelian group $E(\mathbb{Q})$ (Mordell, 1922), so $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$ for an integer $r \ge 0$, the rank. No algorithm is known that decides, for a given curve, whether $r > 0$, i.e. whether there are infinitely many rational points. The Birch and Swinnerton-Dyer conjecture predicts $r$ from an analytic object, the Hasse–Weil $L$-function $L(E,s)$: it asserts that $r$ equals the order of vanishing of $L(E,s)$ at $s = 1$. It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute; the official formulation is Andrew Wiles' problem description, The Birch and Swinnerton-Dyer Conjecture (2000). This mission formalizes that statement, its weak form, and the results Wiles lists as known.

Timeline.

• 1922: L. Mordell (Proc. Cambridge Phil. Soc. 21) proves that $E(\mathbb{Q})$ is finitely generated, answering a question of Poincaré (1901).
• 1936: H. Hasse proves $|p + 1 - \#E(\mathbb{F}_p)| \le 2\sqrt p$ at primes of good reduction, so the Euler product for $L(E,s)$ converges for $\operatorname{Re} s > 3/2$; he conjectures that $L(E,s)$ continues to an entire function.
• 1965: B. Birch and H. P. F. Swinnerton-Dyer, Notes on elliptic curves II, state the conjecture, found experimentally on the EDSAC computer.
• 1977: J. Coates and A. Wiles, On the conjecture of Birch and Swinnerton-Dyer: for curves with complex multiplication, $L(E,1) \ne 0$ implies $E(\mathbb{Q})$ finite.
• 1986: B. Gross and D. Zagier, Heegner points and derivatives of L-series: for modular $E$ with $L(E,1) = 0 \ne L'(E,1)$, a Heegner point has infinite order.
• 1989–1990: V. Kolyvagin, Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves: for modular $E$ with $L(E,s)$ vanishing to order at most $1$ at $s=1$, the rank equals that order (with a non-vanishing theorem of Bump–Friedberg–Hoffstein and Murty–Murty).
• 1995–2001: A. Wiles (Ann. Math. 141), R. Taylor and A. Wiles (Ann. Math. 141), and C. Breuil, B. Conrad, F. Diamond and R. Taylor (J. Amer. Math. Soc. 14): every elliptic curve over $\mathbb{Q}$ is modular, so $L(E,s)$ is entire and Kolyvagin's theorem applies to all $E/\mathbb{Q}$.
• 2000: the Clay Mathematics Institute adopts Wiles' formulation as a Millennium Prize Problem.
• 2014: M. Bhargava, C. Skinner and W. Zhang, A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture: the rank conjecture holds for more than $66\%$ of curves ordered by height. The general case is open.

Setting

A Weierstrass equation over $\mathbb{Q}$ is

$$E :\ y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6, \qquad a_i \in \mathbb{Q},$$

with discriminant $\Delta$; in Lean, WeierstrassCurve ℚ. It is an elliptic curve when $\Delta \ne 0$ (Mathlib's typeclass IsElliptic). Its rational points $E(\mathbb{Q})$ are the rational solutions $(x,y)$ together with the point at infinity $O$, an abelian group under the chord-and-tangent law (W.toAffine.Point). The rank is the rank of this group as a $\mathbb{Z}$-module, $r = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}) \qquad \text{(`BSD.rank W`)},$ the $r$ in $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$.

The Hasse–Weil $L$-series is built prime by prime. For each prime $p$ take a Weierstrass equation for $E$ that is minimal at $p$ (integral coefficients, with the $p$-adic valuation of $\Delta$ as small as possible) and reduce it modulo $p$; put $a_p = p + 1 - \#\tilde E(\mathbb{F}_p)$ when the reduction is smooth (good reduction). The local factor is

$$L_p(E,s) = \begin{cases} (1 - a_p p^{-s} + p^{1-2s})^{-1} & \text{good reduction,}\\ (1 - p^{-s})^{-1} & \text{split multiplicative reduction,}\\ (1 + p^{-s})^{-1} & \text{non-split multiplicative reduction,}\\ 1 & \text{additive reduction,}\end{cases}$$

and $L(E,s) = \prod_p L_p(E,s) = \sum_{n \ge 1} a_n n^{-s}$, convergent for $\operatorname{Re} s > 3/2$ by Hasse's bound. In Lean this is Mathlib's WeierstrassCurve.LSeries W s, defined by exactly this recipe (WeierstrassCurve.LFunction is the arithmetic function $n \mapsto a_n$, an Euler product of local factors computed on a model minimal at each prime); where the Dirichlet series does not converge, Mathlib's LSeries takes the junk value $0$. This is the complete $L$-series $L^*(C,s)$ of Wiles' Remark 1; it differs from the incomplete product over $p \nmid 2\Delta$ in Wiles' display by finitely many factors holomorphic and non-zero at $s = 1$, so both have the same order of vanishing there.

An $L$-function of $E$ is an entire function $\Lambda : \mathbb{C} \to \mathbb{C}$ with $\Lambda(s) = L(E,s)$ for $\operatorname{Re} s > 3/2$ (BSD.IsLFunction W Λ). By the identity theorem there is at most one; by modularity there is exactly one. The order of vanishing of $\Lambda$ at $s = 1$ is the $m$ with $\Lambda(s) = c(s-1)^m + \dots$, $c \ne 0$; in Lean, analyticOrderAt Λ 1, valued in $\mathbb{N} \cup \{\infty\}$, with value $\infty$ exactly when $\Lambda$ vanishes identically near $1$.

Formalization targets

Goal: the Birch and Swinnerton-Dyer conjecture (BSD.birch_swinnerton_dyer)

For every elliptic curve $E$ over $\mathbb{Q}$ there is an entire $\Lambda$ agreeing with $L(E,s)$ on $\operatorname{Re} s > 3/2$ such that

$$\operatorname{ord}_{s=1} \Lambda = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}).$$

This is Wiles' Conjecture (Birch and Swinnerton-Dyer): $L(C,s) = c(s-1)^r + \text{higher order terms}$ with $c \ne 0$ and $r = \operatorname{rank} C(\mathbb{Q})$. Open.

Weaker target: the weak conjecture (BSD.weak_birch_swinnerton_dyer)

There is an $L$-function $\Lambda$ of $E$ with $\Lambda(1) = 0$ if and only if $E(\mathbb{Q})$ is infinite. Wiles: "In particular this conjecture asserts that $L(C,1) = 0 \Leftrightarrow C(\mathbb{Q})$ is infinite." Open.

Milestones: what Wiles lists as known

1. Mordell's theorem (BSD.mordell): $E(\mathbb{Q})$ is a finitely generated abelian group.
2. Convergence of the $L$-series (BSD.lSeriesSummable): $\sum a_n n^{-s}$ converges for $\operatorname{Re} s > 3/2$. Wiles: "this Euler product is then known to converge for $\operatorname{Re}(s) > 3/2$."
3. Analytic continuation (BSD.exists_isLFunction): $E$ has an $L$-function. Wiles: Hasse's conjecture, "now been proved" by Wiles, Taylor–Wiles and Breuil–Conrad–Diamond–Taylor.
4. Gross–Zagier–Kolyvagin (BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one): if an $L$-function of $E$ vanishes to order at most $1$ at $s = 1$, its order equals the rank. Wiles: "If $L(C,s) \sim c(s-1)^m$ with $c \ne 0$ and $m = 0$ or $1$, then the conjecture holds."

A bridging lemma, BSD.isLFunction_unique, records that an $L$-function of $E$ is unique when it exists.

Significance

The result itself. The conjecture makes the finiteness of $E(\mathbb{Q})$ decidable from $L(E,1)$ and, in its refined form, gives an effective procedure for finding generators (Manin, 1971). Conditionally on it, Tunnell (1983) characterises the congruent numbers, the areas of right triangles with rational sides, a problem open since the tenth century. It is the prototype of the conjectures of Tate, Deligne, Beilinson and Bloch–Kato relating ranks of arithmetic groups to orders of vanishing of $L$-functions.

Formalizing it. None of the statements in this mission has a machine-checked proof. Mathlib provides the objects: the group law on $E(\mathbb{Q})$, minimal models and reduction types over discrete valuation rings, and the Hasse–Weil $L$-series as a Dirichlet series (2025–2026). It does not contain Mordell's theorem (no theory of heights), Hasse's bound, modularity, or the continuation of $L(E,s)$. On this platform, earlier library entries named birch_swinnerton_dyer are retired placeholders whose formal statements reduce to trivialities such as $0 = 0$; they carry a notice saying so and are not formalizations of the conjecture. This mission gives the first faithful statement against Mathlib's own $L$-series. Two published platform results bear directly on the milestones: the descent step WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex (finite index of $2E(\mathbb{Q})$ implies finite generation) reduces milestone 1 to the weak Mordell–Weil theorem, and WeierstrassCurve.modularity_of_semistableModel from the platform's Fermat's Last Theorem development proves modularity of semistable curves for a notion of modularity defined through eigenform coefficients; relating that notion to WeierstrassCurve.LSeries would give milestone 3 for semistable curves.

Difficulty

Neither side of the equation is computable in general. On the algebraic side, descent bounds the rank from above by the rank of a Selmer group, but the gap is the Tate–Shafarevich group Ш$(E)$, which is not known to be finite; the obvious plan, compute the Selmer group and show it has the rank of $E(\mathbb{Q})$, founders on Ш. On the analytic side one can certify $\Lambda(1) \ne 0$ or $\Lambda'(1) \ne 0$ numerically but cannot certify an exact zero, and the only known bridge from $L$-values to rational points, the Heegner point construction, produces at most one independent point. This is why milestone 4 stops at order $\le 1$ and the conjecture is not known for a single curve of rank $\ge 2$. Iwasawa theory (Kato, Skinner–Urban) relates $p$-adic $L$-functions to Selmer groups but yields $p$-adic, not Archimedean, orders of vanishing.

The formalization adds its own obstacles: milestone 1 needs heights and the weak Mordell–Weil theorem (Kummer theory over number fields, finiteness of class groups and units); milestone 2 needs Hasse's bound, i.e. the degree of the Frobenius endomorphism; milestones 3 and 4 rest on modularity, Galois representations, modular curves and Euler systems.

Formalization scope

• $E$ is any WeierstrassCurve ℚ with IsElliptic ($\Delta \ne 0$); no minimality or integrality of the model is assumed. Mathlib's $L$-series passes to a minimal model at each prime internally, and the point group depends only on the curve, so every statement is invariant under change of Weierstrass equation.
• The rank is Module.finrank ℤ W.toAffine.Point: for a finitely generated abelian group, the $r$ in $\mathbb{Z}^r \oplus T$; for a group of infinite rank Mathlib's finrank is $0$, a case milestone 1 excludes.
• The $L$-series is Mathlib's WeierstrassCurve.LSeries, with all Euler factors including the bad primes, and junk value $0$ where the Dirichlet series diverges. BSD.IsLFunction constrains $\Lambda$ only on $\operatorname{Re} s > 3/2$; milestone 2 shows the series is genuine there, and the bridging lemma shows $\Lambda$ is then unique.
• The order of vanishing is analyticOrderAt Λ 1 : ℕ∞; equating it with a natural number asserts in particular that $\Lambda \not\equiv 0$ near $1$.

No trivializing formalization. The existential $\Lambda$ cannot be chosen freely: it must agree with the honest, non-zero Dirichlet series on a half-plane, so it is unique, and $\Lambda \equiv 0$ is excluded by the finite value of the rank. Without IsElliptic the statements would concern singular cubics, whose point group is $\mathbb{Q}$ or $\mathbb{Q}^\times$; the hypothesis is required, not decorative.

Out of scope. The refined conjecture (the leading coefficient in terms of Ш$(E)$, the regulator, the real period and the Tamagawa numbers), the finiteness of Ш$(E)$, number fields and abelian varieties, and the functional equation of $L(E,s)$.

Infrastructure needed and welcome contributions. Heights on $E(\mathbb{Q})$ and the weak Mordell–Weil theorem; Hasse's bound and the multiplicativity of $a_n$; a bridge from Mathlib's WeierstrassCurve.LSeries to the $L$-series of a weight-two newform, so that existing modularity results yield milestone 3; Heegner points and Kolyvagin's Euler system for milestone 4; and the bridging lemma, provable now from the identity theorem. Decompositions of every milestone and lemmas about WeierstrassCurve.LFunction (its values at primes, multiplicativity, independence of the model) are welcome.

Selected references

• A. Wiles, The Birch and Swinnerton-Dyer Conjecture, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf
• B. J. Birch, H. P. F. Swinnerton-Dyer, Notes on elliptic curves II, Journal für die reine und angewandte Mathematik 218 (1965), 79–108. https://doi.org/10.1515/crll.1965.218.79
• L. J. Mordell, On the rational solutions of the indeterminate equations of the third and fourth degrees, Proceedings of the Cambridge Philosophical Society 21 (1922), 179–192.
• J. Coates, A. Wiles, On the conjecture of Birch and Swinnerton-Dyer, Inventiones Mathematicae 39 (1977), 223–251. https://doi.org/10.1007/BF01402975
• B. H. Gross, D. B. Zagier, Heegner points and derivatives of L-series, Inventiones Mathematicae 84 (1986), 225–320. https://doi.org/10.1007/BF01388809
• V. A. Kolyvagin, Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves, Mathematics of the USSR-Izvestiya 32 (1989), 523–541. https://doi.org/10.1070/IM1989v032n03ABEH000779
• A. Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559
• R. Taylor, A. Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560
• C. Breuil, B. Conrad, F. Diamond, R. 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
• J. B. Tunnell, A classical Diophantine problem and modular forms of weight 3/2, Inventiones Mathematicae 72 (1983), 323–334. https://doi.org/10.1007/BF01389327
• M. Bhargava, C. Skinner, W. Zhang, A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture, 2014. https://arxiv.org/abs/1407.1826
• J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009. https://doi.org/10.1007/978-0-387-09494-6