Erdős Problem 728: AI Proof, Lean Check & Autonomy Claim

What Erdős Problem 728 asks

Erdős Problem 728, as catalogued on the Erdős Problems website, asks how large the gap k, defined as a + b minus n, can be while the factorial divisibility a! b! divides n! k! still holds. Equivalently, writing N for a + b, the question is how large a binomial coefficient's denominator can be forced to divide its numerator's neighbor. [1]

The writeup's Theorem 1 shows that for any two constants setting a window, there exist infinitely many triples with a and b kept away from the extremes and with the gap k squeezed to logarithmic size in n, roughly between C1 log n and C2 log n. The proof reduces the factorial condition to a binomial divisibility, then to a prime-by-prime carry count under Kummer's theorem: it constructs integers whose base-p digits force many carries when doubled, for every relevant prime, while avoiding the rare case where a nearby integer carries an unusually high power of that prime. [1]

Terence Tao is credited in the writeup with observing that the logarithmic bound is not the best possible: the same argument's own error terms allow the gap to grow as fast as exp(c times the square root of log n) for a small constant c. Days after an earlier draft circulated, Carl Pomerance independently wrote up a closely related extension of his own 2015 work on middle binomial coefficient divisors, and the author calls the two results very similar. [1]

Four days from claim to formal proof

On January 4, 2026, Kevin Barreto announced on the Erdős Problems forum that he had a proof from Aristotle, Harmonic's Lean-based proving system, built from an informal argument supplied by GPT-5.2 Pro. The Erdős Problems website's statement of the problem was vague enough at the time that Barreto's version resolved only one reading of it, and forum participants judged the result a partial one rather than a full resolution. [1]

On January 5, once forum participants had settled on which reading was the intended problem, Barreto asked GPT-5.2 Pro whether its argument could be upgraded to cover it. GPT-5.2 Pro said it could, and Aristotle produced a formal Lean proof from that response on January 6. [1][2]

A dispute followed over whether that January 6 proof secretly depended on a human mathematical observation, which would have broken the autonomy claim. Barreto stated this was a misunderstanding and that no such observation had been supplied. Terence Tao then said publicly that he regarded the result as autonomous, which the writeup describes as cementing the forum's consensus. Separately that same day, Boris Alexeev ran Aristotle again on the proof to simplify it, producing the Lean file the present writeup is based on. [1]

What the autonomy claim covers, and what it doesn't

A forum participant using the name KoishiChan then searched the literature for any prior proof of the problem, a search the writeup says that same person has succeeded at before against other AI-claimed results. No such literature turned up, which is the basis for treating this as newly resolved rather than a rediscovery, though the writeup is explicit that it cannot rule out literature nobody has found yet. [1]

Atlas interpretation: The autonomy claim is narrow by the writeup's own account: it covers the informal argument and the formal Lean proof behind Theorem 1, credited to GPT-5.2 Pro and Aristotle and operated, not authored, by Barreto. It does not cover the document a reader encounters. The author says a large fraction of the writeup's prose was drafted by ChatGPT and checked by hand to roughly the standard he would hold his own writing to, and the result also carries acknowledged human contributions distinct from the proof itself: Alexeev's simplification pass, KoishiChan's literature search, and further ideas and references from Tao. None of that human and second-AI-tool involvement touches the mathematical content the autonomy claim is about, but a reader taking 'resolved autonomously by an AI system' to mean the paper arrived with no other hands on it would be reading past what the writeup itself says. [1]

The same pairing kept going

The same argument, run again through GPT-5.2 Pro and Aristotle, was credited with resolving two further Erdős problems within the week: Problem 729 on January 10 and Problem 401 on January 11, both closely related divisibility questions about the same family of binomial coefficients. [1]

Atlas interpretation: All three problems trace back to the same handful of papers on prime divisors of central binomial coefficients, so the week reads less as evidence of breadth across Erdős's open list and more as one well-scoped corner of it getting cleared quickly once a working template existed. OpenAI's math-focused models kept working that same corner through the year, later credited with disproving a decades-old unit distance conjecture and, by August, with resolutions of three more Erdős problems among a larger batch of results, each with the same kind of machine-checked Lean certificate this writeup describes for Problem 728. [1]