Skip to content

Erdős problem 1055

A prime pp is in class 11 if the only prime divisors of p+1p+1 are 22 or 33. In general, a prime pp is in class rr if every prime factor of p+1p+1 is in some class ≤r−1\leq r-1, with equality for at least one prime factor. Show that for each rr there exists a prime pp of class rr.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1055.lean

Retained formal statement2 of 4

A prime pp is in class 11 if the only prime divisors of p+1p+1 are 22 or 33. In general, a prime pp is in class rr if every prime factor of p+1p+1 is in some class ≤r−1\leq r-1, with equality for at least one prime factor. If prp_r is the least prime in class rr, then how does pr1/rp_r^{1/r} behave? Erdos conjectured that this tends to infinity.

FormalConjectures/ErdosProblems/1055.leanErdos1055.erdos_1055.variants.erdos_limit1 lineExact file
Filter.Tendsto (fun r => ↑(Erdos1055.p r) ^ (1 / ↑↑r)) Filter.atTop Filter.atTop
OpenStatement only, no proof