Erdős problem 418

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

Asked by Erdős and Sierpiński. Numbers not of the form we call non-cototients.

Browkin and Schinzel [BrSc95] provided an affirmative answer to this question, proving that any integer of the shape $2^{k}\cdot 509203$ for $k\geq 1$ is a non-cototient.

This is discussed in problem B36 of Guy's collection [Gu04].

This was formalized in Lean by Alexeev using Aristotle.