---

Claim. Let $f\in\mathbb{Z}[x]$ be irreducible over $\mathbb{Q}$ of degree $k\geq 4$ and suppose that for every prime $p$ some value $f(n)$ is not divisible by $p^{k-2}$. Then the integers $n\geq 1$ for which $f(n)$ is $(k-2)$-power-free have natural density

$$c_{f,k-2}=\prod_p\left(1-\frac{\rho_f(p^{k-2})}{p^{k-2}}\right)>0,$$

where $\rho_f(q)$ counts the residues $a$ modulo $q$ with $f(a)\equiv 0 \pmod q$; the count of such $n\leq X$ is $c_{f,k-2}X+o_f(X)$. This is Corollary 1.2 of the release manuscript Squarefree values of quartics and power-free values of polynomials (OpenAI, 2026-09-24, 55 pages), carded as OpenAI 2026 with the result pages Theorem 1.1 and Corollary 1.2. The manuscript proves the new cases $4\leq k\leq 8$ as its Theorem 1.1 and derives the cases $k\geq 9$ from Browning's theorem, in the published form given by Xiao, through a transfer lemma that moves the density from the primitive positive-leading part of $f$ to $f$ itself. The manuscript imposes no primitivity or sign condition on the leading coefficient and does not assert uniformity of the error term in $f$. Applied to $f=x^4+2$, which is Eisenstein at $2$ and whose values at $0$ and $1$ exclude every fixed prime square, it gives a positive-density set of $n$ with $n^4+2$ squarefree. The release manuscript is the preprint the links carry. The release's README says its manuscripts were produced by an internal OpenAI model and come at different stages of verification, not all with Lean formalizations; this one has the Lean declaration described below.

Covers. Parts 2 and 3 of the page, both answered yes. Part 2: every $f$ in $\mathbb{Z}[x]$ irreducible over $\mathbb{Q}$ of degree $k\geq 4$ such that, for each prime $p$, $p^{k-2}$ fails to divide some $f(n)$, has $f(n)$ $(k-2)$-power-free for a set of $n\geq 1$ with natural density $c=\prod_p(1-\rho_f(p^{k-2})/p^{k-2})>0$, hence for infinitely many $n$. The page's $k\neq 2^l$ and positive-leading-coefficient hypotheses are not needed, so either reading of the page is covered. Part 3: at $f=x^4+2$ (Eisenstein at $2$, degree $4$, $f(0)=2$ not divisible by any $p^2$), $n^4+2$ is squarefree for a positive-density set of $n\geq 1$, so it represents infinitely many squarefree numbers. Part 1 ($(k-1)$-power-free values having positive density, including cubics) is not addressed.

Relation to the question. Problem 978 asks three things. Its first question, positive density of $(k-1)$-power-free values, was settled by Hooley (1967) with an asymptotic, recorded on its own claim page, and is not the subject of this page. Its second question is answered for every $k\geq 4$: the earlier range was $k\geq 10$ (Heath-Brown, its claim page) and $k\geq 9$ (Browning, its claim page), and the release adds $4\leq k\leq 8$. Its third question, whether $n^4+2$ represents infinitely many squarefree numbers, is the quartic case at the polynomial Erdős named in 1953. The result is stronger than asked in both places, since Erdős asked for infinitely many $n$ and the theorem gives positive density. The claim value is proved because both answers are affirmative theorems.

Formalization and acceptance. The release's Lean library states the whole $k\geq 4$ range as the declaration OAI.QuarticPowerFree.allDegrees in the module OAI.NumberTheory.PowerFree.Main: for f : Polynomial ℤ with Irreducible (f.map (Int.castRingHom ℚ)), 4 ≤ f.natDegree and the local condition LocallyAdmissible f (f.natDegree - 2) (every prime $p$ has $\rho_f(p^{k-2})<p^{k-2}$), the conclusion DensityStatement f (f.natDegree - 2) asserts that the Euler product is multipliable, that its value is positive, and that the count of $n\in[1,X]$ with $f(n)$ $(k-2)$-power-free differs from $cX$ by $o(X)$. Power-freeness there is the standard notion: no prime $p$ has $p^{k-2}$ dividing the value, which excludes zero. The comparator challenge lean/ComparatorChallenges/PowerFreeValues.lean pins the same seven definitions and the same statement, importing only Mathlib, and its JSON record names OAI.QuarticPowerFree.allDegrees as the pinned theorem. This corpus's verification built the declaration at the release revision the links pin and checked its axioms: only propext, Classical.choice and Quot.sound, and the comparator fingerprints were identical. That build and audit are the formalized evidence. The bridges from the formal statement to the page's wording are routine but are not written in Lean: irreducibility in $\mathbb{Z}[x]$ gives irreducibility over $\mathbb{Q}$ by Gauss's lemma; a positive density gives infinitely many $n$; and $x^4+2$ meets the three hypotheses, with PowerFree 2 being squarefreeness. No outside reviewer or refereed publication is recorded, so the page lists no reviewed or refereed evidence; the site's label for the problem is OPEN (page last edited 31 March 2026).

Depends on. No page of this wiki; the claim rests on the release manuscript and its Lean declaration.