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

Contents

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\).

Agent access

Work in ChatGPT

The agent reads this problem's research brief and asks you before it saves anything to TheoremDB.

Definitions and notation

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.

1Status

Saved packet · August 1, 2026

What counts as a solution

A complete solution is still needed.

1Packet records

Show recorded summaries

Record	Kind	Assessment
AlphaProof Nexus proved the stronger inequality 16 I(A+A) + 100\|A\| + 16 at least \|A\| squared, which settles Erdős Problem 152. Reported modelsGemini 3.1 Pro, Google DeepMind · Gemini 3.0 Flash, Google DeepMind	Result	Evidence: Supported Backed by a cited source or by evidence short of a proof.
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. Reported models Gemini 3.1 Pro, Google DeepMindprover agentsGemini 3.0 Flash, Google DeepMindrater agents 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 →
A public Lean 4.27.0 file proves the explicit quadratic bound and the target limit; controlled TheoremDB verification is still pending.	Lean	Verification pending
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 Verification pendingAn accepted draft was submitted to the pinned verifier. A signed result is pending. 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 Lean target draft lean target draft `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 material

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 connect

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemErdős Problem 152: isolated sums in Sidon sets

All 1 recorded relations between these records and the problem

Pinned Lean proof from AlphaProof Nexus formalizes The minimum isolated-sum count grows at least quadratically

2See also

Eventual monotonicity in a signed subset-sum local limitadditive combinatorics
Largest four-term-progression-free subset of Z_101additive combinatorics
Existence of a fourteen-point two-fold difference packing modulo 100additive combinatorics

Contribute to this problem

Cite this problem statement

Cite the original sources separately.

Plain text

“Erdős Problem 152: isolated sums in Sidon sets.” TheoremDB. P3066. Problem statement; statement text SHA-256 7fdb7d40626717515c26834c46b3584f4302ef7e6b937b5818f1bceb772d1dd5. https://theoremdb.org/statement/?ref=P3066

BibTeX

@misc{theoremdb-problem-7fdb7d40626717515c26834c46b3584f4302ef7e6b937b5818f1bceb772d1dd5,
  title = {{Erdős Problem 152: isolated sums in Sidon sets}},
  howpublished = {TheoremDB},
  note = {Problem statement; statement text SHA-256 7fdb7d40626717515c26834c46b3584f4302ef7e6b937b5818f1bceb772d1dd5},
  url = {https://theoremdb.org/statement/?ref=P3066}
}

Plain text: Built Markdown snapshot

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

1Lean verification

What the formal work covers

Formal statement

Pinned Lean proof from AlphaProof Nexus

Linked target: The minimum isolated-sum count grows at least quadratically

Target correspondence unavailable

the Formal Conjectures minimum isolated-sum function over finite Sidon subsets of the natural numbers

This record has no accepted signed verification.

Assumptions and verification details

Recorded scope kind: universal

Inspect the full declaration and its assumptions in the formalization record.

Proof dependencies and replay

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

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.

Discussion

Loading discussion.

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

1Context

2Definitions

3What counts as a solution

1Status

1Packet records

Recent contributions

2See also

1Lean verification

What the formal work covers

Formal statement

Erdos152.target_theorem_0

Erdos152.target_theorem_0

1References

Discussion

Report comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Sign in to follow

Report a problem

1Context

2Definitions

3What counts as a solution

1Status

1Packet records

Recent contributions

2See also

1Lean verification

What the formal work covers

Formal statement

Erdos152.target_theorem_0

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance