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

It follows from a slight strengthening of the Goldbach conjecture that every odd number can be written as n−ϕ(n)n - \phi(n). In particular, we assume that every even number greater than 6 can be written as the sum of two *distinct* primes, in contrast to the usual Goldbach conjecture that every even number greater than 2 can be written as the sum of two primes.

FormalConjectures/ErdosProblems/418.leanErdos418.erdos_418.variants.conditional2 linesExact file
(∀ (n : ℕ), 6 < n → Even n → ∃ p q, p ≠ q ∧ Nat.Prime p ∧ Nat.Prime q ∧ n = p + q) →  ∀ (m : ℕ), Odd m → ∃ n, m + n.totient = n
SolvedStatement only, no proof