Skip to content

Erdős problem 1072

Start work

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1072.lean

Retained formal statement3 of 3

Erdős, Hardy, and Subbarao [HaSu02], believed that the number of p≤xp \le x for which f(p)=p−1f(p)=p−1 is o(x/log⁡x)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
(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