Erdős problem 1064
Let be the Euler's totient function, then the satisfies have asymptotic density 1. Reference: [LuPo02] Luca, Florian and Pomerance, Carl, On some problems of {M}\polhk akowski-{S}chinzel and {E}rdős concerning the arithmetical functions {} and {}. Colloq. Math.
Sources
FormalConjectures/ErdosProblems/
1064.lean
Retained formal statement
Let be the Euler's totient function, there exist infinitely many such that Reference: [GLW01] Grytczuk, A. and Luca, F. and Wójtowicz, M., A conjecture of {E}rdős concerning inequalities for the {E}uler totient function.
{n | n.totient < (n - n.totient).totient}.InfiniteSolvedStatement only, no proof