Number theory · Last catalog review 26 Jul 2026

Erdős Problem 932

Let

p_k

denote the

k

th prime. For infinitely many

r

there are at least two integers

p_r < n < p_{r+1}

all of whose prime factors are

< p_{r + 1} - p_r

References

erdosproblems.com/932

Published 10 Jul 2026Never attempted

Formal statement

Lean type

{r |
    2 ≤
      {m ∈ Finset.Ioo (Nat.nth Nat.Prime r) (Nat.nth Nat.Prime r.succ) |
          m.maxPrimeFac < Nat.nth Nat.Prime r.succ - Nat.nth Nat.Prime r}.card}.Infinite

What you must prove

import FormalConjectures.ErdosProblems.«932»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos932.erdos_932" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/932.lean

Source type SHA-256: sha256:e2a1c8b5584f53f4aea241e1cf8d49ba4c980f27759bde1203b81a23be81854c
Task id: fc-e923379e-erdos932-erdos-932-9de464aa38-formalized-v1
Task commitment: sha256:46aa4b4c25c7637d821a8588636e47ae11093ea6e69be90667584064113d0f5c

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.