Number theory

Withdrawn

Date added 5 Aug 2026

Erdős problem 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.

Withdrawn 5 Aug 2026

TYPE_DEPENDS_ON_SORRY (Erdos1055.p := Nat.find (exists_p r), exists_p is sorried)

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«1055»
import TaskSupport

namespace Bounty

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

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

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

Original conjecture source: FormalConjectures/ErdosProblems/1055.lean

Task id: fc-379fc029-variants-erdos-limit-902d2e9797-formalized-v1
Task commitment: sha256:03fc8747f06ef12c246f215f1657406f5bf269a3ade623fdc4a0c21ed68dfe9c

References

erdosproblems.com/1055

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.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord

Erdős problem 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.

Withdrawn 5 Aug 2026

TYPE_DEPENDS_ON_SORRY (Erdos1055.p := Nat.find (exists_p r), exists_p is sorried)