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

Main conjecture:

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

FormalConjectures/ErdosProblems/962.leanErdos962.erdos_9624 linesExact file

1True ↔2  ∃ ε,3    (∀ δ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |ε n| < δ) ∧4      ∀ᶠ (n : ℕ) in Filter.atTop, Real.log ↑(Erdos962.k n) ≤ (Real.log ↑n).rpow (1 / 2 + ε n)

OpenStatement only, no proof

Sources

Search problems.science