2026/01/12 by Nat Sothanaphan · 2 voices · 3 citations
Mathematics · #math.NT
arxiv published 2026/01/12 · arxiv updated 2026/01/26
We provide a writeup of a resolution of Erdős Problem #728; this is the first Erdős problem (a problem proposed by Paul Erdős which has been collected in the Erdős Problems website) regarded as fully resolved autonomously by an AI system. The system in question is a combination of GPT-5.2 Pro by OpenAI and Aristotle by Harmonic, operated by Kevin Barreto. The final result of the system is a formal proof written in Lean, which we translate to informal mathematics in the present writeup for wider accessibility. The proved result is as follows. We show a logarithmic-gap phenomenon regarding factorial divisibility: For any constants 0<C1<C2 and 0 < ε < 1/2 there exist infinitely many triples (a,b,n)∈\mathbb N3 with ε n ≤ a,b ≤ (1-ε)n such that a! b!| n! (a+b-n)!\qquadand C1log n < a+b-n < C2log n. The argument reduces this to a binomial divisibility \binomm+kk|\binom2mm and studies it prime-by-prime. By Kummer's theorem, νp\binom2mm translates into a carry count for doubling m in base p. We then employ a counting argument to find, in each scale [M,2M], an integer m whose base-p expansions simultaneously force many carries when doubling m, for every prime p≤ 2k, while avoiding the rare event that one of m+1,…,m+k is divisible by an unusually high power of p. These "carry-rich but spike-free" choices of m force the needed p-adic inequalities and the divisibility. The overall strategy is similar to results regarding divisors of \binom2nn studied earlier by Erdős and by Pomerance.