Erdős problem 945

Is it true that $F(x) \leq (\log x)^{O(1)}$ ?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

945.lean

Retained formal statement5 of 5

Erdős and Mirsky [ErMi52] proved that Unparsed notation: \log F(x) \ll \frac{(\log x)^{1/2}}.

FormalConjectures/ErdosProblems/945.leanErdos945.erdos_945.variants.upper_bound1 lineExact file

1(fun n => Real.log ↑(Erdos945.F ↑n)) =O[Filter.atTop] fun x => √(Real.log ↑x) / Real.log (Real.log ↑x)

SolvedStatement only, no proof