Erdős problem 945 · problems.science

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

Sources

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

5 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

945.lean

Retained formal statement4 of 5

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

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

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

SolvedStatement only, no proof