Skip to content

Erdős problem 413

Start work

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

Open selected source

FormalConjectures/ErdosProblems/

413.lean

Retained formal statement2 of 5

Does there exist some ε > 0 such that there are infinitely many ε-barriers for ω?

FormalConjectures/ErdosProblems/413.leanErdos413.erdos_413.parts.ii1 lineExact file
True ↔ ∃ ε > 0, {n | Erdos413.IsBarrier (fun n => ε * ↑(ArithmeticFunction.cardDistinctFactors n)) n}.Infinite
OpenStatement only, no proof