Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. For every ϵ>0\epsilon>0 there is an rr, depending only on ϵ\epsilon, such that the integers of the form 2k+n2^k+n with k≥0k\ge0 and nn having at most rr prime divisors have lower density at least 1−ϵ1-\epsilon. This answers the question yes. The argument, as the thread describes it, counts representations n=2k+mn=2^k+m in which mm is divisible by no prime between a large constant zz and x1/tx^{1/t} for a large constant tt, which forces m≤xm\le x 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 tlog⁡zt\log z, and the second moment reduces to showing that a singular series over the primes pp in that range dividing 2k−2l2^k-2^l is close to 11 on average over k≠lk\ne l, which holds because p∣2k−2lp\mid2^k-2^l means that the multiplicative order of 22 modulo pp divides k−lk-l, and few primes have an order of logarithmic size since a Mersenne number 2a−12^a-1 has O(a)O(a) prime factors. Romanoff's 1934 theorem, that the integers 2k+p2^k+p with pp prime have positive lower density, is the r=1r=1 case with a positive constant in place of 1−ϵ1-\epsilon (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 rr by covering congruences, and a later comment places the singular-series bound in a paper of Matthews on counting points modulo pp 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 p+2np+2^n) and 2607.03662 (a Romanoff-type theorem for P2+{aa}P_2+\{a^a\}); 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 rr can be taken independent of ϵ\epsilon 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 r≪log⁡(1/ϵ)/log⁡log⁡(1/ϵ)r\ll\log(1/\epsilon)/\log\log(1/\epsilon), 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 rr independent of ϵ\epsilon seems very difficult and is tied to covering congruences, that a naive heuristic would suggest r=2r=2, which covering congruences and Bang's theorem rule out, and that a bounded rr 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.