Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. : the estimate asked by
Problem 131, determined up to
a factor , with the lower bound the known construction
and the upper bound new. Submitted to the site's proof-claim tab on 24 July
2026 as a full claim by Theofil Xeff (the site account fefemath); the tab
states that GPT 5.6 Sol did all the mathematics and Fable 5 the Lean 4
formalization, after earlier attempts with other models had failed. The
method, in outline: the claim adapts the Pham--Zakharov density increment,
which yields the exponent for non-averaging sets, to the divisibility
condition itself. Divisibility is not preserved by translation, so the
argument represents the integers by lattice points carrying a linear form
that returns the represented integer and projectivizes them onto the
hyperplane where that form equals ; the divisibility relations survive
the projection and one dimension is lost, and the claim attributes the gain
from to to that lost dimension. The write-up is a PDF served
from the claimant's GitHub page; the preprint link pins the copy
committed at 13:49 UTC on 24 July 2026, the one current at the submission
time the tab records (14:01). The author replaced the PDF twice later that
day (19:36 and 20:02 UTC), after the comment of 15:23 on its length
(below), and again on 10 August 2026, so the page's unpinned address
serves a later revision. The repository is linked at its head commit of 24
July 2026. This page rests on the tab's summary and the postings' records,
not on a reading of the write-up or the Lean development.
Submission note. Posted to erdosproblems.com as a proof claim by Theofil Xeff (account fefemath) on 24 July 2026, giving "GPT 5.6 Sol, Fable 5" as the AI used:
We prove that
matching the lower bound from constructions of Erdős. We start with the [PhZa24] density-increment proof for non-averaging sets, which gives only the exponent if used as such. To improve this, one has to use the full divisibility condition, but this creates a problem: divisibility is not preserved by translation. The new idea, found by GPT-5.6 Sol, is to represent the integers by lattice points and a linear map , with equal to the represented integer, and then normalize by
This preserves the divisibility relations and places all points in the hyperplane , lowering the dimension by one. This the step which changes the exponent from to . Notes: GPT 5.6 Sol did all the math and Fable 5 the Lean 4 formalization. I have been trying to solve this problem through prompting LLM models since quite some time already, using various models, but without success. Until recently when GPT 5.6 Sol came with this approach (that none other model had tried before).
Standing. Claimed. The site's label is OPEN and its commentary, last edited 30 September 2025, predates the claim and does not mention it. The claim's five comments, of 24 and 25 July 2026: a request to state the roles of the claimant and the models, answered as above; a remark that the manuscript largely repeats the Pham--Zakharov paper apart from parts of its Sections 5 and 6, after which the claimant shortened it; and a comment that repeating proofs with attribution is acceptable. No comment examines the new step. No refereed version, curator acceptance or outside review was found on 2026-10-07, and the Lean development was not built in this corpus. As a pending full claim it sets the problem's standing to claimed, which certifies nothing.
Depends on. the 1999 bounds, for the lower half of the claimed order.