Erdős problem 18

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

Sources

The source's own material, retained exactly.

11 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

18.lean

Retained formal statement4 of 11

Conjecture 2. Is it true that $h(n!) < n^{o(1)}$ ? That is, for all $\varepsilon > 0$ , is $h(n!) < n^\varepsilon$ for sufficiently large $n$ ?

FormalConjectures/ErdosProblems/18.leanErdos18.erdos_18b1 lineExact file

1True ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos18.practicalH n.factorial) < ↑n ^ ε

OpenStatement only, no proof