Power-saving bounds for square-difference-free sets
Power-saving bounds for square-difference-free sets are the subject of three manuscripts in OpenAI's public mathematics collection (github.com/openai/math). Write s(N) for the largest size of a set A ⊆ {1, …, N} in which no two elements differ by a nonzero perfect square. Furstenberg and Sárközy independently proved s(N) = o(N), and whether a bound s(N) ≤ CN1−c holds was an open question. The manuscripts claim such a bound, together with extensions to intersective polynomials and to polynomial values at primes. A human paper first posted on the same day as the repository proves a weaker bound by a different method, and its second version comments on the OpenAI draft. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original result
- Claim (squares). There are absolute constants c > 0 and C < ∞ such that every square-difference-free A ⊆ {1, …, N} has |A| ≤ CN1−c, for every N ≥ 1 (Theorem 1.1). The manuscript states that this answers the fixed-power question posed by Green and Sawhney. It also says that the exponent is "extremely small" and that the argument "does not yield a useful numerical value". Source: the manuscript A power saving for square-difference-free sets, dated 24 September 2026. Its outline (§1.2) describes the method: a seminorm built from a reflection-positive probability law over prime fields dominates a fixed power of the density; the seminorm is applied to a signed Fourier lift of A; and a comparison along square-step progressions, together with a signed kernel supported on actual square shifts, makes this quantity decay by a power of N.
- Claim (intersective polynomials). For each degree k ≥ 2 there is ck > 0 such that, if h is an intersective integer polynomial of degree k with positive leading coefficient (one with a root modulo every positive integer), every A ⊆ {1, …, N} whose differences avoid the nonzero values h(1), h(2), … has |A| = Oh(N1−ck). The exponent depends only on the degree. Source: the manuscript A power saving for intersective polynomial differences with an exponent depending only on the degree, dated 5 October 2026.
- Claim (prime arguments). If h has degree at least two, a positive leading coefficient and a unit root modulo every positive integer, then every A ⊆ {1, …, N} whose differences avoid the nonzero values h(p) at primes p has |A| ≤ ChN1−ch. Source: the manuscript A Power Saving for Polynomial Differences at Prime Arguments, dated 5 October 2026. Its prime-distribution input (Theorem 5.1) is the zero-free half-plane ℜs > 7/8 for all Dirichlet L-functions, taken from the companion manuscript in the same collection (see The quasi-Riemann hypothesis).
- Formalization, as described by the repository. The scope note lean/docs/182.md lists only the square-difference manuscript. It states that the formalization proves the fixed power saving for sets with no nonzero square difference, uniformly for every N ≥ 1. The Comparator statement is
SquareDifference.lean. The intersective-polynomial and prime-argument results are not covered by that scope note. - Dates. The manuscripts carry the dates given above. The repository's initial public commit,
adc7f12, which contains all three, is timestamped 6 October 2026, 21:58:50 UTC.
Earlier published results
- Upper bounds. Furstenberg (1977) and Sárközy (1978) independently proved s(N) = o(N). Later bounds of the form N/(log N)c log log log log N (Pintz, Steiger and Szemerédi, 1988) and N/(log N)c log log log N (Bloom and Maynard, Compositio Mathematica) followed. Green and Sawhney (arXiv:2411.17448, New bounds for the Furstenberg–Sárközy theorem) prove s(N) ≪ N exp{−c(log N)1/2} and ask whether a fixed power saving holds. For intersective polynomials of degree at least two, Adajar et al. (arXiv:2605.16216) obtain savings exp{−c(log N)μ} for every fixed μ < 1/2.
- Lower bounds. Ruzsa (1984) constructed square-difference-free sets of size ≫ N0.733077…. Beigel and Gasarch (arXiv:0804.4892) and Lewko (2015) improved the exponent to 0.7334117…, and Krachun (arXiv:2608.01325, Square-Difference-Free Sets beyond the Three-Quarter Barrier) to 0.7527964…. After the release, E. Naslund posted a computer-assisted construction with exponent 0.7580758, formalized in Lean (Hexagon 2610.00151v1, 8 October 2026). That note concerns lower bounds and does not refer to the OpenAI manuscripts.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 15 October 2026) |
|---|---|---|---|---|
| 2026-10-06 (v1), 2026-10-12 (v2) | arXiv:2610.07765 (v1, v2), S. Fan and A. Lott; v1 titled A new bound for the Furstenberg–Sárközy theorem using the van der Corput property, v2 retitled The optimal van der Corput property for squares | Parallel work (weaker bound, different method); remark and critique (v2) | Proves s(N) ≤ N exp{−c(log N log log N)1/2}, improving Green and Sawhney, by constructing nonnegative trigonometric polynomials whose frequencies are squares (a quantitative van der Corput property with signed coefficients). Both versions also prove a matching lower bound for the constant coefficient of every such polynomial; the v2 abstract concludes that "the van der Corput property cannot be used to obtain a power-saving bound". A remark in v2, linking to the repository's initial commit and to its Lean scope note, refers to "a draft claiming the power-saving bound". It states that v1 was submitted to arXiv on 6 October 2026 at 05:02:35 UTC, 16 hours and 56 minutes before the repository's initial commit, describes the draft as appearing "AI-written and largely unreadable", and notes that the repository claims a Lean certificate. The paper also announces a forthcoming power saving for cube differences by the same method. Its AI disclosure states that the authors used a language model during the work and verified the manuscript themselves. | arXiv v2. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "partial", which MathVet defines as "only a special case, or only one of several co-equal headline claims". Its note says that only the square case h(x) = x2 is stated in Lean and that the intersective-polynomial and prime-argument results are not formalized. It records a sandboxed Comparator pass for the challenge SquareDifference (8 October 2026). |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.