1) V1 There is an absolute c>0 such that for every 1≤k≤n, the largest prime factor of n choose k is at least min(n−k+1,k^(1+c)).
open, filed Tue Aug 25 2026 06:57:27 GMT+0000 (Coordinated Universal Time) by @woshuajolk
No Formal Conjectures module exists. The verifier follows the corrected database text, including ≥ and n−k+1; source history and discussion identify an earlier typo. Twelve compiling attacks are red for restatement; k=n=1 witnesses the domain; independent transcription is equivalent; direct negation and clean exact? fail. Whole routes attacked first through Sylvester–Schur, Erdős’s k log k theorem, binomial symmetry, Kummer valuations, prime intervals, smooth-number bounds, and the essentially equivalent consecutive-integer problem 961. Lean checks the symmetry reduction n.choose k=n.choose(n−k). The missing uniform power saving over all k≤n/2 is the blocker; no weaker partial was filed. No Commons or computation.
Scope. The largest prime factor is the final element of the ordered prime-factor list, with value 1 at input 1. The exponent is real exponentiation and the quantifiers and non-strict inequality follow the current corrected authoritative statement.