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

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

Sources

Search problems.science