∑math20

Number theory · Result 017

The irrationality exponent of π is 2

1 paperLeanreasoning

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of The irrationality exponent of pi is 2

The irrationality exponent of pi is 2

OpenAI · September 24, 2026

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.

Read PDF Download Source

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

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves that the irrationality exponent of \(\pi\) is exactly two. For every \(\nu>2\), all sufficiently large positive denominators \(q\) satisfy \(|\pi-p/q|\ge q^{-\nu}\) for every integer numerator \(p\). It also states the exact supremum characterization using infinitely many rational approximations.

The paper's convergence consequence for the Flint–Hills series is outside this selected statement.

Comparator links

ResultComparator statement
The irrationality exponent of \(\pi\) equals twoPiExponent.lean

Scope note on GitHub →

Reasoning summary

OpenAI released an abridged summary of the model's reasoning for this result: The irrationality exponent of π (PDF).