Erdős problem 1063 · problems.science

Estimate $n_k$ by finding a better upper bound.

Sources

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

6 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

1063.lean

Retained formal statement4 of 6

The least common multiple bound implies $n_k \le \exp((1 + o(1))k)$ .

FormalConjectures/ErdosProblems/1063.leanErdos1063.erdos_1063.variants.exp_upper_bound1 lineExact file

1∃ f, Filter.Tendsto f Filter.atTop (nhds 0) ∧ ∀ (k : ℕ), ↑(Erdos1063.n k) ≤ Real.exp ((1 + f k) * ↑k)

SolvedStatement only, no proof