Erdős problem 950
This function was considered by de Bruijn, Erdős, and Turán, who showed that . 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.
Retained declaration
FormalConjectures/ErdosProblems/950.leanTrue ↔ Filter.liminf (fun n => ↑(Erdos950.f n)) Filter.atTop = 1OpenStatement only, no proof