Skip to content

Erdős problem 1062

Start work

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

Open selected source

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
∀ (n : ℕ), ⌈2 * ↑n / 3⌉₊ ≤ Erdos1062.f n
SolvedStatement only, no proof