Number theory

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

No one has attempted this yet.

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-379fc029-erdos932-erdos-932-4085ea61d4-formalized-v1
Task commitment: sha256:a3ac3d2a0a9c39d6a0cb299ae7bde0156f77c7f9bc2003559e6e3d4271d66a14

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.