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

$h(12) = 3$ : divisors are {1, 2, 3, 4, 6, 12}. The hardest m is m=11, requiring 3 divisors: 11=1+4+6.

FormalConjectures/ErdosProblems/18.leanErdos18.practicalH_twelve1 lineExact file

1Erdos18.practicalH 12 = 3

TestStatement only, no proof