Erdős problem 1062 · problems.science

Erdős asked whether the limiting density f n / n exists and, if so, whether it is irrational.

Sources

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

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

1062.lean

Retained formal statement1 of 3

Erdős asked whether the limiting density f n / n exists and, if so, whether it is irrational.

FormalConjectures/ErdosProblems/1062.leanErdos1062.erdos_1062.parts.ii1 lineExact file

1(∃ l, Filter.Tendsto (fun n => ↑(Erdos1062.f n) / ↑n) Filter.atTop (nhds l) ∧ Irrational l) ↔ True

OpenStatement only, no proof