Matching works

1 work

math.CO — Combinatorics

An Upper Bound Exponent of 0.9999873 for Square-Difference-Free Sets

Contributed by Eric Naslund

Let A⊆{1,…,N}A\subseteq\{1,\ldots,N\} contain no two distinct elements whose difference is a nonzero square, and let s(N)s(N) be the largest possible size of such a set. We prove \[ s(N)\le CN^{0.9999873} \] with an absolute constant CC. A recent preprint of OpenAI proves $s(N)\le CN^{1-\eps}$ for some absolute $\eps>0$. Their proof utilizes a certain average of the Fourier transform over (24!)161(24!)^{161} points, and for the parameter choices displayed there we calculate that they obtained $\eps\approx \exp_{10}(-\exp_{10}(\exp_{10}(5782.77)))$, in the sense that $\log_{10}\log_{10}\log_{10}(1/\eps)\approx5782.77$. We follow the same overall strategy, with new work at almost every quantitative step. The largest gain is the use of 7272 slots (positions at which the Fourier transform is evaluated) in place of (24!)161(24!)^{161}: the exponent is roughly a fixed constant divided by the number of slots, so this alone gains many orders of magnitude, but leaves far less room for loss elsewhere. Other savings come from the local construction at each prime. Small primes are handled jointly rather than one by one; and errors are measured in the actual half-distributions of the laws being compared, not bounded term by term against a product model. Where sums over the primes of a block of Weil-type error terms of size O(p−1/2)O(p^{-1/2}) would be too weak, we prove bounds of order O(p−1)O(p^{-1}) for the same error terms using \'etale cohomology over finite fields (Deligne's theorems and Katz--Sarnak monodromy for families of curves), the representation theory of GL2(Fp)\mathrm{GL}_2(\mathbf F_p), exact counts at p≡3(mod4)p\equiv3\pmod4, and a modular evaluation of Ahlgren and Ono. Dependence in our distributions is controlled by the correlation inequalities of Peyre and Kassabov. The remaining finitely many numerical inequalities are verified by exact computer arithmetic, listed in the appendices; all analytic steps are proved in the text. The companion repository \cite{NaslundUpperRepository2026} contains a partial Lean 4 formalization, totaling over 600,000 lines of lean. It establishes s(N)≤CN0.99999s(N)\le C N^{0.99999}, conditional on five named analytic inputs and explicit numerical hypotheses. This formalizes the most critical parts of the proof.

Primarily AI-generated textHuman understanding: some parts
Nov 13, 2026603 pages
PDFView work

Advanced search

Text
Human understanding
Linked formalizations