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

Worked, still open.

number theory · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

What you wrote is *not* known to be true at present: it is an open Erdős problem (Erdős Problems Project **#932**) as of January 2026. ([Erdős Problems][1])

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_932 :
    { r : ℕ | 2 ≤ (Finset.Ioo (r.nth Nat.Prime) (r.succ.nth Nat.Prime) |>.filter
      (fun m => m.maxPrimeFac < r.succ.nth Nat.Prime - r.nth Nat.Prime)).card }.Infinite

formal-conjectures/932.lean ↗

oeis

A387864 — Numbers r for which there are at least two integers strictly between prime(r) and prime(r+1), all of whose prime factors are less than prime(r+1) - prime(r).4,9,11,15,24,30,34,37,46,47,53,62,66,92,99,114,137,146,150,154,168,172,180,189,205,217,242,259,263,274,278,283,293,295,3

links

Google DeepMind Formal Conjectures project · link

status