Erdős problem 18
Conjecture 1. Are there infinitely many practical numbers such that ?
Sources
FormalConjectures/ErdosProblems/
18.lean
Retained formal statement
Conjecture 3. Or perhaps even ?
Erdős offered $250 for a proof or disproof.
True ↔ ∃ C, 0 < C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos18.practicalH n.factorial) < Real.log ↑n ^ COpenStatement only, no proof