An AI-Derived Proof of Erdos Problem #728 via Higher-Power Carry Compensation

Jeff Pickhardt

Loading document…

An AI-Derived Proof of Erdos Problem #728 via Higher-Power Carry Compensation

Abstract

We present a complete, self-contained resolution of Erdos Problem #728, a question of Erdos, Graham, Ruzsa, and Straus that remained open until January 2026. Our proof was created autonomously by the Omniscience Research Agent, an AI system, at a total compute cost of under $10 USD. The agent was run in a strict anti-cheat configuration: it operated on a reasoning model whose knowledge predates the first published resolution of the problem, and it was walled off from any existing solution, write-up, or record of partial progress. A post-hoc audit of the agent’s complete research trace confirms that it consulted only standard background material (classical sieve theory together with the theorems of Legendre and Kummer) and never accessed a known solution. Working from first principles, the agent produced a proof that is methodologically distinct from all prior work on the problem: whereas the January 2026 resolution and the surrounding literature on the divisibility of central binomial coefficients proceed by probabilistic “carry-rich” or “carry-poor” digit arguments, the proof given here is deterministic, resting on an exact small-prime congruence together with a higher-power carry-compensation device: a unit carry deficit at a large prime p is offset by a surplus carry at a higher power pj of the same prime. We verify that this compensation technique does not appear in the established literature on the problem. The upshot is the full theorem: for every 0 <C1 <C2 and every fixed 0 <ϵ< 1 2 , there are infinitely many triples of positive integers a,b,n with ϵn≤a,b≤(1−ϵ)n such that a! b! |n! (a+ b−n)! and C1 log n<a+ b−n<C2 log n, the gap driven to an arbitrary prescribed constant multiple of log n, not merely a small one. We also check the proof with Lean, and share a link to the repo. A companion paper presents a second methodologically distinct proof of Erdos Problem #728 as well.

File Details

v2 erdos728.pdf