---
id: "2026-10-06-irrationality-exponent-pi-openai"
url: "https://postcutoff.com/e/2026-10-06-irrationality-exponent-pi-openai/"
as_of: "2026-10-12T07:22:00+02:00"
date: "2026-10-06"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 8
editor: Adam Bicz
human_review: null
version: null
---

As of: 2026-10-12 07:22 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz.
Canonical page: https://postcutoff.com/e/2026-10-06-irrationality-exponent-pi-openai/

# OpenAI model claims the irrationality exponent of π is exactly 2 (Lean-formalized), which implies the Flint–Hills series converges

Family 017 of OpenAI's 6 Oct 2026 math release is "The irrationality exponent of π is 2" (manuscript dated 24 Sept 2026, 23 pages, author "OpenAI"). It claims that for every ν > 2 and all large enough q, |π − p/q| ≥ q^(−ν) for every integer p, so π is approximated by fractions no better than a typical number. The best previous bounds were 7.1032 (Zeilberger–Zudilin, 2019) and 7.1019 (Bai, Sept 2026). A corollary is that the Flint–Hills series Σ 1/(n³ sin² n) converges. OpenAI's Lean library formalizes the exponent statement against Mathlib's Real.pi. No public expert assessment was found by 12 Oct 2026.

## 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
- 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

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff
- Gemini 3.8 Flash (training cutoff March 2026): 189 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 128 days after its cutoff

## Sources

1. [Paper: The irrationality exponent of π is 2 (openai/math, 24 Sept 2026)](https://github.com/openai/math/blob/main/preprints/The-irrationality-exponent-of-pi-is-2-September-24-2026/paper.pdf) (github.com, paper)
2. [openai/math: CONTENTS.md, family 017](https://github.com/openai/math/blob/main/CONTENTS.md) (github.com, code)
3. [Lean scope note for family 017](https://github.com/openai/math/blob/main/lean/docs/017.md) (github.com, code)
4. [Comparator challenge: PiExponent.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/PiExponent.lean) (github.com, code)
5. [openai/math README (procedure and exceptions)](https://github.com/openai/math/blob/main/README.md) (github.com, code)
6. [openai/math history.md (withdrawals and fixes, 7 Oct 2026)](https://github.com/openai/math/blob/main/history.md) (github.com, code)
7. ['Dan Brown': The irrationality measure of the logarithm of a rational number is 2 (Lean)](https://jdb19937.github.io/log-irrationality-measure/) (jdb19937.github.io, code)
8. [Hacker News: The logarithms of rational numbers have irrationality exponent 2](https://news.ycombinator.com/item?id=50027884) (news.ycombinator.com, discussion)

## Changes

- 2026-10-12 (filed): Created from the openai/math repository (paper, Lean scope note and challenge) and the Hacker News thread

## Related

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-10-06: [OpenAI model claims the quasi-Riemann hypothesis](https://postcutoff.com/e/2026-10-06-quasi-riemann-hypothesis-openai/index.md)
- 2026-09-25: [New record bound on the irrationality measure of ζ(2), μ ≤ 5.0495243, released as a 92k-line Lean proof written by Claude; beaten a week later by a Claude-assisted paper](https://postcutoff.com/e/2026-09-25-zeta2-irrationality-measure-claude-lean/index.md)
- 2026-09-10: [Irrationality measure of π lowered to 7.101862832357, the first improvement on Zeilberger–Zudilin (2019), with GPT-5.6 Sol and GPT-6 Astra; four weeks later OpenAI claimed the exact value 2](https://postcutoff.com/e/2026-09-10-pi-irrationality-measure-bai-gpt/index.md)
- People: [Terence Tao](https://postcutoff.com/person/terence-tao/)