Wiki
Wiki

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 ϵ>0\epsilon>0. Is there some r≪ϵ1r\ll_\epsilon 1 such that the density of integers of the form 2k+n2^k+n, where k≥0k\geq 0 and nn has at most rr prime divisors, is at least 1−ϵ1-\epsilon?

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 ϵ>0\epsilon>0 there is an rr such that the integers 2k+m2^k+m, with mm having at most rr distinct prime factors, have lower density greater than 1−ϵ1-\epsilon. 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 1−ϵ1-\epsilon; 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 2k+m2^k+m with mm free of primes in (z,x1/t](z,x^{1/t}] for large constants z,tz,t, 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 2k−2l2^k-2^l. 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 r=1r=1 case with a positive density in place of 1−ϵ1-\epsilon. 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 r≪log⁡(1/ϵ)/log⁡log⁡(1/ϵ)r\ll\log(1/\epsilon)/\log\log(1/\epsilon) 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.

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 2k+p2^k+p with pp prime have positive lower density, his Satz II with the base 22 (Romanoff card); this is the r=1r=1 case of the question with a positive constant in place of 1−ϵ1-\epsilon. Price's argument (claim page) answers the question yes: for every ϵ>0\epsilon>0 there is an rr depending only on ϵ\epsilon such that the integers 2k+n2^k+n with nn having at most rr prime divisors have lower density at least 1−ϵ1-\epsilon, by a sieve count of the representations 2k+m2^k+m with mm 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 r≪log⁡(1/ϵ)/log⁡log⁡(1/ϵ)r\ll\log(1/\epsilon)/\log\log(1/\epsilon), which the site's commentary also records; no write-up was found on 2026-10-07. Whether rr can be chosen independent of ϵ\epsilon is open; the same comment ties that question to covering congruences, which with Bang's theorem rule out r=2r=2. The site's commentary points to Problem 205, which asks whether every large integer is 2k+m2^k+m with Ω(m)<log⁡log⁡m\Omega(m)<\log\log m.

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.