erdős #463
Is there a function with as such that, for all large , there is a composite number such that(Here is the least prime factor of .)
Open problem — our best result is machine-sealed: partial proof, reproduced by an independent verifier. The conjecture itself is unsettled.
number theory · open · possible · formalized (Lean) · 3 attempts
machinery: least-prime-factor,semiprime-near-sqrt,prime-distribution,short-interval-primes,consecutive-integer-window,sieve/Brun-Titchmarsh,value-set-gap-statistics
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
partial proof
needs verification
Reduced Erdos #463 to a clean self-contained criterion: the answer is YES iff g(n)->infinity, where g(n)=max{m-n : m composite, m-n<p(m)}. Gave an explicit construction (p-rough unique multiple of a p
obstruction map
machine-sealed
Erdos #463: lean/Vela/Erdos463.lean proves the square-root finite-search bound for qualifying offsets, and scripts/erdos463_margin_search.py exactly recomputes g(n)=max{d>0 : n+d is composite and d<minFac(n+d)} for n<=10000000; this is finite-prefix evidence only and leaves g(n)->infinity open.
{"scope":{"lean_file":"lean/Vela/Erdos463.lean","artifact":"examples/erdos-problems/attack/erdos463-margin-prefix-10m-draft.v1.json","script":"scripts/erdos463_margin_search.py","proves":["Every qu...
depends on (the wall): lean/Vela/Erdos463.lean; scripts/erdos463_margin_search.py; examples/erdos-problems/attack/erdos463-margin-prefix-10m-draft.v1.json
[{"method":"lean_kernel","command":"cd lean && lake build Vela.Erdos463","result":"passed"},{"method":"axiom_sorry_scan","command":"rg -n \"sorry|axiom|unsafe|admit\" lean/Vela/Erdos463.lean lean/V...
honest null
machine-sealed
Erdos #463: literature scoping (GPT-Pro, Opus-verified) shows g(n)->infinity is OPEN and NOT implied by any known result, so #463 is not closeable by citation. The equivalent reformulation is N - F_c(N) -> infinity with F_c(N)=min_{m>N composite}(m-p(m)); Erdos's stronger recorded conjecture N - F_c(N) ~ c N^{1/2} would imply it (matches our Lean sqrt(n) offset bound) but is itself open. The obstruction: at scale z ~ H no pointwise 'every length-H interval contains an H-rough number' bound can hold, since Rankin/Ford-Green-Konyagin-Maynard-Tao long-gap constructions (Y(x) >> x log x log_3 x / (log_2 x)^2 > x) give intervals fully covered by small-prime classes; sieve gives only almost-all intervals. Sibling: #385. Decision: do not re-fire GPT-Pro at #463.
{"result_type":"literature-scope / not citation-closeable","reformulation":"g(n)->inf <=> N-F_c(N)->inf, F_c(N)=min_{m>N composite}(m-p(m))","erdos_conjecture":"N-F_c(N) ~ c N^{1/2} (open; would ...
Crossref-verified citations (Ford et al., Annals 2016) + open-status check
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
This is **open** (no proof or disproof is known).
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_463 : answer(sorry) ↔ ∃ (f : ℕ → ℕ) (_ : Tendsto f atTop atTop),
∀ᶠ n in atTop,
∃ m, m.Composite ∧
n + f n < m ∧ m < n + m.minFacformal-conjectures/463.lean ↗Vela formalization: Erdos463.lean (sorry-free)
links
related: #385
status
open