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.