Isolated sums of finite Sidon sets

A Sidon set has no repeated pair sums except those forced by exchanging the summands. For n-element Sidon sets A⊂N, how many elements of A+A are isolated, with both neighboring integers absent from A+A?

Why it matters and what counts as progress

Why it matters: Isolated sums test a finer structural feature of Sidon sumsets than their large total cardinality.

What counts as progress: Prove a quadratic lower bound for isolated sums, improve its leading coefficient or construct Sidon sets approaching the minimum.

How the problem developed

1994 · Open question [1]
Paul Erdős, András Sárközy and Vera T. Sós Published the finite Sidon-set problem asking whether sufficiently large sets have arbitrarily many isolated elements in A+A.
3 Apr 2026 · Theorem [2][3][5]
Google DeepMind AlphaProof Nexus Posted a formal proof of a quadratic lower bound on the number of isolated sums, stronger than the original divergence question.
21 May 2026 · Publication [4][5]
Tsoukalas and collaborators Released a research paper reporting the AlphaProof Nexus result; its finite-set bound does not address the separate infinite-Sidon-set variant.

AI contribution

Advancing Mathematics Research with AI-Driven Formal Proof Search

George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferraiuolo, Henryk Michalewski, Edward Lockhart, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri

For every n-element Sidon set A of natural numbers, AlphaProof Nexus proves 16 I(A+A)+100n+16≥n², where I counts sums whose neighboring integers are both absent from A+A. Thus the minimum isolated-sum count grows at least quadratically, answering the finite-set form of Erdős Problem 152.

AI involvementAI-autonomous

ImportanceNotable

Technical verificationFormal (Lean 4)

Human understandingFull