# Erdős Problem #1063: a substantially stronger upper bound on n_k **The problem** ([erdosproblems.com/1063](https://www.erdosproblems.com/1063), Erdős–Selfridge [ErSe83]). Let n_k be 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."** That is open-ended — it does not ask for one specific bound, and it stays open no matter what follows here. Known prior bounds: Monier's n_k ≤ k! (k≥3), sharpened by Cambie (in the page's comments) to n_k ≤ k·lcm(1,…,k−1) ≤ e^{(1+o(1))k}. **What this repository actually claims — read this before the theorem below.** We are **not** claiming to have solved Erdős Problem #1063. We are claiming to have proved a genuine, checkable theorem that answers a *narrower*, precisely-formalized sub-question: Google DeepMind's [Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) project has a Lean theorem, `erdos_1063.better_upper`, tagged `category research open`, whose statement is exactly "find any upper bound for n_k that is little-o of Cambie's k·lcm(1,…,k−1) bound." That specific, formally-stated target is what the theorem below fills. The general "estimate n_k" question is much bigger than that — our own computations (§6) show the *true* minimal n_k behaves close to chaotically as k grows, nowhere near matching this bound — and it remains completely open here. **Correction note (2026-07-25).** An earlier public description of this result (on [erdosproblemaday.com](https://erdosproblemaday.com)) stated a different, much weaker bound — n_k ≤ (3/2+o(1))·lcm(1,…,k−1), via a "single large prime removed" construction — with a title that read as though the Erdős problem itself had been resolved. A reader on X ([@Liam06972452](https://x.com/Liam06972452)) correctly flagged both that this was only ever a partial result, and that no actual checkable proof had been published, just prose. On investigation we could not locate any saved derivation of that specific weaker bound or its worked example anywhere in our own working files — only this stronger, fully-documented result below, which had been computed the same day but never made it onto the site. The site entry has been corrected and now points here. We're leaving this note because the mistake is worth being visible about, not because it changes anything about the theorem below, which stands on its own and was independently re-verified before this repository was published. **Provenance:** the construction was produced by GPT-5.6 Sol via Codex (OpenAI's agentic coding tool, at its highest reasoning-effort tier), given the exact valuation-transport reformulation of the problem and told to either find a genuine improvement or a precise negative diagnosis — either would have been a valid, useful output. It found the improvement below. Independently re-verified by Claude (Anthropic) via a from-scratch checker (§6) re-run fresh for this repository across 17 values of k from 4 to 300, zero discrepancies. **We have not sought review from a human mathematician or a different model lineage, and this has not been posted to erdosproblems.com's own forum** — their posting rules require independent human or Lean verification before posting there, and an AI's internal rigor, however careful, doesn't clear that bar on its own. This repository is offered for outside scrutiny. — Patrick White & Claude (MathDyad) --- ## Theorem There is an absolute constant C such that, for all sufficiently large k, n_k ≤ exp( C · k·log log k / log k ). In particular, n_k = exp(o(k)) = o( k · lcm(1,…,k−1) ). This is substantially stronger than the little-o improvement the DeepMind placeholder asks for — Cambie's bound is exp((1+o(1))k); this pulls the exponent's leading order down to o(k) entirely, not just by a polynomial factor. The construction is explicit apart from one standard simultaneous Dirichlet pigeonhole step, which is itself constructive by direct search over at most Q^d boxes (and is executed literally, not just cited, in the checker at §6). ## 1. Exact valuation and carry dictionaries Write W_j = n−j (0 ≤ j < k), so C(n,k) = ∏ W_i / k!. For every prime p, W_j | C(n,k) ⟺ v_p(k!) ≤ Σ_{i≠j} v_p(W_i) ⟺ v_p(W_j) ≤ v_p(C(n,k)) for every p. (1)(2) For q = p^a, let c_{p,a}(n) = #{0≤iA_p}(c_{p,a}(n) − 1[p^a|n−j]). The first sum is Σ_p(n) − y_{p,j}. Every term of the second sum is nonnegative: since p^a > k, the window has at most one multiple of p^a, and if that multiple is n−j both terms are one. ∎ This is why prime powers above k never need individual control: a high power on a non-excused coordinate adds equally to that coordinate and to the binomial coefficient; a high power on the excused coordinate adds slack for every other coordinate. ## 2. The precise obstruction to level-by-level two-covering The most literal "deletion-resilient" proposal is to demand, at every level q=p^a≤k, one more multiple than the ⌊k/q⌋ demanded by v_p(k!). This is impossible whenever q | k, because then k mod q = 0 ⟹ ε_{p,a}(n) = 0 for every n (6). If additionally q ≤ k/2, the window has at least two multiples of q — one global deletion can't remove all of them. So any proof insisting each prime-power level separately survive deletion is blocked by every proper prime-power divisor of k. This is not a vague CRT difficulty; it names the exact levels where the naive surplus is arithmetically impossible. The repair has to transport surplus *between* different powers of the same prime — missing low-level surplus paid for by extra p-adic depth at the one excused coordinate. That's what the construction below does. ## 3. The finite construction Fix 1 ≤ E < k (the excused coordinate). Put r = k−1−E, ρ = max(E,r), y = max(E, ⌊√k⌋). Construct n = E + x, x = Sm (7). ### 3.1 Small-prime anchors For every prime p ≤ k: σ_p = Σ_{a=1}^{A_p} 1[E mod p^a < k mod p^a], T_p = max_{j≠E} v_p(E−j) = max{t : p^t ≤ ρ} (8), H_p = max(0, T_p − σ_p) (9). For small primes p ≤ y, require p^{A_p+H_p} | S (10). Accounting identity: at each p^a ≤ k, ⌊k/p^a⌋ − ⌊E/p^a⌋ − ⌊r/p^a⌋ = 1 − 1[E mod p^a < k mod p^a]. Summing over a: A_p − σ_p = v_p( k! / (E! r!) ) = v_p( k·C(k−1,E) ) (11). Since T_p ≤ A_p, H_p ≤ A_p − σ_p (12) — the total extra depth in (10) is controlled by the comparatively small integer k·C(k−1,E). ### 3.2 Large primes: exceptional and regular For p > y, p² > k. Put s_p = k mod p. Call p **exceptional** if s_p < 2E (13); require p²|S for every exceptional prime (14). All remaining p > y are **regular**, so s_p ≥ 2E (15) — these are coordinated simultaneously rather than placed into S. ### 3.3 Forcing exactly one failure By (11), D = k·C(k−1,E) > 1 has a prime divisor. Choose p* with A_{p*} − σ_{p*} = v_{p*}(D) > 0 (16). Augment S so p*^{A_{p*}+1} | S (17), removing p* from the regular set if needed (cost ≤ 2 log k in log S). This condition isn't needed to make the other k−1 coordinates work — it's included only to *prove from scratch* that coordinate E really fails, giving exactly one failure, not merely at most one. ### 3.4 Simultaneous approximation for the regular primes Let ℛ be the regular set after removing p*, d = |ℛ|. Set Q = ⌈k/E⌉ (18). By simultaneous Dirichlet pigeonhole, there is 1 ≤ m ≤ Q^d (19) with ‖mS/p‖ < 1/Q for every p ∈ ℛ (20) (‖·‖ = distance to nearest integer). *Proof, literal*: consider the Q^d+1 points ({tS/p})_{p∈ℛ}, 0≤t≤Q^d, partition the unit d-cube into Q^d boxes of side 1/Q; two points share a box, their nonzero index difference is m. Let z_p be the least-absolute residue of mS mod p; (18)+(20) give |z_p| < p/Q ≤ k/Q ≤ E (21). Set n = E + Sm. ## 4. Proof that the construction works Fix j≠E, d_j = E−j (d_j≠0, |d_j|0.** p^{A_p+1} > k > |d_j| divides x, so v_p(n−j)=v_p(d_j)≤T_p. The first A_p levels give σ_p carries; each of the next H_p levels has p^a>k, x≡0 mod p^a, n mod p^a = E < k = k mod p^a — another carry each. So v_p(C(n,k)) ≥ σ_p+H_p ≥ T_p ≥ v_p(n−j). **Case 3 — p>y exceptional.** p²>k, p²|x, so v_p(n−j)=v_p(d_j)≤1. At the p²-level, n mod p² = E < k = k mod p², giving v_p(C(n,k))≥1 — covers every non-excused coordinate regardless of the p-level. This is the cross-level repair of obstruction (6): a missing p-level surplus is replaced by a p²-level carry created at the excused coordinate. **Case 4 — p>y regular.** By (21), x≡z_p mod p, |z_p|k, the truncated covering lemma with A_p=1 covers every coordinate. Primes p>k never occur in k!, so cause no obstruction. This proves n−j | C(n,k) for every j≠E. **Coordinate E really fails.** Let b=v_{p*}(x)≥A_{p*}+1 (by (17)). The first A_{p*} levels give σ_{p*} carries; every level from A_{p*}+1 through b contributes one carry; no later carries occur (modulo p*^{b+1}, the nonzero base-p* digit of x/p*^b makes the residue exceed p*^b>k, and subsequent residues can't decrease). So v_{p*}(C(n,k)) = σ_{p*}+b−A_{p*} < b = v_{p*}(n−E), strict by (16) — n−E ∤ C(n,k), and E is exactly the one failure. ## 5. Size of the construction Choose E = ⌈k/(log k)³⌉ (22); for large k, E>√k so y=E. **Small-prime base cost.** Using θ(t)=Σ_{p≤t}log p, ψ(t)=Σ_{p^a≤t}log p, y≥√k: Σ_{p≤y} A_p log p = θ(y) + ψ(k) − θ(k) (23). Elementary Chebyshev bounds give θ(y)=O(y), ψ(k)−θ(k)=O(√k log k), so (23) is o(k). By (11)–(12), the extra small-prime depth Σ_{p≤y} H_p log p ≤ log(k·C(k−1,E)) ≤ log k + E log(ek/E) = o(k) (24). **Exceptional-prime cost.** For exceptional p>y, ℓ=⌊k/p⌋; k−ℓp<2E places p in (k−2E)/ℓ < p ≤ k/ℓ (25), with 1≤ℓ≤k/y — at most 2E/ℓ+1 integers per ℓ. So Σ_{exceptional p>y} log p ≤ log k · Σ_{ℓ≤k/y}(2E/ℓ+1) = O(log k·(E log(k/y)+k/y)) (26), which with (22) is O(k log log k/(log k)² + (log k)⁴) = o(k). The p² usage doubles this; the failure prime p* adds only O(log k). So log S = o(k) (27). **Simultaneous-approximation cost.** d≤π(k)=O(k/log k). From (18),(19),(22): Q=O((log k)³), log m ≤ d log Q = O(k log log k/log k) (28). Combining (7),(27),(28): log n = O(k log log k/log k). Since S contains every prime p≤y and θ(y)≫y≫log k, S>2k for k large, so n≥2k as required. (Finitely many small k are covered by Cambie's construction directly.) Since log lcm(1,…,k−1)=ψ(k−1)=k+o(k), n_k / (k·lcm(1,…,k−1)) ≤ exp(−(1−o(1))k) → 0 exponentially on the k-scale. ## 6. Reproducible verification `verify.py` has no third-party dependencies. It: (1) sieves primes; (2) builds S from (8)–(17); (3) executes the literal Q^d+1-point box collision to find m; (4) recomputes v_p(C(n,k)) by Legendre's floor formula; (5) independently recomputes the same valuations by the carry formula; (6) recomputes the demand v_p(k!) and the supply from the other k−1 window entries, for every j,p; (7) for moderate k, also constructs `math.comb(n,k)` directly and checks every remainder. ```bash python3 verify.py # the original default suite, k=10..250 python3 verify.py --k 300 --E 90 # spot-check any k (E defaults to the asymptotic rule) ``` **Independently re-run for this repository (2026-07-25), 17 values of k, zero discrepancies:** | k | E | n (truncated where huge) | bad index (predicted / found) | direct C(n,k) check | |---:|---:|---|:---:|:---:| | 4 | 2 | 74 | 2 / 2 | ✓ | | 5 | 2 | 1,802 | 2 / 2 | ✓ | | 10 | 1 | 75,601 | 1 / 1 | ✓ | | 13 | 1 | 56,216,161 | 1 / 1 | ✓ | | 16 | 1 | 86,486,401 | 1 / 1 | ✓ | | 19 | 1 | 79,615,055,521 | 1 / 1 | ✓ | | 23 | 1 | 2,709,239,813,281 | 1 / 1 | ✓ | | 30 | 8 | 6,457,926,418,504,637,076,008 | 8 / 8 | ✓ | | 50 | 12 | 1,154,891,394,816,897,005,531,813,086,911,934,560,012 | 12 / 12 | ✓ | | 60 | 14 | ≈6.97×10⁴³ | 14 / 14 | ✓ | | 100 | 21 | ≈3.27×10⁷⁵ | 21 / 21 | ✓ | | 125 | 25 | ≈6.14×10⁸⁸ | 25 / 25 | valuation-only¹ | | 150 | 29 | ≈1.65×10¹⁰⁸ | 29 / 29 | valuation-only¹ | | 175 | 33 | ≈9.08×10¹²² | 33 / 33 | valuation-only¹ | | 200 | 37 | ≈2.22×10¹⁵³ | 37 / 37 | valuation-only¹ | | 250 | 45 | ≈1.26×10¹⁸³ | 45 / 45 | valuation-only¹ | | 300 | 90 | ≈1.96×10²⁴⁷ | 90 / 90 | valuation-only¹ | ¹ Beyond k≈200 the direct `math.comb` check gets slow at these sizes; the valuation-based check (two independently-implemented formulas — Legendre floor-sum and Kummer carry-count — cross-checked against each other and against the construction's own accounting on *every* prime up to k, for *every* window coordinate) still runs and is itself two independent derivations agreeing, not a single trusted path. Every row above: exactly one bad index, always the predicted E, never an off-by-one or wrong coordinate. The k=4,5,30,50,300 rows are new for this repository (outside the original default suite's k=10–250 range); everything else reproduces the original run exactly. ## 7. What the construction says about the naive method The initial "two suitably placed coordinates at every prime power" idea has the right intuition and a fatal over-strong requirement: its exact obstruction is (6) — if p^a|k, that level can never have an extra multiple regardless of CRT choices, so demanding separate per-level surplus can't beat Cambie's bound uniformly (composite k already blocks it locally). Aggregating valuations across powers of the *same* prime removes the obstruction — one p²-carry at the excused coordinate covers a missing p-level for every other coordinate. Moving the excused coordinate from the endpoint to E≍k/(log k)³ makes the good-residue interval for every regular large prime contain the symmetric interval (−E,E) around the anchor — the symmetry that ordinary simultaneous Dirichlet approximation needs (at endpoint E=0 the intervals are one-sided and the same pigeonhole argument fails). Primes with too-short residue intervals are confined to thin neighborhoods of k/ℓ; their total p²-anchor cost is o(k), quantified in §5. So the CRT coordination itself isn't the ultimate obstruction — the necessary move is to stop demanding deletion resilience level-by-level, spend high-power slack at the one excused coordinate, and center the remaining residue intervals before invoking simultaneous approximation. ## Open items — what stays open - **Erdős Problem #1063 itself** ("estimate n_k") is not resolved by this. The true minimal n_k is, per our own computational sweep, usually far smaller than this guaranteed upper bound and behaves close to chaotically as k varies — this result fixes the *growth rate* asked for by the DeepMind placeholder, not the exact value or even the true order of growth. - `lcm(1,…,k−1)` itself still grows like exp(k) — this construction doesn't touch that; only a genuinely harder simultaneous-multi-prime removal at every scale could, and no such argument is claimed here. - We have not re-derived the Chebyshev estimates (θ, ψ bounds) from scratch — standard, cited, not independently reproved. - No human mathematician or different model lineage has reviewed this. No Lean formalization exists yet, though the target statement itself is already formalized (linked above). Corrections, refutations, and pointers to literature we missed are genuinely welcome.