Erdős problem 1062

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1062.lean

Retained formal statement2 of 3

Lebensold proved that for large n, the function f n lies between 0.6725 n and 0.6736 n.

FormalConjectures/ErdosProblems/1062.leanErdos1062.erdos_1062.variants.lebensold_bounds1 lineExact file

1∀ᶠ (n : ℕ) in Filter.atTop, 0.6725 * ↑n ≤ ↑(Erdos1062.f n) ∧ ↑(Erdos1062.f n) ≤ 0.6736 * ↑n

SolvedStatement only, no proof