The Erdos-Graham Semiprime Unit Fraction Problem
Every natural number is a finite sum of distinct unit fractions whose denominators are semiprimes. This is the integer case of a problem of Erdos and Graham, left as a conjecture by Butler, Erdos and Graham, who proved the analogue.
- Result
- Proved(see note)
- Status
- Resolved
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Number theory
- Posed by
- Paul Erdos, Ronald Graham
- Year posed
- 2015
- Years open
- 11y
- Solved
- 2026-06-13
- Model
- Claude (via Claude Code)
- Vendor
- Anthropic
- Collaborators
- Shisheng Li
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 15 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
the omega = 2 integer case, the one Butler, Erdos and Graham left open
What the AI did
The paper describes itself as a human-AI collaboration and says the tools contributed substantially to the Lean formalisation.
Verification
A Lean formalisation accompanies the work, with the model credited as a substantial contributor to it. We have not compiled it. arXiv preprint, not peer-reviewed.
Source
arXiv:2606.15159 - Every natural number is a sum of distinct semiprime unit fractions