Erdős problem 1072

Erdős, Hardy, and Subbarao [HaSu02], believed that the number of $p \le x$ for which $f(p)=p−1$ is $o(x/\log x)$ .

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1072.lean

Retained formal statement1 of 3

Is it true that there are infinitely many $p$ for which $f(p) = p − 1$ ?

FormalConjectures/ErdosProblems/1072.leanErdos1072.erdos_1072.parts.i1 lineExact file

1True ↔ {p | Nat.Prime p ∧ Erdos1072.f p = p - 1}.Infinite

OpenStatement only, no proof