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(p^a) = p for a prime p and a ≥ 2 (recorded by Erdős–Szekeres [ErSz78]). In particular, since (p^a) / P(p^a) = p^{a-1}, the prime power p^a is a "hit" (f(n) = n / P(n)) if and only if a = 2.
∀ (p a : ℕ), Nat.Prime p → 2 ≤ a → Erdos700.f (p ^ a) = pSolvedStatement only, no proof