Claims

../

2026_01_19_sedov: A Lean 4 proof of the case M equal to 3, resting on one stated external theorem, with arguments for M equal to 1 and 2, posted to the thread and credited in the site's remarks.

2026_04_27_sandhu: A proof by GPT 5.5 Pro, prompted by Sandhu, that for every M and all large N every Sidon set in the first N integers admits a Sidon set of size M whose differences meet its own only at zero; accepted by the site's curator.

---