Problem 42

../

claims/: The 2 claim pages of Problem 42, one per claimant's result; the problem's standing derives from them.

---

Statement. Let $M\geq 1$ and $N$ be sufficiently large in terms of $M$. Is it true that for every Sidon set $A\subset \{1,\ldots,N\}$ there is another Sidon set $B\subset \{1,\ldots,N\}$ of size $M$ such that $(A-A)\cap(B-B)=\{0\}$?

Formulation. Read as the site words it, the question fails for the empty Sidon set: then $A-A$ is empty, so no $B$ gives $(A-A)\cap(B-B)=\{0\}$. The site and the sources read it for non-empty $A$, where the condition says that $A$ and $B$ share no nonzero difference. The site's remarks call the case $M=1$ trivial, which holds only for non-empty $A$. Tao noted in the thread on 2025-12-05 that the problem's original form took $A$ maximal. Formal-conjectures quantifies over maximal Sidon sets. Sedov's Lean asks only that the positive differences of $B$ avoid those of $A$. The write-ups of Sothanaphan, Barreto and Chojecki state the theorem for non-empty $A$. The claim pages answer the question so read.

Status. The site labels the problem “SOLVED (LEAN)”: the question, read for non-empty $A$ as the Formulation records, is answered yes, by a proof for every $M$ posted 2026-04-27 and formalized 2026-05-10, so the problem stands proved; the acceptance and the Lean qualifications are on the claim pages below.

Source. erdosproblems.com/42, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #42, https://www.erdosproblems.com/42.

Formalization. Statement in formal-conjectures, tagged research solved and quantifying over maximal Sidon sets; its formal_proof attribute cites the Lean 4 formalization recorded on [[problems/additive_bases/E0042/claims/2026_04_27_sandhu|Sandhu's claim page]], and a variant asking only that some threshold function $f$ exist, with the conclusion for $N\geq f(M)$, cites a second public Lean proof (repository erdos-42-constructive-variant, 2026-08-10), a short derivation from the first formalization that chooses the thresholds and gives no explicit bound. The corpus built and audited neither.

Current assessment

The site's formulation of 2026-10-07 asks whether, for every $M$ and all $N$ large in terms of $M$, every 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\}$. Read as the site words it, it fails for the empty set; read for non-empty $A$, as the Formulation records, it is answered yes: Sandhu's claim page records the proof, generated by GPT 5.5 Pro and posted on 2026-04-27, which the site's curator accepted; a Lean 4 formalization of 2026-05-10 is linked from that page; the corpus has not built it. Earlier partial progress, the cases $M\leq3$, is on Sedov's claim page.

Tao's remarks of 2025-12-05 in the thread: $A$ may be taken maximal (the problem's original form); the requirement that $B$ be Sidon can be removed, since a large set contains a Sidon subset of about square-root size; and a positive answer with $\lvert A\rvert=f(N)$ gives a negative answer to the first question of Problem 43. A separate write-up that Barreto generated with GPT, an Overleaf document linked from his thread post of 2026-04-29, claims an effective threshold $N_0(M)\leq\exp(\exp(CM^2\log 2M))$ and, by a later edit of that post, a $B$ of size $\gg(\log\log N/\log\log\log N)^{1/2}$; the site's remarks record that bound only as what the method seems able to prove. Two further write-ups of the theorem produced with GPT, Barreto's note of 2026-04-29 and Chojecki's draft note of 2026-04-30, are disclosed on Sandhu's claim page. The curator sketched an alternative Fourier route with better bounds on 2026-04-30, not written up in the thread. No refereed publication of the proof is known. The corpus holds no compiled or reviewed proof.