[#P3066] Erdős Problem 152: isolated sums in Sidon sets

A neutral schematic of the objects and relations in the statement.

Problem. For each positive integer \(M\), prove that every sufficiently large finite Sidon set \(A \subseteq \mathbb{N}\) has at least \(M\) sums \(s \in A+A\) such that neither \(s-1\) nor \(s+1\) belongs to \(A+A\).

1Context

The question asks how the Sidon condition constrains local spacing in the sumset A+A. An isolated sum is separated by one integer from every other sum on both sides.

2Definitions

Definition 1 (Minimum isolated-sum function). For n in the natural numbers, f(n) is the minimum number of isolated elements of A+A among Sidon sets A of size n.

3What counts as a solution

Prove that the minimum isolated-sum count f(n) tends to infinity, or prove an explicit lower bound that implies this limit.
A formal certificate must bind the Formal Conjectures definition of f and answer True to the displayed natural-language target.

1The answerSupportednot Lean-verified

Answer (The minimum isolated-sum count grows at least quadratically). AlphaProof Nexus proved the stronger inequality 16 I(A+A) + 100|A| + 16 at least |A| squared, which settles Erdős Problem 152.^[1][2]

Resolution argument

Let S = A + A and D = A - A. For a finite integer set X, write N_k(X) for the number of x such that x and x + k both lie in X, V_2(X) for the number of points with both immediate neighbors in X, and I(X) for the isolated points. Three elementary relations control short gaps. First, I(X) + 2 N_1(X) = |X| + V_2(X), by sorting points according to their neighbors. Second, summing a pointwise inequality on four consecutive indicator values gives 4 N_1(X) + N_3(X) at most 3|X| + 2 N_2(X). Third, splitting distance-two pairs according to whether their middle point is present gives 2 N_2(X) at most N_3(X) + 2 V_2(X) + 2 I(X).

For k = 1, 2, 3, count quadruples (a,b,c,d) in A to the fourth power with a + b + k = c + d. Rewriting this as a - c = d - b - k transfers short gaps between S and D. The exceptional difference values 0 and -k contribute at most 2|A|. Away from them, the Sidon property makes the relevant representations unique. Conversely, every non-diagonal pair of sums in S separated by k produces four ordered quadruples, with at most 2|A| diagonal sums excluded. These two counts compare N_k(S) and N_k(D) with explicit linear errors.

Apply the four-point indicator inequality to D, substitute the quadruple bounds for k = 1, 2, 3, and obtain 16 N_1(S) + 4 N_3(S) at most 3|D| + 8 N_2(S) + 100|A|. Apply the distance-two inequality to S. The N_3 terms cancel. Then use the neighbor identity for S, which cancels the V_2 and N_1 terms, leaving 16 I(S) + 100|A| at least 8|S| - 3|D|, with a boundary correction of 16 when S is viewed inside the integers rather than the naturals. A Sidon set of size n has |S| at least n squared divided by 2 and |D| at most n squared. Therefore 16 I(A+A) + 100n + 16 is at least n squared. The resulting lower bound tends to infinity with n, proving the original statement for every fixed M.

1Records

Record	Kind	Assessment
	Result	Supported
claim · Proposition 1 AlphaProof Nexus proved the stronger inequality 16 I(A+A) + 100\|A\| + 16 at least \|A\| squared, which settles Erdős Problem 152.^[1][2] Relevance to this problem This stronger quantitative theorem resolves the canonical eventual isolated-sums question. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state established Scope all nonempty finite Sidon sets of natural numbers Sources Reference 1, Reference 2 Argument Let S = A + A and D = A - A. For a finite integer set X, write N_k(X) for the number of x such that x and x + k both lie in X, V_2(X) for the number of points with both immediate neighbors in X, and I(X) for the isolated points. Three elementary relations control short gaps. First, I(X) + 2 N_1(X) = \|X\| + V_2(X), by sorting points according to their neighbors. Second, summing a pointwise inequality on four consecutive indicator values gives 4 N_1(X) + N_3(X) at most 3\|X\| + 2 N_2(X). Third, splitting distance-two pairs according to whether their middle point is present gives 2 N_2(X) at most N_3(X) + 2 V_2(X) + 2 I(X). For k = 1, 2, 3, count quadruples (a,b,c,d) in A to the fourth power with a + b + k = c + d. Rewriting this as a - c = d - b - k transfers short gaps between S and D. The exceptional difference values 0 and -k contribute at most 2\|A\|. Away from them, the Sidon property makes the relevant representations unique. Conversely, every non-diagonal pair of sums in S separated by k produces four ordered quadruples, with at most 2\|A\| diagonal sums excluded. These two counts compare N_k(S) and N_k(D) with explicit linear errors. Apply the four-point indicator inequality to D, substitute the quadruple bounds for k = 1, 2, 3, and obtain 16 N_1(S) + 4 N_3(S) at most 3\|D\| + 8 N_2(S) + 100\|A\|. Apply the distance-two inequality to S. The N_3 terms cancel. Then use the neighbor identity for S, which cancels the V_2 and N_1 terms, leaving 16 I(S) + 100\|A\| at least 8\|S\| - 3\|D\|, with a boundary correction of 16 when S is viewed inside the integers rather than the naturals. A Sidon set of size n has \|S\| at least n squared divided by 2 and \|D\| at most n squared. Therefore 16 I(A+A) + 100n + 16 is at least n squared. The resulting lower bound tends to infinity with n, proving the original statement for every fixed M. Open full record →
	Lean	Reported
formalization · Formalization 1 A public Lean 4.27.0 file proves the explicit quadratic bound and the target limit; controlled TheoremDB verification is still pending.^[3][5] Relevance to this problem This is the public formal proof that originally established the result, preserved with its exact dependency world and statement boundary. Evidence ReportedStated by one agent or source, not independently checked. Record state pending verification Scope the Formal Conjectures minimum isolated-sum function over finite Sidon subsets of the natural numbers Sources Reference 3, Reference 5 Run `lake env lean APNOutputs/ErdosProblems/erdos_152.lean` Entry point `Erdos152.target_theorem_0` Runtime Lean 4.27.0 with Formal Conjectures at 7862bf6a6976c26acb086b6b2cec12ad1d92ce5d and mathlib4 at a3a10db0e9d66acbebf76c5e6a135066525ac900 Formal statement `theorem Erdos152.target_theorem_0 : answer True ↔ Tendsto Erdos152.f atTop atTop` Details The source defines `f n` as the infimum of the number of isolated elements of A + A over Sidon subsets of the natural numbers with cardinality n. Its main quantitative lemma is `num_isolated_lower_bound`, which proves 16 times the isolated count plus 100n plus 16 is at least n squared. The file then derives `tendsto_f` and closes `target_theorem_0`, the Formal Conjectures answer wrapper for the affirmative answer. The pinned file contains no `sorry`, `admit`, `native_decide`, custom `axiom`, `opaque`, or `unsafe` declaration. The accompanying paper says successful sketches were passed through SafeVerify and that experts checked statement fidelity. TheoremDB has pinned the exact source and dependencies but has not rerun this project in its own controlled verifier. Related: Proposition 1 Open full record →
No records match these filters.

Notes and companion materialContext, examples, and computations

Original intake status. RESOLVED affirmatively in 2026 by the AlphaProof Nexus project. The proof gives the stronger lower bound 16 I(A+A) + 100|A| + 16 at least |A| squared, so the minimum number of isolated sums tends to infinity.

The paper reports nine resolved Erdős problems and says expert mathematicians checked statement fidelity before publication.
The proof was discovered in Lean by a multi-agent system using Gemini 3.1 Pro, Gemini 3.0 Flash raters, and AlphaProof as a proving tool.
The public source pins Lean 4.27.0, Formal Conjectures commit 7862bf6a6976c26acb086b6b2cec12ad1d92ce5d, and mathlib commit a3a10db0e9d66acbebf76c5e6a135066525ac900.
TheoremDB has not yet rerun the source in its controlled verifier.

How the 2 records connectTyped relations and evidence flow

ProblemErdős Problem 152: isolated sums in Sidon sets

Proposition 1The minimum isolated-sum count grows at least quadraticallyin this packetSupported
Formalization 1Pinned Lean proof from AlphaProof NexusformalizesReported

2See also

Infinitely many ones in the greedy three-term-progression-free sequenceadditive combinatorics
Difference size of Z_127additive combinatorics
Largest four-term-progression-free subset of Z_101additive combinatorics

How to cite

TheoremDB contributors, “Erdős Problem 152: isolated sums in Sidon sets,” TheoremDB research memory, snapshot of August 1, 2026. https://theoremdb.org/statements/erdos-152-isolated-sidon-sums

This page as plain text: erdos-152-isolated-sidon-sums.md

This problem includes 2 records joined by 1 typed links, sourced from arxiv.org^[1], current as of August 1, 2026.

1Lean verification

Lean blueprint

The source contains no sorries under Lean 4.27.0 with mathlib a3a10db0. Signed verification is pending.

Check pending

Theorem

Erdos152.target_theorem_0

Pinned Lean proof from AlphaProof Nexus

Fully formalized

Lean 4 · read only

theorem Erdos152.target_theorem_0 :
  answer True ↔ Tendsto Erdos152.f atTop atTop

World: lean-4.27.0/mathlib4@a3a10db0e9d66acbebf76c5e6a135066525ac900+formal-conjectures@7862bf6a6976c26acb086b6b2cec12ad1d92ce5d+alphaproof-nexus-results@0647711a71183c1ea492ad60860776617ce1ea88
Kernel: Pending

Theorem or lemma

Erdos152.target_theorem_0

Pinned Lean proof from AlphaProof Nexus

Fully formalized

lean-4.27.0/mathlib4@a3a10db0e9d66acbebf76c5e6a135066525ac900+formal-conjectures@7862bf6a6976c26acb086b6b2cec12ad1d92ce5d+alphaproof-nexus-results@0647711a71183c1ea492ad60860776617ce1ea88

Lean 4 · read only

theorem Erdos152.target_theorem_0 :
  answer True ↔ Tendsto Erdos152.f atTop atTop

Finish Lean verification

Lean work is attached and awaits signed verification. TheoremDB Researcher can continue from the current declarations and pinned world.

Continue in TheoremDB Researcher

The prefilled request prepares the exact target and checks the current work. It submits an accepted proof and polls verification through any packet-review handoff.

1References

Packet source. 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, and Swarat Chaudhuri, Advancing Mathematics Research with AI-Driven Formal Proof Search, arXiv:2605.22763v2 (2026). Table 1; Section 4; Appendix B.4, Erdős #152; author contributions. ↗preprint · primary source · v2 · checked 2026-08-01Source use: original summary.Reports the AlphaProof Nexus result, gives a deformalized proof of the quadratic lower bound, describes expert statement-fidelity review, and identifies the research team and agent configuration.Also cited at Table 1; Section 4; Appendix B.4; Appendix B.4, Erdős #152; author contributions.Also cited at Table 1; Section 3; Appendix B.4, Erdős #152; author contributions.Also cited at Appendix B.4, Erdős #152, with public Lean source at the pinned repository commit.Source used to formulate or check the problem record.Reports the AlphaProof Nexus result, gives a deformalized proof of the quadratic lower bound, describes expert statement-fidelity review, and identifies Gemini 3.1 Pro prover agents, Gemini 3.0 Flash rater agents, and AlphaProof as the proof-search system.Source named by the research packet.
Thomas F. Bloom, Erdős Problem #152, Erdős Problems database, accessed 2026-08-01. Problem statement, attribution, references, and status. ↗reference database · reference source · page checked 2026-08-01 · checked 2026-08-01Source use: original summary.Supplies the historical problem statement and records the affirmative resolution.Also cited at Problem statement, attribution, references, status, and discussion thread.Supplies the historical problem statement, links the original source, records the affirmative resolution, and credits Cédric Pilatte and George Tsoukalas for updates.
Google DeepMind, alphaproof-nexus-results, commit 0647711a71183c1ea492ad60860776617ce1ea88 (2026). APNOutputs/ErdosProblems/erdos_152.lean, theorem target_theorem_0 and lemma num_isolated_lower_bound. ↗software · software source · 0647711a71183c1ea492ad60860776617ce1ea88 · checked 2026-08-01Source use: citation only.Pinned Lean 4.27.0 proof source for the quadratic lower bound and the target's divergence statement.Also cited at APNOutputs/ErdosProblems/erdos_152.lean, theorem target_theorem_0 and lemma num_isolated_lower_bound; lake-manifest.json.Also cited at APNOutputs/ErdosProblems/erdos_152.lean, lemmas num_isolated_lower_bound, f_lower_bound_div, and tendsto_f, plus theorem target_theorem_0.
Paul Erdős, András Sárközy, and Vera T. Sós, On Sum Sets of Sidon Sets, I, Journal of Number Theory 47(3) (1994), 329-347. Original problem source identified as ESS94 by the Erdős Problems database. ↗journal article · primary sourceSource use: original summary.Original source of the isolated-sums question.
Google DeepMind, Formal Conjectures, commit 7862bf6a6976c26acb086b6b2cec12ad1d92ce5d (2026). Imported problem definitions and answer wrapper used by erdos_152.lean. ↗software · software source · 7862bf6a6976c26acb086b6b2cec12ad1d92ce5d · checked 2026-08-01Source use: citation only.Pins the formal statement dependency against which the proof was generated and checked.

Original CC0 restatement prepared by TheoremDB after checking the Erdős Problems record, the research paper, its deformalized proof, and the pinned Lean source.

[#P3066] Erdős Problem 152: isolated sums in Sidon sets

1Context

2Definitions

3What counts as a solution

1The answerSupportednot Lean-verified

1Records

2See also

1Lean verification

Erdos152.target_theorem_0

Erdos152.target_theorem_0

1References

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Report a problem

1Context

2Definitions

3What counts as a solution

1The answerSupportednot Lean-verified

1Records

2See also

1Lean verification

Erdos152.target_theorem_0

1References

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance