Erdős problem 700
f n is a lower bound: f n ≤ gcd(n, C(n,k)) for every 1 < k ≤ n/2.
Sources
FormalConjectures/ErdosProblems/
700.lean
Retained formal statement
f(pq) = p for distinct primes p < q (recorded by Erdős–Szekeres [ErSz78]); in particular pq is always a "hit" (f(pq) = pq / P(pq) = p). Proof via Lucas' theorem: p ∤ C(pq,k) ⟹ p ∣ k (and the same for q), so any k with gcd(pq, C(pq,k)) = 1 must be a multiple of pq, of which there are none in (1, pq/2]; the witness k = q gives gcd(pq, C(pq,q)) = p.
∀ (p q : ℕ), Nat.Prime p → Nat.Prime q → p < q → Erdos700.f (p * q) = pSolvedStatement only, no proof