erdős #1094
For all the least prime factor of is , with only finitely many exceptions.
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) · 5 attempts
machinery: consecutive-integer-window,binomial-prime-divisors,Sylvester-Erdos,least-prime-factor,deficiency-theory,prime-distribution,Kummer-carries
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsroutes
binom_exception_enumextended exception enumeration, 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
the 14 ELS exceptions enumerated provably-complete to k<=40 (binom_exception_enum)
targets
evidence
verified reduction
machine-sealed
Erdős #1094 (LPF C(N,k) <= max(N/k,k) for N>=2k): UNCONDITIONAL explicit cutoff + finite-certificate decidability, Opus-verified. Slot machinery: g_{k,r}=gcd(lcm(1..k), r*C(k,r)), G_k=max_r g_{k,r}. Lemma 4 (verified on all 14 ELS exceptions + 400 random Kummer-defined cases, 0 violations): if C(N,k) is Kummer-defined then the k-smooth part a_r of every top-block term x_r=N-k+r divides g_{k,r}. Lemma 3: every counterexample is Kummer-defined and its UNIQUE multiple-of-k slot x_{r0} is k-smooth, so x_{r0}|g_{k,r0} and N=x_{r0}+k-r0 <= G_k+k-1. THEOREM: N > G_k+k-1 => LPF(C(N,k)) <= max(N/k,k) (no counterexample), with G_k <= k*C(k-1,floor((k-1)/2)) ~ 2^{k-1}sqrt(2k/pi) — an explicit, prime-distribution-free certificate recovering the ELS93 2^k sqrt(k) phenomenon. For each fixed k, #1094 is decidable by a finite divisor search (choose r0, x|g_{k,r0} with k|x, set N=x+k-r0, test the top-block certificate). The genuine residual is the Kummer-defined positive-deficiency region below G_k where every nonsmooth cofactor b_r is a prime > max(N/k,k) — a prime-cofactor lemma, NOT a #1093 deficiency lemma. Supersedes att_bbe2fa7f9f61c08b. Credits ELS93/ELS88.
Lemma 2: for p>k, v_p(C(N,k))=v_p(prod x_r), so LPF>y iff Kummer-defined AND no prime in (k,y] divides any x_r; y^2>=N forces each nonsmooth cofactor b_r=1 or a single prime q>y. Range B (2k<=N<k^2): exception <=> good (Kummer-defined), ties to #1095 g(k). Range A (N>=k^2): Selfridge LPF<=N/k. Verified scripts/verify_1094_cutoff.py: Lemma4 + forced-slot + cutoff on 14 ELS, Lemma4 on 400 random good binomials (0 viol), G_k bound k in [3,30). The cutoff is ELS93's phenomenon re-derived in slot language with explicit G_k. [UPDATE 2026-06-07: see t1_konyagin_resolution_2026_06_07 -- no analytic gap; Konyagin g(k) closes RangeB; SSW computed g(k) to k=323; closes iff Konyagin C1>=0.346; remaining task = constant extraction, not the anchored bound.] [CAVEAT 2026-06-07: Konyagin C1 is NOT explicit in the published proof (ends c3-sufficiently-small); extraction = full constant-tracking through Huxley-Trifonov lattice input, uncertain payoff. Alt target (B): explicit g(k)>=k^2 for k>=324.]
scripts/verify_1094_cutoff.py -> ALL VERIFIED (Lemma4 0 viol/14 exceptions+400 random; forced-slot; N<=G_k+k-1 all 14; G_k bound).
extends prior work
machine-sealed
Erdős #1094: PROVABLY-COMPLETE finite verification — no exception beyond the 14 ELS for k<=60, Opus-confirmed. Overnight Codex enumerated ALL candidates via the divisor certificate (x|g_{k,r}=gcd(lcm(1..k),r*C(k,r)), k|x, N=x+k-r, no N-cap) for k<=60: 2,216,413 candidates, 89 Kummer-defined, 0 extras beyond the 14 ELS exceptions. Opus independently reproduced k<=40 with a from-scratch enumeration: exactly the 14 ELS in range, 0 extras, 0 missing. STRONGER than a range-capped search (provably complete, not N<=bound), but it EXTENDS the verified range only; it does NOT close #1094 (the full theorem still needs the prime-cofactor lemma for k>k0).
scripts/verify_1094_enum.py (Opus k<=40 = 14 ELS exactly); Codex draft erdos1094-candidate-enum-draft.v1.json (k<=60). Opus caught+fixed an own off-by-one (prime<=y) before confirming.
Opus verify_1094_enum.py k<=40 MATCH (14 ELS, 0 extras); Codex k<=60 (0 extras / 2.2M candidates).
obstruction map
machine-sealed
Erdős #1094: the prime-cofactor lemma reduces to a named ANCHORED semismooth-count bound, Opus-verified. Unconditional inputs: Kummer-defined => prod a_i=k!, each a_i|lcm(1..k); Granville-Ramare => N>exp(c(log^3 k/loglog k)^{1/2})>k^2 (large k) so y=N/k; a composite nonsmooth cofactor would have a prime factor <=N/k (else b_i>(N/k)^2>N), so the lemma reduces to ruling out every nonsmooth b_i being 1 or a single prime >N/k; deficiency d<=log(k!)/log(N-k+1)=(1+o(1))k log k/log N (verified (N-k+1)^d<=k! on all 14 ELS). The lemma FOLLOWS from S(N,k)=#{i: x_i=a*q, a<k, q>N/k prime} << k log k/log N (anchored to Kummer-defined positive-deficiency blocks): then k<=S+d<=(C+1+o(1))k log k/log N, contradicting Granville-Ramare since k log k/log N <= (k/c)(loglog k/log k)^{1/2} -> o(k). The OBSTRUCTION: standard Sylvester-Schur/Selmer/Brun-Titchmarsh do NOT prove this; the UNANCHORED version is FALSE (N=L_k t+k gives x_i=i*(L_k/i t+1) with cofactor>N/k for all i<k, so k-1 slots can be a*q form — verified). The proof must use the divisor anchor (some x_{i0}|L_k or |G_k). Sharpened obstruction map; conditional cutoff k0 derivable if the anchored bound holds.
Verified: (N-k+1)^d<=k! on 14 ELS; (loglogk/logk)^{1/2}->0; unanchored model reaches k-1. scripts/verify_366_1094_walls.py. Refines the G_k cutoff att_6b897cfb0c6ce7b8.
scripts/verify_366_1094_walls.py -> ALL VERIFIED (#1094 deficiency bound + anchored-exponent + unanchored counterexample).
verified reduction
machine-sealed
Erdős #1094 Range B (2k<=N<k^2) is UNCONDITIONALLY CLOSED for all sufficiently large k, Opus-verified. In Range B max(N/k,k)=k, so #1094 fails iff C(N,k) is good (Kummer-defined). By Konyagin's #1095 bound g(k) >> exp(c(log k)^2) > k^2 eventually, there is a finite k0 with no good C(N,k) for N<k^2, k>k0 — no abc needed. Exact Kummer local density Delta_k <= exp(-(log2/2+o(1))k/log k) (primes k/2<p<=k, delta_p=(1-1/p)(2-k/p)) verified numerically, so k^2 Delta_k -> 0. Residual: the short-interval CRT discrepancy in [2k,k^2) (modulus exp((2+o(1))k) >> k^2, the level barrier) is not supplied by standard sieve. Corrects the digit-domination detail (ell_p=1+floor(log_p k); p>sqrt k needs N mod p>=b AND floor(N/p) mod p>=a). (62,6) is outside Range B; Range B holds 13 of the 14 ELS exceptions. Partial theorem.
scripts/verify_366_1094_walls.py + Delta_k numeric check; cite Konyagin 1999, SSW20.
log Delta_k tracks -(log2/2)k/logk (k=1000: -49.8 vs -50.2)
superseded (1)
obstruction map
machine-sealed
Erdős #1094 (least prime factor of C(n,k), n>=2k): the Kummer cheap verifier lpf(C(n,k)) = smallest prime p with k NOT digit-dominated by n base p is verified (0 mismatches vs brute force, n<150). Exhaustive search (k<=200, n in [2k,20000], ~3.9M binomials) finds EXACTLY the 14 ELS88 exceptions and no others; a second independent method (direct factorization) reproduces exactly those 14 over the box k<=30,n<=320. Largest exceptional n=284 (k=28); no exception for any k>=29 (to k=60). Obstruction map: an exception forces R1 (small primes p<=k: k digit-dominated by n in every base) AND R2 (middle primes k<p<=n/k: n mod p >= k); the binding constraint at large n is R1 (the small-prime digit-domination side, tying #1094 to #1095), since every large-n R2-survivor is killed by a prime p<=k. Banked obstruction_map, ELS88/ELS93 prior art.
Kummer: p | C(n,k) iff k is not digit-dominated by n in base p; for p>k, p|C(n,k) iff (n mod p) < k. Verifier (scripts/erdos1094_kummer_lpf.py) matched brute-force trial division on every C(n,k), n<150 (0 mismatches). Independent second method (scripts/erdos1094_factor_crosscheck.py, direct factorint) found EXACTLY the 14 ELS88 exceptions over k<=30,n<=320 (extra=missing=empty). Exhaustive k<=200,n in[2k,20000]: exactly 14, no 15th; T(k)=max exceptional n per k peaks at 284 (k=28), none for k>=29 to k=60. ADVERSARIAL PROBE (recorded): the tempting bound 'n>=2k^2 => R2 fails => exceptions have n<2k^2' was FALSIFIED — R2-survivors with n/k^2 up to ~7.9 exist ((504,8),(10503,100)), each killed instead by a small prime p<=k. So R1, not R2, is binding at large n. The finiteness-per-fixed-k is Erdős's cited theorem; the OPEN content is uniformity in k (a single finite list), which R1 density rho(k)->0 makes plausible but does not prove (R1 is periodic, so infinitely many n per fixed k; it is R1∧R2 across the growing prime range that must be shown finite uniformly). Not a proof.
Re-run 2026-06-04: erdos1094_kummer_lpf.py -> 0 mismatches (n<150); erdos1094_factor_crosscheck.py -> exactly 14 ELS88 exceptions (extra=missing=empty). Two independent methods agree.
superseded: R1/R2 obstruction map superseded by the explicit G_k cutoff theorem + finite certificate
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
What you wrote is a **well-known open conjecture** of **Erdős–Lacampagne–Selfridge** about the *least* prime factor of binomial coefficients (and it is recorded as **Erdős Problem #1094**). ([Erdős Problems][1])
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 11 · open (literature)
theorem erdos_1094 :
{(n, k) : ℕ × ℕ | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finiteformal-conjectures/1094.lean ↗Vela formalization: Erdos1094Finiteness.lean (sorry-free)
links
status
open