The first Erdos problem is closed by AI autonomously
A human writeup appeared on arXiv of a formal Lean proof produced by GPT-5.2 Pro together with Harmonic's Aristotle. The abstract states this is the first Erdos problem regarded as fully resolved autonomously by an AI system.
Why it matters
For the first time a named open problem from the Erdos list was closed by machine, and the answer is checkable in Lean rather than dependent on a referee's judgement.
Nat Sothanaphan submitted the paper on 12 January 2026, with a last revision on 26 January. The proof came from two systems working together: OpenAI's GPT-5.2 Pro produced an informal argument and Harmonic's Aristotle turned it into a formal Lean proof, both operated by Kevin Barreto. The paper itself is a translation of the formal proof into ordinary mathematical exposition so that people can read it. The mathematical content: for infinitely many triples where a!b! divides n!k!, the gap k = a + b - n is of logarithmic order, lying between C1 log n and C2 log n. Barreto had announced the result publicly on 4 January, but forum participants noted that the problem statement was ambiguous and initially treated the proof as partial; the argument was brought to the intended version over the following days.