Number theory

Erdős 1055 - erdos 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? Erdos conjectured that this tends to infinity.

References

erdosproblems.com/1055

No one has attempted this yet.

Formal statement

Lean type

Filter.Tendsto (fun r => ↑(Erdos1055.p r) ^ (1 / ↑↑r)) Filter.atTop Filter.atTop

What you must prove

import FormalConjectures.ErdosProblems.«1055»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1055.lean

Source type SHA-256: sha256:c6f6e6642963acf686d9afce67c051cac0d607dc841eaaf64b840e0c6dd0bf7f
Task id: fc-379fc029-variants-erdos-limit-902d2e9797-formalized-v1
Task commitment: sha256:03fc8747f06ef12c246f215f1657406f5bf269a3ade623fdc4a0c21ed68dfe9c

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.