Rational approximation to π

Rational numbers approximate π to different degrees of accuracy. A useful question is how the error depends on the denominator, rather than how many decimal digits a particular fraction happens to match. The irrationality measure records the boundary between exponents that allow infinitely many exceptionally close rational approximations and exponents whose approximations eventually stop. It is a quantitative question: knowing that π is irrational alone does not determine this boundary.

OpenAI's family 017 formalization selects the assertion that this boundary is exactly 2. This mission imports that precise Lean statement and records its upper-bound consequence in the campaign. The source is pinned to commit adc7f1241b42e322a6451854ab7e4b4c146bf78a, so later repository changes do not change the target.

The quantities and conventions

Let $p$ be an integer, let $q$ be a positive integer, and measure the approximation error by $|\pi-p/q|$. A real exponent $\nu$ sets the comparison scale $q^{-\nu}$. Larger exponents require smaller errors. A bound that holds for every sufficiently large denominator must have a threshold uniform in the numerator, rather than a separate threshold for each fraction.

For a rational number $r$, write $d(r)$ for its positive denominator in lowest terms. Define the set

$$S=\{\nu>0:\text{ infinitely many distinct }r\in\mathbb Q\text{ have }d(r)\ge2\text{ and }0<|\pi-r|<d(r)^{-\nu}\}.$$

The source's supremum is taken in the real numbers. Infinitely many rational values are required; repeatedly writing one rational number with larger unreduced denominators does not satisfy this condition. The restriction on $d(r)$ excludes integers. These conventions are part of the imported proposition.

Formalization targets

The campaign goal is the existing shared predicate $\mathrm{UpperBound}(2)$:

$$\forall\varepsilon>0,\ \exists Q\in\mathbb N,\ \forall p\in\mathbb Z,\ \forall q\in\mathbb N,\quad q>0\land q\ge Q\Longrightarrow \frac{1}{q^{2+\varepsilon}}<|\pi-p/q|.$$

The threshold may depend on $\varepsilon$, but must work for every numerator and every eligible denominator. This is the goal named PiIrrationality.openai_bound_two and supplies the campaign value 2.

A separate theorem, OAI.PiExponent.main, preserves both conjuncts of the upstream challenge:

$$\left(\forall\nu>2,\ \exists Q\in\mathbb Z,\ Q\ge2\land\forall p,q\in\mathbb Z,\ q\ge Q\Longrightarrow q^{-\nu}\le|\pi-p/q|\right)\quad\land\quad\sup S=2.$$

The eventual inequality here is non-strict; the campaign formulation uses a strict inequality with a positive epsilon. They express compatible upper-bound conclusions. The supremum clause additionally records the exact value. No conclusion that the exponent 2 itself belongs to $S$ is asserted by the supremum equality alone.

What completion establishes

A verified solution to the campaign goal would place the upper bound 2 alongside the campaign's existing bounds, using exactly the same definition. A verified solution to the imported source theorem would also establish the explicit real-supremum characterization. Keeping that theorem separate preserves the stronger original statement while allowing the campaign to compare like-for-like upper bounds.

The OpenAI solution entry point supplies proof terms through its project dependencies. The Comparator challenge file intentionally ends with a proof placeholder. This mission imports statements; the upstream proof development has not yet been imported and verified in this mission. An external proof reference does not by itself complete either target here.

The uniformity requirement

Numerically checking many rational approximations cannot establish either target. The eventual bound quantifies over every real exponent above 2 and every sufficiently large denominator, with no finite upper limit. The threshold must also be independent of the numerator. Conversely, the supremum clause concerns infinitely many distinct rational values, so a finite list of strong approximations does not establish it. These are the mathematical obligations that a submitted proof must discharge.

Formalization scope

The imported statement uses Mathlib's real number π, real powers, rational coercions, reduced rational denominators, set infinitude, and real supremum. No custom replacement for π or the campaign's upper-bound predicate is introduced. The source first conjunct quantifies over integer denominators but forces them to be at least 2; the campaign definition uses positive natural denominators. The campaign goal imports Definitions.Def_PiIrrationality_UpperBound from its existing foundation.

The original source uses Lean 4.34.1 and Mathlib revision d13f23b723b8a846827a245b89c10fc7d3f11612. This entry targets the campaign's environment. The existing published source theorem is reused without changing its proposition or Mathlib import. Proof porting, supporting lemmas, and a verified connection between the exact source theorem and the shared campaign goal are welcome. Flint–Hills summability is outside this mission's scope, matching the selected upstream statement.

Selected references

• OpenAI, math: PiExponent, family 017, 2026: exact challenge, scope, and proof entry point.
• Upstream code is distributed under Apache License 2.0. The immutable source attribution is recorded with the theorem.