Erdős problem 418

Are there infinitely many integers not of the form $n - \phi(n)$ ?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

418.lean

Retained formal statement3 of 5

It is open whether the set of non-cototients has positive density.

FormalConjectures/ErdosProblems/418.leanErdos418.erdos_418.variants.density1 lineExact file

1True ↔ ∃ S, ∃ (_ : S.HasPosDensity), S ⊆ {x | ∃ n, n - n.totient = x}ᶜ

OpenStatement only, no proof