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 statement2 of 3

Is it true that $f(n)\leq n^{o(1)}$ ?

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

1sorry ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ (n : ℕ), ↑(Erdos92.f n) ≤ ↑n ^ o n

OpenStatement only, no proof

Sources

Search problems.science