Erdős Problem #152 — For any $M\geq 1$, if $A\subset \mathbb{N}$ is a sufficiently large finite Sidon set then there are at least $M$ many $a\in A+A$ such that $a+1,a-1 ot\in A+A$.

The problem asks whether every sufficiently large finite Sidon set contains arbitrarily many isolated sums. It is associated with Erdős, Sárközy, and Sós (1994), whose cited paper is “On Sum Sets of Sidon Sets.”

April–May 2026 formalization claim

The problem page marks the assertion proved in Lean and records the stronger claim that the number of such sums is $a0\gg |A|^2$. The formal-conjectures entry attributes both claims to the “DeepMind prover agent,” but the displayed Lean theorem ends with by sorry, so this is not independently verifiable as presented.

Current status (as of May 2026): The conjecture is claimed proved, even in the stronger form $a0\gg |A|^2$, but no independently checkable proof artifact is available in the retrieved material.