Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. For every there is an , depending only on , such that the integers of the form with and having at most prime divisors have lower density at least . This answers the question yes. The argument, as the thread describes it, counts representations in which is divisible by no prime between a large constant and for a large constant , which forces to have a bounded number of prime factors; the fundamental lemma of sieve theory estimates the first and second moments of this representation function, the mean number of representations is of order , and the second moment reduces to showing that a singular series over the primes in that range dividing is close to on average over , which holds because means that the multiplicative order of modulo divides , and few primes have an order of logarithmic size since a Mersenne number has prime factors. Romanoff's 1934 theorem, that the integers with prime have positive lower density, is the case with a positive constant in place of (source card).
The posting. The claimant posted the argument on 5 February 2026 in the site's thread as a document shared through Overleaf, writing that it was produced by GPT-5.2 Pro over about ten prompted rounds and that the poster did not claim its accuracy; the document is not held, and this page does not rest on it. The site names the claimant as Liam Price; the statement collection's reference gives the initial D. and the Lean development linked below gives the given name Lisa, so the sources disagree on the first name, and this page uses the surname.
Acceptance. Reviewed: Tao's thread comment of 5 February 2026 first judged
the strategy viable and then, in an edit, confirmed the proof correct, naming
the reduction to the averaged singular series and the Mersenne factor-count
bound (the document's Lemma 7) as the step that closes it; the site's curator,
Thomas Bloom, labels the problem PROVED with the note that the answer is yes,
the page last edited 2 April 2026, and the curator's commentary credits the
solution to Price using GPT-5.2 Pro (accessed 2026-09-05 and 2026-10-07; five
comments, no proof claim, no exposition). Tao's comment also records that the
literature had overlooked the question, the nearest work being Zhao's 2024 paper
on counterexamples in arithmetic progressions for fixed by covering
congruences, and a later comment places the singular-series bound in a paper of
Matthews on counting points modulo for finitely generated subgroups of
algebraic groups; neither paper is held. Not refereed: no journal or arXiv
version was found on 2026-10-07. The arXiv API query abs:Romanoff returned ten
records, five of them from 2026, among them 2609.38408 (large gaps between
integers of the form ) and 2607.03662 (a Romanoff-type theorem for
); none is a posting of this argument or of the quantitative
version announced in the thread. The query abs:"powers of two" AND abs:"prime factors" AND abs:density returned no record. Not counted as formalized: the
linked Lean file, Erdos851.lean in Boris Alexeev's lean-proofs repository,
declares itself a formalization of a solution to the problem, names Price and
GPT-5.2 Pro as its informal authors and Codex and GPT-5.6 Sol as its formal
authors, and proves the statement without sorry from a development of its own;
this page rests on its top-level file only, and it was not built or audited
here. The statement collection's ErdosProblems/851.lean states the theorem
with a sorry body and points at that file through a formal_proof attribute;
a statement file is not a formalization and is not linked here. The site's
formalized-statement indicator refers to the statement collection. This page
rests on no review of its own.
Scope. Full for the site's statement. Whether can be taken independent of is a further question raised in the thread, which the thread connects to covering congruences and does not settle. A thread comment of 6 February 2026 by Sawhney announces that Sawhney and Green have had a version of this argument for some time which gives , replacing the second-moment argument by a high-moment argument, and that this seems to be the limit of a direct sieve approach; the comment adds that an independent of seems very difficult and is tied to covering congruences, that a naive heuristic would suggest , which covering congruences and Bang's theorem rule out, and that a bounded would need at least Hough's theorem on covering systems. The comment links no write-up, and no manuscript of that version was found on 2026-10-07, so it has no claim page of its own.
Depends on. No page of this wiki.