Erdős problem 456
Erdős [Er79e] writes it is 'easy to show' that for infinitely many we have .
Sources
FormalConjectures/ErdosProblems/
456.lean
Retained formal statement
Are there infinitely many primes such that is the only for which ?
True ↔ {q | Nat.Prime q ∧ ∀ (n : ℕ), Erdos456.m n = q ↔ n = q - 1}.InfiniteOpenStatement only, no proof