Claim. In ZFC there is a $2$-coloring of $\mathbb R$ under which no uncountable set $A\subseteq\mathbb R$ has all sums $a+b$, $a\ne b\in A$, of one color; in particular no set of cardinality $\aleph_1$ has, so the answer to Problem 965 is no without the continuum hypothesis. This answers Question 3.3 of Hindman, Leader and Strauss for two colors, whose CH disproof is the accepted conditional claim Hindman, Leader and Strauss 2015. The same theorem was proved independently in the unpublished manuscript of Soukup and Weiss, the accepted claim Soukup and Weiss 2015, which states on its first page that Komjáth proved the same result independently.

Acceptance. Refereed: P. Komjáth, A certain 2-coloring of the reals, Real Anal. Exchange 41 (2016), no. 1, 227--231 (the publisher's record, gives volume 41, issue 1, first page 227; it gives no day, so the day in the page name is a placeholder and the page is dated by the volume year). Reviewed: the site's curator, Thomas Bloom, credits the paper as one of two independent ZFC disproofs in the problem's commentary (page last edited 16 January 2026, accessed 2026-09-18); the formal-conjectures statement file for the problem cites it in its docstring as the counterexample. Semantic Scholar's ten citing records include, by title, no dispute.

Formalization. The file src/latest/ErdosProblems/Erdos965.lean of the GitHub repository plby/lean-proofs (Boris Alexeev's repository), linked above at the fixed commit that the formal-conjectures file's formal_proof attribute names, declares itself a Lean formalization of a solution to the problem with Komjáth as its informal author and Codex and GPT-5.6 Sol as its formal authors; it describes its argument as a ZFC finite-union coloring transferred through a Hamel basis of $\mathbb R$ over $\mathbb Q$. For Lean and Mathlib v4.33.0, it proves

not_erdos_965 : ¬ ∀ f : ℝ → Fin 2, ∃ A : Set ℝ, ¬ A.Countable ∧ ∀ᵉ (a ∈ A) (b ∈ A) (c ∈ A) (d ∈ A), a ≠ b → c ≠ d → f (a + b) = f (c + d)

the negation of the right-hand side of the collection's statement erdos_965, which asks for an uncountable set rather than one of cardinality $\aleph_1$ (equivalent, since every uncountable set of reals has a subset of cardinality $\aleph_1$ and the property passes to subsets), from a finite-support anti-Ramsey coloring (supportColor_finset_pair_antiramsey) transferred to $\mathbb R$ by a Hamel basis (exists_bad_real_coloring_of_finset_pair_antiramsey). The repository's commit history adds the file on 16 August 2026; the community database lists the problem "disproved (Lean)" as of its last update, of 23 August 2026, and the site's (Lean) suffix is the catalog label for this file. The file (1,808 bytes) and the three project modules it imports (FiniteColoring, FiniteMain, HamelTransfer), at the linked commit, contain no sorry and no axiom declaration, and the file ends with #print axioms without recording the output; the six deeper modules they import were not read. Nothing was built or kernel-checked here and no statement-fidelity review exists, so formalized is not listed.

Read depth. The paper is not held; no open copy was found, and no author copy was found. Everything attributed to it here is second-hand, from the site's commentary, the Soukup--Weiss manuscript, the formal-conjectures docstring and the header of the Lean file. Reopening condition: a copy of the paper read at its main theorem.