Erdős problem 962 · problems.science

Main conjecture:

Sources

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

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

962.lean

Retained formal statement2 of 3

Tang's lower bound [Tang]:

$\log k(n) \ge (1/\sqrt{2} - o(1)) * \sqrt{\log n * \log \log n}$

FormalConjectures/ErdosProblems/962.leanErdos962.erdos_962.variants.tang_lower_bound3 linesExact file

1∃ ε,2  (∀ δ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |ε n| < δ) ∧3    ∀ᶠ (n : ℕ) in Filter.atTop, (1 / √2 - ε n) * √(Real.log ↑n * Real.log (Real.log ↑n)) ≤ Real.log ↑(Erdos962.k n)

SolvedStatement only, no proof

Sources

Search problems.science