Skip to content

Erdős problem 962

Start work

Main conjecture:

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

962.lean

Retained formal statement1 of 3

Main conjecture:

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

FormalConjectures/ErdosProblems/962.leanErdos962.erdos_9624 linesExact file
True ↔  ∃ ε,    (∀ δ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |ε n| < δ) ∧      ∀ᶠ (n : ℕ) in Filter.atTop, Real.log ↑(Erdos962.k n) ≤ (Real.log ↑n).rpow (1 / 2 + ε n)
OpenStatement only, no proof