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

$$\mu(x)=\sup\Bigl\{\nu>0:\ 0<\Bigl|x-\frac pq\Bigr|<q^{-\nu}\ \text{for infinitely many coprime } p,q\in\mathbb Z,\ q\ge2\Bigr\}.$$

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

$$\Bigl|\pi-\frac pq\Bigr|\ \ge\ q^{-\nu}\qquad\text{for all } p,q\in\mathbb Z \text{ with } q\ge Q;$$

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/