#1063: a real upper-bound jump on n_k — corrected after a reader caught us overclaiming it
Correction, first. The version of this entry that shipped yesterday described a different, weaker construction (removing one large prime, bound n_k ≤ (3/2+o(1))·lcm(1,...,k−1)) under a title that read like the Erdős problem itself had fallen. A reader on X, @Liam06972452, correctly called that out on both counts: it was only ever a partial result, and we'd posted prose, not an actual checkable proof. Fair on both. Worse, when we went to write up a proper proof to publish, we couldn't find any saved derivation of that specific weaker bound anywhere in our own working files — only this stronger, fully-documented result below, computed the same day but never shipped. We don't have a clean explanation for that gap and aren't going to pretend we do. What follows is the real, corrected result, independently re-verified before publishing.
The target (erdosproblems.com/1063). n_k is the least n≥2k such that all but one of n, n−1, ..., n−k+1 divides C(n,k). The page's own statement of the problem is simply "estimate n_k" — open-ended, and nothing here closes it. Cambie's known bound: n_k ≤ k·lcm(1,...,k−1) ≤ exp((1+o(1))k). A specific, formalized, narrower target does exist and is what we're actually answering: Google DeepMind's Formal Conjectures repo has a Lean theorem, tagged "research open," asking for any upper bound that's little-o of Cambie's — a literal unfilled placeholder, confirmed still open the day we worked on it.
The result: n_k ≤ exp(C·k·log log k / log k) for an absolute constant C — so n_k = exp(o(k)), which is substantially stronger than the little-o improvement asked for: it pulls the exponent's whole leading order down, not just a polynomial factor off it. This came from Codex (GPT-5.6 Sol, agentic coding tool, highest reasoning-effort tier), given the exact valuation-transport reformulation of the problem (write C(n,k) = ∏(n−i)/k!; divisibility becomes a prime-by-prime demand-vs-supply covering condition) after our scout flagged #1063 as a clean match to the same toolkit that closed pieces of #389 and #677.
The idea. The naive fix — demand one extra multiple of every prime power p^a≤k, to survive any single deletion — is provably impossible whenever p^a divides k exactly (that level can never have a surplus, for any n). The real construction instead designates one "excused" coordinate E≈k/(log k)³ and lets primes fail at that coordinate on purpose: small primes get extra p-adic depth stacked there; "exceptional" large primes get a forced p² there; "regular" large primes get centered into a window via simultaneous Dirichlet approximation. Every non-excused coordinate ends up covered from one of three independent directions; the excused one is proven, not assumed, to be the sole failure.
Independently re-verified before publishing, not just checked once: a from-scratch checker recomputes every valuation two independent ways (Legendre's floor formula and Kummer's carry count), recomputes the demand/supply dictionary directly, and for moderate k builds the actual big-integer C(n,k) and checks every remainder. Re-run fresh across 17 values of k from 4 to 300 (5 of them new, outside the original run) — every single one: exactly one failing coordinate, always the predicted one, zero exceptions.
What this doesn't do — same honest caveat as before, just higher up now instead of buried at the end. lcm(1,...,k−1) itself still grows like exp(k); this result doesn't touch that. Our own computational sweep shows the TRUE minimal n_k is usually far smaller than this guaranteed bound and behaves close to chaotically as k grows — this fixes the growth-rate target that was asked for, not the exact value, and Erdős's actual "estimate n_k" stays open.
The full proof, publicly checkable this time. Same bar as #477 — independently rebuilt, independently re-verified, zero discrepancies, but not posted to erdosproblems.com, whose own bar is human or Lean verification, not an AI's internal rigor. Unlike yesterday's version, there's now an actual proof document with a runnable checker, not just a summary.