Browse › Combinatorics › 182 Power savings for intersective polynomial differences and prime arguments
A power saving for square-difference-free sets
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove that there are absolute constants c > 0 and C < ∞ such that every set $A\subseteq\{1,\ldots,N\}$ with no nonzero square difference satisfies $|A|\le C N^{1-c}$. This answers the fixed-power question posed by Green and Sawhney.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Comments and discussion
- Steve Fan and Andrew Lott, The optimal van der Corput property for squares (arXiv:2610.07765v2, 12 October 2026). An introductory remark says "A prominent AI company has circulated a draft claiming the power-saving bound", calls it "largely unreadable", notes its claimed Lean certificate, and records that their first submission preceded the release's initial repository commit; the paper itself proves an $N\exp(-c\sqrt{\log N\log\log N})$ bound and shows the van der Corput property cannot give a power saving.
Formalization
- OpenAI, Power savings for intersective polynomial differences and prime arguments: Lean scope (OpenAI Math Release, lean/docs/182.md, 6 October 2026). The family scope note states that the formalization proves Theorem 1.1 of this paper, $|A|\le CN^{1-c}$ for square-difference-free $A\subseteq[N]$ with absolute constants, uniformly for all $N\ge1$. [family-level]
- OpenAI math release, SquareDifference.lean (lean/ComparatorChallenges). The comparator statement
OAI.SquareDifference.power_savingthat the scope note links for this theorem.
Possibly relevant literature (found by the agent, not checked)
- Eric Naslund (contributor), Square-difference-free sets of exponent 0.7580758 (Hexagon 2610.00151v1, Oct 2026). Gives a computer-assisted lower-bound construction with exponent $0.7580758\ldots$, above the Krachun exponent the paper cites as the lower end of the remaining gap; the page says the Lean formalization is registered as PALOMAR-2026-09-19-000006. [AI-generated per source]
- Khalid Younis, Sets whose differences avoid a bracket quadratic (arXiv:2608.30078, 30 Aug 2026). Proves a fixed power saving $N^{1-c}$ in a Furstenberg–Sárközy-type problem with a bracket-quadratic difference set, obtained via the van der Corput property.
- Alexandros Kalogirou, Andrew Lott, Ákos Magyar, Akash Singha Roy, The Furstenberg–Sárközy theorem for sums of an even number of odd powers (arXiv:2609.16595, 15 Sep 2026). Proves power-saving bounds for sets whose differences avoid sums of an even number of odd $k$-th powers, a multi-variable relative of the single-square problem treated here.
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 182
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:A-power-saving-for-square-difference-free-sets-September-24-2026,
author = {{OpenAI}},
title = {{A power saving for square-difference-free sets}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/A-power-saving-for-square-difference-free-sets-September-24-2026/paper.pdf}{OAI:A-power-saving-for-square-difference-free-sets-September-24-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/182.md. The Lean statements have not been checked by people against the paper's claims.
Family 182: Power savings for intersective polynomial differences and prime arguments
For every fixed intersective integer polynomial h of degree k ≥ 2 with positive leading coefficient, proves that a subset of $\{1,\ldots,N\}$ avoiding nonzero values $h(1),h(2),\ldots$ as differences has size $O_h(N^{1-c_k})$, with $c_k\gt 0$ depending only on degree. Here intersective means having a root modulo every modulus. For prime arguments, a power saving also holds when h has a unit root modulo every modulus, with exponent allowed to depend on h.
Other papers in this family: