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 statement3 of 5

The two ways of phrasing the conjecture are equivalent.

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

1Erdos945.Erdos945Prop ↔ Erdos945.Erdos945Constant

TextbookStatement only, no proof