Aftermath bot: Add Hexagon and Palomar follow-ups and the quasi-Riemann tracker

2026-10-21T13:51:13Z

Add Hexagon and Palomar follow-ups and the quasi-Riemann tracker

← Older revision		Revision as of 06:51, 21 October 2026
Line 24:		Line 24:
	\| 2026-10-09 \|\| W. van Doorn, ''Short Egyptian fractions'' ([https://github.com/Woett/Mathematical-shorts/blob/a65db1e49e255ca363768cc51398f73079520dd5/Short%20Egyptian%20fractions.pdf Woett/Mathematical-shorts], commit <code>a65db1e</code>) \|\| Exposition (simplified proof) \|\| A human-written exposition and simplification of the proof of the first theorem, giving at most (16/log 2 + ''o''(1)) log log ''b'' terms. In comments on the blog post above, the author discusses which arguments of the manuscript its Lean formalizations follow. \|\| Note; the author states on the blog that it was written with the help of ChatGPT.		\| 2026-10-09 \|\| W. van Doorn, ''Short Egyptian fractions'' ([https://github.com/Woett/Mathematical-shorts/blob/a65db1e49e255ca363768cc51398f73079520dd5/Short%20Egyptian%20fractions.pdf Woett/Mathematical-shorts], commit <code>a65db1e</code>) \|\| Exposition (simplified proof) \|\| A human-written exposition and simplification of the proof of the first theorem, giving at most (16/log 2 + ''o''(1)) log log ''b'' terms. In comments on the blog post above, the author discusses which arguments of the manuscript its Lean formalizations follow. \|\| Note; the author states on the blog that it was written with the help of ChatGPT.
	\|-		\|-
	\| 2026-10-10 (current file dated 15 October 2026) \|\| T. F. Bloom, W. van Doorn, ''Optimal bounds for the length and number of unit fraction representations'' ([https://www.erdosproblems.com/static/UnitFractions.pdf PDF] on erdosproblems.com) \|\| Exposition (simplified proofs) \|\| A human-written exposition and simplification of the proofs of all three results, with a section comparing them with the manuscript's proofs; the authors describe the manuscript as difficult to read and as containing much unnecessary material. \|\| 15-page PDF hosted on erdosproblems.com.		\| 2026-10-10 (current file dated 15 October 2026) \|\| T. F. Bloom, W. van Doorn, ''Optimal bounds for the length and number of unit fraction representations'' ([https://www.erdosproblems.com/static/UnitFractions.pdf PDF] on erdosproblems.com) \|\| Exposition (simplified proofs) \|\| A human-written exposition and simplification of the proofs of all three results, with a section comparing them with the manuscript's proofs; the authors describe the manuscript as difficult to read and as containing much unnecessary material. \|\| 15-page PDF hosted on erdosproblems.com. Also posted on Hexagon as [https://hexagonmath.org/2610.00407v1 hexagon:2610.00407v1] on 20 October 2026, CC BY 4.0, whose provenance statement calls it an entirely human-written exposition and partial simplification of AI-generated proofs posted by OpenAI.
	\|-		\|-
	\| 2026-10-10 \|\| cert-machine, openai/math lane K: runs [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/ShortEgyptianFractions.json 38019899278] and [https://github.com/carlostoledo1891/cert-machine/blob/910dddee72220b30c85da00fc414b6c987f8c954/corpus/openai-math/kernel-runs/38051470892/EgyptianFractions.json 38051470892] \|\| Verification (two kernels) \|\| Records that Lean's default kernel and the nanoda kernel accept the <code>ShortEgyptianFractions</code> solution, in 443 s, and the <code>EgyptianFractions</code> solution, in 745 s. \|\| Repository.		\| 2026-10-10 \|\| cert-machine, openai/math lane K: runs [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/ShortEgyptianFractions.json 38019899278] and [https://github.com/carlostoledo1891/cert-machine/blob/910dddee72220b30c85da00fc414b6c987f8c954/corpus/openai-math/kernel-runs/38051470892/EgyptianFractions.json 38051470892] \|\| Verification (two kernels) \|\| Records that Lean's default kernel and the nanoda kernel accept the <code>ShortEgyptianFractions</code> solution, in 443 s, and the <code>EgyptianFractions</code> solution, in 745 s. \|\| Repository.

Aftermath bot: New page on short Egyptian fractions

2026-10-21T08:36:13Z

New page on short Egyptian fractions

New page

An '''Egyptian-fraction expansion''' writes a positive rational number as a sum of distinct unit fractions. Erdős conjectured that every ''a''/''b'' with 1 ≤ ''a'' < ''b'' has such an expansion with ''O''(log log ''b'') terms (Erdős problem 304); Erdős and Graham also asked how many expansions of 1 have exactly ''k'' terms (problem 148) and which denominators occur in them (problem 293). A manuscript dated 25 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claims all three, with a Lean formalization. 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.

== Background ==
* As recounted in the introduction of the manuscript:
** Erdős reported de Bruijn's bound for the maximal minimum length ''N''(''b'') and improved it to ''O''(log ''b''/log log ''b''), proposed the double-logarithmic bound and proved the matching lower order; Vose obtained ''O''(√log ''b''). Tenenbaum and Yokota controlled the length and the size of the denominators simultaneously.
** For the number ''F''(''k'') of ''k''-term expansions of 1, Konyagin and Elsholtz gave lower bounds with double logarithm of order ''k''/log ''k'', and Elsholtz and Planitzer an upper bound with double logarithm ''O''(''k''). For the least integer ''v''(''k'') absent from all ''k''-term expansions of 1, van Doorn and Tang proved ''v''(''k'') ≥ e''ck''2 and anticipated the link with uniform short expansions.

== The original result ==
* '''Claim.''' Theorem 1.1 of ''Short Egyptian fractions'' states that there are absolute constants ''c''1, ''c''2 > 0 such that ''c''1 log log ''b'' ≤ ''N''(''b'') ≤ ''c''2 log log ''b'' for all large ''b'', where ''N''(''b'') is the largest, over 1 ≤ ''a'' < ''b'', of the least number of terms in an expansion of ''a''/''b''. Corollaries give log log ''F''(''k'') of order ''k'' and log log ''v''(''k'') of order ''k'', with explicit constants in the bounds for ''v''(''k'').
* ''Method, as described:'' after a bounded number of greedy steps, the remainder is written with a denominator in a prescribed range; an auxiliary integer is constructed so that almost every fraction in a large interval of numerators has a short expansion, obtained by descending through numerator ranges, and the remaining numerator is a sum of two numerators from this dense family.
* '''Sources.''' The manuscript [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Short-Egyptian-fractions-September-25-2026 Short Egyptian fractions] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/025.md scope note] states that the formalization proves that the largest minimum length at denominator ''b'' is of order log log ''b'', that log log ''F''(''k'') is of order ''k'', and the stated bounds for prescribed denominators. The Comparator statements are <code>EgyptianFractions.lean</code> and <code>ShortEgyptianFractions.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 21 October 2026)
|-
| 2026-10-07 || [https://github.com/eigendash/openai-math-visualised eigendash/openai-math-visualised] (GitHub; commit <code>021c0f8</code>) || Numerical illustration || Computes the exact maximal minimum length ''N''(''b'') for ''b'' ≤ 220, with ''N''(''b'')/log log ''b'' between 2.43 and 4.80. || Repository; it states that agreement with an asymptotic law is evidence about the statement, not about the proof.
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statement) || Rates the family "full" with no note, the expansions being stated with plain lists of strictly increasing natural numbers and rational sums, and records sandboxed Comparator passes for <code>EgyptianFractions</code> and <code>ShortEgyptianFractions</code>. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-08 || T. F. Bloom, ''Erdős problems in the OpenAI proofs'' ([https://www.erdosproblems.com/forum/thread/blog:10 blog post] on erdosproblems.com), entry for problems 148, 293 and 304 || Catalogue (remark) || Lists the three claims, notes that the proofs have been formalised, that the manuscript mostly establishes the first theorem and deduces the other two, and that it appears to use many of the usual methods of the subject. || Blog post, read on 21 October 2026, which the author says he will update. The author states that he had not yet examined the proofs or checked the Lean files and that the post is not an endorsement.
|-
| 2026-10-09 || W. van Doorn, ''Short Egyptian fractions'' ([https://github.com/Woett/Mathematical-shorts/blob/a65db1e49e255ca363768cc51398f73079520dd5/Short%20Egyptian%20fractions.pdf Woett/Mathematical-shorts], commit <code>a65db1e</code>) || Exposition (simplified proof) || A human-written exposition and simplification of the proof of the first theorem, giving at most (16/log 2 + ''o''(1)) log log ''b'' terms. In comments on the blog post above, the author discusses which arguments of the manuscript its Lean formalizations follow. || Note; the author states on the blog that it was written with the help of ChatGPT.
|-
| 2026-10-10 (current file dated 15 October 2026) || T. F. Bloom, W. van Doorn, ''Optimal bounds for the length and number of unit fraction representations'' ([https://www.erdosproblems.com/static/UnitFractions.pdf PDF] on erdosproblems.com) || Exposition (simplified proofs) || A human-written exposition and simplification of the proofs of all three results, with a section comparing them with the manuscript's proofs; the authors describe the manuscript as difficult to read and as containing much unnecessary material. || 15-page PDF hosted on erdosproblems.com.
|-
| 2026-10-10 || cert-machine, openai/math lane K: runs [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/ShortEgyptianFractions.json 38019899278] and [https://github.com/carlostoledo1891/cert-machine/blob/910dddee72220b30c85da00fc414b6c987f8c954/corpus/openai-math/kernel-runs/38051470892/EgyptianFractions.json 38051470892] || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>ShortEgyptianFractions</code> solution, in 443 s, and the <code>EgyptianFractions</code> solution, in 745 s. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) lists neither <code>EgyptianFractions</code> nor <code>ShortEgyptianFractions</code>, so both were accepted by con-leche and by Lean's official kernel. || Development journal.
|}

== Notes ==
* The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
* 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]]

Erdős's conjecture on short Egyptian fractions - Revision history

Aftermath bot: Add Hexagon and Palomar follow-ups and the quasi-Riemann tracker

Aftermath bot: New page on short Egyptian fractions