Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof
Nat Sothanaphan
TL;DR
The paper resolves Erdős Problem #728 by proving a logarithmic-gap phenomenon: there exist infinitely many triples with $a!\,b! \mid n!\, (a+b-n)!$ and $C_1\log n < a+b-n < C_2\log n$. The approach reduces to showing $\binom{m+k}{k} \mid \binom{2m}{m}$ with $k \asymp \log m$, and uses Kummer's theorem to interpret $v_p\bigl(\binom{2m}{m}\bigr)$ as carries in base $p$; the construction enforces many carries for all primes $p\le 2k$ while avoiding spikes via a probabilistic interval argument and Chernoff bounds. A carry-rich, spike-controlled selection of $m$ in each scale $[M,2M]$ yields the desired divisibility, and the result is formalized in Lean with a detailed correspondence to the informal proof. The work connects to and extends classical results on central binomial divisors, illustrating an autonomous AI-driven path to a nontrivial number-theoretic result and providing a formal certificate of correctness.
Abstract
We provide a writeup of a resolution of Erdős Problem #728; this is the first Erdos problem (a problem proposed by Paul Erdős which has been collected in the Erdos 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<C_1<C_2$ there exist infinitely many triples $(a,b,n)\in\mathbb N^3$ such that \[ a!\,b!\mid n!\,(a+b-n)!\qquad\text{and}\qquad C_1\log n < a+b-n < C_2\log n. \] The argument reduces this to a binomial divisibility $\binom{m+k}{k}\mid\binom{2m}{m}$ and studies it prime-by-prime. By Kummer's theorem, $ν_p\binom{2m}{m}$ 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\le 2k$, while avoiding the rare event that one of $m+1,\dots,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 $\binom{2n}{n}$ studied earlier by Erdős and by Pomerance.