Source authenticated

Erdős Problem #1: sum-distinct sets

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$ .

Exact FrontierDelta

disproved→disproved

Scope and record

Occurred: Oct 29, 2026

Delta type: REGISTRY REVISION

Assumptions: VibeMathed verification: lean-verified. Publication: announcement. AI contribution: ai-discovered. VibeMathed editorial classifications, scores, notes, relations, and dataset structure are CC BY 4.0. Source statements and linked content retain their own rights.

Canonical aliases: Erdős Problem #1: sum-distinct sets · Erdős #1: Sum-Distinct Sets · Problem 1

Confidence: Not scored

Registry verification: lean verified · announcement · resolved

Open the source record ↗

Attribution

VibeMathed
registry · event recorded by

Tom Adamczewski
human · human collaborator

GPT-6 Astra (pre-release)
model · ai model contributor · OpenAI

Evidence vector

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review

Named evidence

VibeMathed record: Erdős Problem #1: sum-distinct sets

specialist registry · passed

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.

Source ↗

Solution.lean and the Lean development

lean artifact · passed

lean-proof link supplied by the VibeMathed registry.

Source ↗

Erdős Problem #1: sum-distinct sets

witness · pending

Primary source named by the VibeMathed record. Presence in this import is not an independent mathematical verification.

Source ↗

erdosproblems.com/1: status and Thomas Bloom's proof exposition

specialist registry · pending

problem-record link supplied by the VibeMathed registry.