Erdős’s "first serious problem" disproved
On 3 September 2026 Epoch AI published a Lean disproof of Erdős problem 1 (1931): sets of n integers with all subset sums distinct can fit in {1, …, N} with N below any fixed fraction of 2^n. It was found by a pre-release GPT-6 Astra in the FrontierMath Erdős runs. Lean checked it; by the paper’s own account people have not yet "digested" the argument.
Why it matters
Erdős called this problem "perhaps my first serious problem", and the Epoch paper takes it to be probably his longest-standing open problem. The bound 2^n/√n from below had stood since Erdős and Moser, and the best earlier example had N ≤ 0.22002·2^n. This is the state "checked formally, not yet worked through by people", which differs from the state of the Erdős–Sós conjecture, which people have already re-expounded.
State of the claim. Claimed: the article by Adamczewski and Bloom (arXiv 2609.25050, 6 September), appendix B.1, and the repository github.com/tadamcz/erdos1, created 3 September 21:48 UTC. Formalised in Lean: by the README, the disproof was found "autonomously" by a pre-release GPT-6 Astra; the primary attempt is the default configuration, 28 August (benchmark run), $405, 27.1 hours; a second, different one is a ReAct agent with a larger budget, 26 August, $1,384, 84 hours; Comparator accepts a disproof only with the identical statement and only the three standard axioms. The pass did not build the repository. Checked by people: the article says the formalisation gives confidence that the proofs are correct, but they "have not yet been properly digested", and the informal expositions on erdosproblems.com are "placeholders" until human experts write a traditional paper. Bloom (the second author) reinterpreted the argument in terms of lattices; his sketch on the problem page was not read (on 10 October the page for problem 1 gives only the statement). Content. A finite set A of natural numbers is "dissociated" if all subset sums are distinct. Erdős asked whether N ≫ 2^n always holds when A ⊆ {1, …, N} has n elements; the example {1, 2, 4, …, 2^(n−1)} shows N ≤ 2^(n−1) is possible. Theorem 1 of the article: for any ε > 0 there are arbitrarily large n and dissociated sets of size n with N ≤ ε·2^n. The argument is ineffective (it does not say how large n must be). The repository README adds that the problem site lists a $500 prize; the article does not say so. What the record does not claim: that a person has checked the argument, or that the pass built the proof.