---

Claim. For every Sidon set $S\subset\mathbb R$ (all sums $a+b$ with $a,b\in S$ distinct up to the order of the summands) there is a set $A\subseteq\mathbb R\setminus S$ of cardinality $\mathfrak c$ with $A+A\subseteq\mathbb R\setminus S$, and the same holds for every $S\subset\mathbb R$ with $|S|<\mathfrak c$. Restricted to sum-free $S$, these are instances of Problem 949 answered yes. The proof is the theorem erdos_949.variants.sidon of the formal-conjectures statement file for the problem, merged on 6 January 2026 from the pull request linked above, whose description says that AlphaProof found several proofs of the variant and that the author of the pull request cleaned one up, keeping AlphaProof's version in the pull request's history. A comment in the site's discussion thread on 7 January 2026, by the same author, gives the argument in prose and links the Lean proof. The argument has two cases. If $|S|<\mathfrak c$, Zorn's lemma gives a maximal $A\subseteq\mathbb R\setminus S$ with $A+A\subseteq\mathbb R\setminus S$; maximality puts every real outside $S\cup\tfrac12S$ into $A\cup\bigcup_{a\in A}(S-a)$, a set of cardinality at most $|A|+|A|\,|S|$, so $|A|=\mathfrak c$. This case does not use the Sidon hypothesis. If $|S|=\mathfrak c$, pick $a\in S$ with $a\ne0$ and set $A=((S\setminus\{a\})-a/2)\setminus S$; the Sidon property leaves at most one point of $(S\setminus\{a\})-a/2$ inside $S$, so $|A|=\mathfrak c$, and $A+A\subseteq(S\setminus\{a\})+(S\setminus\{a\})-a$ is disjoint from $S$. The variant as formalized asks the question for every Sidon $S$, sum-free or not; the theorem is stated for IsSidon S and proved without sorry inside the statement file.

Submission note. Posted to the site's forum by Yaël Dillies on 7 January 2026:

For the question from the additional material: “Erdős suggests that if the answer is no, one could consider the variant where we assume that $S$ is Sidon.” AlphaProof found the following solution:

We case on whether $S$ has cardinality the continuum or strictly less. If $S$ has cardinality strictly less than the continuum, then we pick by Zorn some maximal $A$ such that both $A$ and $A + A$ are disjoint from $S$. Now, to see $A$ has size the continuum, note that

$$> A \cup \bigcup_{a \in A} (S - a) \cup S \cup S/2 = \mathbb R >$$

by maximality of $A$. By assumption, $|S^c \cap (S / 2)^c| = |\mathbb R|$. If $|A| < |\mathbb R|$, we would therefore have

$$> |\mathbb R| = |S^c \cap (S / 2)^c| ≤ |A \cup \bigcup_{a \in A} (S - a)| ≤ |A| + |A| |S| <|\mathbb R|, >$$

contradiction. If $S$ has cardinality the continuum, then we pick some $a\ne 0$ in $S$ and set $A := (S \setminus \{a\} - a / 2) \setminus S$. Since $S$ is Sidon and $a\ne 0$,

$$> (S - a / 2) \cap S \supseteq (S \setminus \{a\} - a / 2) \cap S >$$

has at most one element. In particular, $|A| = |S \setminus {a} - a / 2| = |S| = |\mathbb R|$ as wanted. Since $S$ is Sidon,

$$> A + A \subseteq S \setminus \{a\} + S \setminus \{a\} - a >$$

is disjoint from $S$, as wanted.

Here is the Lean proof discovered by AlphaProof as well as a cleaned up version.

(The site has been updated to address this comment.)

Covers. Every sum-free Sidon $S$, and every sum-free $S$ with $|S|<\mathfrak c$: for these the answer is yes. Not covered: sum-free $S$ of cardinality $\mathfrak c$ that are not Sidon, which is where the problem stays open.

Depends on. No page of this wiki.

Acceptance. None recorded. The site labels the problem OPEN; its commentary states that a thread comment proves the Sidon variant by an argument that AlphaProof found, which is commentary on an open problem and not an acceptance of a solution. The proof is attributed to AlphaProof, as the pull request and the comment name it. This corpus has not built the file at the linked commit or audited the theorem's statement, so the link is not formalized evidence; nothing on this page is this project's own review. No refereed source carries the result.