Erdős #42 — every Sidon set has a same-scale Sidon set with disjoint differences

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\}?$$ (erdosproblems.com/42, statement verbatim; a *Sidon set* $S$ has all pairwise sums $a+b$, $a,b\in S$, distinct up to the trivial $\{a,b\}=\{c,d\}$ coincidence, equivalently every nonzero difference $s-s'$ occurs for at most one ordered pair.) Origin: Erdős [Er95,p.5]. See also the equal-cardinality companion, erdosproblems.com/43.

Facts

- Status: SOLVED (LEAN). erdosproblems.com badge: "This has been resolved in some other way than a proof or disproof, and that resolution verified in Lean." No prize was attached to #42. - Answer: YES, for every fixed $M$ — every Sidon set $A\subseteq[N]$ (not just maximal ones) admits, for all sufficiently large $N=N_0(M)$, a companion Sidon set $B\subseteq[N]$ of size $M$ with $(A-A)\cap(B-B)=\{0\}$. - Small cases done first, in the erdosproblems.com comment thread: $M=1$ trivial; $M=2$ "a little less trivial," proved by Daniil Sedov; $M=3$ proved by Sedov using ChatGPT and Codex (formalized in Lean 4, ~8000 lines, github.com/Gusarich/erdos42 — per the forum-thread summary this Lean proof relies on one external axiom, the Balogh–Liu–Sharifzadeh–Treglown theorem on sum-free subsets; not independently verified here). - General case (all $M$) solved ~27 Apr 2026 by GPT‑5.5 Pro, prompted by Harjas Sandhu ("after approximately 20 attempts, with only 2 successful runs," per WebFetch summary of the discussion thread). Two independent Lean formalization routes exist, both in github.com/Shashi456/erdos-formalizations under Erdos/P42: - Route B ("compact Cayley") — fully axiom-free (depends only on Mathlib core: propext, Classical.choice, Quot.sound); this is the qualitative existence proof and the one detailed below. - Route A ("Fourier-positive") — depends on an extra unformalized axiom finite_fourier_avoidance_count (Green–Tao $U^2$-regularity / complexity-1 counting); gives the stronger *quantitative* remark noted on erdosproblems.com that one can in fact take $|B| \gg (\log\log N/\log\log\log N)^{1/2}$ rather than a fixed constant $M$. - Open variant remaining: an explicit constructive bound $N\geq f(M)$ (a function bounding how large $N$ must be) is still sorry in the formal-conjectures Lean skeleton (erdos_42.variants.constructive) — the compactness route (Route B) is intrinsically non-constructive (an ultralimit/diagonalization argument), so it proves existence of $N_0(M)$ without producing one. - Contributors credited on erdosproblems.com: Kevin Barreto, Zach Hunter, Harjas Sandhu, Daniil Sedov; formalization also cross-linked into Google DeepMind's formal-conjectures repo (FormalConjectures/ErdosProblems/42.lean, formal_proof using lean4 pointing at the Route-B file). - Related problems: Erdős #43 — Sidon-pair size bound (disproved) — the equal-cardinality variant (does $A$ itself admit such a $B$ with $|B|=|A|$?), explicitly cross-referenced on the erdosproblems.com page ("See also [43]"), still only a Lean *scaffold* per github.com/Shashi456/erdos-formalizations ("First half inherits Route A's axiom via #42; second half (Bose–Chowla parity construction) is still sorry").

Solution

Answer: YES. For every $M\geq1$ there is $N_0(M)$ such that for all $N\geq N_0(M)$ and every Sidon set $A\subseteq[N]$, a Sidon set $B\subseteq[N]$ with $|B|=M$ and $(A-A)\cap(B-B)=\{0\}$ exists (Theorem 3.3 of the compact-Cayley writeup).

The transferable idea — force a clique in a Cayley graph via a compactness/ultralimit passage to a connected compact abelian group, then read the clique's existence back down to a finite construction. The route-B proof (fully axiom-free in Lean) has four layered pieces:

1. Reduce "find a disjoint-difference Sidon set $B$" to "find a clique in a Cayley graph." Embed $[N]$ into $\mathbb Z_p$ for a prime $p\in(4N,8N)$ (Bertrand's postulate). Let $D_A=(A-A)\setminus\{0\}$ — since $A$ is Sidon, $\binom{|A|}{2}\le N-1$, so $|D_A|\le 2N-2 = O(N)$, a small minority of $\mathbb Z_p$. Set $T=\mathbb Z_p\setminus(D_A\cup\{0\})$, the "allowed difference set": $|T|>p/2$. Any clique $C$ in the Cayley graph $\mathrm{Cay}(\mathbb Z_p,T)$ — i.e. any $C$ with all pairwise differences landing in $T$ — automatically avoids every difference of $A$, because $T\cap D_A=\varnothing$.

2. Bound the Fourier bias of $T$ using that $A$ is Sidon. A short character-sum computation shows the normalized Fourier coefficients satisfy $\widehat{1_T}(r)\le (|A|-1)/p=O(N^{-1/2})$ for every nonzero $r$ — i.e. $T$ is Fourier-*non-positively-biased* at every nontrivial frequency, quantitatively small. This is exactly where Sidon-ness (not just "$A-A$ is small") is used: the pair-sum-distinctness controls $|\widehat{1_A}(r)|$, which controls $\widehat{1_{D_A}}(r)$, which controls $\widehat{1_T}(r)$.

3. The Compact Cayley Lemma (the reusable engine, Theorem 2.1): a dense, low-Fourier-bias Cayley graph on $\mathbb Z_p$ contains a clique of every fixed size, once $p$ is large enough. Precisely: fix $\ell,\eta>0$; there exist $\varepsilon,p_0$ such that for prime $p>p_0$, any symmetric $0$-free $T\subseteq\mathbb Z_p$ with $|T|\ge\eta p$ and $\widehat{1_T}(r)\le\varepsilon$ for all $r\ne0$ forces a clique of size $\ell$ in $\mathrm{Cay}(\mathbb Z_p,T)$. The proof is by contradiction via a genuine compactness passage: take a sequence of counterexamples $(p_n,T_n)$ with bias $\to0$; extract (diagonal subsequence / Fourier-coefficient limits) a connected compact abelian group $G$ (Pontryagin dual of a countable torsion-free discrete group $\Gamma$ built as a direct limit of the finite dual groups $\widehat{\mathbb Z_{p_n}}$) and a limiting symmetric function $f:G\to[0,1]$ with $\int_G f\,d\mu\ge\eta$ and $\widehat f(\chi)\le0$ for every nontrivial character $\chi$. A clique-forcing lemma on connected compact groups (Lemma 2.7 — a positive-definiteness / Cauchy–Schwarz argument on $g=1-f$, splitting into "does $g$ hit its max only at $0$" vs. "the level set $\{g=1\}$ is a proper closed subgroup, use connectedness + Baire category to escape it") shows the homomorphism density $t_{K_\ell}(f)>0$. A separate counting-convergence lemma (finite quasirandomness / cut-norm control, Lemma 2.5–2.6) transfers this positive limiting clique density back down to $t_{K_\ell}(h_n)>0$ for the finite graphs, for $n$ large — i.e. an actual $\ell$-clique exists in $\mathrm{Cay}(\mathbb Z_{p_n},T_n)$, contradicting the assumed counterexample.

4. Pigeonhole the clique into an interval, then greedily extract a genuine Sidon set. A clique of size $\ell=8R_M$ in $\mathbb Z_p$ (where $R_M$ is an explicit greedy threshold, Lemma 3.2: $R_M=1+(M-1)+\binom{M-1}{2}+2(M-1)\binom{M-1}{2}$ — any $R_M$-element integer set contains a Sidon subset of size $M$, by greedily forbidding at most $R_M-1$ "bad" next-elements at each step) must, by averaging over the $p$ cyclic translates of an $N$-window, intersect some length-$N$ cyclic interval $I$ in $\ge R_M$ points. Translating $I$ back to $[N]$ gives an integer set $X$, $|X|\ge R_M$, all of whose differences avoid $D_A$ (since $|x-y|<N<p/2$, the $\mathbb Z_p$-difference *is* the integer difference). Lemma 3.2's greedy extraction pulls a genuine Sidon subset $B\subseteq X$ of exactly size $M$ out of $X$, and $B\subseteq X$ inherits $(B-B)\cap(A-A)=\{0\}$.

Why this is the transferable move. The heavy machinery (steps 2–3) is a general-purpose "forbidden-differences $\Rightarrow$ clique" black box: *any* finite additive-combinatorics obstruction that can be phrased as "avoid a small, Fourier-non-positively-biased difference set in $\mathbb Z_p$" reduces to finding a large clique in a Cayley graph, and the Compact Cayley Lemma supplies that clique unconditionally (for $p$ large enough, non-constructively) whenever the forbidden set has density bias $\to 0$. The compactness step — passing from a sequence of finite $\mathbb Z_{p_n}$ to a *connected* compact limit group via Pontryagin duality — is exactly analogous to (and could be swapped for) the ultraproduct/graph-limit machinery used in graph-regularity and hypergraph-removal arguments; here it is done "by hand" with explicit Fourier-coefficient diagonalization rather than an ultrafilter, which is what let it be formalized in Lean with zero extra axioms. The price of using a genuine compactness argument is that the resulting $N_0(M)$ is non-constructive/non-explicit — hence the separate open "constructive variant" asking for an explicit function $f(M)$.

Related

- Erdős #43 — Sidon-pair size bound (disproved) — the equal-cardinality companion ("does $A$ itself have such a $B$ with $|B|=|A|$?"), explicitly cross-referenced from #42's own page; still open/scaffold, and its Lean proof plan explicitly inherits #42's Route-A axiom for one half and needs a separate Bose–Chowla-style parity construction for the other half. - Erdős #41 — $B_3$ (distinct-triple-sum) set density liminf, Erdős #39 — density $N^{1/2-\\epsilon}$ infinite Sidon set, Erdős #30 — sharp $N^{1/2}$ asymptotics for Sidon sets — the classical Sidon/$B_h$-set density cluster (same underlying object, different questions: liminf density of infinite Sidon/$B_3$ sets, sharp finite-$N$ asymptotics); #42 is a different axis (disjoint-difference coexistence) on the same base structure. - Sidon sets / B_2 sets / Golomb rulers — the central combinatorial object; #42 uses only the elementary Sidon $\Rightarrow$ $\binom{|A|}{2}\le N-1$ counting bound plus its Fourier-coefficient consequence. - concept/compact-cayley-lemma — the reusable engine of this proof: dense + low-Fourier-bias $\Rightarrow$ arbitrarily large cliques in a Cayley graph on $\mathbb Z_p$, proved via a Pontryagin-duality compactness passage to a connected compact abelian limit group; the concept page to expand with the full Lemma 2.2–2.7 machinery for reuse on other "avoid a low-bias forbidden difference set" problems. - concept/greedy-sidon-extraction — Lemma 3.2's elementary greedy pigeonhole bound ($R_M$-element integer sets always contain a size-$M$ Sidon subset), the finite bridge from "large clique/interval-intersection" back to "genuine Sidon set," reusable whenever a large "structured enough" set needs to be pruned down to a Sidon (or similarly locally-constrained) subset. - concept/ai-formalized-erdos-problems — #42 is a 2026 example of an Erdős problem cracked by an LLM (GPT-5.5 Pro / ChatGPT+Codex) with the result subsequently Lean-formalized along two independent routes (one axiom-free), alongside #694, #750, #283/#351, #202, #1190 in the same github.com/Shashi456/erdos-formalizations repo.