Erdős Problem #131
Erdős problem #131 · erdosproblems.com/131
Let be the maximal size of such that no divides the sum of any nonempty subset of . Estimate . The lower bound is classical, from constructions of Erdős and Csaba, and every non-dividing set is non-averaging, which gave . The claimed new result is the matching upper bound , obtained by running the Pham-Zakharov density-increment argument one dimension lower through a projective normalization, hence .
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Number Theory, Additive Combinatorics
- Posed by
- Paul Erdős
- Year posed
- 1975
- Years open
- 51y
- Solved
- 2026-07-24
- Model
- GPT-5.6 Sol, Claude
- Vendor
- OpenAI, Anthropic
- Collaborators
- —
- Verification
- Lean-verified
- Publication
- Announced
- Significance
- 10 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The new content is the upper bound; the matching N^(1/5) construction is prior work of Erdős and Csaba. erdosproblems.com has not accepted the claim
What the AI did
The paper states that the novel idea - the projective normalization that survives the divisibility constraints and drops the associated convex geometry by one dimension, moving the exponent from 1/4 to 1/5 - was found by GPT-5.6 Sol. The Lean formalization was then completed by a Claude agent loop working autonomously against a human-written route document until the development compiled with no sorry and a clean axiom audit.
Verification
Built and audited by the site on 2026-08-02. A clean clone of the author's Lean 4 development (50 files, 17,408 lines) compiles against the pinned mathlib revision on Lean 4.32.0 with no sorry, admit or native_decide. `#print axioms Nondividing.main_log_limit` returns exactly the eleven whitelisted axioms - propext, Classical.choice, Quot.sound and the eight declared external interfaces - and notably no sorryAx, so no placeholder is load-bearing. Statement fidelity checked against the trusted Challenge.lean: the definitions of non-dividing and F, and the theorem type log F(N)/log N -> 1/5, match. NOT verified: the eight external axioms are assumed rather than proved. Each cites a published result (Schneider, Rogers-Shephard, Betke-Henk-Wills, Pham-Zakharov Lemmas 1, 7 and 13, Conlon-Fox-Pham) but none was checked line by line against its source, and the density-increment exponent in convex_density_set is where the 1/4 to 1/5 improvement lives. erdosproblems.com still lists the problem open with no comments.
Sources
Submitted by Theofil Xeff
Verified before publishing. I installed Lean 4.32.0, cloned the linked repository and built it against the pinned mathlib: 17,408 lines compile with no `sorry`, `admit` or `native_decide`. `#print axioms Nondividing.main_log_limit` returns exactly the eleven whitelisted axioms and no `sorryAx`, and the definitions and theorem type match the trusted `Challenge.lean`, so the formalization proves what it says it proves.
What is still open: the eight external interfaces are assumed rather than proved. They are each cited to published work, but I have not checked them against the sources, and `convex_density_set` carries the exponent the whole 1/4 to 1/5 improvement rests on. The entry is therefore a candidate rather than resolved, and erdosproblems.com has not accepted the claim yet - posting it there would be the natural next step.