OpenAI model claims the irrationality exponent of π is exactly 2 (Lean-formalized), which implies the Flint–Hills series converges
Awaiting review
Importance: major (4 of 5)The takeaway
Since Mahler’s 1953 bound of 42, mathematicians had lowered the irrationality exponent of π only to about 7.1. OpenAI’s release claims the conjectured value 2 in a 23-page paper with a Lean proof. Six days on, no expert has publicly assessed it; an outsider has already adapted the Lean proof to log 2.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 12 October 2026
Your AI and this story
- GPT-6 Astra159 days after its cutoff
- Claude Opus 5.598 days after its cutoff
- Gemini 3.8 Flash189 days after its cutoff
- Grok 4.7128 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 98 days before it.
Key facts
- Catalogue text (openai/math CONTENTS.md, family 017): ‘Proves that the irrationality exponent of π is exactly 2: for every ε > 0 and all sufficiently large denominators q, every rational p/q satisfies |π − p/q| ≥ q^(−2−ε). This also proves convergence of the Flint–Hills series Σ 1/(n³ sin² n), with angles in radians.’
- Paper: ‘The irrationality exponent of π is 2’, author ‘OpenAI’, dated 24 Sept 2026, 23 pages. Theorem 1.1 is ineffective: ‘The threshold may depend on ν, and the argument does not give it effectively.’ The paper stresses that exponent 2 does not mean bounded continued-fraction partial quotients
- History given in the paper: Mahler (1953) exponent 42; Mignotte 20; Hata 8.0160…; Salikhov 7.6063…; Zeilberger–Zudilin 7.103205334137…; Bai (Sept 2026) 7.101862832357. ‘These quantitative bounds are context, not inputs to our proof.’
- Method (paper’s outline): ‘a multivariable interpolation theorem to construct a nonzero determinant’, then two incompatible estimates for its absolute value; related to Laurent’s interpolation determinants and to Roth’s many-variable method, with an interpolation statement ‘adapted to logarithmic curves’
- Flint–Hills: Alekseyev showed convergence requires μ(π) ≤ 5/2 and Meiburg that μ(π) < 5/2 suffices; Theorem 1.1 supplies this. More generally Σ 1/(n^a |sin n|^b) converges if and only if a > max{1, b} (Corollary 5.2)
- Earlier claims (paper): a convergence claim by Mantzakouras and López Zapata ‘was withdrawn in September 2026’; Carella’s claim of exponent two with bounded partial quotients ‘contains a sign obstruction’. Neither is used
- Lean: the scope note says ‘The formalization proves that the irrationality exponent of π is exactly two’; the Comparator challenge PiExponent.lean states it for Mathlib’s Real.pi, including the supremum characterization. ‘The paper’s convergence consequence for the Flint–Hills series is outside this selected statement.’
- Status in OpenAI’s own log: history.md (7 Oct 2026) lists three withdrawn manuscripts and 14 repaired ones; family 017 is in neither list
Show 2 more
- Follow-up by an outsider (9 Oct): a pseudonymous ‘Dan Brown’ (GitHub jdb19937) published ‘The logarithms of rational numbers have irrationality exponent 2’, claiming μ(log α) = 2 for every positive rational α ≠ 1 (so μ(log 2) = 2), with a Lean proof described as ‘a module-by-module modification of OpenAI’s formalization of μ(π) = 2’. Hacker News, 22 points; the author’s comment: ‘This is a Lean-verified variation of the OpenAI proof for pi.’ Not peer-reviewed; the author’s identity is unconfirmed
- Not found as of 12 Oct 2026 (web and Hacker News search; X not searched): public assessments by specialists such as Wadim Zudilin, Frank Calegari or Terence Tao, or an independent re-run of this Lean proof
What happened
The irrationality exponent of a number measures how closely fractions can approximate it. Almost every real number has exponent 2, and π was expected to, but proofs were far from it: the record stood at about 7.10 after decades of refinements of integral constructions. Among the 722 manuscripts OpenAI published on 6 Oct 2026, family 017 claims the exact value 2 by a different route, an interpolation-determinant argument in many variables. The result is ineffective, meaning it gives no explicit point after which the inequality holds.
The claim settles a question that became popular outside research mathematics: whether the Flint–Hills series converges. That depends on how often sin n is very small, which is the same as how well π is approximated by fractions.
OpenAI’s Lean library contains a proof of the exponent statement, written against Mathlib’s definition of π. Three days after the release, a pseudonymous programmer published a modification of that Lean proof which, he says, gives exponent 2 for the logarithm of every rational number, including log 2. If both hold, the technique is general.
Why it matters
Among the release’s claims this is one of the easiest to state and one with a long, well-known history of small improvements, including an AI-assisted one in September 2026. The Lean statement is short and uses only standard Mathlib definitions, so a successful independent kernel check would leave little room for doubt about the theorem itself. As of 12 Oct no such check and no specialist’s assessment had been published, so the entry’s status is pending.
What is disputed or not yet verified
| Verification | Lean formalization by OpenAI of the exponent statement (Comparator challenge published); not independently re-checked or expert-reviewed as far as found |
|---|
Sources
8 sources from 3 sites. Numbers match the chips in the text.
8 sources: 7 primary, 1 reaction
Primary
- Paper: The irrationality exponent of π is 2 (openai/math, 24 Sept 2026)github.com, paper
- openai/math: CONTENTS.md, family 017github.com, code
- Lean scope note for family 017github.com, code
- Comparator challenge: PiExponent.leangithub.com, code
- openai/math README (procedure and exceptions)github.com, code
- openai/math history.md (withdrawals and fixes, 7 Oct 2026)github.com, code
- ‘Dan Brown’: The irrationality measure of the logarithm of a rational number is 2 (Lean)jdb19937.github.io, code
Reactions
- Hacker News: The logarithms of rational numbers have irrationality exponent 2news.ycombinator.com, discussion
Changes
- Filed from the openai/math repository (paper, Lean scope note and challenge) and the Hacker News thread