Skip to content

Erdős problem 418

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

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

418.lean

Retained formal statement5 of 5

A solution to erdos_418 was shown by Browkin and Schinzel [BrSc95] by showing that any integer of the form 2(k+1)⋅5092032^(k + 1)\cdot 509203 is not of the form n−ϕ(n)n - \phi(n).

FormalConjectures/ErdosProblems/418.leanErdos418.erdos_418.variants.soln1 lineExact file
{x | ∃ k, 2 ^ (k + 1) * 509203 = x} ⊆ {x | ∃ n, n - n.totient = x}ᶜ
SolvedStatement only, no proof