---

Claim. The second question has a negative answer. There is no constant $c>0$ such that

$$\binom{\lvert A\rvert}{2}+\binom{\lvert B\rvert}{2}\leq(1-c+o(1))\binom{f(N)}{2}$$

for all large $N$ and all Sidon sets $A,B\subseteq\{1,\ldots,N\}$ with $\lvert A\rvert=\lvert B\rvert$ and $(A-A)\cap(B-B)=\{0\}$: for infinitely many $N$ such pairs reach $(1-o(1))\binom{f(N)}{2}$.

Covers. The second question, on pairs of equal size. The first question is answered no through the solution of Problem 42 on the first question's claim page; Barreto's write-up of 2026-04-29 and comment of 2026-05-01 in Problem 42's thread state the combined resolution of both questions, crediting the first to Tao's observation and the solution of Problem 42.

Construction (2025-12-19). Take an odd prime power $q$, put $M=q^2-1$ and $N=M/2$, and let $S\subseteq\{1,\ldots,M-1\}$ be a Bose–Chowla set of size $q$ that is Sidon modulo $M$. If $S$ has $a$ even and $b$ odd elements then $a(a-1)+b(b-1)\leq N-1$, because the directed differences inside each parity class are distinct nonzero even residues modulo $M$ and the two families are disjoint; hence $\min(a,b)=q/2-O(\sqrt q)$. Halving $m=\min(a,b)$ even elements, and $m$ odd elements after subtracting one, and shifting by one gives Sidon sets $A,B\subseteq\{1,\ldots,N\}$ of size $m$ whose nonzero differences cannot coincide, since a common difference would make an even pair of $S$ equal an odd pair modulo $M$. Then $2\binom{m}{2}=m(m-1)=N/2+O(N^{3/4})=(1-o(1))\binom{f(N)}{2}$, as $f(N)=(1+o(1))\sqrt N$. Barreto formalized this half in Lean 4 on 2025-12-21, through the Lean web-editor link listed above, whose URL carries the code itself since no repository commit holds it, stating that the Erdős–Turán bound and the Bose–Chowla construction in it were formalized by Harmonic's Aristotle. The write-up of 2026-04-29 that Barreto had GPT produce (the preprint link) proves the construction as its Theorem 1.3. A second formalization, the file Erdos43.lean of Alexeev's lean-proofs repository (the second formalization link, added 2026-08-20), declares itself a Lean formalization of a solution to Problem 43 with Barreto as informal author and Codex and GPT-5.6 Sol as formal authors; it proves both formal-conjectures parts, not_erdos_43 through the repository's formalization of Problem 42's solution and not_erdos_43_part_ii for this construction. The corpus built and audited neither development.

Acceptance. Reviewed: Thomas Bloom, the site's curator, labels the problem disproved and states in the remarks that the first question fails because of Problem 42's solution and that Barreto's construction settles the second (page last edited 2026-05-10; accessed 2026-10-07); in the thread Tao remarked that the construction follows simply from known Sidon set constructions (2025-12-19). Tao's upper bound without the $-c$, $\lvert A\rvert=\lvert B\rvert\leq(1/\sqrt2+o(1))\sqrt N$ (2025-12-03), bounds how far the second question's inequality can fail. No refereed publication is known; the corpus has built or reviewed none of this.

Depends on. Nothing in this wiki; the construction stands on its own.