---

Claim. For any $\ell$ distinct integers $a_1,\ldots,a_\ell$ there are infinitely many $n$ for which the number of solutions of $n=p+a_i$ with $p$ prime exceeds $\tfrac18\log\ell-1.6$. Consequently, if $a_1<\cdots<a_t\le x$ with $t>\log x$, infinitely many $n$ have more than $\tfrac18\log\log x-1.6$ such representations, and for every infinite set $A\subseteq\mathbb N$ the representation function $f(n)=\#\{(p,a):n=p+a\}$ satisfies $\limsup f(n)=\infty$. These are Theorem 1.1 and Corollaries 1.2 and 1.3 of Y.-G. Chen and Y. Ding, On a conjecture of Erdős, C. R. Math. Acad. Sci. Paris 360 (2022), 971–974, first posted as arXiv:2201.10727 on 26 January 2022 and summarized on its library card. Corollary 1.3 answers the question of Problem 237 in the affirmative and shows that its growth hypothesis $\lvert A\cap\{1,\ldots,N\}\rvert\gg\log N$ can be dropped: any infinite $A$ suffices. The proof removes one residue class modulo each small prime to extract from the $a_i$ an admissible subset of size $\gg\ell/\log\ell$, using Mertens' product estimate, and applies the Maynard–Tao theorem that an admissible $k$-tuple has infinitely many translates containing at least $m$ primes when $k\log k$ is large in terms of $m$. Erdős proved the case $A=\{2^k\}$ in 1950 (Theorem 1 of the paper on its library card, the accepted partial claim), and the conjecture in Corollary 1.2's form is his.

Acceptance. The paper is a refereed journal publication, published online on 29 September 2022, the refereed evidence. The site's curator, Thomas Bloom, labels the problem proved and credits the affirmative answer to this paper, noting that infinitude of $A$ suffices, the reviewed evidence. The page is dated by the preprint's first posting.

Formalization. Two Lean files are linked. The first is a conditional formalization: the gist posted in the site's discussion thread on 4 April 2026 by Pietro Monticone, who writes that the solution was autoformalized by the system Aristotle conditionally on the Maynard–Tao theorem and Mertens' third theorem, which the file declares as the axioms maynard_tao and mertens_third_theorem; a later thread post by the user Woett supplies a Lean proof of the Mertens input, and the thread marks Monticone's post with the site's note that the page was updated to address it. The second is the file in Boris Alexeev's lean-proofs repository, pinned at the commit in the link, which declares itself a Lean formalization of a solution to Problem 237, names Chen and Ding as its informal authors and Aristotle and Pietro Monticone as its formal authors, and declares its status as unconditional on Lean's standard axioms. At the pinned commit it imports that repository's ErdosProblems.Axioms module, which declares the four custom axioms dusart_mertens_product, dusart_pi_lower, dusart_pi_upper and dusart_chebyshev beside the theorem maynard_tao, and its Util.MertensThird module. The file's own text carries no sorry or axiom token, and it ends with #print axioms erdos_237 and a comment recording the output as only propext, Classical.choice and Quot.sound; an imported axiom enters a theorem only when its proof uses it, so by that recorded output erdos_237 uses none of the four custom axioms. Its theorem erdos_237 states that for an infinite $A\subseteq\mathbb N$ and every $C$ some $n$ has more than $C$ representations, and the repository also holds an alternative proof under the name Erdos237b. The site's problem page links no Lean proof and lists no formal statement in google-deepmind/formal-conjectures; these are the Lean files the page records, not the recorded basis of the site's label. This corpus has not built or kernel-checked either, so no formalized evidence is listed.

Depends on. Nothing beyond the cited paper.