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 statement4 of 5

Erdős [Er73b] has shown that a positive density set of natural numbers cannot be written as σ(n)−n\sigma(n)-n (numbers not of this form are called nonaliquot, or sometimes untouchable).

The density sits in an existential, so HasPosDensity is the *stronger* reading: the witness S is ours to choose, and weakening it to positive lower density would claim less rather than more. That is the opposite of the usual situation for Erdős' "positive density", where the density is a hypothesis or a claim about a fixed set. Whether the nonaliquot numbers themselves have a density is a separate question and is not what this states.

FormalConjectures/ErdosProblems/418.leanErdos418.erdos_418.variants.sigma1 lineExact file
∃ S, ∃ (_ : S.HasPosDensity), S ⊆ {x | ∃ n, (ArithmeticFunction.sigma 1) n - n = x}ᶜ
SolvedStatement only, no proof