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

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

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

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)

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.

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

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

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

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.

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

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

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

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

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$

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

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

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

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

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

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

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$:

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

Motivation

How well can an irrational number be approximated by fractions? Dirichlet's pigeonhole argument shows that every irrational $x$ has infinitely many fractions with $|x-p/q|<q^{-2}$. The irrationality exponent $\mu(x)$ measures how much better than this the best approximations can be: it is the supremum of the exponents $\nu$ for which $|x-p/q|<q^{-\nu}$ has infinitely many solutions. Almost every real number has $\mu=2$, as do all algebraic irrationals (Roth's theorem), but for specific transcendental constants such as $\pi$ proving any finite bound is hard, and the expected value $2$ has been conjectured for decades (recorded, in its $\varepsilon$-dependent form, in Waldschmidt, Open Diophantine problems, Moscow Math. J. 2004, p. 265). Upper bounds on $\mu(\pi)$ also control how often integers come close to multiples of $\pi$, which decides convergence of series such as the Flint–Hills series $\sum_{n\ge1}1/(n^3\sin^2 n)$.

This mission asks for a formal proof that $\mu(\pi)=2$, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1953 — Mahler proves the first finite bound, $\mu(\pi)\le42$ (eventually $30$) (On the approximation of $\pi$, Proc. KNAW 1953).
• 1974 — Mignotte improves this to $21$ (eventually $20$) (Journées arithmétiques 1974).
• 1993 — Hata's integrals give $\mu(\pi)\le8.0160\ldots$ (Acta Arith. 1993).
• 2008–2010 — Salikhov's symmetric integrals give $7.6063\ldots$ (Russian Math. Surveys 2008; Math. Notes 2010).
• 2011–2022 — Alekseyev shows Flint–Hills convergence requires $\mu(\pi)\le5/2$ (arXiv:1104.5100); Meiburg shows $\mu(\pi)<5/2$ suffices (arXiv:2208.13356).
• 2020 — Zeilberger and Zudilin obtain $7.103205334137\ldots$ (Moscow J. Comb. Number Theory 2020).
• September 2026 — Bai claims $7.101862832357$ (arXiv:2609.11276); the OpenAI preprint claims $\mu(\pi)=2$ (Theorem 1.1, p. 1).

Setting

For an irrational real $x$,

Equivalently, $\mu(x)\le\nu_0$ means that for every $\nu>\nu_0$ only finitely many reduced fractions approximate $x$ to within $q^{-\nu}$. Here $\pi$ is the usual circle constant, Real.pi.

Formalization targets

Goal: Theorem 1.1 (p. 1)

The Lean goal is the conjunction of:

1. for every real $\nu>2$ there is an integer $Q\ge2$ such that

2. $\sup\{\nu>0:\ \text{infinitely many } r\in\mathbb Q \text{ with denominator}\ge2 \text{ satisfy } 0<|\pi-r|<\operatorname{den}(r)^{-\nu}\}=2$, i.e. $\mu(\pi)=2$.

Part 1 is the quantitative form stated in Theorem 1.1; it applies to all numerators and denominators, reduced or not. The threshold $Q(\nu)$ is allowed to depend on $\nu$ and is not effective in the source.

Significance

The result itself. It settles the value of the irrationality exponent of $\pi$, previously bounded only by about $7.1$. It does not claim a uniform bound $|\pi-p/q|\ge c/q^2$ (equivalently, bounded continued-fraction partial quotients), which remains a different question. As a consequence the preprint derives convergence of the Flint–Hills series (Corollary 1.2, p. 1) and, more generally, that $\sum_n 1/(n^a|\sin n|^b)$ converges if and only if $a>\max\{1,b\}$ (Corollary 5.2, p. 20).

Formalizing it. The statement is elementary and fully expressible with real numbers and integers, so a formal proof certifies it without definitional subtleties. The proof combines a weighted multivariable interpolation theorem (zero estimates, intersection-theoretic positivity on blowups) with an interpolation-determinant argument. Mathlib has Liouville-type results and continued fractions, but none of the zero-estimate or interpolation-determinant machinery; those would be reusable for transcendence proofs generally. No machine-checked finite bound on $\mu(\pi)$ is known.

Difficulty

The classical route to bounds on $\mu(\pi)$ constructs explicit integrals or Padé approximants with small values and controlled denominators; each refinement lowers the bound slightly, and these methods have no visible path to the value $2$. The preprint instead argues by contradiction from a sequence of successively separated exceptional approximations (Section 1.2, p. 2). Two incompatible estimates are needed for one nonzero determinant: an arithmetic lower bound after clearing denominators (Lemma 3.1, p. 13) and an analytic upper bound (Proposition 3.4, p. 16). Nonvanishing requires an interpolation theorem at centers whose locations are not known in advance (Theorem 2.1, p. 4), and a dimension count alone does not give full rank at these special centers; this is where the curve inequality (Proposition 2.3, p. 7) enters.

Formalization scope

• The goal is a statement about Real.pi, integers and rationals only; there is no auxiliary definition file.
• Part 1 quantifies over all integers p q with Q ≤ q, using Real.rpow for $q^{-\nu}$ (here $q\ge Q\ge2>0$).
• Part 2 uses sSup in ℝ of the set of $\nu>0$ with infinitely many rationals r (in lowest terms, r.den ≥ 2) satisfying the strict inequalities. Since the goal asserts the value $2$, the default sSup conventions for empty or unbounded sets cannot make it trivially true: the set must be nonempty, bounded above, with supremum exactly $2$.
• Part 2 follows from Part 1 and Dirichlet's theorem; both are included so that the goal states the exponent literally.

Welcome contributions: Dirichlet's approximation theorem in the form needed for Part 2, Siegel-type lemmas, and determinant estimates over $\mathbb Q(i)$.

