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

Updated Oct 8

Problem 237

claims/: The 2 claim pages of Problem 237, one per claimant's result; the problem's standing derives from them.

Statement. Let $A\subseteq \mathbb{N}$ be a set such that $\lvert A\cap {1,\ldots,N}\rvert \gg \log N$ for all large $N$ . Let $f(n)$ count the number of solutions to $n=p+a$ for $p$ prime and $a\in A$ . Is it true that $\limsup f(n)=\infty$?

Status. PROVED (LEAN), the site's label. The accepted claim is Chen and Ding's 2022 theorem, refereed and credited by the site's curator, which also shows that any infinite $A$ suffices. Erdős's 1950 theorem for $A=\{2^k:k\ge0\}$ , credited in the site's commentary, is the accepted partial claim a prime plus a power of two. The site's page links no Lean proof; the two Lean files recorded on Chen and Ding's page, one conditional and one that declares itself unconditional, were built by neither the site nor this corpus.

Source. erdosproblems.com/237, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #237, https://www.erdosproblems.com/237.

References.

[ChDi22] Chen, Y.-G. and Ding, Y., On a conjecture of Erdős. arXiv:2201.10727 (2022).
[Er50] Erdős, P., On integers of the form $2^k+p$ and some related problems. Summa Brasil. Math. (1950), 113-123.

Formalization. No statement in google-deepmind/formal-conjectures is listed on the site, and the site's page links no Lean proof. Two Lean files are recorded on the claim page: an Aristotle autoformalization posted in the site's thread, conditional on the Maynard–Tao theorem and Mertens' third theorem, which it declares as axioms, and a file in Boris Alexeev's lean-proofs repository that declares itself unconditional and records an axiom check listing only Lean's standard axioms, although it imports a module that declares four custom axioms. This corpus has built neither.

Progress

Not yet compiled.

Known Results

Not yet compiled.

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.

Linked from (8)

Erdős: unboundedly many representations as a prime plus a power of two Chen and Ding: unboundedly many representations as a prime plus a member problems/primes/E0237/claims Primes primes/chen_2022_conjecture_erdos primes/erdos_1950_integers_form_related_problems Conjectures, p. 115: f(n) = o(log n), 105 as the largest n with every n - 2^k prime, and a generalization of Theorem 1 Theorem 1 (p. 113): the number f(n) of representations n = 2^k + p is unbounded, f(n) > c log log n infinitely often

Graph