Erdős problem 1057
Is it true that ?
Sources
FormalConjectures/ErdosProblems/
1057.lean
Retained formal statement
Alford, Granville, and Pomerance [AGP94] proved that .
Filter.Tendsto Erdos1057.carmichaelCounting Filter.atTop Filter.atTopSolvedStatement only, no proof