Selected references

• OpenAI, The irrationality exponent of π is 2, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-irrationality-exponent-of-pi-is-2-September-24-2026/paper.pdf
• K. Mahler, On the approximation of π, Proc. Kon. Ned. Akad. Wet. A 56 (1953). https://ems.press/books/dms/252/4986
• M. Mignotte, Approximations rationnelles de π et quelques autres nombres, Journées arithmétiques (Grenoble, 1973), Mém. SMF 37 (1974). https://doi.org/10.24033/msmf.139
• M. Hata, Rational approximations to π and some other numbers, Acta Arith. 63 (1993), 335–349. https://doi.org/10.4064/aa-63-4-335-349
• V. Kh. Salikhov, On the irrationality measure of π, Russian Math. Surveys 63 (2008). https://doi.org/10.1070/RM2008v063n03ABEH004543
• D. Zeilberger, W. Zudilin, The irrationality measure of π is at most 7.103205334137…, Moscow J. Comb. Number Theory 9 (2020). https://doi.org/10.2140/moscow.2020.9.407
• M. Waldschmidt, Open Diophantine problems, Moscow Math. J. 4 (2004). https://webusers.imj-prg.fr/~michel.waldschmidt/articles/pdf/odp.pdf
• M. A. Alekseyev, On convergence of the Flint Hills series, arXiv:1104.5100 (2011). https://arxiv.org/abs/1104.5100v1
• A. Meiburg, Bounds on irrationality measures and the Flint-Hills series, arXiv:2208.13356 (2022). https://arxiv.org/abs/2208.13356v1
• K. F. Roth, Rational approximations to algebraic numbers, Proc. ICM 1958 (1960).
• M. Laurent, Sur quelques résultats récents de transcendance, Astérisque 198–200 (1991). https://www.numdam.org/item/AST_1991__198-199-200__209_0/

Rational approximation to π

Rational numbers approximate π to different degrees of accuracy. A useful question is how the error depends on the denominator, rather than how many decimal digits a particular fraction happens to match. The irrationality measure records the boundary between exponents that allow infinitely many exceptionally close rational approximations and exponents whose approximations eventually stop. It is a quantitative question: knowing that π is irrational alone does not determine this boundary.

OpenAI's family 017 formalization selects the assertion that this boundary is exactly 2. This mission imports that precise Lean statement and records its upper-bound consequence in the campaign. The source is pinned to commit adc7f1241b42e322a6451854ab7e4b4c146bf78a, so later repository changes do not change the target.

The quantities and conventions

Let $p$ be an integer, let $q$ be a positive integer, and measure the approximation error by $|\pi-p/q|$. A real exponent $\nu$ sets the comparison scale $q^{-\nu}$. Larger exponents require smaller errors. A bound that holds for every sufficiently large denominator must have a threshold uniform in the numerator, rather than a separate threshold for each fraction.

For a rational number $r$, write $d(r)$ for its positive denominator in lowest terms. Define the set

The source's supremum is taken in the real numbers. Infinitely many rational values are required; repeatedly writing one rational number with larger unreduced denominators does not satisfy this condition. The restriction on $d(r)$ excludes integers. These conventions are part of the imported proposition.

Formalization targets

The campaign goal is the existing shared predicate $\mathrm{UpperBound}(2)$:

The threshold may depend on $\varepsilon$, but must work for every numerator and every eligible denominator. This is the goal named PiIrrationality.openai_bound_two and supplies the campaign value 2.

A separate theorem, OAI.PiExponent.main, preserves both conjuncts of the upstream challenge:

The eventual inequality here is non-strict; the campaign formulation uses a strict inequality with a positive epsilon. They express compatible upper-bound conclusions. The supremum clause additionally records the exact value. No conclusion that the exponent 2 itself belongs to $S$ is asserted by the supremum equality alone.

What completion establishes

A verified solution to the campaign goal would place the upper bound 2 alongside the campaign's existing bounds, using exactly the same definition. A verified solution to the imported source theorem would also establish the explicit real-supremum characterization. Keeping that theorem separate preserves the stronger original statement while allowing the campaign to compare like-for-like upper bounds.

The OpenAI solution entry point supplies proof terms through its project dependencies. The Comparator challenge file intentionally ends with a proof placeholder. This mission imports statements; the upstream proof development has not yet been imported and verified in this mission. An external proof reference does not by itself complete either target here.

The uniformity requirement

Numerically checking many rational approximations cannot establish either target. The eventual bound quantifies over every real exponent above 2 and every sufficiently large denominator, with no finite upper limit. The threshold must also be independent of the numerator. Conversely, the supremum clause concerns infinitely many distinct rational values, so a finite list of strong approximations does not establish it. These are the mathematical obligations that a submitted proof must discharge.

Formalization scope

The imported statement uses Mathlib's real number π, real powers, rational coercions, reduced rational denominators, set infinitude, and real supremum. No custom replacement for π or the campaign's upper-bound predicate is introduced. The source first conjunct quantifies over integer denominators but forces them to be at least 2; the campaign definition uses positive natural denominators. The campaign goal imports Definitions.Def_PiIrrationality_UpperBound from its existing foundation.

The original source uses Lean 4.34.1 and Mathlib revision d13f23b723b8a846827a245b89c10fc7d3f11612. This entry targets the campaign's environment. The existing published source theorem is reused without changing its proposition or Mathlib import. Proof porting, supporting lemmas, and a verified connection between the exact source theorem and the shared campaign goal are welcome. Flint–Hills summability is outside this mission's scope, matching the selected upstream statement.

Selected references

• OpenAI, math: PiExponent, family 017, 2026: exact challenge, scope, and proof entry point.
• Upstream code is distributed under Apache License 2.0. The immutable source attribution is recorded with the theorem.