The irrationality measure of $\pi$

Upper bound, last-listed row

| $7.103205334137$ | [ZZ2020] | Current record bound. |tracked since 2026-07-24 — no movement seen yet

Lower bound, last-listed row

| $2$ | [D1842] | Dirichlet's theorem; holds for every irrational number (in particular for $\pi$). |tracked since 2026-07-24 — no movement seen yet

Outside the source table: a claim in OpenAI's math release

• Family 017, “The irrationality exponent of π is 2”, claims that the irrationality measure of π is exactly 2.

  Its Lean statement, PiExponent.lean:

  theorem main : (∀ ν : ℝ, 2 < ν → ∃ Q : ℤ, 2 ≤ Q ∧ ∀ p q : ℤ, Q ≤ q → (q : ℝ) ^ (-ν) ≤ |Real.pi - (p : ℝ) / (q : ℝ)|) ∧ sSup {ν : ℝ | 0 < ν ∧ Set.Infinite {r : ℚ | 2 ≤ r.den ∧ 0 < |Real.pi - (r : ℝ)| ∧ |Real.pi - (r : ℝ)| < (r.den : ℝ) ^ (-ν)}} = 2

  Same quantity: the first half says that for every ν > 2, |π − p/q| ≥ q^(−ν) once q is large enough, and the second that the supremum of exponents with infinitely many such approximations is 2. That makes this constant 2, against 7.103205334137 in its last-listed upper-bound row.

  Status: a Lean statement of it is published with a proof by its authors. We read the statement and it matches this constant's definition; we have not compiled the proof, and we have not read the paper.

A claim in a preprint release, read at openai/math@fd4aeeb on 2026-10-12. It is not in the source table, and this ledger has not changed the rows above because of it.