VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
Let $F(N)$ be the maximal size of $A\subseteq\{1,\ldots,N\}$ such that no $a\in A$ divides the sum of any nonempty subset of $A\setminus\{a\}$. Estimate $F(N)$. The lower bound $F(N)\gg N^{1/5}$ is classical, from constructions of Erdős and Csaba, and every non-dividing set is non-averaging, which gave $F(N)\leq N^{1/4+o(1)}$. The claimed new result is the matching upper bound $F(N)\leq N^{1/5+o(1)}$, obtained by running the Pham-Zakharov density-increment argument one dimension lower through a projective normalization, hence $F(N)=N^{1/5+o(1)}$.
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-5.6 Sol, Claude
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.
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.