Number theory

Erdős 1055 - selfridge limit

A prime

p

is in class

1

if the only prime divisors of

p+1

are

2

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.

References

erdosproblems.com/1055

No one has attempted this yet.

Formal statement

Lean type

∃ M, ∀ (r : ℕ+), ↑(Erdos1055.p r) ^ (1 / ↑↑r) ≤ M

What you must prove

import FormalConjectures.ErdosProblems.«1055»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1055.erdos_1055.variants.selfridge_limit" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1055.lean

Source type SHA-256: sha256:f7b1d731b04e15c137e6a01d29894372e52cb1ecdc7f8035bde494e9ac638c72
Task id: fc-379fc029-variants-selfridge-limit-fae6b54fdc-formalized-v1
Task commitment: sha256:6ef9f19a9a03ab277471b668edd535c6f7755d6f7369aed2758dd3feada1ef6b

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.