Erdős problem 683
There exists such that for all .}
Sources
FormalConjectures/ErdosProblems/
683.lean
Retained formal statement
Standard heuristics suggest that for some constant .
∃ c > 0, ∀ (n k : ℕ), 0 < k ∧ k ≤ n / 2 → ↑(Erdos683.P n k) > Real.exp (c * √↑k)OpenStatement only, no proof