Erdős problem 700
f n is a lower bound: f n ≤ gcd(n, C(n,k)) for every 1 < k ≤ n/2.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/700.lean∀ (n : ℕ), ¬Nat.Prime n → 1 < n → (Erdos700.f n = n / Erdos700.P n ↔ True)OpenStatement only, no proof