Squarefree quartics and power-free polynomial values

1 paperLean

Proves the squarefree-values conjecture for irreducible integer quartics with no fixed prime-square divisor: squarefree values on positive integers have the predicted positive Euler-product density. More generally, establishes the \((d-2)\)-power-free density for irreducible integer polynomials of degrees four through eight under the necessary local condition; together with Browning's higher-degree theorem, this covers every d ≥ 4.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Squarefree values of quartics and power-free values of polynomials

OpenAI · September 24, 2026

We prove that every irreducible integer quartic with no fixed prime-square divisor takes squarefree values with the predicted positive Euler-product density. More generally, we obtain the corresponding \((d-2)\)-power-free density in degrees \(4\le d\le8\). The proof combines number-field factorization, determinant estimates with adaptive auxiliary primes, and explicit low-degree geometry. Together with Browning's theorem for higher degrees, this gives the \((d-2)\)-power-free density for every d ≥ 4.

Read PDF Download Source

Cite

@misc{OAI:Squarefree-values-of-quartics-and-power-free-values-of-polynomials-September-24-2026,
  author = {{OpenAI}},
  title = {{Squarefree values of quartics and power-free values of polynomials}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Squarefree-values-of-quartics-and-power-free-values-of-polynomials-September-24-2026/manuscript.pdf}{OAI:Squarefree-values-of-quartics-and-power-free-values-of-polynomials-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):

Squarefree values of quartics and power-free values of polynomials

Scope

The formalized result proves positive-density power-free values for every integer polynomial \(f\) irreducible over \(\mathbb Q\) of degree \(d\ge4\). Put \(k=d-2\) and assume no prime \(k\)th power divides every value of \(f\). Then the number of positive integers \(n\le X\) for which \(f(n)\) is \(k\)-free is \(c_fX+o_f(X)\), where \(c_f>0\) is the convergent product of local factors. Negative values are allowed and zero is excluded. No monicity, primitivity, or coefficient-height restriction is imposed.

Comparator links

Result	Comparator statement
Positive density of power-free polynomial values	PowerFreeValues.lean

Scope note on GitHub →