Source and verification

This article explains family 020 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ Power-free values and local obstructions

An integer is -power-free if no prime th power divides it. Negative integers are allowed; zero is excluded. For , put

If for some prime , every value fails the desired condition. The necessary local admissibility condition is therefore for all primes.

The Chinese remainder theorem gives the density surviving any finite collection of primes:

Passing to all primes requires a uniform tail estimate. The finite product formula by itself does not justify the infinite-prime conclusion.

Claimed density theorem

For every fixed polynomial irreducible over , of degree , put . Under local admissibility, the source concludes

The new argument treats degrees through . For , the manuscript invokes the existing range and checks that satisfies it. It also handles content and leading-coefficient sign. No uniformity as the polynomial varies is asserted. (OpenAI, 2026)

🏷️ A quartic example

For , Eisenstein’s criterion at two gives irreducibility. For any odd prime , shows that is not a fixed divisor. Also excludes a fixed divisor four.

Thus the local hypotheses hold. The claimed theorem gives a positive density of squarefree values, not merely infinitely many inputs.

For a fixed separable polynomial, all but finitely many primes have at most roots modulo : its roots modulo are simple and each lifts uniquely. Consequently

Together with local admissibility, this ensures positivity of the candidate Euler product. It still leaves the large-prime tail to control.

🏷️ Separating the sieve ranges

Fix beyond the exceptional primes. For , counting residue classes in an interval of length gives

After division by , this becomes small by first letting grow and then grow.

The difficult primes satisfy . The source’s central estimate, for primitive positive-leading irreducible with , is

for some . This estimate does not require local admissibility. It supplies the missing tail control, after which sign and content reductions restore the general theorem.

Notice the order of limits: the finite cutoff is held fixed during the limit in . The resulting density theorem does not automatically inherit a power-saving error from just one of its component estimates.

🏷️ Determinants in the large-prime range

Write , with in a dyadic interval near . Then has size approximately . The integer triples lie on the surface

A weighted determinant argument is sufficient in the upper part of the prime range. In the harder range, factorization in the field generated by a root produces balanced elements satisfying

for a fixed nonzero integer . Balancing keeps their conjugate sizes comparable, allowing coordinates in integer boxes.

The determinant method evaluates many polynomial monomials at points in a small box. If the determinant is an integer and an analytic estimate makes its absolute value less than one, it must vanish. This gives an auxiliary polynomial equation containing those points. Repeated cuts reduce the dimension of the set to be counted.

The actual source needs weighted counts of independent monomials, reduced lattice bases, and uniform control at auxiliary primes. Quartics require additional surface and curve estimates. These are stated here as the difficult counting input; the underlying algebraic geometry is outside this reading series’ instructional scope.

🏷️ Simultaneous values

The manuscript also treats fixed separable products whose irreducible factors have degree at most . For several polynomials , the correct local bad set is

The joint density uses , rather than multiplying the individual densities. The conditions on different can overlap modulo a prime.

Requiring every to be power-free also differs from requiring their product to be power-free: factors shared by two values can create a forbidden power in the product.

🏷️ Key steps and proof outlines

Removing content must preserve the original local factors

Write , with and primitive with positive leading coefficient. For a prime dividing , set . Admissibility forces .

Proof outline. The condition is equivalent to . Each solution modulo has exactly lifts modulo , so

Thus division by the content changes finitely many local conditions; it does not justify replacing the final product by the product for at exponent . Outside the primes dividing the content, leading coefficient, or discriminant, every root is simple. Writing a proposed lift as , the congruence determines a unique . Hence there. Summability of and strict positivity of every exceptional factor prove that the original Euler product is positive. (OpenAI, 2026)

A density sandwich isolates precisely the missing estimate

Let count the inputs in avoiding for , and let count those avoiding all primes. Set and let be the corresponding finite product.

Proof outline. Chinese remaindering gives exactly allowed classes, so . For beyond the exceptional primes, the additional loss from is at most

Let count inputs hit by a prime . Once exceeds all content primes this is also the large-prime exceptional set for . Therefore

Assuming the source’s estimate, divide by and first send with fixed. The lower and upper limiting densities lie between and . Then let . This proves the density on a dyadic interval. For , use finitely many dyadic intervals and bound the remaining initial interval by its length ; take first and afterwards. No uniform estimate for a growing finite-sieve modulus was assumed.

The large-prime argument has two complementary counting routes

For each exceptional input choose one witnessing prime, and group witnesses into . Since and , the companion coordinate has size . Choosing one witness avoids a multiplicity problem when converting a count of triples back to a count of inputs.

Proof outline of the determinant route. Evaluate weighted polynomial monomials at the integer points in a small box. After clearing the specified denominators, a nonzero evaluation determinant has an arithmetic lower bound. Taylor expansion inside the box supplies an upper bound; if it is smaller, the determinant must vanish. Linear dependence then produces an auxiliary equation on that box. The source controls how many independent monomials are available and repeats the cuts until a point-count estimate is possible. In the direct surface range its estimates yield an exponent below one, with the strict margins retained rather than rounded to the endpoint.

In the complementary range, the source balances the conjugates in and groups the resulting paired coordinate boxes. A grouping enlarges each coordinate scale but reduces the number of boxes. The parameter inequalities are designed so the increased per-box counting exponent is paid for by the decreased box count. Their strict remaining saving absorbs the small coordinate slack. Quartics also require deletion estimates for exceptional curves and fibers, and these losses are bounded before the final sum. The detailed geometric cutting theorems are the deep inputs here; this outline identifies what they must deliver without introducing a separate algebraic-geometry course.

Only prime blocks occur, because . If each allowed route has a fixed power saving and the exceptional sets do too, then their sum remains for a smaller . Indeed , so the block factor costs only an arbitrarily small part of the margin. This is the estimate inserted into the density sandwich.

Simultaneous conditions use one union of bad residue classes

For several fixed polynomials, form their union of forbidden classes modulo . The finite sieve counts exactly the classes outside this union. For the tails, the union bound permits summing the individual polynomial tail estimates. Thus the same sandwich works with local factors . No probabilistic independence between the polynomial values is required: overlap is handled exactly at each finite prime and by an upper bound in the vanishing tail.

🏷️ Connections

Jacobsthal’s function studies uniform survival under prescribed congruence exclusions. Prime predecessors explains why extracting primes from multiplicatively constrained candidates needs information beyond local densities.

🏷️ Manuscripts and verification scope

The family scope page describes selected formalization coverage. The page selects the irreducible-polynomial theorem for all degrees at least four, including sign and content generality. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026. Squarefree values of quartics and power-free values of polynomials.