Erdős problem 968
Does the set {n | u n < u (n+1)} have positive lower density?
Sources
FormalConjectures/ErdosProblems/
968.lean
Retained formal statement
Erdős and Prachar proved that the set {n | u n > u (n+1)} has positive lower density (see [ErPr61]).
0 < {n | Erdos968.u n > Erdos968.u (n + 1)}.lowerDensitySolvedStatement only, no proof