Erdős problem #728 resolved and formalized in Lean
Erdős problem #728 resolved and formalized in Lean is graded formally verified on whataifound.org, with the AI's role graded autonomous.
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.
- Verification
- Formally verified
- Autonomy
- Autonomous
- Lab
- OpenAI / Harmonic
- Model
- GPT-5.2 Pro + Aristotle
- Field
- Mathematics
- Date
- 2026-01-13
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
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
Sources
How this is graded
whataifound.org grades every entry on two axes: verification (how solid the result is, from a machine-checked proof down to refuted) and autonomy (how much the AI did versus its human collaborators). This finding is formally verified and autonomous. Full definitions are in the methodology.
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-728