Erdős problem 950 · problems.science

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

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

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

950.lean

Retained formal statement6 of 7

Erdős writes that a 'weaker conjecture which is perhaps not quite inaccessible' is that, for every $\epsilon>0$ , if $x$ is sufficiently large there exists $y<x$ such that $\pi(x)< \pi(y)+\epsilon \pi(x-y)$ . Compare this to [855].

FormalConjectures/ErdosProblems/950.leanErdos950.erdos_950.variants.weaker_pi1 lineExact file

1True ↔ ∀ ε > 0, ∀ᶠ (x : ℕ) in Filter.atTop, ∃ y < x, ↑x.primeCounting < ↑y.primeCounting + ε * ↑(x - y).primeCounting

OpenStatement only, no proof

Sources

Search problems.science