Erdős problem 1072 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

1072.lean

Retained formal statement3 of 3

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)$ .

[HaSu02] Hardy, G. E. and Subbarao, M. V., _A modified problem of Pillai and some related questions._ Amer. Math. Monthly (2002), 554--559.

FormalConjectures/ErdosProblems/1072.leanErdos1072.erdos_1072.variants.littleo1 lineExact file

1(fun x => ↑({p | Nat.Prime p ∧ Erdos1072.f p = p - 1} ∩ Set.Icc 0 x).ncard) =o[Filter.atTop] fun x => ↑x / Real.log ↑x

OpenStatement only, no proof