Browse › Number theory › 017 The irrationality exponent of π is 2
The irrationality exponent of pi is 2
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove the conjecture that the irrationality exponent of π is 2. As a consequence, the classical Flint–Hills series $\sum_{n\ge1}1/(n^3\sin^2 n)$ converges, with angles in radians.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-23) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- Manuscript at jdb19937.github.io (author line "Dan Brown"), The irrationality measure of the logarithm of a rational number is 2 (PDF, dated October 7, 2026). Claims $\mu(\log\alpha)=2$ for every positive rational $\alpha\ne1$ by moving the interpolation centres of this paper's determinant argument from $(1,2\pi i j)$ to $(\alpha^j, j\log\alpha)$, with a Lean 4 formalization; the paper is cited throughout by section and equation number.
- Kenta Kitamura (KitaKen1), log2-irrationality-exponent (GitHub repository, October 2026). Solution notes and a Lean proof that $\mu(\log 2)=2$, prepared for a formal-conjectures proposal; the README credits this paper's "interpolation, determinant, and parameter-selection arguments" and imports the pinned OpenAI Lean source. [AI-generated per source]
- Ryan Matthew Casper, The irrationality exponent of positive rational logarithms is 2 (preprint with Lean formalization, 2026-10-07). Reports an extension of this paper's method and the released Lean library to $\log r$ for every positive rational $r\ne1$, with automated reviews distinguished from external human peer review. [AI-generated per source]
- Ryan Matthew Casper, The irrationality exponent of nonzero rational arctangents is 2 (preprint with Lean formalization, 2026-10-07). Reports an extension of the weighted interpolation and determinant method, using Gaussian arithmetic, to obtain exponent two for $\arctan r$ at every nonzero rational $r$. [AI-generated per source]
- Ryan Matthew Casper, The irrationality exponent of real and imaginary quadratic periods is 2 (preprint with Lean formalization, 2026-10-09). Building on this paper's interpolation and determinant method, reports exponent two for $\pi/\sqrt r$ with positive rational $r$ and for specified normalized real and imaginary quadratic logarithmic periods. [AI-generated per source]
- Sean Litsey (contributor), Irrationality measures for $G\pm5\pi^2/48$ and $L(2,\chi_{-3})$ (hexagon:2610.00401v1, 2026-10-20). Builds on the release's determinant method for Catalan's constant and lists this paper in its bibliography; the abstract does not say it uses this paper's argument. [AI-generated per source]
Comments and discussion
- Persiflage, A Brief Digest of Some New OpenAI Results, item 8 (blog, 2026-10-08). Reports Wadim Zudilin's observation of a close similarity to Roth's argument for algebraic irrationals, while stating that the blog author had not yet examined this paper.
- もの(換気中) (@monoxxxx), post on X (2026-10-07). In Japanese, describes the proof as an argument by contradiction that assumes an unusually good rational approximation to π, builds an algebraic construction from it and rules that construction out, in contrast with earlier work that lowered numerical bounds such as 7.103.
- Almost Sure (@Almost_Sure), post on X (2026-10-14). Remarks that the paper's derivation of Flint–Hills convergence from an irrationality measure below 5/2 is "way shorter" than two other proofs the author had seen.
- UnstableReserves (@UnstableReserve), post on X (2026-10-13). Follows the paper's parameter lemma to estimate the size of the proof (3,977 variables for ν = 5/2) and reports certifying 292,361 terms of π's continued fraction.
Formalization
- OpenAI math release, Lean scope note for family 017 (lean/docs/017.md, 2026-10-06). States that the formalization proves $\mu(\pi)=2$, both as an eventual bound $|\pi-p/q|\ge q^{-\nu}$ for every $\nu>2$ and as a supremum characterization, with the comparator statement in
ComparatorChallenges/PiExponent.lean; the Flint–Hills corollary is outside the selected Comparator statement. - google-deepmind/formal-conjectures, FormalConjectures/OptimizationConstants/7a.lean (formal-conjectures). Formalizes the irrationality exponent of $\pi$ as Tao's optimization constant 7a and states
c7a_eq_two($C_{7a}=2$), citing this paper; the proof issorryin this file and points to OpenAI's PiExponent.lean. - Ryan Matthew Casper, Flint Hills and Cookson Hills (GitHub formalization, accessed 2026-10-21). Reuses OpenAI's formal Flint–Hills theorem, adds Cookson–Hills convergence by comparison with even-indexed Flint terms, and supplies declarations matching the FormalConjectures series statements. [AI-generated per source]
Related prior literature mentioned by others
- Michel Laurent, Sur quelques résultats récents de transcendance (Astérisque 198–199–200, 1991, pp. 209–230). José Hdz. Stgo.'s MathOverflow discussion points readers to this antecedent of the paper's method, which is also in the paper's bibliography.
- Stéphane Fischler and Michael Nakamaye, Seshadri Constants and Interpolation on Commutative Algebraic Groups (arXiv:1205.4088, 2012; Ann. Inst. Fourier 64, 2014). The survey arXiv:2610.17090 lists Masser (1981), Fischler (2005), and Fischler–Nakamaye (2014) as related interpolation mechanisms and antecedents of this paper's interpolation argument.
Possibly relevant literature (found by the agent, not checked)
- Sully F. Chen and Erin P. J. Pearse, The irrationality measure of π as seen through the eyes of cos(n) (arXiv:1807.02955, 2018–2019). Gives a criterion via $\limsup|\cos n|^{n^2}$ that implies $\mu(\pi)=2$, and numerical evidence for it; this relates to Theorem 1.1 and to the trigonometric-series consequences in Section 5.
- Yann Bugeaud and Dong Han Kim, On the b-ary expansion of a real number whose irrationality exponent is close to 2 (arXiv:2510.02059v2, 2025–2026). Proves complexity lower bounds for the $b$-ary expansion of numbers with irrationality exponent below about 2.324, which would apply to $\pi$ if Theorem 1.1 holds.
Digests and expositions
- Ying Xie, What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics (arXiv:2610.17090, math.HO, 2026-10-12). Section 8.1.3 of this AI-assisted survey extracts the paper's "separated-weight interpolation" theorem, weighted transverse multiplicity lemma and determinant control, compares them with earlier interpolation work, and gives the provisional verdict "combination bordering new"; it does not verify the proofs or compile the Lean development. [family-level]
- Latent Seminar, The irrationality exponent of pi and sine-denominator series (exposition, 2026-10-06). Explains the weighted interpolation, determinant comparison, and sine-series consequences, distinguishing exponent two from bounded partial quotients and disclaiming independent proof verification.
News and blogs
- John D. Cook, Irrationality exponent of π (blog, 2026-10-07). Short explanatory post on what $\mu(\pi)=2$ means for rational approximations of $\pi$; it links the preprint.
Elsewhere
- VibeMathed: Problem record
- VibeMathed: Problem record
- Emergent Mind: family 017
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:The-irrationality-exponent-of-pi-is-2-September-24-2026,
author = {{OpenAI}},
title = {{The irrationality exponent of $\pi$ is $2$}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/The-irrationality-exponent-of-pi-is-2-September-24-2026/paper.pdf}{OAI:The-irrationality-exponent-of-pi-is-2-September-24-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/017.md. The Lean statements have not been checked by people against the paper's claims.
Family 017: The irrationality exponent of π is 2
Proves that the irrationality exponent of π is exactly 2: for every ε > 0 and all sufficiently large denominators q, every rational $p/q$ satisfies $|\pi-p/q|\ge q^{-2-\varepsilon}$. This also proves convergence of the Flint–Hills series $\sum_{n\ge1}1/(n^3\sin^2 n)$, with angles in radians.
This is the only paper in this family.