# P3066: Erdős Problem 152: isolated sums in Sidon sets - ID: `P3066` - Reference: `erdos-152-isolated-sidon-sums` - Page: https://theoremdb.org/statements/P3066 - Record maturity: Reviewed problem with recorded work ## 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\). ### Context 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. ### Definitions - **Definition (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. ### What 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. ## The answer AlphaProof Nexus proved the stronger inequality 16 I(A+A) + 100|A| + 16 at least |A| squared, which settles Erdős Problem 152. [1](#reference-1) [2](#reference-2) **Review status:** Supported. **Lean verification:** not Lean-verified. ### 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. ## Work ### Proof and evidence for the resolution **Proposition 1 (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. 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. ### Background and intake notes - 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. ### Formalizations - **Formalization 1** (reported): A public Lean 4.27.0 file proves the explicit quadratic bound and the target limit; controlled TheoremDB verification is still pending. [3](#reference-3) [5](#reference-5) ### Working on this Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `erdos-152-isolated-sidon-sums`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome. ## Lean verification 1 declaration, with 0 open proof obligations. ### Erdos152.target_theorem_0 - State: source contains no sorry; verification pending - Role: target declaration - Lean world: `lean-4.27.0/mathlib4@a3a10db0e9d66acbebf76c5e6a135066525ac900+formal-conjectures@7862bf6a6976c26acb086b6b2cec12ad1d92ce5d+alphaproof-nexus-results@0647711a71183c1ea492ad60860776617ce1ea88` ```lean theorem Erdos152.target_theorem_0 : answer True ↔ Tendsto Erdos152.f atTop atTop ``` ### Continue Lean verification Lean work is attached and awaits signed verification. TheoremDB Researcher can continue from the current declarations and pinned world. [Continue Lean verification with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20erdos-152-isolated-sidon-sums%0A%0AExact%20title%3A%20Erd%C5%91s%20Problem%20152%3A%20isolated%20sums%20in%20Sidon%20sets%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Ferdos-152-isolated-sidon-sums%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.). ## References 1. 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 https://arxiv.org/abs/2605.22763v2 - 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 - preprint; primary source; v2; checked 2026-08-01 - Source 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. - 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. 2. Thomas F. Bloom, Erdős Problem #152, Erdős Problems database, accessed 2026-08-01. Problem statement, attribution, references, and status https://www.erdosproblems.com/152 - Also cited at Problem statement, attribution, references, status, and discussion thread - reference_database; reference source; page checked 2026-08-01; checked 2026-08-01 - Source use: original_summary - Supplies the historical problem statement and records the affirmative resolution. - Supplies the historical problem statement, links the original source, records the affirmative resolution, and credits Cédric Pilatte and George Tsoukalas for updates. 3. Google DeepMind, alphaproof-nexus-results, commit 0647711a71183c1ea492ad60860776617ce1ea88 (2026). APNOutputs/ErdosProblems/erdos_152.lean, theorem target_theorem_0 and lemma num_isolated_lower_bound https://github.com/google-deepmind/alphaproof-nexus-results/tree/0647711a71183c1ea492ad60860776617ce1ea88 - 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 - software; software source; 0647711a71183c1ea492ad60860776617ce1ea88; checked 2026-08-01 - Source use: citation_only - Pinned Lean 4.27.0 proof source for the quadratic lower bound and the target's divergence statement. 4. 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 https://doi.org/10.1006/jnth.1994.1040 - journal_article; primary source - Source use: original_summary - Original source of the isolated-sums question. 5. Google DeepMind, Formal Conjectures, commit 7862bf6a6976c26acb086b6b2cec12ad1d92ce5d (2026). Imported problem definitions and answer wrapper used by erdos_152.lean https://github.com/google-deepmind/formal-conjectures/tree/7862bf6a6976c26acb086b6b2cec12ad1d92ce5d - software; software source; 7862bf6a6976c26acb086b6b2cec12ad1d92ce5d; checked 2026-08-01 - Source use: citation_only - Pins the formal statement dependency against which the proof was generated and checked.