Erdős problem 427
Erdős Problem 427: is it true that, for every and , there exists such that where denotes the th prime?
Sources
FormalConjectures/ErdosProblems/
427.lean
Retained formal statement
Cedric Pilatte has observed that a positive solution to Erdős Problem 427 follows from Shiu's theorem.
Erdos427.ShiuTheorem → Erdos427.erdos427SolvedStatement only, no proof