Did an AI system truly solve Erdős Problem 728 autonomously?

The writeup describes its result as "the first Erdős problem ... regarded as fully resolved autonomously by an AI system." The system was GPT-5.2 Pro by OpenAI combined with Aristotle by Harmonic, operated by Kevin Barreto. Its final output is "a formal proof written in Lean," which the authors "translate to informal mathematics in the present writeup for wider accessibility." The theorem is a logarithmic-gap window: for constants 0 < C1 < C2 and 0 < ε < 1/2 there are infinitely many triples (a, b, n) with a! b! | n! (a + b − n)! and C1 log n < a + b − n < C2 log n. The excerpt keeps two objects apart: the Lean proof, which is the formal object carrying the result, and the informal writeup, which is the route a human reader takes to follow it. This note keeps the same split.

The mechanism reduces the problem to the binomial divisibility (m+k choose k) | (2m choose m), with n = 2m, b = m and a = m + k. Working prime by prime, Kummer's theorem turns the p-adic valuation of (2m choose m) into a count of carries when m is doubled in base p (Lemma 3). A counting argument then selects, in each scale [M, 2M], an m whose base-p digits force many carries for every prime p ≤ 2k, while avoiding the case where one of m+1, …, m+k is divisible by an unusually high power of p. Lemma 4 bounds the factorial-weighted count by νp(k!) plus the largest single valuation in the window, and Lemma 5 treats primes above 2k as holding "for free." The writeup is terse at points: the proofs of Lemmas 1 and 2 consist of the single word "Immediate."

Against the nearest notes, the contrast with the Darwin Gödel Machine is sharp. Can AI systems improve themselves through trial and error? swaps formal proof for empirical validation on benchmarks. Here the object that counts is a formal proof, and the search runs over mathematical argument rather than over the system's own code. The guardrails pattern is a closer relation: Can deterministic checks protect LLM judges from failure? puts unarguable checks first. A Lean proof is about the most unarguable check available, and this source gives a case of one used without any LLM judgment at all.

The excerpt does not include the Lean code, the formal statement of Theorem 1, or the Lean check itself, so it cannot confirm that the formal statement matches the problem as posed. It also omits the proof of Lemma 6, which moves straight to "Conclusion," and it cites Lemma 14 for the existence of the good m without showing it. That existence step carries the most weight, so it is asserted here, not shown. "Autonomously" describes the proof search, and the excerpt names a human operator, so the autonomy claim is the authors' and the excerpt does not test it. At the strength the excerpt allows, it supports that a formally checked proof is described and that the writeup gives an informal route to it. It does not show that readers outside the authors have followed the argument, or what the system itself grasped.