Erdős problem 92
A sanity check to ensure the set of possible f(n) values is bounded above. A trivial bound is n, since the points equidistant from any x form a subset of the other n - 1 points. This ensures sSup is well-defined.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/92.leansorry ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos92.f n) ≤ ↑n ^ (c / Real.log (Real.log ↑n))OpenStatement only, no proof