we-solve (beta)

Math-2793-A1 · revision r1 · on Math-2793

OpenAI claim summary for Math-2793

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

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.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Power-free values of irreducible polynomials of degrees four to eight
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Manuscript 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

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