---

Claim. For $M\leq3$ and all large $N$, every non-empty Sidon set $A\subseteq\{1,\ldots,N\}$ has a Sidon set $B\subseteq\{1,\ldots,N\}$ of size $M$ with $(A-A)\cap(B-B)=\{0\}$.

Covers. The cases $M=1$, $M=2$ and $M=3$ of the question; the general case is the result on [[problems/additive_bases/E0042/claims/2026_04_27_sandhu|Sandhu's claim page]].

Argument. For $M=3$ Sedov posted on 2026-01-19 a Lean 4 development of about 8,000 lines, pinned to its commit of that day, with one declared axiom, the 2/5 trichotomy for strongly sum-free subsets of an interval: Theorem 2.2 of Balogh, Liu, Sharifzadeh and Treglown (arXiv:1409.5661), attributed there to Deshouillers, Freiman, Sós and Temkin (Astérisque 258, 1999). For $M=1$ a singleton $B$ works, since its difference set is $\{0\}$; for $M=2$ Sedov posted on 2026-01-22 an argument in a ChatGPT transcript (the second discussion link). Sedov states that the Lean development was produced, without human mathematical input, by an autonomous agent powered by GPT-5.2 in Codex CLI, which used Aristotle for the Lean and GPT-5.2 Pro in ChatGPT for ideas, and that GPT-5.2 Pro reviewed the result; the site's remarks name ChatGPT and Codex.

Standing. Claimed. The site's remarks, written while the problem was labeled OPEN, credit Sedov with the cases $M=3$ and $M=2$ and call $M=1$ trivial. The problem has no parts, and its later solved label rests on the general proof on Sandhu's claim page. In the thread Sothanaphan judged the $M=3$ development a correct partial solution whose axiom matches the cited Theorem 2.2, an assessment Sothanaphan states was made with ChatGPT's help (2026-01-19); that check does not cover $M=2$. The corpus has not built the development or discharged its axiom.

Depends on. Nothing in this wiki.