View source for The irrationality exponent of π is 2

'''The irrationality exponent of π is 2''' is a manuscript dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' The irrationality exponent of π equals 2: for every ε &gt; 0 and all sufficiently large denominators ''q'', every rational ''p''/''q'' satisfies |π &minus; ''p''/''q''| &ge; ''q''<sup>&minus;2&minus;ε</sup>. The manuscript derives the convergence of the Flint–Hills series ∑<sub>''n''&ge;1</sub> 1/(''n''<sup>3</sup> sin<sup>2</sup> ''n'') as a consequence.
* '''Source.''' [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-irrationality-exponent-of-pi-is-2-September-24-2026 Manuscript folder] in the openai/math repository (commit <code>adc7f12</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/017.md lean/docs/017.md] states that the Lean formalization proves the exponent-two statement and the corresponding supremum characterization, and that the Flint–Hills convergence is outside the formalized statement. The comparator statement is [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/PiExponent.lean ComparatorChallenges/PiExponent.lean].
* '''Earlier published bound.''' D. Zeilberger and W. Zudilin, ''The irrationality measure of π is at most 7.103205334137…'' ([https://arxiv.org/abs/1912.06345 arXiv:1912.06345]).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 13 October 2026)
|-
| 2026-10-07 || KitaKen1, [https://github.com/KitaKen1/log2-irrationality-exponent log2-irrationality-exponent] || Extension || The irrationality exponent of log 2 is 2, with a Lean proof that imports OpenAI's formal library for this result. The earlier published bound was 3.5746 (R. Marcovecchio, 2009). || The author reports a Lean build and a browser (Lean4Web) check. A formal-conjectures pull request, [https://github.com/google-deepmind/formal-conjectures/pull/6923 #6923], is open (labels: ''arxiv'', ''awaiting-author'').
|-
| 2026-10-07 to 2026-10-12 || Ryan Matthew Casper, [https://github.com/Mattie/math Mattie/math] || Extensions || Preprints with Lean formalizations claiming exponent 2 for log ''a'' (''a'' a positive rational, ''a'' &ne; 1), for nonzero rational arctangents, for arctan(√2)/√2 and log(3+2√2)/√2, for real and imaginary quadratic periods (9 October) and the statement that reciprocal quadratic integrals with rational data are rational or have exponent 2 (10 October); and upper bounds of 4 for log 2 + √2, √2 log 2, log(3/2) + √2 and positive quadratic logarithms. || For the rational-logarithm result the author's verification notes report a Lean 4.34.1 build, a Nanoda 0.4.19 replay and a second official-kernel replay, with proof exports in the release [https://github.com/Mattie/math/releases/tag/proof-exports-2026-10-08 proof-exports-2026-10-08]. Formal-conjectures pull request [https://github.com/google-deepmind/formal-conjectures/pull/6925 #6925] and issues [https://github.com/google-deepmind/formal-conjectures/issues/6924 #6924] and [https://github.com/google-deepmind/formal-conjectures/issues/6927 #6927] are open.
|-
| 2026-10-07 || Formal-conjectures issue [https://github.com/google-deepmind/formal-conjectures/issues/6909 #6909] || Use || Reports that the formal-conjectures statement <code>flint_hills_series_converges</code> follows from the OpenAI result. || Open; label ''solution found''.
|}

== Notes ==
* Both repositories above describe substantial AI assistance in producing their proofs and texts.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]