Erdős Problem #728 — Factorial Divisibility
Erdős problem #728 · erdosproblems.com/728
Whether there are infinitely many integers a, b, n with a, b ≥ εn such that a!·b! divides n!·(a+b−n)! while a+b exceeds n by more than C·log n.
- Result
- Proved
- Field
- Number Theory
- Posed by
- Paul Erdős, Ronald Graham, Imre Ruzsa, Ernst Straus
- Year posed
- 1975
- Years open
- 51y
- Solved
- 2026-01-06
- Model
- Aristotle (Harmonic) + GPT-5.2 Pro
- Vendor
- Harmonic / OpenAI
- Collaborators
- Boris Alexeev, Kevin Barreto, Liam Price, Nat Sothanaphan
- Verification
- Expert-verified
- Notability
- No dedicated article
What the AI did
Aristotle (Harmonic's Lean-based prover) and GPT-5.2 Pro produced a fully autonomous, Lean-verified proof. Regarded by the erdosproblems.com maintainers as the first Erdős problem resolved autonomously by AI systems, about three months before the more widely covered #1196 result.
Verification
Machine-checked end to end in the Lean proof assistant - every logical step formally verified, not just human-reviewed. Written up formally by Nat Sothanaphan.