Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 851
claims/: The 1 claim page of Problem 851, one per claimant's result; the problem's standing derives from them.
Statement. Let . Is there some such that the density of integers of the form , where and has at most prime divisors, is at least ?
Formulation. The site's statement bounds the density. Erdős's source asks for the lower density: in [Er85c], p. 75, he asks whether to every there is an such that the integers , with having at most distinct prime factors, have lower density greater than . This page reads the site's question that way. The formal-conjectures statement bounds the lower density too, and the site's acceptance of Price's argument needs this reading. Price's argument gives lower density at least ; it does not show that the density exists.
Status. Proved. The answer is yes. Price posted an argument generated with GPT-5.2 Pro in the site's thread on 5 February 2026: a sieve count of the representations with free of primes in for large constants , whose first and second moments the fundamental lemma of sieve theory estimates, the second moment resting on an averaged bound for a singular series over the primes dividing . Tao confirmed the proof correct in an edit to his thread comment of 5 February 2026, and the site's curator, Thomas Bloom, labels the problem PROVED and credits the solution to Price (page last edited 2 April 2026, accessed 2026-09-05 and 2026-10-07; five comments, no proof claim, no exposition). No refereed or arXiv version was found on 2026-10-07. Romanoff (1934) gives the case with a positive density in place of . Claim page: Price 2026 (accepted on Tao's confirmation and the site's curator's acceptance; not refereed, not counted as formalized). A thread comment of 6 February 2026 by Sawhney announces that he and Green have a version of the argument that gives by a high-moment argument in place of the second moment, which the site's commentary also mentions; it is a thread comment without a write-up, no manuscript was found on 2026-10-07, and it has no claim page.
Source. erdosproblems.com/851, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #851, https://www.erdosproblems.com/851.
References.
- [Er85c] Erdős, P., On some of my problems in number theory I would most like to see solved. Number Theory (Ootacamund, 1984), Lecture Notes in Math. 1122 (1985), 74--84. Library home: erdos_1985_my_problems_number_theory_i_would.
- [Ro34] Romanoff, N. P., Über einige Sätze der additiven Zahlentheorie. Math. Ann. 109 (1934), 668--678. Library home: romanoff_1934_uber_einige_satze_der_additiven.
Formalization. Statement in
formal-conjectures,
ErdosProblems/851.lean, with a sorry body, marked research solved; at
the pinned commit the statement carries a formal_proof attribute pointing at
Erdos851.lean in Boris Alexeev's lean-proofs repository, a Lean development
that declares itself a formalization of a solution to the problem, proves the
statement, and names Price and GPT-5.2 Pro as its informal authors and Codex
and GPT-5.6 Sol as its formal authors. Neither file was built or audited
here, and the community database records no formal-proof URL; the claim page
links the Lean development at a pinned commit as a formalization and counts
it as no formalized evidence, and the statement file is not a formalization
link.
Current assessment
Scope. Search scope, 2026-09-05 and 2026-10-07: the site's problem page, its thread of five comments, the statement file of formal-conjectures at the pinned commit, the top-level file of the Lean development it points at, and Romanoff's paper through its library card. Not part of that basis: Price's document; the proof coverage of the argument was not assessed here; the acceptance rests on Tao's confirmation and the curator's label, as the claim page records. No literature search beyond the site and the arXiv queries the claim page lists was made.
Claims. One result is claimed from outside the project and accepted by
the site:
Price's sieve argument
of 5 February 2026, a yes for the site's statement, confirmed by Tao and
credited by the curator, so the problem's standing is solved with the claim
proved. The quantitative version Sawhney announced in the thread has no
write-up and no claim page.
Known Results
Romanoff [Ro34] proved that the integers of the form with prime have positive lower density, his Satz II with the base (Romanoff card); this is the case of the question with a positive constant in place of . Price's argument (claim page) answers the question yes: for every there is an depending only on such that the integers with having at most prime divisors have lower density at least , by a sieve count of the representations with free of primes in a middle range, whose first and second moments the fundamental lemma estimates. Sawhney's thread comment of 6 February 2026 announces that he and Green have a version of the argument, replacing the second moment by a high moment, that gives , which the site's commentary also records; no write-up was found on 2026-10-07. Whether can be chosen independent of is open; the same comment ties that question to covering congruences, which with Bang's theorem rule out . The site's commentary points to Problem 205, which asks whether every large integer is with .
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.