Erdős Problem #729

Full solution by Aristotle and GPT-5.2 Pro, formalized in Lean (8 Jan 2026).

Problem
Erdős problem #729 (number theory, factorials); current status: proved (Lean)
Credit
Aristotle and GPT-5.2 Pro · AI building on known literature
Checked
Lean formalizationListed in Tao's wiki
Timeline
First AI contribution 2026-01-08 · wiki data as of 2026-06-30
Sources
Problem page (erdosproblems.com)Tao's AI-contributions wiki
SOLVEDPer Tao's AI-contributions wiki

The problem

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

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

contains only primes ≪C1\ll_C 1?

Statement quoted from erdosproblems.com/729, maintained by Thomas Bloom. Original source: [EGRS75]. Current status there: proved (Lean).

AI contributions

As recorded in Terence Tao's wiki AI contributions to Erdős problems (data as of 30 Jun 2026). 🟢 full, 🟡 partial, ⚪ unverified, 🔴 incorrect.

Date Kind AI systems Outcome Literature
8-10 Jan, 2026 AI building on known literature Aristotle, GPT-5.2 Pro 🟢 Full solution (Lean) 🟡 Aristotle, Barreto, and GPT-5.2 Pro (2026) (full solution to [728])
Jan 10, 2026 Literature search ChatGPT Deep research 🟡 Related results found —

Caveats

The wiki's classifications are provisional and are not a benchmark. Many Erdős problems have never had a thorough literature review, so a result that looks new may later turn out to be known; some problems were also stated ambiguously or incorrectly. See the problem page for the full discussion.

∎