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
Erdős believed there should be infinitely many barriers for Ω, the total prime multiplicity.
True ↔ {n | Erdos413.IsBarrier (fun m => ↑(ArithmeticFunction.cardFactors m)) n}.InfiniteOpenStatement only, no proof