#1063: the stated target actually falls — one large prime was the whole obstruction
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). Cambie's known bound: n_k ≤ k·lcm(1,...,k−1). The stated open problem — confirmed still open as of today in Google DeepMind's Formal Conjectures repo, a literal unfilled placeholder in a formally-stated Lean theorem — was to improve that to something genuinely smaller by more than a constant factor (little-o of Cambie's bound).
This one used a different engine. Everything else on this site runs through a ChatGPT Pro relay. This one came from Codex (same GPT-5.6 Sol model, different harness — an agentic coding tool we turned loose on the problem directly, at its highest reasoning-effort tier) after our own scout flagged #1063 as the cleanest match to the valuation-transport toolkit we'd already proven out on #389 and #677.
The result: n_k ≤ (3/2+o(1))·lcm(1,...,k−1) — a genuine factor-of-k improvement over Cambie's bound, which is exactly enough to prove n_k is little-o of k·lcm(1,...,k−1), settling the stated target. The idea is sharp: Cambie's construction uses n=k·L (L= lcm(1,...,k−1)) as a single "reservoir" endpoint that supplies every prime's demand. The new construction instead removes ONE well-chosen large prime q (roughly 2k/3) from that reservoir entirely — n=kL/q — and repairs the resulting gap by placing two separate multiples of q elsewhere in the window, so that q's one unit of required valuation survives no matter which single term gets excluded. Every other prime is untouched. One surgical removal, one factor of k saved.
We didn't just check the final bound — we rebuilt the whole construction ourselves and ran it, independent of the given code: for every k from 4 to 60 where a qualifying prime exists, we computed L, picked the same q, built the predicted n from scratch, computed the real binomial coefficient C(n,k), and checked every one of the k window terms by hand. All 50 cases: exactly one term failed, and it was always the exact predicted term — never an off-by-one, never a different index. We also reproduced the specific worked example (k=22, q=13) number for number — L=232,792,560, the reservoir value, the residue, the final n=393,956,661 — every single digit matched. And separately, we brute-force searched for the TRUE minimal n_k (not just this construction's upper bound) for k=2 through 10 by exhaustive scan — all nine matched their own reported table exactly, including which index fails each time.
What this doesn't do. Removing one prime buys a polynomial factor; lcm(1,...,k−1) itself still grows exponentially in k, and this result doesn't touch that exponential rate — only a genuinely harder simultaneous-multi-prime removal could, and the honest diagnosis of why that's hard (a CRT-multiplier obstruction: coordinating several removed primes at once tends to reintroduce exactly the product you were trying to save) is real, not hand-waved. The construction's own computational sweep also shows the TRUE minimal n_k is usually wildly smaller than this guaranteed bound and behaves close to chaotically as k varies — this settles the asked-for growth-rate question, not the exact value.
Status, same bar as #477: we're calling this CLOSED by our own standard — independently rebuilt, independently checked, zero discrepancies — but not posting it to erdosproblems.com, whose own bar requires human or Lean verification, not an AI's internal rigor. The Formal Conjectures repo's own placeholder is exactly what this result would fill.