The irrationality exponent of π is 2
The irrationality exponent of π is 2 is a manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original result
- Claim. The irrationality exponent of π equals 2: for every ε > 0 and all sufficiently large denominators q, every rational p/q satisfies |π − p/q| ≥ q−2−ε. The manuscript derives the convergence of the Flint–Hills series ∑n≥1 1/(n3 sin2 n) as a consequence.
- Source. Manuscript folder in the openai/math repository (commit
adc7f12). - Formalization, as described by the repository. The scope note lean/docs/017.md states that the Lean formalization proves the exponent-two statement and the corresponding supremum characterization, and that the Flint–Hills convergence is outside the formalized statement. The comparator statement is ComparatorChallenges/PiExponent.lean.
- Earlier published bound. D. Zeilberger and W. Zudilin, The irrationality measure of π is at most 7.103205334137… (arXiv:1912.06345).
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 13 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | KitaKen1, log2-irrationality-exponent | Extension | The irrationality exponent of log 2 is 2, with a Lean proof that imports OpenAI's formal library for this result. The earlier published bound was 3.5746 (R. Marcovecchio, 2009). | The author reports a Lean build and a browser (Lean4Web) check. A formal-conjectures pull request, #6923, is open (labels: arxiv, awaiting-author). |
| 2026-10-07 to 2026-10-12 | Ryan Matthew Casper, Mattie/math | Extensions | Preprints with Lean formalizations claiming exponent 2 for log a (a a positive rational, a ≠ 1), for nonzero rational arctangents, for arctan(√2)/√2 and log(3+2√2)/√2, for real and imaginary quadratic periods (9 October) and the statement that reciprocal quadratic integrals with rational data are rational or have exponent 2 (10 October); and upper bounds of 4 for log 2 + √2, √2 log 2, log(3/2) + √2 and positive quadratic logarithms. | For the rational-logarithm result the author's verification notes report a Lean 4.34.1 build, a Nanoda 0.4.19 replay and a second official-kernel replay, with proof exports in the release proof-exports-2026-10-08. Formal-conjectures pull request #6925 and issues #6924 and #6927 are open. |
| 2026-10-07 | Formal-conjectures issue #6909 | Use | Reports that the formal-conjectures statement flint_hills_series_converges follows from the OpenAI result. |
Open; label solution found. |
Notes
- Both repositories above describe substantial AI assistance in producing their proofs and texts.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.