Skip to content

Erdős problem 950

Start work

This function was considered by de Bruijn, Erdős, and Turán, who showed that ∑n<xf(n)∼∑n<xf(n)2∼x\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

Open selected source

FormalConjectures/ErdosProblems/

950.lean

Retained formal statement3 of 7

Is it true that f(n)=o(log⁡log⁡n)f(n)=o(\log\log n) for all nn?

FormalConjectures/ErdosProblems/950.leanErdos950.erdos_950.parts.iii1 lineExact file
True ↔ Erdos950.f =o[Filter.atTop] fun n => Real.log (Real.log ↑n)
OpenStatement only, no proof