Lean formalization in OpenAI math repository (Result 025)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Short Egyptian fractions'. We prove a conjecture of Erdős: for every sufficiently large integer b, every rational number a/b with 1\le a\lt b is a sum of O(\log\log b) distinct positive unit fractions, with an absolute implied constant. This order is best possible when the numerator varies. We also show that both the number of expansions of 1 with exactly k distinct terms and the least integer at least 2 that never occurs as a denominator in such an expansion grow doubly exponentially in k: their double logarithms have order k.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 025). The Lean development was not rebuilt locally.