https://openai-aftermath.mathnt.net/index.php?action=history&feed=atom&title=The_irrationality_exponent_of_%CF%80_is_2 2026-10-14T16:20:38Z Revision history for this page on the wiki MediaWiki 1.46.2 https://openai-aftermath.mathnt.net/index.php?title=The_irrationality_exponent_of_%CF%80_is_2&diff=15&oldid=prev 2026-10-13T11:12:44Z

<p>Main Page and first result page: published claims and public follow-ups (sources linked)</p> <p><b>New page</b></p><div>&#039;&#039;&#039;The irrationality exponent of π is 2&#039;&#039;&#039; is a manuscript dated 24 September 2026 in OpenAI&#039;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&#039; claims; the publication of a paper, code or a formal proof is not presented here as independent verification.<br /> <br /> == The original result ==<br /> * &#039;&#039;&#039;Claim.&#039;&#039;&#039; The irrationality exponent of π equals 2: for every ε &amp;gt; 0 and all sufficiently large denominators &#039;&#039;q&#039;&#039;, every rational &#039;&#039;p&#039;&#039;/&#039;&#039;q&#039;&#039; satisfies |π &amp;minus; &#039;&#039;p&#039;&#039;/&#039;&#039;q&#039;&#039;| &amp;ge; &#039;&#039;q&#039;&#039;&lt;sup&gt;&amp;minus;2&amp;minus;ε&lt;/sup&gt;. The manuscript derives the convergence of the Flint–Hills series ∑&lt;sub&gt;&#039;&#039;n&#039;&#039;&amp;ge;1&lt;/sub&gt; 1/(&#039;&#039;n&#039;&#039;&lt;sup&gt;3&lt;/sup&gt; sin&lt;sup&gt;2&lt;/sup&gt; &#039;&#039;n&#039;&#039;) as a consequence.<br /> * &#039;&#039;&#039;Source.&#039;&#039;&#039; [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 &lt;code&gt;adc7f12&lt;/code&gt;).<br /> * &#039;&#039;&#039;Formalization, as described by the repository.&#039;&#039;&#039; 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].<br /> * &#039;&#039;&#039;Earlier published bound.&#039;&#039;&#039; D. Zeilberger and W. Zudilin, &#039;&#039;The irrationality measure of π is at most 7.103205334137…&#039;&#039; ([https://arxiv.org/abs/1912.06345 arXiv:1912.06345]).<br /> <br /> == Public follow-up work ==<br /> {| class=&quot;wikitable&quot;<br /> ! Date !! Work !! Relation !! Public claim !! Public status (checked 13 October 2026)<br /> |-<br /> | 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&#039;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: &#039;&#039;arxiv&#039;&#039;, &#039;&#039;awaiting-author&#039;&#039;).<br /> |-<br /> | 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 &#039;&#039;a&#039;&#039; (&#039;&#039;a&#039;&#039; a positive rational, &#039;&#039;a&#039;&#039; &amp;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&#039;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.<br /> |-<br /> | 2026-10-07 || Formal-conjectures issue [https://github.com/google-deepmind/formal-conjectures/issues/6909 #6909] || Use || Reports that the formal-conjectures statement &lt;code&gt;flint_hills_series_converges&lt;/code&gt; follows from the OpenAI result. || Open; label &#039;&#039;solution found&#039;&#039;.<br /> |}<br /> <br /> == Notes ==<br /> * Both repositories above describe substantial AI assistance in producing their proofs and texts.<br /> * The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.<br /> <br /> [[Category:OpenAI results]]</div>

Aftermath bot