erdős #1093
For we define the deficiency of as follows. If is divisible by a prime then the deficiency is undefined. Otherwise, the deficiency is the number of such that is -smooth, that is, divisible only by primes . Are there infinitely many binomial coefficients with deficiency ? Are there only finitely many with deficiency ?
Open problem — our best result is machine-sealed: verified reduction, reproduced by an independent verifier. The conjecture itself is unsettled.
number theory · open · formalized (Lean) · 7 attempts
machinery: smooth-numbers-consecutive-window,abc/kernel-bound,xyz-conjecture-Lagarias-Soundararajan,S-unit-equation,Kummer-carries/binomial-prime-divisors,prime-distribution,consecutive-integer-window
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsroutes
binom_deficiencyextended deficiency witness table, frozen-verified
leanLean patch building clean under the math CI profile (no sorry, no new axioms)
reviewprecise, artifact-backed reason a route cannot work
banked
three delta=1 examples beyond ELS93 (k=106/126/129) verified; the density model leans finite
targets
evidence
honest null
needs verification
Prior-art audit of Erdős #1093: attendedness=unattended; baseline_source=no_source_found; actors=none.
baseline: (none located) | novelty: open_lane | venues searched: ['semantic_scholar', 'researchgate']
prior-art search (no theorem asserted)
verified reduction
machine-sealed
#1093 DIVISOR-LEMMA REDUCTION (GPT-Pro, Opus-verified through gate): when C(n,k) is defined, the deficiency reformulates EXACTLY as delta(n,k)=#{1<=i<=k : n-k+i | i*C(k,i)} -- smoothness disappears, the smooth term is a divisor of the finite quantity i*C(k,i), NOT free. This REFUTES the proposed 'choose an arbitrary k-smooth S' Q1 construction (a Kummer obstruction). Consequence: positive deficiency forces n < k + 2^k*sqrt(k) (fix-k-grow-n is dead); ELS93 conjectured even deficiency-1 may be FINITE.
GPT-Pro (with ELS93 source) gave the Divisor Lemma (ELS93 Lemma 2): C(n,k) defined + x_i=n-k+i k-smooth => x_i | i*C(k,i). Proof via Kummer digit condition (k <=_p n) forcing p^a | (k-j)C(k,j)=i*C(k,i) for j=k-i. So when defined, delta = divisibility count against B_{k,i}=i*C(k,i), and smoothness is illusory. CONSEQUENCES: (1) delta>0 => some x_i <= i*C(k,i) => n < k+2^k*sqrt(k); fix-k-grow-n branch of Q1 DEAD. (2) my proposed Q1 'arbitrary k-smooth S in window + CRT' is INVALID -- Kummer forces S | i*C(k,i). (3) Q2 naive 'finitely many windows with 2 k-smooth' is FALSE without Kummer: bounded prime gaps give k=q,n=2q with window [q+1,2q] containing 2p,2q both q-smooth (but C(2q,q) not defined) -- Kummer is the MAIN condition. CORRECT REFORMULATIONS: Q1 = infinitely many (k,i,s): s|i*C(k,i), n=s+k-i>=2k, k<=_p n all p<=k, and n-k+r does NOT divide r*C(k,r) for r!=i. Q2 reduces to: for large k, no i<j,X with X|i*C(k,i), Y=X+(j-i)|j*C(k,j), j-i<k, plus Kummer on n -- a Kummer-admissible close-divisor-pair finiteness sublemma. Conditional Q2 via S-unit/xyz needs a strengthened xyz (kappa_0>1) + height-forcing input; CLASSICAL abc does NOT close it (rad(ABC)<=e^k vs n~2^k*sqrt(k), scales too close). PRIOR-ART: ELS93 (Erdos-Lacampagne-Selfridge 1993) already has Lemma 2 + the 2^k bound + the conjecture that deficiency-1 may be finite -- so Q1's 'infinite family' framing is likely WRONG (the answer may be 'finitely many'). OPUS VERIFICATION: Divisor Lemma 0 violations and smooth-count==divisor-count 0 violations over k<=15, n<5000; examples 360=8C(10,8), 1386|6C(11,6) confirmed; positive-deficiency n bounded per k.
extends prior work
machine-sealed
Erdős #1093 (ELS93 deficiency): exhaustive verified search confirms the Erdős–Lacampagne–Selfridge deficiency conjecture over the extended range k=2..127 — 177 positive-deficiency cases, 161 with deficiency 1, 16 with deficiency>1 (all N>=2k), and NO new deficiency>1 example beyond the ELS93 k<101 table. Two NEW deficiency-1 examples beyond ELS93 are found: (k=106, N=275204387105968945551700859, smooth position i=47) and (k=126, N=36859713316079485808433663, smooth position i=63). Banked as extends_prior_work, crediting ELS93 prior art.
Deficiency delta(N,k)=#{1<=i<=k : (N-k+i) | i*C(k,i)} for C(N,k) Kummer-defined (no prime p<=k divides it). Codex enumerated divisors d of B_{k,i}=i*C(k,i) with B_{k,i+1}=B_{k,i}(k-i)/i, testing N=d+k-i over (N-k)^2 <= k*4^k; largest k certified = 127. Opus independent recompute (scripts/verify_1093_deficiency.py): for both new examples C(N,k) is defined, delta=1, the cited i is the UNIQUE smooth slot, (N-k+i) | i*C(k,i), and the factorizations match — k=106: N-k+i = 2^6*3*5^2*13*17*31*53*61*67*71*73*83*89*97*101*103 (ends 700800); k=126: N-k+i = 2^6*3^2*5^2*11*13*17*23*37*41*67*73*79*83*89*97*109 (ends 433600). The full ELS93 deficiency>1 table (16 rows, k=8..42) reproduces exactly under independent recompute; corrupt-the-witness (+1 on the smooth term) breaks divisibility (probe survived); dense sample k<=40,N<3000 surfaces no table-missed deficiency>=2 case. Confirms ELS93's conjecture in-range; does not prove it for all k.
Opus independent exact-arithmetic recompute (verify_1093_deficiency.py): ALL CHECKS VERIFIED — 2 new examples, 16-row table reproduced, self-test passed.
extends prior work
machine-sealed
Erdős #1093: NEW deficiency-1 example at k=129 (beyond the k<=127 exhaustive search), Opus-verified. N=3180883073384828665489: C(N,129) Kummer-defined, exactly one smooth slot at i=65 with x=N-64=3180883073384828665425 = 3*5^2*11^2*13*23*37*67*71*79*83*89*101*113; x | 65*C(129,65) and x | lcm(1..129). Extends the verified deficiency-1 list. extends_prior_work.
Verified: N-64==x, factorization product==x, x|lcm(1..129), x|65*C(129,65), N Kummer-defined for all p<=129, unique divisor-test hit at i=65 (scripts/verify_1093_lcm_density.py).
scripts/verify_1093_lcm_density.py [2] -> all k=129 checks True.
obstruction map
machine-sealed
Erdős #1093 delta=1: the finiteness density heuristic is arithmetically WRONG — corrected local model leans INFINITUDE, Opus-verified. Slot indexing x=N-k+r, g_{k,r}=gcd(lcm(1..k), r*C(k,r)); every smooth slot has x|g_{k,r}. Sharpened supply: S_k=sum_r tau(g_{k,r})=exp(((log2)^2+o(1))k/log k), so the true supply constant is c=(log2)^2=0.48045 < C=0.78853 (verified; F(y)=int 1[{yt}>{t}]dt/t^2 = -y log y-(1-y)log(1-y), max F(1/2)=log2; indicator identity exact). Naively S_k*D_k=exp(-(C-(log2)^2)k/log k) with C-(log2)^2=+0.30808>0 would predict FINITELY many. But this multiplies by D_k assuming equidistribution that FAILS: the exact correlation — for p>sqrt(k), p|g_{k,r}, p|x => N=x+k-r is automatically Kummer-defined at p (verified 0 violations/2715) — couples the divisor and Kummer conditions through the SAME carry inequality. The corrected central first-moment exponent J(1/2)=+0.0437>0 (verified numeric +0.041) REVERSES the sign vs the naive -0.308<0. So the residual delta=1 question is a sparse subset-product CRT problem at r~k/2 (choose x including primes p>sqrt(k) with floor(k/p) odd, which self-certify Kummer), NOT an xyz or smooth-density problem; it leans infinite. Supersedes the naive finiteness-leaning record att_7beb86a84cc530ec. Honest obstruction map; infinitude/finiteness still open.
Unconditional: S_k exponent (log2)^2 (primes p>sqrt(k) dominate, F(y) integral identity); the correlation p|g_{k,r},p|x => Kummer-defined at p (since N=x+k-r ≡ k-r mod p, and p|r*C(k,r) forces k-r into the Kummer-pass range). NOT unconditional: the bound #{x|g_{k,r}: x+k-r Kummer-defined} <= tau(g_{k,r})*D_k*exp(o(k/log k)) — its independence model is wrong (divisor and Kummer coupled). Corrected local factor for p|g_{k,r} is 1+q_p not 2q_p, giving J(1/2)=int log(1-{t}+1[{yt}>{t}])dt/t^2 = +0.0437 at central slot. Construction route: r~k/2, x a product of self-certifying primes. Verified scripts/verify_1093_correlation.py.
scripts/verify_1093_correlation.py -> ALL VERIFIED (c=(log2)^2; identity 0 mismatches; correlation 0 violations/2715; J(1/2)>0).
obstruction map
machine-sealed
Erdős #1093 delta=1: the central subset-product CONSTRUCTION is blocked by two exact obstructions, Opus-verified — the J(1/2)>0 infinitude signal is real but not constructively realizable by forced primes. (a) Self-certification is only FIRST-ORDER: for p>sqrt(k), p^2>k requires two base-p digit conditions; p|x auto-satisfies Kummer only for p in (k/2,k] (m=floor(k/p)=1) — verified: x=p fails 0/13 in (k/2,k] but 2/2 in (k/4,k/3]. (b) ENTROPY COST: forcing top primes in (k/2,k] to make 'no second slot' automatic costs local exponent int_T^2 log(3-t)/t^2 dt = 0.10834 (T=1/(3/2-log2)=1.23938), EXCEEDING the positive first-moment margin J(1/2)=0.04367 (0.04367-0.10834<0), so the forced-prime route destroys the margin. Infinitude would require instead (i) a subset-product CRT mixing theorem mod M_0(k)=exp((2+o(1))sqrt k) and (ii) a second-slot pair-sieve — neither available. Honest obstruction map; refines att_e22fba0dfbc2bccf; infinitude open.
Self-cert second digit: p|x needs (x/p+floor((k-r)/p)) mod p >= floor(k/p); auto only for m=1. Entropy: forced top-prime log-measure 1-log2=0.30685 over t in [T,2], 1/T-1/2=1-log2 => T=1.23938, lost exponent int_T^2 log(3-t)/t^2=0.10834 > J(1/2)=0.04367. Needs subset-product character-sum control prod_{p in P_k}(1+chi(p)) small for all nontrivial chi mod M_0(k). Verified scripts/verify_699_1093_obstructions.py.
scripts/verify_699_1093_obstructions.py [#1093] -> constants + self-cert refinement (ALL VERIFIED).
superseded (1)
verified reduction
machine-sealed
Erdős #1093 deficiency: sharper necessary condition + density obstruction, Opus-verified. A deficiency smooth slot x=N-i is not merely k-smooth but DIVIDES lcm(1..k): if p^e|x with p^e>k then Kummer at modulus p^e forces N mod p^e >= k, contradicting N=x+a, a<k. Verified on every known deficiency>=1 example (16-row ELS93 table + k=106,126,129). Combined with the divisor lemma x | i*C(k,i), the Kummer-compatible smooth-slot supply is exp((log2+o(1))k/log k) while the Kummer-definedness density is exp(-(C+o(1))k/log k) with C=sum_{m>=2} log m/(m(m+1)) ~ 0.78853 > log2; since C-log2 ~ +0.0954 > 0, the density model predicts FINITELY many deficiency-1 cases. This refutes a positive-density delta=1 construction; finiteness itself needs uniform divisor-equidistribution mod Q_k=prod p^ceil(log_p(k+1)) (open). Sharpened reduction plus obstruction map, not a proof.
x | lcm(1..k) verified on all known examples (scripts/verify_1093_lcm_density.py). tau(Lambda_k) ~ exp((log2+o(1))k/log k); D_k=prod_{p<=k} prod_nu (1-d_{p,nu}/p) ~ exp(-(C+o(1))k/log k), C=0.78853057 (Opus recompute 0.78852 at 2M terms). Naive compatible count k*tau(Lambda_k)*D_k = exp(-(C-log2+o(1))k/log k) -> 0. Not a proof: assumes divisors of Lambda_k equidistribute among Kummer classes mod Q_k (Q_k~exp((1+o(1))k), divisor set ~exp((log2+o(1))k/log k)).
scripts/verify_1093_lcm_density.py -> ALL VERIFIED (lcm condition on all known examples; C-log2>0).
superseded: naive S_k*D_k finiteness lean corrected: equidistribution fails (Kummer/divisor correlation), J(1/2)>0 leans infinite
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
Your “deficiency is undefined” condition is exactly the condition that [ \gcd\left(\binom{n}{k},k!\right)=1, ] i.e. **no prime (\le k)** divides (\binom{n}{k}). Binomial coefficients with this property are often called **good binomial coefficients**; equivalently, their least prime factor is (>k). ([MathWorld][1])
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 5 · open (literature)
theorem erdos_1093.parts.i :
answer(sorry) ↔ {x : ℕ × ℕ | let k := x.1; let n := x.2; 2 * k ≤ n ∧ deficiency n k = 1 ∧
∀ p, p.Prime → (p ∣ choose n k) → k < p}.Infiniteformal-conjectures/1093.lean ↗links
status
open