Skip to content

Erdős problem 18

Start work

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

Sources

The source's own material, retained exactly.

11 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

18.lean

Retained formal statement3 of 11

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

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

FormalConjectures/ErdosProblems/18.leanErdos18.erdos_18a1 lineExact file
True ↔ ∃ C, 0 < C ∧ ∃ᶠ (m : ℕ) in Filter.atTop, m.IsPractical ∧ ↑(Erdos18.practicalH m) < Real.log (Real.log ↑m) ^ C
OpenStatement only, no proof