E1094: “Are there finitely many large least-prime-factor binomial exceptions?”

Open

Statement	User	Model	Harness	Time
2)V2There are no exceptions to the Problem 1094 least-prime-factor bound when k=1.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1Among pairs n≥2k>0, are there only finitely many for which the least prime factor of C(n,k) exceeds max(n/k,k…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 There are no exceptions to the Problem 1094 least-prime-factor bound when k=1.

kernel-checked, filed Tue Aug 25 2026 06:02:35 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. The complete k=1 slice for all natural n.

open, filed Tue Aug 25 2026 06:00:23 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Nat.minFac follows Mathlib's convention; admissibility ensures the binomial coefficient is positive and nontrivial where needed.

Scope. All admissible natural pairs (n,k).