Erdős problem 413

Erdős proved that the barrier set for `expProd` is infinite and even has positive density.

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

413.lean

Retained formal statement1 of 5

Are there infinitely many barriers for ω?

FormalConjectures/ErdosProblems/413.leanErdos413.erdos_413.parts.i1 lineExact file

1True ↔ {n | Erdos413.IsBarrier (fun m => ↑(ArithmeticFunction.cardDistinctFactors m)) n}.Infinite

OpenStatement only, no proof