Erdős problem 1057
Is it true that ?
Sources
FormalConjectures/ErdosProblems/
1057.lean
Retained formal statement
The lower bound was proved by Harman [Ha08].
∀ᶠ (x : ℝ) in Filter.atTop, Erdos1057.carmichaelCounting x > x ^ 0.33336704SolvedStatement only, no proof