---

E. F. Ecklund, Jr. proved that for positive integers $n,k$ with $n\geq2k$ the coefficient $\binom nk$ has a prime divisor

$$p\leq\max\{n/k,\,n/2\},$$

with the single exception $\binom73=35$ (On prime divisors of the binomial coefficient, Pacific J. Math. 29 (1969), no. 2, 267--270; received 1968-07-08, published 1969-05-01 by the publisher's record). For $k\geq2$ the maximum is $n/2$, and $\binom nk=\binom n{n-k}$ carries the bound across the midpoint, so every $\binom nk$ with $1<k<n-1$ has a prime divisor $p\leq n/2$ except $\binom73=\binom74=35$, which is the corrected Statement of Problem 384. The source's theorem page gives a complete rewritten proof with the symmetry transfer to this problem, and the full-proof review filed with the source accepted the five rewritten components relative to the quoted Rosser--Schoenfeld estimates and the Faulkner implication.

The acceptance evidence is the refereed publication in the Pacific Journal of Mathematics and the site's curator, Thomas Bloom, who marks Problem 384 proved and credits Ecklund's paper for the proof; the linked formal-conjectures statement reads the problem with Ecklund's bound. Guy's collection (section B33) states the theorem in the same non-strict form. The curator's label carries a Lean qualification, which links no file and mirrors the community database's formal status Lean from 24 August 2026; the Lean development matching that date is Alexeev's refutation of the strict wording. The formal-conjectures statement file FormalConjectures/ErdosProblems/384.lean, added on 22 September 2026 and linked by the site as the formalized statement, states the non-strict theorem with 2 * p ≤ n and leaves it unproved (sorry), and no kernel-checked proof of Ecklund's theorem is recorded here or linked there.