# The irrationality exponent of <i>π</i> is 2

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

- [The irrationality exponent of $\pi$ is 2](../../preprints/The-irrationality-exponent-of-pi-is-2-September-24-2026/paper.pdf)

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

| Result | Comparator statement |
| --- | --- |
| The irrationality exponent of $\pi$ equals two | [PiExponent.lean](../ComparatorChallenges/PiExponent.lean) |