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 statement4 of 5

Selfridge computed that the largest Ω-barrier below 10^5 is 99840.

FormalConjectures/ErdosProblems/413.leanErdos413.erdos_413.variants.bigOmega_largest_barrier_lt_100k1 lineExact file
IsGreatest {n | n < 10 ^ 5 ∧ Erdos413.IsBarrier (fun m => ↑(ArithmeticFunction.cardFactors m)) n} 99840
SolvedStatement only, no proof