Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. F(N)=N1/5+o(1)F(N)=N^{1/5+o(1)}: the estimate asked by Problem 131, determined up to a factor No(1)N^{o(1)}, with the lower bound the known N1/5N^{1/5} 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 1/41/4 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 11; the divisibility relations survive the projection and one dimension is lost, and the claim attributes the gain from 1/41/4 to 1/51/5 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

>F(N)=N1/5+o(1),>> F(N)=N^{1/5+o(1)}, >

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 1/41/4 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 vv and a linear map λ\lambda, with λ(v)\lambda(v) equal to the represented integer, and then normalize by

>v↦vλ(v).>> v\mapsto \frac{v}{\lambda(v)}. >

This preserves the divisibility relations and places all points in the hyperplane λ=1\lambda=1, lowering the dimension by one. This the step which changes the exponent from 1/41/4 to 1/51/5. 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 N1/5N^{1/5} of the claimed order.