Erdős problem 18
Conjecture 1. Are there infinitely many practical numbers such that ?
Sources
FormalConjectures/ErdosProblems/
18.lean
Retained formal statement
Conjecture 2. Is it true that ? That is, for all , is for sufficiently large ?
True ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos18.practicalH n.factorial) < ↑n ^ εOpenStatement only, no proof