What was already known
Romanoff proved positive lower density when n is prime.
AI involvement
Price reports that GPT-5.2 Pro developed the sieve argument through an interactive exchange; Price posed and managed the problem.
Price's first-person account credits GPT-5.2 Pro with producing the central sieve proof across an interactive exchange.
Importance
This answers Erdős #851 by making the lower density arbitrarily close to one.
Limitations
Terence Tao checked the moment and singular-series steps and confirmed Price’s argument. A later Lean theorem states the lower-density result. Green and Sawhney’s stronger quantitative variant is separate human work.
Technical verification
Tao explicitly confirmed the submitted argument after checking the first and second moments and singular-series averaging. The later Lean file reports a proof of the lower-density formulation, which is narrower than a natural-density assertion.
Formal checking
Price and GPT-5.2 Pro's near-one lower-density sieve argument; Mathematical review of the moment estimates and average singular-series bound, followed by explicit confirmation
- Checker
- Terence Tao
- Scope
- Price and GPT-5.2 Pro's near-one lower-density sieve argument
- Basis
- Reported by the linked checker
Formal checking
erdos_851: for every 0<ε<1 some r gives lower density at least 1−ε; Proof-bearing Lean theorem importing the uniform beta estimates development
- Checker
- Lean 4 in the plby/lean-proofs release
- Scope
- erdos_851: for every 0<ε<1 some r gives lower density at least 1−ε
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Tao explains the central sieve, moment and singular-series argument and the remaining prime-order estimate; Green and Sawhney describe a related stronger method.
Correction and publication history
This answers Erdős #851 by making the lower density arbitrarily close to one.
Read this published revision