Squarefree values of quartics and power-free values of polynomials

For an integer k ≥ 2, an integer is k-power-free if no kth power of a prime divides it. Erdős asked whether an irreducible integer polynomial of degree d takes infinitely many (d − 2)-power-free values, and in particular whether n⁴ + 2 is squarefree for infinitely many n (Erdős problem 978). A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims that, when no prime (d − 2)th power divides every value, such values have the predicted positive density for every degree d ≥ 4. It proves the degrees 4 ≤ d ≤ 8 and cites Browning's theorem for higher degrees. This page summarizes the published claim 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.

Background

• As recounted in the introduction of the manuscript:
  • Ricci obtained the asymptotic count of k-power-free values for k ≥ d. For d ≥ 3, Erdős proved that there are infinitely many (d − 1)-power-free values, and Hooley obtained the corresponding asymptotic. Erdős singled out the squarefreeness of n⁴ + 2 in 1953 and returned to it in his 1965 survey as an example of the obstacle at exponent d − 2.
  • Nair's 1976 bound reaches exponent d − 2 for d ≥ 24. Heath-Brown's determinant method gave the range k ≥ (3d + 2)/4, which reaches d − 2 for d ≥ 10, and Browning, combining it with Salberger's global determinant estimates, obtained k ≥ (3d + 1)/4, which reaches d ≥ 9. Heath-Brown also treated irreducible binomials x^d + c for k ≥ (5d + 3)/9, and Reuss obtained a power-saving error term at exponent d − 1. Granville showed that the abc conjecture implies the predicted density of squarefree values.
  • The manuscript cites two earlier preprint claims and does not use either as an input: N. A. Carella's (arXiv 2310.16952v1), for n⁴ + 1 and n⁴ + 2, and S. R. Zapata Ceballos and F. Jalalvand's (arXiv 2608.10335v1), for monic irreducible polynomials of degree 2q whose root field contains a Galois subfield of prime degree q, a class that includes n⁴ + 1.
• Version 2 of the latter preprint (arXiv 2608.10335v2, 15 October 2026) carries the authors' comment that the proof of its Proposition 2.3 is incomplete, that the claimed squarefreeness result is therefore not established, and that they do not currently know how to complete the proof.
• The erdosproblems.com page for problem 978 records Heath-Brown's result for d ≥ 10 and Browning's for d ≥ 9. It notes that the absence of a fixed prime (d − 2)th-power divisor, which Erdős did not state, is a necessary condition. A comment of 31 March 2026 in its forum thread reports that the DeepMind prover agent formally verified an explicit degree-six counterexample to the question without that condition.

The original result

• Squarefree values of quartics and power-free values of polynomials (24 September 2026). Write ρ_f(q) for the number of roots of f modulo q. Theorem 1.1 of the manuscript states: let f ∈ Z[x] be irreducible over Q of degree d with 4 ≤ d ≤ 8, put k = d − 2, and suppose that ρ_f(p^k) < p^k for every prime p. Then the number of 1 ≤ n ≤ X with f(n) k-power-free is c_f,kX + o_f(X), where c_f,k = ∏_p (1 − ρ_f(p^k)/p^k) > 0. No primitivity or sign condition on the leading coefficient is required, and the error term is not claimed to be uniform in f.
  • In particular x⁴ + 2 and x⁴ + 1 take squarefree values with positive density. Corollary 1.2 extends the statement to every d ≥ 4 through Browning's theorem, in the formulation of Xiao. Corollary 1.3 gives the corresponding density for separable products, and for simultaneous values of a fixed family of polynomials, whose irreducible factors have degree at most k + 2.
  • Method, as described: the proof combines number-field factorization with approximating determinants, following the framework of Reuss. It adds a uniform affine counting theorem with adaptive auxiliary primes, bihomogeneous determinant cuts, explicit weighted Hilbert calculations, additional surface and curve geometry for quartics, and an exact finite parameter certificate (Appendix A). Section 12 works through the cyclotomic quartic x⁴ + 1.
• Source. Commit 1581d4c of the openai/math repository, folder Squarefree values of quartics and power-free values of polynomials.
• Formalization, as described by the repository. The scope note lean/docs/020.md states that the formalization proves the positive density of (d − 2)-power-free values for every integer polynomial irreducible over Q of degree d ≥ 4 with no fixed prime (d − 2)th-power divisor, with the convergent product of local factors as the constant. Negative values are allowed and zero is excluded; no monicity, primitivity or coefficient-height restriction is imposed. The Comparator challenge is PowerFreeValues.lean.
• Catalogue status. Google DeepMind's Formal Conjectures project marks erdos_978.parts.ii and erdos_978.parts.iii (the case n⁴ + 2) in FormalConjectures/ErdosProblems/978.lean as "research solved", with formal_proof links to the openai/math repository. Its docstring notes that the linked proof gives positive density and needs neither the condition d ≠ 2^l nor a positive leading coefficient. The Justin Sun Prize record on GitHub lists the problem as entry JSP-000811, with status "Solved" (independent mathematical review pending) and a Lean proof "reported complete; independent verification pending". Both were checked on 26 October 2026, at commits 49ba26b and c06d67a.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 26 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit 899d421, 25 October 2026)	Review (fidelity of the formal statements)	Rates this family "full" and records a sandboxed Comparator pass for the challenge PowerFreeValues (8 October 2026). Its note says that the Lean statement covers every degree d ≥ 4, which is stronger than the new range 4 ≤ d ≤ 8 alone.	Repository.
2026-10-10	cert-machine, openai/math lane K, run 38019899278 (PowerFreeValues)	Verification (kernel replay)	Records that Lean's default kernel and the nanoda kernel both accept the solution.	Repository.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all 416 Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (failures, time-outs and memory overruns) does not list PowerFreeValues, so the challenge is among the 401 accepted by both con-leche and Lean's official kernel.	Development journal.
2026-10-11	nealmcb/openai-math-lean-tooling (GitHub; Comparator results at commit c9570a8)	Verification (Comparator replay)	Its Comparator run over the collection's 416 challenge configurations records PowerFreeValues as accepted on 11 October 2026, without the nanoda kernel.	Repository.
2026-10-11	Formal Conjectures pull request #6898	Catalogue (formal statement)	Marks parts (ii) and (iii) of Erdős problem 978 as "research solved" and links the Lean proof in the openai/math repository.	Merged.
2026-10-22	Erdős Problem a Day, entry for Erdős Problem #978 and verification bundle 978/openai-squarefree-quartics-refereed in pw/erdosproblemaday-verification	Review (AI-assisted audit)	Two mathematical referee seats and a Lean seat report that the manuscript holds as read in their scopes. A literature seat reports a minor, fillable gap in the proof of Corollary 1.3 in the case of factors of degree k + 1, where a cited argument written for monic polynomials is applied without the reduction from the non-monic case, and states that this does not affect Theorem 1.1, Corollary 1.2 or Erdős problem 978. The site replayed OpenAI's Lean (63 modules; leanchecker --fresh passed) and derived Formal Conjectures' statements for problem 978 from it. Its computations give the densities 0.756684… for n4 + 2 and 0.980817… for n4 + 1, and counts of 756,674 and 980,831 squarefree values for n ≤ 106.	Machine refereeing, replay and computation by the site; the bundle credits the earlier Comparator replays by cert-machine and nealmcb and lists Claude Opus 5.5 for all of its seats. The site is built by Patrick White, and Claude, an AI made by Anthropic, does its checking; its verdicts are labelled as the site's own. The bundle repository was published on 25 October 2026.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.