Erdős Problem #1095

Partial progress by Aristotle (30 Dec 2025): new proof of (slightly weaker) partial result (Lean). 2 AI contributions are recorded in all.

Problem
Erdős problem #1095 (number theory, binomial coefficients); current status: open
Credit
Aristotle · AI building on known literature
Checked
Lean formalizationListed in Tao's wiki
Timeline
First AI contribution 2025-12-30 · wiki data as of 2026-06-30
Sources
Problem page (erdosproblems.com)Tao's AI-contributions wiki
PARTIALPer Tao's AI-contributions wiki

The problem

Let g(k)>k+1g(k)>k+1 be the smallest nn such that all prime factors of (nk)\binom{n}{k} are >k>k. Estimate g(k)g(k).

Statement quoted from erdosproblems.com/1095, maintained by Thomas Bloom. Original source: [EES74]. Current status there: open.

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 Humans Outcome Literature
30 Dec, 2025 AI building on known literature Aristotle — 🟡 New proof of (slightly weaker) partial result (Lean) 🟡 Ecklund, Erdős, and Selfridge (1975)
13 Mar, 2026 AI working with humans Claude Opus 4.6, Gemini 3.1 Pro, GPT-5.4 Pro shtuka 🟡 Partial result —

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.

∎