Skip to content

Erdős problem 968

Start work

Does the set {n | u n < u (n+1)} have positive lower density?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

968.lean

Retained formal statement2 of 5

Erdős and Prachar proved that the set {n | u n > u (n+1)} has positive lower density (see [ErPr61]).

FormalConjectures/ErdosProblems/968.leanErdos968.erdos_968.variants.decreasing_steps_pos_lower_density1 lineExact file
0 < {n | Erdos968.u n > Erdos968.u (n + 1)}.lowerDensity
SolvedStatement only, no proof