Erdős Problem 1055

Reference: erdosproblems.com/1055

def Erdos1055.IsOfClass : ℕ+ → ℕ → Prop

A prime $p$ is in class $1$ if the only prime divisors of $p+1$ are $2$ or $3$. In general, a prime $p$ is in class $r$ if every prime factor of $p+1$ is in some class $\leq r-1$, with equality for at least one prime factor.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos1055.exists_p (r : ℕ+) : ∃ (p : ℕ), Nat.Prime p ∧ IsOfClass r p

A prime $p$ is in class $1$ if the only prime divisors of $p+1$ are $2$ or $3$. In general, a prime $p$ is in class $r$ if every prime factor of $p+1$ is in some class $\leq r-1$, with equality for at least one prime factor. Show that for each $r$ there exists a prime $p$ of class $r$.

noncomputable def Erdos1055.p (r : ℕ+) : ℕ

A prime $p$ is in class $1$ if the only prime divisors of $p+1$ are $2$ or $3$. In general, a prime $p$ is in class $r$ if every prime factor of $p+1$ is in some class $\leq r-1$, with equality for at least one prime factor. Let $p_r$ is the least prime in class $r$.

Equations

• Erdos1055.p r = Nat.find ⋯

theorem Erdos1055.erdos_1055 (r : ℕ+) : {p : ℕ | Nat.Prime p ∧ IsOfClass r p}.Infinite

A prime $p$ is in class $1$ if the only prime divisors of $p+1$ are $2$ or $3$. In general, a prime $p$ is in class $r$ if every prime factor of $p+1$ is in some class $\leq r-1$, with equality for at least one prime factor. Are there infinitely many primes in each class?

theorem Erdos1055.erdos_1055.variants.erdos_limit : Filter.Tendsto (fun (r : ℕ+) => ↑(p r) ^ (1 / ↑↑r)) Filter.atTop Filter.atTop

A prime $p$ is in class $1$ if the only prime divisors of $p+1$ are $2$ or $3$. In general, a prime $p$ is in class $r$ if every prime factor of $p+1$ is in some class $\leq r-1$, with equality for at least one prime factor. If $p_r$ is the least prime in class $r$, then how does $p_r^{1/r}$ behave? Erdos conjectured that this tends to infinity.

theorem Erdos1055.erdos_1055.variants.selfridge_limit : ∃ (M : ℝ), ∀ (r : ℕ+), ↑(p r) ^ (1 / ↑↑r) ≤ M

A prime $p$ is in class $1$ if the only prime divisors of $p+1$ are $2$ or $3$. In general, a prime $p$ is in class $r$ if every prime factor of $p+1$ is in some class $\leq r-1$, with equality for at least one prime factor. If $p_r$ is the least prime in class $r$, then how does $p_r^{1/r}$ behave? Selfridge conjectured that this is bounded.