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
Are there infinitely many barriers for ω?
True ↔ {n | Erdos413.IsBarrier (fun m => ↑(ArithmeticFunction.cardDistinctFactors m)) n}.InfiniteOpenStatement only, no proof