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 statement3 of 3

The interval [⌊n/3⌋, n] is fork-free, and therefore f n is at least ⌈2n / 3⌉.

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

1∀ (n : ℕ), ⌈2 * ↑n / 3⌉₊ ≤ Erdos1062.f n

SolvedStatement only, no proof