Erdős problem #728 resolved and formalized in Lean
GPT-5.2 produced a proof of a previously open Erdős problem; Harmonic's Aristotle formalized it in Lean, making it the first Erdős problem regarded as fully resolved by AI with machine-checked proof.
- Model
- GPT-5.2 Pro + Aristotle
- Field
- Mathematics
- Date
- 2026-01-13
Sources
Original work
Media coverage
What was found
The problem concerns the existence of infinitely many integers a, b, n satisfying divisibility and inequality conditions involving factorials. GPT-5.2 generated the argument, Aristotle formalized it in Lean, and a human-readable writeup was posted to arXiv. Modifications of the same argument also resolved problems #729 and #401.
Novelty check
Recorded as open in the Erdős problems database prior to resolution. Terence Tao's AI-contributions wiki tracked the resolution and did not find the result in existing literature.
Caveats and known objections
Tao cautioned that the win 'says more about speed than difficulty': the problem was open but not considered deep. Lean formalization makes correctness essentially certain; significance is the contested part, not validity.
Independent checks
The open problem
315787
Nothing mechanically. It records what a problem says, what is known about it, and the standing of any claimed solution.
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
History of this entry
- CorrectedRecorded the MathDB record for this problem as a registration. No grade moved.
- AddedEntered the registry graded Formally verified and Autonomous.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and autonomous for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Erdős problem #728 resolved and formalized in Lean. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-01-erdos-728BibTeX
@misc{whataifound-openai-2026-728,
title = {Erdős problem #728 resolved and formalized in Lean},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by OpenAI / Harmonic. Verification: Formally verified. Autonomy: Autonomous.},
url = {https://whataifound.org/finding/2026-01-erdos-728}
}