Erdős problem 950

This function was considered by de Bruijn, Erdős, and Turán, who showed that $\sum_{n<x}f(n)\sim \sum_{n<x}f(n)^2\sim x$ . They gave no proofs, but a proof of the (harder) second claim is given by Gorodetsky here [mathoverflow/508491].

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

950.lean

Retained formal statement5 of 7

The study of $f(p)$ is even harder, and Erdős could not prove that $\sum_{p<x}f(p)^2\sim \pi(x)$ .

FormalConjectures/ErdosProblems/950.leanErdos950.erdos_950.variants.sum_primes3 linesExact file

1True ↔2  Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ p ∈ Finset.range x with Prime p, Erdos950.f p ^ 2) fun x =>3    ↑x.primeCounting

OpenStatement only, no proof