Problem 729

Let $C>0$ be a constant. Are there infinitely many integers $a,b,n$ with $a+b> n+C\log n$ such that the denominator of

\frac{n!}{a!b!}

contains only primes $\ll_C 1$ ?

Source: erdosproblems.com/729

Number theory
Factorials

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

PROVED (LEAN). The site labels the problem PROVED (LEAN) (page last edited 11 January 2026) and credits Barreto and Leeham, using ChatGPT and Aristotle, for an affirmative proof that modifies the argument used for Problem 728; the result is recorded on the claim page Barreto and Price 2026. The Lean qualifier refers to Aristotle's formalization of the GPT-5.2 Pro argument, in Boris Alexeev's repository of formalized Erdős problems, which this corpus has not built; nothing is refereed. The standing in the frontmatter derives from the claim page.

Er68c: P. Erdős, Aufgabe 557. Elemente Math. (1968), 111-113.
EGRS75: Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of $(\sp{2n}\sb{n})$ . Math. Comp. (1975), 83-92. Library home: Erdős et al. 1975.
So26: Sothanaphan, N., Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof. arXiv:2601.07421 (2026). Library home: Sothanaphan 2026.

Problem 729

Status

Proof claims

Discussion