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

Tang's lower bound [Tang]:

log⁡k(n)≥(1/2−o(1))∗log⁡n∗log⁡log⁡n\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
∃ ε,  (∀ δ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |ε n| < δ) ∧    ∀ᶠ (n : ℕ) in Filter.atTop, (1 / √2 - ε n) * √(Real.log ↑n * Real.log (Real.log ↑n)) ≤ Real.log ↑(Erdos962.k n)
SolvedStatement only, no proof