Erdős–Sárközy question

For a finite set $A\subseteq\mathbb{Z}_{>0}$ , define its subset-sum set by $H(A)=\left\{\sum_{a\in B}a:B\subseteq A\right\}$ . Let $g_3(n)$ be the least integer $N$ such that there exists an $n$ -element set $A\subseteq\{1,\ldots,N\}$ for which $H(A)$ contains no nonconstant three-term arithmetic progression; equivalently, there are no distinct $x,y,z\in H(A)$ with $x+z=2y$ . The Erdős–Sárközy question asks whether $g_3(n)\gg 3^n$ , that is, whether there exists a constant $c>0$ such that $g_3(n)\ge c3^n$ for all sufficiently large $n$ .

References

Primary source

Zenodo (CERN European Organization for Nuclear Research)

Additional references

A negative answer to the Erdős–Sárközy question — Zenodo (CERN European Organization for Nuclear Research) — Simone Costa
A negative answer to the Erdős–Sárközy question — Zenodo (CERN European Organization for Nuclear Research) — Simone Costa

additive-combinatorics number-theory

Posted 1 month ago

Progress summary

Refreshed 4 weeks ago

Claimed solved

A September 2026 deposit claims the conjecture is false, but no independent verification has established that claim.

Erdős and Sárközy posed the question in 1970: whether $g_3(n)\gg 3^n$ . On September 5, 2026, Simone Costa deposited records claiming a negative answer, but the available records do not expose an assessable argument.

Known results

Erdős and Sárközy proved $g_3(n)\gg 3^n/n^{O(1)}$ .
The construction $A=\{1,3,\ldots,3^{n-1}\}$ gives $g_3(n)\le 3^{n-1}$ .
A June 2026 paper proves $g_3(n)\ge (T_n-1)/2+\sum_{j=0}^{n-1}T_j$ , hence $g_3(n)\ge (\sqrt{3}/(2\sqrt{\pi})+o(1))3^n/\sqrt n$ ; the target $g_3(n)\gg 3^n$ remains open.

Community submission (unverified)

A submission dated September 8, 2026 argues that the official formalization marks the principal theorem as open, while a weaker theorem proves only a lower bound of order $2^n/n$ for sum-distinct sets; it does not claim to resolve the Erdős–Sárközy question.

Current status (as of September 2026): The claimed negative answer is unverified; the established lower bound remains below $3^n$ by a factor of order $n\sqrt n$ , and whether $g_3(n)\gg 3^n$ remains open.

Sources

ProofErdős Problem 1: Distinct Subset Sums Mathematical Analysis and Lean 4 FormalizationSee full solutionHide full solution

We study the Lean 4 formalization of Erdős Problem 1, the distinct subset sums problem. The principal Erdős conjecture remains open in the formal-conjectures development considered here. The formalization nevertheless contains an important elementary theorem, erdos_1.variants.weaker, establishing a lower bound of order 2^n/n for a sum-distinct set of cardinality n. We give the mathematical pigeonhole argument, explain the Lean representation of sum-distinctness, describe the principal Mathlib constructions used in the proof, and distinguish formally verified results from conjectural or externally reported claims. The manuscript is designed as a reproducible bridge between the paper proof and its machine-checkable implementation.

Erdos_Sarkozy_Subset_Sum_Manuscript.pdf338,553 bytesOpen
Erdos_Problem_1_Manuscript_Lean4_Draft.pdf305,589 bytesOpen
Erdos.pdf5,768,948 bytesOpen
Erdos_Sarkozy_Multiscale_Rigidity_Stage_II.pdf376,362 bytesOpen
Erdos_Problem_1_Final_Manuscript.pdf368,461 bytesOpen

ProofErdős Problem 1 Source-Verified Lean 4 Proof of the Weaker BoundSee full solutionHide full solution

This revision uses the current official FormalConjectures/ErdosProblems/1.lean source. The source marks the principal theorem erdos_1 as research open and leaves it with sorry. The theorem erdos_1.variants.weaker is marked textbook and contains a complete proof.

The source currently displayed on GitHub has 172 lines. The weaker theorem begins at source line 615; its proof begins at line 618 and ends at line 649. The source describes the result as the trivial lower bound N ≫ 2^n/n.

Erdos_Problem_1_Publication_Manuscript_V4_Source_Corrected.pdf447,488 bytesOpen
Erdos_Problem_1_Final_Manuscript_V2_Source_Verified.pdf327,182 bytesOpen
Erdos_Problem_1_Publication_Manuscript_V3.pdf395,132 bytesOpen
Erdos_Problem_1_Publication_Manuscript_V5_Final.pdf382,113 bytesOpen