Power savings for intersective polynomial differences and prime arguments

3 papersLean

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.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 3

A power saving for intersective polynomial differences with an exponent depending only on the degree

OpenAI · October 5, 2026

An integer polynomial is intersective if it has a root modulo every positive integer. For each degree k ≥ 2, we prove that there is an exponent \(c_k\gt 0\) such that every set \(A\subseteq\{1,\ldots,N\}\) whose differences avoid all nonzero values \(h(1),h(2),\ldots\), where h is an intersective polynomial of degree k with positive leading coefficient, satisfies \(|A|=O_h(N^{1-c_k})\). The implied constant may depend on h, but the power-saving exponent depends only on its degree.

Read PDF Download Source

Cite

@misc{OAI:A-power-saving-for-intersective-polynomial-differences-with-an-exponent-depending-only-on-the-degree-October-5-2026,
  author = {{OpenAI}},
  title = {{A power saving for intersective polynomial differences with an exponent depending only on the degree}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-power-saving-for-intersective-polynomial-differences-with-an-exponent-depending-only-on-the-degree-October-5-2026/power-saving-intersective-polynomial-differences.pdf}{OAI:A-power-saving-for-intersective-polynomial-differences-with-an-exponent-depending-only-on-the-degree-October-5-2026}},
  year = {2026}
}

A Power Saving for Polynomial Differences at Prime Arguments

OpenAI · October 5, 2026

Let h be a fixed integer polynomial of degree at least two with positive leading coefficient, having a unit root modulo every positive integer. We prove that any set \(A\subseteq\{1,\ldots,N\}\) whose differences avoid all nonzero values \(h(p)\) at primes satisfies \(|A|\le C_hN^{1-c_h}\), where \(c_h\gt 0\) and \(C_h\ge1\) depend only on h. Thus the local unit-root condition gives a fixed power saving even when polynomial arguments are restricted to primes. The proof uses the companion zero-free half-plane theorem for Dirichlet L-functions to obtain the required prime-distribution estimates.

Read PDF Download Source

Cite

@misc{OAI:A-Power-Saving-for-Polynomial-Differences-at-Prime-Arguments-October-5-2026,
  author = {{OpenAI}},
  title = {{A Power Saving for Polynomial Differences at Prime Arguments}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Power-Saving-for-Polynomial-Differences-at-Prime-Arguments-October-5-2026/prime-argument-polynomial-differences.pdf}{OAI:A-Power-Saving-for-Polynomial-Differences-at-Prime-Arguments-October-5-2026}},
  year = {2026}
}

A power saving for square-difference-free sets

OpenAI · September 24, 2026

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.

Read PDF Download Source

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}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

A power saving for square-difference-free sets

Scope

The formalization proves a fixed power saving for sets with no nonzero square difference. There are absolute constants \(c>0\) and \(C\) such that every \(A\subseteq\{1,\ldots,N\}\) satisfying \(a-b\ne m^2\) for all \(a,b\in A\) and integers \(m\ge1\) has \(|A|\le C N^{1-c}\). The bound is uniform for every integer \(N\ge1\).

Comparator links

Result	Comparator statement
Power saving for square-difference-free sets	SquareDifference.lean

Scope note on GitHub →