The cardinality of a set containing the pairwise sums of four positive integers

Choi, Erdős and Szemerédi showed that there exists an absolute constant $C$ such that for all subsets $A\subseteq \{1,2,\dots ,2n\}$ with at least $n+C$ elements, there exist four distinct positive integers whose pairwise sums are all contained in $A$. A proof that one can take $C=3166$ was recently sketched by the first author, and here we show that we actually have $C=4$ for all $n\ge 6$, which is optimal. The proof we present was originally conceived of by AI, with the final result proved and formalized by Aristotle, the formal reasoning agent developed by Harmonic.