Erdős problem 92 · problems.science

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.

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

92.lean

Retained formal statement1 of 3

Or even $f(n) < n^{c/\log\log n}$ for some constant $c > 0$ ?

FormalConjectures/ErdosProblems/92.leanErdos92.erdos_92.variants.strong1 lineExact file

1sorry ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos92.f n) ≤ ↑n ^ (c / Real.log (Real.log ↑n))

OpenStatement only, no proof

Sources

Search problems.science