Erdős problem 828

Is it true that, for any $a \in \mathbb{Z}$ , there are infinitely many $n$ such that $\phi(n) | n + a$ ?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

828.lean

Retained formal statement3 of 3

It is an easy exercise to show that $\phi(n) | n$ if and only if $n = 0, 1$ or $n = 2^a 3^b$ for some $a > 0$ .

FormalConjectures/ErdosProblems/828.leanErdos828.erdos_828.variants.phi_dvd_self_iff_pow2_pow31 lineExact file

1∀ {n : ℕ}, n.totient ∣ n ↔ n ≤ 1 ∨ ∃ a > 0, ∃ b, n = 2 ^ a * 3 ^ b

TextbookProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.