---

Claim. For every $M\geq1$ there is $N_0(M)$ such that for every $N\geq N_0(M)$ and every non-empty Sidon set $A\subseteq\{1,\ldots,N\}$ there is a Sidon set $B\subseteq\{1,\ldots,N\}$ with $\lvert B\rvert=M$ and $(A-A)\cap(B-B)=\{0\}$. This answers the question yes, read as the problem page's Formulation records.

Argument. As the thread summarizes it: place $A$ in $\mathbb{F}_p$ for a prime $p$ a little larger than $2N$, so that $A-A$ is still the difference set of a Sidon set; the Sidon property keeps every Fourier coefficient of $1_{A-A}$ above $-c\sqrt p$. The key lemma says that a symmetric $F\subseteq\mathbb{F}_p$ with $\lvert F\rvert\leq p/2$ and no Fourier coefficient below $-o(p)$ is avoided by the nonzero differences of a uniformly random $M$-subset of $(0,p/4)$ with probability bounded below in terms of $M$ alone. A random $M$-set fails to be Sidon with probability $O(M^4/p)$, so for $p$ large in terms of $M$ some $B$ is Sidon and avoids $A-A$. The posted proof phrases the key lemma in a continuous limit; Sothanaphan's exposition of 2026-04-30 (the Drive link of 2026-04-30, a PDF dated 2026-05-01 that states it was produced with use of GPT-5.5 Thinking) arranges the argument around that limit and a compactness step; it is a third-party exposition, not a posting by the claimant. Sandhu's post links two ChatGPT sessions, the proof session and the audit and formalization discussion (the two chat links). On 2026-05-01 Sandhu posted a second proof from another GPT 5.5 Pro run, A Compact Cayley Lemma and a Sidon Difference-Avoidance Theorem (the preprint link), which goes through a compact Cayley graph lemma; the formalization follows that route.

Acceptance. Reviewed: Thomas Bloom, the site's curator, labels the problem solved and credits the proof for all $M$ to GPT 5.5 Pro prompted by Sandhu (page last edited 2026-05-10). In the thread Bloom asked for a careful examination and a formalization of the key lemma; the forum user paws posted on 2026-05-10 a Lean 4 and Mathlib formalization of the solution (the first formalization link, pinned to the repository's last commit touching the file that day), and the label was set the same day. The proof text was generated by GPT 5.5 Pro; Sandhu prompted it, audited it in further sessions, and posted it on 2026-04-27. A separate write-up that Barreto generated with GPT, an Overleaf document linked in Barreto's thread post of 2026-04-29, extends the method to a $B$ of size $\gg(\log\log N/\log\log\log N)^{1/2}$, a bound added by a later edit of that post; the site's remarks record it as what the method seems able to prove. Two later write-ups restate the theorem for non-empty $A$. Barreto's note Sidon difference avoidance, dated 29 April 2026, proves it as its Theorem 1.1. Barreto had GPT produce the note to combine the work on Problems 42 and 43, and linked it from the thread post of that day (the Drive link of 2026-04-29). Chojecki's draft note A Fourier-positive proof of Erdős Problem 42, dated 30 April 2026, states it as its Theorem 1.1 (the ulam.ai link). Chojecki posted it in the thread as a note obtained from GPT-5.5 Pro after prompting it with Tao's suggested approach. Tao replied that the note rests more on the thread's posted proof than on that approach, omits many key details and gives no quantitative bound on $N$ in terms of $M$. No refereed publication is known; the corpus has built or reviewed none of this.

Formalization. The file Erdos/P42/CompactCayley/Proof.lean of the erdos-formalizations repository (GitHub account Shashi456) follows the compact Cayley route. The poster reports no sorry, admit or unsafe, an axiom closure of propext, Classical.choice and Quot.sound for all five exposed theorems, a check under Lean and Mathlib 4.28 with SafeVerify, and a proved equivalence with the formal-conjectures statement; the Lean was produced with Codex 5.5 and GPT-5.5 Pro. Sothanaphan confirmed it correct in the thread on 2026-05-12, a check Sothanaphan made with ChatGPT, and formal-conjectures (as of 2026-10-07) cites the file, unpinned, as the formal proof of its Erdos42.erdos_42. That statement quantifies over inclusion-maximal Sidon sets $A$ (IsMaximalSidonSetIn) where the site quantifies over all Sidon sets; Tao noted on 2025-12-05 that $A$ may be taken maximal without loss of generality, and Barreto spelled out the bridge on 2026-04-30: a Sidon set extends to an inclusion-maximal one, and a $B$ whose differences avoid the larger difference set avoids the smaller. The corpus has not built the proof, checked its axioms, or audited its statement or the maximality bridge, so the formalization is not counted as evidence. A second development, the file Erdos42.lean of Alexeev's lean-proofs repository (the second formalization link, added 2026-05-13), declares itself a Lean formalization of a solution to Problem 42 with GPT-5.5 Pro and Sandhu as informal authors and Codex 5.5, GPT-5.5 Pro and Pawan Sasanka Ammanamanchi as formal authors; it bundles the compact Cayley development into one file importing Mathlib alone and proves theorem_1_1_via_cayley and erdos_42; the corpus built and audited it no more than the original.

Depends on. Nothing in this wiki.