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
Let .
(c) Is it true that, for every composite , for every ?
Erdős–Szekeres [ErSz78] prove the weaker bound (the case ). Here is spelled out as: for every A > 0 there is a constant C (depending on A) with f(n) ≤ C · n/(log n)^A for every composite n.
True ↔ ∀ (A : ℝ), 0 < A → ∃ C, 0 < C ∧ ∀ (n : ℕ), ¬Nat.Prime n → 1 < n → ↑(Erdos700.f n) ≤ C * ↑n / Real.log ↑n ^ AOpenStatement only, no proof