Disproved. In ZFC there is a $2$-coloring of $\mathbb R$ under which no uncountable set has the sums of its distinct pairs monochromatic: Komjáth's theorem [Ko16] (Real Anal. Exchange 41 (2016), no. 1, 227--231; refereed; not held, quoted second-hand from the site, the Soukup--Weiss manuscript and the formal-conjectures file) and, independently, Corollary 3.2 of the Soukup--Weiss manuscript [SoWe] (unpublished as far as was found on 2026-09-18), whose coloring makes the sums of $N$ distinct elements take both colors for every uncountable set and every $N\ge2$. Under CH the same follows from Theorem 3.2 of Hindman, Leader and Strauss [HLS17] (refereed), a ZFC theorem about sets of size $\mathfrak c$ whose $\aleph_1$ case needs $\mathfrak c=\aleph_1$; the authors state that, when $\mathfrak c>\omega_1$, their coloring admits a set of size $\omega_1$ whose sums of $k$ distinct elements are monochromatic for every $k\ge2$, and ask (Question 3.3) for a ZFC proof, which is what the ZFC strand supplies. Erdős himself reported in 1975 that he could prove a negative statement under CH. The site's (Lean) suffix is a catalog label explained under Formalization; the external Lean file, which declares itself a formalization of Komjáth's argument and is linked from his claim page, was not built here. The claim pages Komjáth 2016 and Soukup and Weiss 2015 record the two ZFC disproofs and Hindman, Leader and Strauss 2015 the disproof under CH as a conditional claim; the frontmatter standing derives from these pages.