Erdős problem 18 · problems.science

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

Sources

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

11 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

18.lean

Retained formal statement3 of 11

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

More precisely: does there exist a constant $C > 0$ such that for infinitely many practical numbers $m$ , we have $h(m) < (\log \log m)^C$ ?

FormalConjectures/ErdosProblems/18.leanErdos18.erdos_18a1 lineExact file

1True ↔ ∃ C, 0 < C ∧ ∃ᶠ (m : ℕ) in Filter.atTop, m.IsPractical ∧ ↑(Erdos18.practicalH m) < Real.log (Real.log ↑m) ^ C

OpenStatement only, no proof