Skip to content

Erdős problem 18

Start work

Conjecture 1. Are there infinitely many practical numbers mm such that h(m)<(log⁡log⁡m)O(1)h(m) < (\log \log m)^{O(1)}?

Sources

The source's own material, retained exactly.

11 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

18.lean

Retained formal statement2 of 11

Vose's Theorem. Vose proved the existence of infinitely many practical numbers mm such that h(m)≪(log⁡m)1/2h(m) \ll (\log m)^{1/2}. This gives a positive answer to a weaker form of Conjecture 1.

FormalConjectures/ErdosProblems/18.leanErdos18.erdos_18_vose1 lineExact file
∃ C, 0 < C ∧ ∃ᶠ (m : ℕ) in Filter.atTop, m.IsPractical ∧ ↑(Erdos18.practicalH m) < C * Real.log ↑m ^ (1 / 2)
SolvedStatement only, no proof