Erdős problem 968

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

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

968.lean

Retained formal statement3 of 5

Erdős asked whether there are infinitely many solutions to uₙ > uₙ₊₁ > uₙ₊₂.

FormalConjectures/ErdosProblems/968.leanErdos968.erdos_968.variants.infinite_decreasingTriples1 lineExact file

1sorry ↔ {n | Erdos968.u n > Erdos968.u (n + 1) ∧ Erdos968.u (n + 1) > Erdos968.u (n + 2)}.Infinite

OpenStatement only, no proof