---

Claim. The answer to Problem 728 is yes, in the reading the site's commentary identifies as the intended one. For every $0<\varepsilon<1/2$ and every $0<C_1<C_2$ there are infinitely many triples $(a,b,n)$ with $\varepsilon n\le a,b\le(1-\varepsilon)n$,

$$a!\,b!\mid n!\,(a+b-n)! \qquad\text{and}\qquad C_1\log n<a+b-n<C_2\log n.$$

The examples have $n=2m$, $b=m$ and $a=m+k$ with $k\asymp\log n$, so the divisibility is $\binom{m+k}{k}\mid\binom{2m}{m}$, and the triples satisfy the statement's $a,b\ge\varepsilon n$ and $a+b>n+C\log n$ for every $C$. The statement as the site prints it also has trivial solutions, for instance $a=b=n$, which is why the commentary reads the question with an upper bound on $a$ and $b$; the theorem answers that reading, and the literal one with it.

Submission note. Posted to the site's forum by Kevin Barreto on 5 January 2026:

On the edit: I had noticed that as well prior to your edit and had asked GPT-5.2 if it could be fixed, and it said that, quote: "If we instead use $k!$ that is already present in $(2m)! k!$, then the main $k/(p-1)$ contribution cancels and you only need carries to beat an $O(\log k)$ (plus rare "spike") error". I asked it to produce a new PDF with this correction, and it has given the following here. Again, I do not claim accuracy of this informal paper, and Aristotle is still in the process of attempting to formalise GPT-5.2's new attempt.

Posted to the site's forum by Kevin Barreto on 6 January 2026:

Aristotle has successfully formalised GPT-5.2's new attempt here. It takes a long time to compile and is not very readable, so I am currently working on making things more readable.

I believe we have reached a consensus that this should constitute a non-trivial, full resolution to the problem.

(The site has been updated to address this comment.)

The argument. For a prime $p$, Kummer's theorem makes $\nu_p\binom{2m}{m}$ the number of carries when $m$ is added to itself in base $p$, and $\nu_p\binom{m+k}{k}$ is at most the largest $\nu_p(m+i)$ with $1\le i\le k$ (for $p>2k$ exactly the valuation of $(m+1)\cdots(m+k)$). Primes $p>2k$ are handled directly: a high power of $p$ dividing some $m+i$ forces as many carries. For $p\le2k$ the proof counts, on each dyadic interval, the $m$ with too few carries (a Chernoff bound on the base-$p$ digits) and the $m$ with an unusually high prime power among $m+1,\ldots,m+k$, and a union bound over these primes leaves an $m$ that is good for every $p$ at once; no sieve input and no Chinese remainder step is needed. The informal argument was produced by the AI system ChatGPT-5.2 (GPT-5.2 Pro), the formal proof by Harmonic's Aristotle. Kevin Barreto submitted both to the site's discussion thread, is the claimant here, and names the two systems; the thread records that a first attempt of 2026-01-04 only reached $a+b-n=c\log n$ for a small constant $c$. Barreto posted the informal proof for every $C$ on 2026-01-05, saying they did not claim its accuracy, and the Lean proof on 2026-01-06; both postings are linked above, and the page is dated by the posting of the formally verified proof because the earlier post disclaimed accuracy.

Formalization. The Lean development linked above at its pinned commit, in Boris Alexeev's repository of formalized Erdős problems, is Aristotle's proof rerun by Alexeev to shorten it, and it includes a proof of the statement in the formal-conjectures project, which adds the upper bound $a+b<n+C'\log n$ on the gap. The same file, at the repository's current Lean version, is the second formalization link; that version carries the header naming ChatGPT-5.2 and Barreto as the informal authors and Aristotle, Barreto and Alexeev as the formal authors. The informal proof was written up as a paper by Nat Sothanaphan, Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof, arXiv:2601.07421 (first version 2026-01-12), whose Theorem 1 is the statement above with the $(1-\varepsilon)n$ bound and whose appendices derive the same method's consequences for Problems 729 and 401; the writeup is carded at Sothanaphan 2026. This corpus has not built or audited the Lean development, so the page lists no formalized evidence.

Depends on. No page of this wiki.

Acceptance. Thomas Bloom, the site's curator, marks the problem proved and credits Barreto and ChatGPT-5.2 on the problem page (last edited 6 January 2026), which the page lists as reviewed; the community database records the problem as proved, with a Lean proof, as of its last update on 2026-01-05. The writeup is an arXiv preprint and nothing is refereed. A separate proof by Carl Pomerance, published in Integers, is on the claim page Pomerance 2026, and two later AI-generated proofs are on the page Pickhardt 2026.