Erdős Problem #1: sum-distinct sets

Erdős problem #1 · erdosproblems.com/1

A finite set $A\subseteq\{1,\dots,N\}$ is sum-distinct if all subset sums $\sum_{a\in S} a,\qquad S\subseteq A,$ are distinct. Erdős asked whether there is an absolute constant $C>0$ such that every sum-distinct set $A\subseteq\{1,\dots,N\}$ satisfies $N>C\,2^{|A|}.$ The conjecture is false: for every $\varepsilon>0$ there are arbitrarily large $n$ and sum-distinct sets $A\subseteq\{1,\dots,N\}$ with $|A|=n,\qquad N\le \varepsilon 2^n.$

Result: Disproved(see note)
Status: Resolved
AI contribution: AI-discovered
Method: Argument
Field: Additive combinatorics
Posed by: Paul Erdős
Year posed: 1931
Years open: 95y
Solved: 2026-08-28
Model: GPT-6 Astra (pre-release)
Vendor: OpenAI
Collaborators: Tom Adamczewski
Verification: Lean-verified
Publication: Announced
Significance: 50 / 100
Disclosed cost: $405
Wikipedia: No dedicated article

What was actually shown

The formal theorem proves that no universal constant $C>0$ can satisfy $N>C\,2^{|A|}$ for every nonempty interval bound $N$ and every sum-distinct $A\subseteq\{1,\dots,N\}$ .

Equivalently, for every $\varepsilon>0$ there are arbitrarily large $n$ and sum-distinct $n$ -element sets contained in $\{1,\dots,N\}$ with $N\le\varepsilon 2^n.$
The proof is ineffective: it establishes the existence of arbitrarily large such $n$ but gives no explicit bound for how large $n$ must be in terms of $\varepsilon$ .

What the AI did

A pre-release GPT-6 Astra autonomously solved the Formal Conjectures benchmark statement with no human steering during proof search. The primary run constructs, for large $n$ , rational $n\times n$ matrices with small determinant and additional admissibility properties, then uses integral changes of basis, saturated bidiagonal perturbations, and a binary-block construction to obtain sum-distinct sets with $N\le\varepsilon 2^n$ . An independent larger-budget Astra run found an essentially equivalent lattice-based argument. Astra also wrote the Lean proofs; Claude was later used to prepare repository documentation from the completed runs.

Verification

Lean-verified. Checked here on 6 September 2026 from a clone of tadamcz/erdos1 at db6f909: 4,608 lines of Lean, zero sorry outside the statement stubs, zero axiom declarations, no native_decide, unsafe or implemented_by; Comparator configuration present and CI runs it with only propext, Quot.sound and Classical.choice. The statement is copied verbatim from Formal Conjectures' ErdosProblems/1.lean at commit 488aade2, the human-curated formalization the model was given, and the proved theorem is its negation. Two independent runs found essentially equivalent lattice-based arguments. The proof is ineffective: it gives no bound on how large n must be. erdosproblems.com, the field's own record, marks the problem DISPROVED (LEAN) with a proof exposition by Thomas Bloom, which is why this is Resolved rather than Candidate: the canonical tracker has accepted it.

Sources

Lean proofSolution.lean and the Lean development
Lean statementChallenge.lean: the compared statement
CodeGithub
AnnouncementEpoch AI, Announcing FrontierMath Erdős (1 September 2026)
Problem recorderdosproblems.com/1: status and Thomas Bloom's proof exposition

Submitted by VibeGene on 06 Sep 2026

Erdős Problem #1: sum-distinct sets

What was actually shown

What the AI did

Verification

Sources

Discussion