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

$h(n!)$ is well-defined since $n!$ is practical for $n ≥ 1$ .

FormalConjectures/ErdosProblems/18.leanErdos18.factorial_isPractical1 lineExact file

1∀ (n : ℕ), n.factorial.IsPractical

TextbookStatement only, no proof