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

Open selected source

FormalConjectures/ErdosProblems/

1072.lean

Retained formal statement2 of 3

Is it true that $f(p)/p \to 0$ for $p \to \infty$ in a density 1 subset of the primes?

FormalConjectures/ErdosProblems/1072.leanErdos1072.erdos_1072.parts.ii4 linesExact file

1True ↔2  ∃ P ⊆ {p | Nat.Prime p},3    P.HasDensity 1 {p | Nat.Prime p} ∧4      Filter.Tendsto (fun p => ↑(Erdos1072.f p) / ↑p) (Filter.atTop ⊓ Filter.principal P) (nhds 0)

OpenStatement only, no proof