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].

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/950.lean

Formal Conjectures

FormalConjectures/ErdosProblems/950.leanErdos950.erdos_950.parts.i1 lineExact file

1True ↔ Filter.liminf (fun n => ↑(Erdos950.f n)) Filter.atTop = 1

OpenStatement only, no proof