VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
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.
$$
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
GPT-6 Astra (pre-release)
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.
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.
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$.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.