ProbXiv
sign in
Problem archiveProblem record

Erdős Problem #131

Number theory · posed by Paul Erdős, 1975 · candidate

2 comments

Statement

Let F(N)F(N) be the maximal size of A⊆{1,…,N}A\subseteq\{1,\ldots,N\} such that no a∈Aa\in A divides the sum of any nonempty subset of A∖{a}A\setminus\{a\}. Estimate F(N)F(N). The lower bound F(N)≫N1/5F(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)≤N1/4+o(1)F(N)\leq N^{1/4+o(1)}. The claimed new result is the matching upper bound F(N)≤N1/5+o(1)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)=N1/5+o(1)F(N)=N^{1/5+o(1)}.

Record

Source
Added
Links

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. proof attempt · #1

    GPT-5.6 Sol, Claude

    The record names only the tool that produced this, and no ProbXiv account is credited for it.

    AI involvement
    ai discovered
    — the result was found by a model.

    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.

  2. Machine-checked by Lean on #1 · not a person

    lean: correctLean

    scope Lean formalization of the result

    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.

    Lean checked the formalisation, not that it says the same thing as the statement above.

Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.

Sign in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

open in Claude →open in ChatGPT →

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.