we-solve (beta)

Math-2793 · mathematics · Number theory

Power-free values of irreducible polynomials of degrees four to eight

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For irreducible f in Z[x] of degree d in {4,5,6,7,8}, set $k=d-2$ and suppose no prime p has $p^k$ dividing every value f(n). Does the count of positive $n<=X$ for which f(n) has no prime-kth-power divisor equal $c_{f,k}$ X+o(X), where $c_{f,k}$ is the positive product over primes of 1 minus the proportion of roots of f modulo $p^k$?

Short English statement

For irreducible f in Z[x] of degree d in {4,5,6,7,8}, set $k=d-2$ and suppose no prime p has $p^k$ dividing every value f(n). Does the count of positive $n<=X$ for which f(n) has no prime-kth-power divisor equal $c_{f,k}$ X+o(X), where $c_{f,k}$ is the positive product over primes of 1 minus the proportion of roots of f modulo $p^k$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2793-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2793

The density theorem covers every degree $d\in\{4,5,6,7,8\}$ and $k=d-2$, with exactly the fixed-prime-power obstruction excluded in this question. Its positive Euler product and $o_f(X)$ error give the requested asymptotic. The subsequent corollary extends the conclusion to every degree $d\ge4$; neither primitivity nor a sign condition on the leading coefficient is imposed.

Power-free values of irreducible polynomials of degrees four to eight

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 020; 2026-09-24), the asserted result is that irreducible quartics without a fixed square divisor have the predicted squarefree density; degrees four through eight satisfy the corresponding $(d-2)$-power-free density and known higher-degree results extend it.

Mathematical statement of the claimed result

Manuscript 1.
For an irreducible $f\in\mathbb Z[x]$ of degree $d\ge4$, put $k=d-2$ and $\rho_f(p^k)=|\{a\bmod p^k:f(a)\equiv0\pmod{p^k}\}|$. Assume no prime has its $k$th power dividing every value of $f$, equivalently $\rho_f(p^k)<p^k$ for every prime. The claimed asymptotic is \[ |\{1\le n\le X:f(n)\text{ is }k\text{-free}\}| =c_{f,k}X+o_f(X),\qquad c_{f,k}=\prod_p(1-\rho_f(p^k)/p^k)>0. \] The theorem proves the range $4\le d\le8$, and its cited all-degree corollary extends the assertion to all $d\ge4$. No primitivity or leading-coefficient sign requirement is imposed; the quartic case is squarefreeness.

Outline of the argument

For manuscript 1 (family 020; 2026-09-24), the finite-prime sieve leaves a tail involving primes larger than the input interval. Number-field factorization and paired boxes are cut by adaptive auxiliary-prime determinants, with explicit geometry in low degrees controlling that tail before the cutoff is removed.

Formal verification

For manuscript 1 (family 020; 2026-09-24), OpenAI lists Lean statements for this assertion: irreducible quartics without a fixed square divisor have the predicted squarefree density; degrees four through eight satisfy the corresponding $(d-2)$-power-free density and known higher-degree results extend it.

This coverage does not establish a formal proof of the complete problem as stated here.

The linked family Comparator checks are PowerFreeValues.lean.

Their named declarations include OAI.QuarticPowerFree.allDegrees.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →