Erdős problem 962 · problems.science

Main conjecture:

Sources

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

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

962.lean

Retained formal statement3 of 3

Tao's upper bound [Tao]:

$k(n) \le (1 + o(1)) * n^{1/2}$

FormalConjectures/ErdosProblems/962.leanErdos962.erdos_962.variants.tao_upper_bound1 lineExact file

1∃ ε, (∀ δ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |ε n| < δ) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos962.k n) ≤ (1 + ε n) * √↑n

SolvedStatement only, no proof