Erdős problem 1057
Is it true that ?
Sources
FormalConjectures/ErdosProblems/
1057.lean
Retained formal statement
This exponent was improved to by Lichtman [Li22].
∀ᶠ (x : ℝ) in Filter.atTop, Erdos1057.carmichaelCounting x > x ^ 0.3389SolvedStatement only, no proof