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 statement5 of 11

Conjecture 3. Or perhaps even $h(n!) < (\log n)^{O(1)}$ ?

Erdős offered $250 for a proof or disproof.

FormalConjectures/ErdosProblems/18.leanErdos18.erdos_18c1 lineExact file

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

OpenStatement only, no proof