Erdős problem 413
Erdős proved that the barrier set for expProd is infinite and even has positive density.
Sources
FormalConjectures/ErdosProblems/
413.lean
Retained formal statement
Does there exist some ε > 0 such that there are infinitely many ε-barriers for ω?
True ↔ ∃ ε > 0, {n | Erdos413.IsBarrier (fun n => ε * ↑(ArithmeticFunction.cardDistinctFactors n)) n}.InfiniteOpenStatement only, no proof