---

Claim. For a Sidon set $A\subseteq\mathbb{N}$ of size $n$ let $I(A)$ be the number of $s\in A+A$ with $s-1,s+1\notin A+A$. Then

$$16\,I(A)+100n+16\geq n^2,$$

so the minimum $f(n)$ of $I(A)$ over Sidon sets of size $n$ satisfies $f(n)\geq(n^2-100n-16)/16$. In particular $f(n)\to\infty$, which answers the question yes, and $f(n)\gg n^2$, the strengthening the site's remarks ask about.

Argument. As the thread summarizes it: for $X\subseteq\mathbb{Z}$ write $N_k(X)$ for the number of $x\in X$ with $x+k\in X$ and $V_2(X)$ for the number with both neighbors in $X$. Three counting facts hold for every finite $X$: $I(X)+2N_1(X)=\lvert X\rvert+V_2(X)$; $4N_1(X)+N_3(X)\leq3\lvert X\rvert+2N_2(X)$, a pointwise inequality of indicator values summed over $X$; and $2N_2(X)\leq N_3(X)+2V_2(X)+2I(X)$. For $k=1,2,3$ the quadruples $(a,b,c,d)\in A^4$ with $a+b+k=c+d$ are compared with $N_k$ of the difference set $D=A-A$ and of the sumset $S=A+A$: the Sidon property gives at most $N_k(D)+2n$ quadruples, and each counted element of $S$ other than a double $2a$ yields at least four, so $4N_k(S)$ is at most the number of quadruples plus $8n$. Applying the indicator inequality to $D$ and transferring to $S$, the $N_1$, $N_3$ and $V_2$ terms cancel and leave $16\,I(S)+100n\geq8\lvert S\rvert-3\lvert D\rvert$; with $\lvert S\rvert\geq n^2/2$, $\lvert D\rvert\leq n^2$ and a boundary correction of $16$ at zero this is the claim.

Formalization. The proof is a Lean 4 development by the DeepMind prover agent in a fork of formal-conjectures, posted to the thread by GTsoukalas on 2026-04-03: the first pinned commit of 2026-04-02 proves erdos_152, the limit statement, and the second commit of that day proves the quadratic variant erdos_152.variants.square, which the poster says was formalized by hand from the same argument. formal-conjectures (the record link,) tags both statements research solved and cites these two commits as their formal proofs. A further Lean development, the file Erdos152.lean of Alexeev's lean-proofs repository (the third formalization link, added 2026-08-16), declares itself a formalization of a solution to Problem 152, listing the DeepMind prover agent among its informal authors with Erdős, Sárközy and Sós, and Codex and GPT-5.6 Sol as its formal authors; it proves erdos_152_unbounded, that $f(n)\to\infty$, and erdos_152, that $n^2\leq64\,f(n)$ for all large $n$.

Acceptance. Reviewed: Thomas Bloom, the site's curator, states in the thread on 2026-05-16 that the problem is solved by this proof, which has been formalized, and the remarks credit DeepMind with the stronger $\gg\lvert A\rvert^2$ bound; the page is labeled proved (last edited 2026-05-17; accessed 2026-10-07). Bloom's remark of 2026-04-03 that the methods of Erdős, Sárközy and Sós already give the result was withdrawn by Bloom on 2026-05-16, leaving this the only proof known. The corpus has built none of the Lean developments and has not audited the agreement of their statements with the site's formulation.

Depends on. Nothing in this wiki.