Erdős problem 413 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

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

1IsGreatest {n | n < 10 ^ 5 ∧ Erdos413.IsBarrier (fun m => ↑(ArithmeticFunction.cardFactors m)) n} 99840

SolvedStatement only, no proof