math.CO — Combinatorics
An Upper Bound Exponent of 0.9999873 for Square-Difference-Free Sets
Let contain no two distinct elements whose difference is a nonzero square, and let be the largest possible size of such a set. We prove \[ s(N)\le CN^{0.9999873} \] with an absolute constant . 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 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 slots (positions at which the Fourier transform is evaluated) in place of : 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 would be too weak, we prove bounds of order 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 , exact counts at , 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 , conditional on five named analytic inputs and explicit numerical hypotheses. This formalizes the most critical parts of the proof.