Erdős Problem #978
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Let `f ∈ ℤ[X]` be an irreducible polynomial with positive leading coefficient. Suppose that the degree `k` of `f` is larger than `2`, is not equal to a power of `2`, and `f n` has no fixed `(k - 1)`-th power divisors other than `1`. Then the set of `n` such that `f n` is `(k - 1)`-th power free has positive density, and this is proved in [Ho67].
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 5 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/978.Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, n⁴+2 is squarefree with positive density; (d−2)-power-free values with the Euler-product density for every d ≥ 4 — read by four AI referee seats here 22 Oct, see /day/978-openai-squarefree-quartics-refereed — family 20 at
github.com/openai/math, OpenAI's own Lean proves Corollary 1.2 — for every f ∈ ℤ[x] irreducible over ℚ of degree d ≥ 4 with ρ_f(p^(d−2)) < p^(d−2) for all p, the (d−2)-power-free values have the Euler-product density c_f > 0 (allDegrees) — for every d, including d ≥ 9 without Browning's theorem. Kernel-replayed on our machine on 22 Oct 2026, after two earlier third-party Comparator replays (cert-machine 10 Oct, with Lean's kernel and nanoda; nealmcb 11 Oct): 63 modules importing only Mathlib, 0 errors, standard axioms, the theorem and its seven definitions matched to the comparator challenge under pp.all. Its route is shorter than the paper's: no archimedean determinant cuts, no quintic deletion, no Appendix A certificate. A kernel-checked bridge of ours proves verbatim copies of Formal Conjectures' erdos_978.parts.ii, parts.iii (n⁴+2) and variants.sub_two (tagged solved there, proofs sorry) and a density form in FC's vocabulary — see our /day entry. This problem is not among the 25 on Bloom's 8 Oct list of the release's Erdős claims; the match to family 20 is our own reading, not Bloom's.
Prizenone
Solution in Leanno
FULL WRITE-UP BY THIS SITE · OCT 22, 2026
Erdős wrote in 1953 that he could not prove n⁴+2 squarefree for infinitely many n, and in 1981 that there was no quartic polynomial about which anyone could. Hooley had the (d−1)-power-free case in 1967; at d−2 the record for general polynomials stopped at degree 9 (Browning 2011; binomials to degree 6). OpenAI's preprint, dated 24 September and public since 6 October, claims the (d−2)-power-free values have the predicted Euler-product density for every irreducible f of degree d ≥ 4 with no fixed prime (d−2)-th-power divisor: n⁴+2 is squarefree for about 75.67% of n. We replayed its Lean (63 modules, Mathlib only) in the kernel: standard axioms, statement and seven definitions matched to the comparator, independently of two earlier third-party replays. The Lean takes a shorter route than the paper (no archimedean determinant cuts, no quintic deletion) and proves degrees ≥ 9 itself, without Browning. Four AI seats read the paper: HOLDS AS READ on everything #978 needs, one fillable gap in a side corollary. Ours: Lean proofs of Formal Conjectures' three #978 statements, tagged solved there but still sorry, counts by two different methods, and a correction to our own July report. The theorem is OpenAI's.
CLOSED