---

Claim. The module src/latest/ErdosProblems/Erdos1.lean of Boris Alexeev's lean-proofs repository (added 2026-09-15 with its seventeen submodules under Erdos1/, pinned at the commit of the same day) proves Erdos1.erdos_1_quantitative: for every $n\ge2$ there are $N>0$ and a sum-distinct $A\subseteq\{1,\ldots,N\}$ with $|A|=n$ and

$$N<\frac{2^{n+1}}{\log_2 n},$$

and from it Erdos1.erdos_1 (restated as Erdos1.not_erdos_1, the name the repository's comparator challenge checks), the exact negation of the uniform-bound conjecture of Problem 1 as Formal Conjectures first stated it, with the same IsSumDistinctSet predicate; Formal Conjectures now records that negation itself as erdos_1. This answers the question no and, unlike the earlier disproof, gives an explicit bound at every cardinality. The companion module Erdos1b.lean (added the same day) proves Erdos1b.not_erdos_1b: for every $\varepsilon>0$ and all large $n$ there is such a set with

$$N<\Bigl(\bigl(\tfrac94\bigr)^{1/3}+\varepsilon\Bigr)\frac{2^n}{n^{1/3}},$$

a polynomial saving over $2^n$. The site's proof claim, submitted by Boris Alexeev on 2026-09-15 and credited to GPT-6 Astra, describes the ingredients: distinct subset sums restricted to subsets of equal size, a modular trick connecting that to the problem, a recursively defined dyadic graph, and the avoidance of balanced ternary relations in $\{-1,0,1\}^n$; the repository's two PDFs, linked above, are the write-ups, pdf/Erdos1.pdf for the dyadic bound and pdf/Erdos1b.pdf for the cube-root saving. The module's README states that its #print axioms audit of both main theorems returns only propext, Classical.choice and Quot.sound, and that some elementary binary-sum lemmas adapt code from the earlier disproof's repository; the mathematics is a different construction.

Submission note. Posted to erdosproblems.com as a proof claim by GPT-6 Astra (account BorisAlexeev) on 15 September 2026, giving "GPT-6 Astra" as the AI used:

The proof claim posted earlier mentions that GPT-6 Astra found a solution to this problem as part of FrontierMath Erdős. This is an alternate solution, which I believe is simpler and also offers a nice, explicit bound. Here are some of the ingredients: looking at the related problem of distinct subset sums only for subsets of the same size, a modular trick that connects that to the main problem, a "dyadic graph" (pictured in Figure 1), and something about the "balanced" ternary "lattice" {-1,0,1}^n. [Note: at the moment of writing, the Lean formalization link is broken, but it should be fixed somewhat soon.]

Depends on. Nothing in this wiki: the construction is independent of the earlier disproof, which it reproves with an explicit bound.

Acceptance. Formalized. This corpus's verification built the modules ErdosProblems.Erdos1 and ErdosProblems.Erdos1b of src/latest at the pinned commit of 2026-09-15 with the repository's comparator challenges Erdos1 and Erdos1b, and checked the axioms of Erdos1.not_erdos_1, Erdos1.erdos_1_quantitative and Erdos1b.not_erdos_1b, which are exactly propext, Classical.choice and Quot.sound; the challenges pin those three declarations with the predicate Erdos1.IsSumDistinctSet, and the fingerprint of each was found identical to its challenge. The compared statements are the exact negation of the problem's statement, with the hypothesis $N\ne0$ that excludes only the trivial witness $N=0$; the bound $N<2^{n+1}/\log_2n$ at every $n\ge2$; and the cube-root saving with the constant $(9/4)^{1/3}$ for all large $n$. The companion module's other declarations, Erdos1b.erdos_1b and Erdos1b.erdos_1b_asymptotic, have no challenge and are outside the compared statement. Not reviewed: on the claim thread the site's curator welcomed the polynomial saving (2026-09-16) without recording acceptance of this route, the site's label and its credit to GPT-6 Astra date from the earlier claim, and no outside reviewer has published an examination. Not refereed: the write-ups are the repository's two PDFs. The claim is recorded as a second disproof, and the problem's standing is solved through the two accepted full claims.