View source for Squarefree values of quartics and power-free values of polynomials

For an integer ''k'' ≥ 2, an integer is '''''k''-power-free''' if no ''k''th 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''<sup>4</sup> + 2 is squarefree for infinitely many ''n'' (Erdős problem 978). A manuscript dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math 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''<sup>4</sup> + 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'' ≥ (3''d'' + 2)/4, which reaches ''d'' − 2 for ''d'' ≥ 10, and Browning, combining it with Salberger's global determinant estimates, obtained ''k'' ≥ (3''d'' + 1)/4, which reaches ''d'' ≥ 9. Heath-Brown also treated irreducible binomials ''x''<sup>''d''</sup> + ''c'' for ''k'' ≥ (5''d'' + 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 ([https://arxiv.org/abs/2310.16952v1 arXiv 2310.16952v1]), for ''n''<sup>4</sup> + 1 and ''n''<sup>4</sup> + 2, and S. R. Zapata Ceballos and F. Jalalvand's (arXiv 2608.10335v1), for monic irreducible polynomials of degree 2''q'' whose root field contains a Galois subfield of prime degree ''q'', a class that includes ''n''<sup>4</sup> + 1.
* Version 2 of the latter preprint ([https://arxiv.org/abs/2608.10335v2 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 [https://www.erdosproblems.com/978 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 [https://www.erdosproblems.com/forum/thread/978 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 ρ<sub>''f''</sub>(''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 ρ<sub>''f''</sub>(''p''<sup>''k''</sup>) < ''p''<sup>''k''</sup> for every prime ''p''. Then the number of 1 ≤ ''n'' ≤ ''X'' with ''f''(''n'') ''k''-power-free is ''c''<sub>''f'',''k''</sub>''X'' + ''o''<sub>''f''</sub>(''X''), where ''c''<sub>''f'',''k''</sub> = ∏<sub>''p''</sub> (1 − ρ<sub>''f''</sub>(''p''<sup>''k''</sup>)/''p''<sup>''k''</sup>) > 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''<sup>4</sup> + 2 and ''x''<sup>4</sup> + 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''<sup>4</sup> + 1.
* '''Source.''' Commit <code>1581d4c</code> of the openai/math repository, folder [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Squarefree-values-of-quartics-and-power-free-values-of-polynomials-September-24-2026 Squarefree values of quartics and power-free values of polynomials].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/020.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/PowerFreeValues.lean PowerFreeValues.lean].
* '''Catalogue status.''' Google DeepMind's Formal Conjectures project marks <code>erdos_978.parts.ii</code> and <code>erdos_978.parts.iii</code> (the case ''n''<sup>4</sup> + 2) in [https://github.com/google-deepmind/formal-conjectures/blob/49ba26bac3212084999860c575fcc70af42b3128/FormalConjectures/ErdosProblems/978.lean FormalConjectures/ErdosProblems/978.lean] as "research solved", with <code>formal_proof</code> links to the openai/math repository. Its docstring notes that the linked proof gives positive density and needs neither the condition ''d'' ≠ 2<sup>''l''</sup> nor a positive leading coefficient. The Justin Sun Prize record on GitHub lists the problem as entry [https://github.com/TheJustinSunPrize/awards/blob/c06d67a66a8ba426c68e475eff22ee98a86f4e75/problems/catalog-0801-0900.md#JSP-000811 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 <code>49ba26b</code> and <code>c06d67a</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 26 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, [https://github.com/mathvet/mathvet/blob/899d421729f1e4c5f08d302773762b141c52b845/reviews/openai-math/fidelity-table.csv tables] at repository commit <code>899d421</code>, 25 October 2026) || Review (fidelity of the formal statements) || Rates this family "full" and records a sandboxed Comparator pass for the challenge <code>PowerFreeValues</code> (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 || [https://github.com/carlostoledo1891/cert-machine/blob/4e9beba0ca689365e70fcd01303775f21a687540/corpus/openai-math/kernel-runs/38019899278/PowerFreeValues.json cert-machine], openai/math lane K, run 38019899278 (<code>PowerFreeValues</code>) || 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all 416 Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (failures, time-outs and memory overruns) does not list <code>PowerFreeValues</code>, so the challenge is among the 401 accepted by both con-leche and Lean's official kernel. || Development journal.
|-
| 2026-10-11 || [https://github.com/nealmcb/openai-math-lean-tooling/blob/c9570a82f79b78a1a969a6316ac0fdd69aabef55/results/cmp-all/all.jsonl nealmcb/openai-math-lean-tooling] (GitHub; Comparator results at commit <code>c9570a8</code>) || Verification (Comparator replay) || Its Comparator run over the collection's 416 challenge configurations records <code>PowerFreeValues</code> as accepted on 11 October 2026, without the nanoda kernel. || Repository.
|-
| 2026-10-11 || [https://github.com/google-deepmind/formal-conjectures/pull/6898 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, [https://erdosproblemaday.com/day/978-openai-squarefree-quartics-refereed entry for Erdős Problem #978] and verification bundle [https://github.com/pw/erdosproblemaday-verification/tree/fc14c82ce5ab736fefe3cb6c79bebc54cde77e1c/978/openai-squarefree-quartics-refereed <code>978/openai-squarefree-quartics-refereed</code>] in [https://github.com/pw/erdosproblemaday-verification 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; <code>leanchecker --fresh</code> passed) and derived Formal Conjectures' statements for problem 978 from it. Its computations give the densities 0.756684… for ''n''<sup>4</sup> + 2 and 0.980817… for ''n''<sup>4</sup> + 1, and counts of 756,674 and 980,831 squarefree values for ''n'' ≤ 10<sup>6</sup>.
| 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.

[[Category:OpenAI results]]