Erdős problem 822

Does the set of integers of the form $n + \varphi(n)$ have positive (lower) density?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

822.lean

Retained formal statement1 of 1

Does the set of integers of the form $n + \varphi(n)$ have positive (lower) density?

[GIL24] proved this was true.

FormalConjectures/ErdosProblems/822.leanErdos822.erdos_8221 lineExact file

1True ↔ (Set.range fun n => n + n.totient).HasPosDensity

SolvedStatement only, no proof