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