Lean formalization in OpenAI math repository (Result 020)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Squarefree values of quartics and power-free values of polynomials'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 020). The Lean development was not rebuilt locally.