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$ .

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

932.lean

Retained formal statement2 of 2

Erdős could show that the density of $r$ such that at least one such $n$ exists is $0$ .

FormalConjectures/ErdosProblems/932.leanErdos932.erdos_932.variants.one_le5 linesExact file

1{r |2      1 ≤3        {m ∈ Finset.Ioo (Nat.nth Nat.Prime r) (Nat.nth Nat.Prime r.succ) |4            m.maxPrimeFac < Nat.nth Nat.Prime r.succ - Nat.nth Nat.Prime r}.card}.HasDensity5  0

SolvedStatement only, no proof