#978: n⁴+2 is squarefree infinitely often — OpenAI's proof that every irreducible quartic with no fixed square divisor takes squarefree values with the predicted density, its Lean replayed here (a shorter route than the paper's) and its paper read by AI seats; Formal Conjectures' three #978 statements proved in Lean from it

The problem. Erdős problem #978 [Er65b, p. 219; Er81h, p. 178; see also Er53]. Write d for the degree (the problem page writes k). Erdős proved in 1953 that an irreducible integer polynomial of degree d ≥ 3 takes infinitely many (d−1)-power-free values, apart from a 2-adic exception when d is a power of 2. Hooley proved in 1967 that it does so with positive density. One power lower, nothing was known in small degree. Erdős wrote in 1953: "I have also not been able to prove, for example, that n⁴+2 is squarefree for infinitely many n" (p. 425). In 1965: "I could prove nothing about the representation of (k − 2)-th power-free numbers, for example, I cannot show that n⁴ + 2 represents infinitely many squarefree numbers" (§6, p. 219). In 1981: "there is no quartic polynomial about which we can prove that it represents infinitely many squarefree integers" (p. 178). The problem page asks: if d > 3 and no prime p has p^d−2 dividing every value f(n), are there infinitely many n with f(n) (d−2)-power-free? In particular, is n⁴+2 squarefree infinitely often?

The local condition was added to the page on 31 March 2026. Moritz Firsching had posted a counterexample to the question without it, found by DeepMind's prover agent: x⁶+33x⁵+21x⁴+63x³+18x²+24x+48. It is congruent to x(x−1)⋯(x−5) mod 16, so 2⁴ divides every value.

Before this release the asymptotic for r-power-free values was known for these ranges of the exponent r:

• r ≥ (√2 − ½)d (Nair 1976), which reaches r = d−2 only for d ≥ 24;
• r ≥ (3d+2)/4 (Heath-Brown 2006, Theorem 16), so d ≥ 10;
• r ≥ (3d+1)/4 (Browning 2011), so d ≥ 9.

Two other results bear on it:

• For binomials x^d+c only, r ≥ (5d+3)/9 suffices (Heath-Brown 2013), so r = d−2 for d ≥ 6. Heath-Brown wrote there that "the most interesting open question then concerns quartic polynomials taking square-free values".
• Granville (1998) obtained squarefree values in every case, but conditionally on the abc conjecture.

Our July report on #978 (/report/978) found the problem open. It counted 75,670 squarefree values of n⁴+2 for n ≤ 10⁵, with every factorisation checked independently. It enclosed the predicted density between 0.75668370 and 0.75668401, and found a sign error in the decisive step of the one public claim then on record (Carella, arXiv 2310.16952).

It also named "the exact unresolved range" as primes p > √X. That was wrong. The elementary count Σ_p≤X ρ(p²)(X/p² + 1) = O(X/Y) + O(π(X)), taken over primes p > Y, already handles every p ≤ X; this is the paper's (2.5). So the open range was p > X, which is exactly OpenAI's Proposition 1.4. The report now carries a dated correction.

The claim. OpenAI, "Squarefree values of quartics and power-free values of polynomials" (dated 24 September 2026, 55 pages, public since 6 October as family 020 of github.com/openai/math). In the paper's notation k = d − 2 is the exponent.

Theorem 1.1: let f ∈ ℤ[x] be irreducible over ℚ of degree d with 4 ≤ d ≤ 8, and suppose ρ_f(p^k) < p^k for every prime p, so that no prime k-th power divides every value. Then

#{1 ≤ n ≤ X : f(n) is k-power-free} = c_f,kX + o(X), c_f,k = ∏_p(1 − ρ_f(p^k)/p^k) > 0.

No primitivity or sign condition is needed. The rest of the paper:

• Theorem 1.1 rests on Proposition 1.4, the large-prime tail: #{X < n ≤ 2X : p^k | f(n) for some prime p > X} ≪ X^1−δ.
• Corollary 1.2 extends Theorem 1.1 to every d ≥ 4, citing Browning (in Xiao's form) for d ≥ 9.
• Corollary 1.3 does the same for products and families of polynomials whose irreducible factors have degree at most k+2. Its proof also cites Reuss and Xiao.

For #978 this answers both parts that were open. Every irreducible quartic with no fixed square divisor takes squarefree values with the predicted positive density. n⁴+2 is one: it is Eisenstein at 2, and f(0) = 2 is divisible by no prime square. The page's (d−2)-question is answered for every degree d ≥ 4, with density rather than just infinitude, and without the page's restriction that d is not a power of 2 or its positive leading coefficient.

The argument. The paper follows Reuss's framework for power-free values: factorisation in a number field, plus approximate determinants. It adds new pieces.

• §2 reduces the density to Proposition 1.4. It uses a finite sieve for small primes, the bound ρ(p^k) ≤ d (by Hensel, outside a finite set of primes) for primes between the cut-off and X, and the tail for primes above X. The limit in X is taken before the sieve cut-off goes to infinity.
• §3 proves a uniform affine counting theorem. It counts integer points of bounded weighted size on algebraic sets whose equations may change from box to box, given lower bounds on the weighted Hilbert functions of their subvarieties. The proof cuts residue classes at auxiliary primes. A random deletion argument handles the primes at which later, moving equations fail to give smooth local coordinates.
• §4 factors the ideal (n−θ) in K = ℚ(θ) as α^kβ = μ(n−θ), with balanced conjugates of sizes P^1/d and X^b/d. The integer coordinates of α and β fill two boxes.
• §§5–9 cut the paired boxes by archimedean determinants, change to reduced lattice coordinates, and compute weighted Hilbert bounds. They add explicit surface and curve geometry for quartics. On a curve the extreme case is a quintic polynomial with four prescribed critical values. Its integer values form one set of size O(X^1/5), which is deleted once, before any box is counted (Proposition 8.2).
• §10 and Appendix A choose the parameters and check the exponent margins with an exact finite certificate.
• §11 assembles the tail. For large η = log p/log X it counts directly on the surface f(x) = yz^k (§11.1). Elsewhere it uses the number-field count (§11.2). Every box exponent there is below 24979/25000, and every removed-fibre exponent in the quartic mode is below 3122/3125. These are uniform bounds from the 999/1000 certificate; Table 1's are stronger.

The Lean, and our replay. OpenAI's comparator challenge (ComparatorChallenges/PowerFreeValues.lean) states OAI.QuarticPowerFree.allDegrees, which is Corollary 1.2. Take f ∈ ℤ[x] irreducible over ℚ with natDegree ≥ 4 and LocallyAdmissible f (natDegree − 2). Then:

• the local factors are multipliable;
• their product is positive;
• count − c·X = o(X) as real X → ∞.

The solution, OAI.NumberTheory.PowerFree.Main, is 63 modules and 23,269 lines, and it imports nothing but Mathlib.

We compiled all 63 from source on our machine with Lean v4.34.1 and Mathlib d13f23b7, the repository's pins. We built module by module, with no cache for anything but Mathlib: 63 of 63, 0 errors, 0 warnings, 17 minutes of wall time, peak 6.8 GiB. Only one module ever ran at a time, because the 63 files form a single import chain. The checks on the result:

• #print axioms under --trust=0 gives exactly propext, Classical.choice and Quot.sound for allDegrees.
• The fully elaborated (pp.all) printouts of allDegrees and of the seven definitions it uses match the comparator's character for character, after collapsing whitespace: 8 of 8. The definitions are PowerFree, rho, count, LocallyAdmissible, localFactor, densityConstant and DensityStatement.
• A mutation test of the matching script caught all eight mutants: a product in place of the power in PowerFree, Ico in place of Icc in the count, big-O in place of little-o, degree 5 in place of 4, an added axiom, the challenge's sorry removed, a missing block and a missing file.
• A planted sorry surfaces as sorryAx.
• We scanned the 63 files and the challenge for sorry, axiom, native_decide, implemented_by, extern, unsafe, opaque, meta code and set_option. The only hit is the challenge's own sorry; there is not a single set_option in the closure.

A second check by leanchecker --fresh covered the whole environment: Mathlib, OpenAI's 63 modules and our bridge. It re-checks every declaration from the stored terms through the kernel, independently of the build's elaboration, and it re-checks Mathlib's cached files too, which --trust=0 does not. It exited 0 after 3,502 seconds (peak 8.2 GiB). Its control, run on a module that does not exist, fails as it should.

We were not first. Two third-party replays ran OpenAI's Comparator on this challenge before us:

• carlostoledo1891/cert-machine (GitHub Actions run 38019899278, committed 10 October). Both Lean's kernel and the independent nanoda kernel accepted the solution.
• nealmcb/openai-math-lean-tooling. It accepted PowerFreeValues on 11 October, same pins, the same 63-module closure, as part of a run over all 416 challenges recorded on 13 October.

Ours is a third, independent replay. Comparator compares the theorem against the challenge, but this challenge's configuration lists no definitions for it to compare (its definition_names is empty). Ours adds a pp.all match of the seven definitions the statement names, under a mutation-tested matcher. It also adds the module-by-module build, the source scan and the Formal Conjectures bridge below. Our own literature seat had searched for the namespace and missed both; they appear under the challenge's name, and the blind reader found them.

The Lean does not follow the paper. Seat L read all 63 files against the paper. The closure has no comments, so its map of files to sections is by content.

What the kernel-checked proof shares with the paper:

• the sieve transfer (§2) and the balanced factorisation of Lemma 4.1;
• an affine counting theorem of Theorem 3.1's shape, which is itself a determinant method with cuts at auxiliary primes;
• weighted Hilbert thresholds of §7's shape;
• quartic surface and curve alternatives of its own, in the spirit of §§8–9.

Then it takes a shorter route:

• No archimedean cut. It never makes the archimedean (Taylor) determinant cut of §5. Instead it applies the counting theorem to the whole (d+1)-dimensional norm variety in ℤ^2d. The coordinates are those of α and β in a fixed integral basis, and the equations are a_i^kb_i − a₀^kb₀ = θ₀ − θ_i. This needs a top-dimensional threshold the paper never states.
• Exceptional fibres, arithmetically. A fixed n gives one point. A fixed α gives at most a bounded number, since ρ(p^k) ≤ d and p^k > X. For "radial" fibres α′ = cα, prime norms force c = ±1.
• Its own certificates. For 5 ≤ d ≤ 8 it uses one box for the whole range of η, with exponents U = 1/3 and V = 2/5. For d = 4 it uses 100 bins in η, with a certificate checked by kernel decide. The tail saving is X^−3/1000 for 4 ≤ d ≤ 8. L re-checked every certificate inequality in exact arithmetic, and all hold. The closest calls: for d = 5 the exponent sum meets its 997/1000 bound exactly (allowed, since the inequality is ≤), and the full-dimension thresholds clear their envelopes by as little as 0.00049 (d = 7) and 0.00059 (d = 4, first bin).
• d ≥ 9 without Browning. It proves d ≥ 9 itself, using the paper's own §11.1 device: the surface f(x) = yz^k in two weight boxes, with saving X^−1/2000. No result of Browning, Xiao, Heath-Brown or Reuss enters anywhere. L notes the paper could have done the same: on [1, d/k], η(1 − kη/d) is largest at η = 1, where it is 2/d ≤ 2/9, well inside the range §11.1 handles.

So the Lean needs none of the following: Lemma 4.2, §§5–6, Proposition 8.2 (the quintic deletion), Proposition 10.1, Appendix A, §11.1 in degrees d ≤ 8, or Browning's theorem. Its quartic surface bound is its own analogue of Proposition 8.1, with different alternatives. Two things follow.

• If the replay is right, no objection to those parts of the paper can sink Theorem 1.1, Corollary 1.2 or #978.
• The Lean cannot vouch for those parts either. They stand on the paper alone, and so do Corollary 1.3 and §12, which have no formal counterpart.

Formal Conjectures' three statements of #978, proved in Lean (ours). Formal Conjectures has two statements tagged "research solved" since PR #6898 (merged 11 October), each with a link to OpenAI's allDegrees:

• Erdos978.erdos_978.parts.ii: infinitely many (d−2)-power-free values;
• parts.iii: {n | Squarefree (n⁴+2)} is infinite.

Their proofs are still sorry. So is that of variants.sub_two, which is Browning's d ≥ 9 case. Our file Bridge978.lean proves verbatim copies of all three from OpenAI's theorem. A script checks the copies against FC at a7b87c8d, and a mutated copy fails the check. The steps:

• Irreducible in ℤ[X] with positive degree gives primitive, and Gauss's lemma then gives irreducible over ℚ.
• FC's local condition (for every p, some n ≥ 0 with p^k ∤ f(n)) gives ρ(p^k) < p^k, by reducing n mod p^k.
• A positive density makes the count unbounded, so the set is infinite.
• OpenAI's PowerFree (no prime k-th power divides a) and FC's Powerfree (x^k | a forces x to be a unit) give the same set.
• For parts.iii, X⁴+2 is irreducible by Eisenstein at 2, local admissibility comes from f(0) = 2, and Squarefree in ℕ is matched to PowerFree 2 in ℤ.

The file also proves the density form in FC's own vocabulary. FC currently states density only for Hooley's (d−1) case (parts.i). Our form: {n | Powerfree (d−2) (f(n))} has natural density equal to OpenAI's Euler product, in FC's Set.HasDensity (which counts 0 ≤ n < b), and so it has positive density.

This form needs neither the restriction that d is not a power of 2 nor a sign condition. That matters because FC's parts.ii keeps the page's preamble excluding powers of 2. Read literally, the preamble removes every power-of-two degree (4, 8, 16, …), including 4 and 8 from Theorem 1.1's new range. Quartics enter FC only through parts.iii.

The seven top-level bridge theorems (the file's other six are lemmas they use) depend only on propext, Classical.choice and Quot.sound under --trust=0. Three mutants behave as they should:

• With the conclusion's exponent d−2 changed to d−3, the proof fails at the step that uses the exponent.
• With the local condition dropped, it fails where it tries to supply local admissibility. That statement is false: DeepMind's degree-6 polynomial is a counterexample.
• With a sorry planted in the density-to-infinitude lemma, sorryAx appears in the axioms of all three FC theorems.

The reading. Four seats, all Claude Opus 5.5, were each briefed to refute, to quote the sentence they objected to by the paper's printed numbering, and to grade every objection FATAL, GAP, ERROR or EXPOSITION:

• seat M1: §§2–4, §10 with Appendix A, and §11;
• seat M2: §§5–9 and §12;
• seat L: the Lean against the paper;
• seat W: the sources and the world.

A fifth seat read this page blind against the files. None found a FATAL error, or a gap in Theorem 1.1, Corollary 1.2 or anything #978 needs. M1, M2 and L returned HOLDS AS READ. W returned HOLDS AS READ on the Erdős sourcing, the cited ranges and the priority record, and one minor GAP, in Corollary 1.3 (below). The blind reader's corrections (among them that ours was not the first replay) are applied on this page.

• M1 recomputed the certificate of §10 and Appendix A in exact arithmetic, independently of the paper's own listing, which also runs and passes.
  • The cells of width 1/3000 in η are closed and contiguous, and they cover η = 1 up to the stopping point. The direct-surface range of §11.1 covers the rest up to d/k, including b = 0 and the O(1/log X) overshoot.
  • Every margin is strictly positive. The tightest exponent gap is 0.0019350 (d = 4, cell 3555, η ∈ [1.18500, 1.18533]); Table 1's 0.00191 is a rigorous lower bound for it.
  • One cut inequality of (10.4) holds by a relative margin of only 1.5·10⁻⁸ (d = 4, cell 4902), because w is the least grid point that works. It is strict, so it is valid, but the "sufficiently large" in Proposition 5.2 is enormous there. That costs nothing, since no effective δ is claimed.
  • Six mutations each make M1's checker fail: a gap of 10⁻⁶ in one cell, a raised stopping threshold, a weaker top-dimensional threshold, and w shrunk by 1% in one cell, plus two that matter for the route. Replacing the quartic curve constant g = 4 by 3 (no quintic deletion) breaks 434 cells, and replacing the quartic surface bound 3/U² by 2/U² breaks 609. So the paper's quartic route really does need Propositions 8.1 and 8.2.
  • The Lean uses g = 3 and its own analogue of Proposition 8.1, with different alternatives. It needs no quintic deletion, because it counts on a different variety.
• M1 on the saving. The paper never computes the δ of Proposition 1.4. From its own certificate it is at most about 5·10⁻⁴. The limit is set by the direct range, where 1/2 + √(b′η′/d) reaches 0.99954 for d = 8 and 0.99943 for d = 4, not by Table 1's gaps. The Lean's 3/1000 is larger than anything the paper's route gives; the two agree only in being positive.
• M1 on §§2–4.
  • The sieve transfer takes its limits in a valid order: cut-off fixed, X → ∞, then the cut-off, then the dyadic pieces.
  • (2.2) is right for every e ≥ 1, and local admissibility forces e < k. The tail is the primitive part's once X exceeds the content primes.
  • Every constant inside §3 is independent of the coefficients of the moving varieties, because Theorem 3.1 pushes all the uniformity into its hypotheses. The weakest link is therefore whether Propositions 7.1, 8.1 and 9.2 hold uniformly for every subvariety in moving coordinates, which is M2's ground.
  • The box sizes of §4 depend only on f, and the bound of at most k^d root choices holds.
  • Expository: §11 needs its dyadic intervals anchored at P = 2ⁱX. Otherwise the first η falls just below 1, where no cell of the main theorem applies.
• M2 read §§5–9, checked the rest by hand, and computed every Hilbert-function claim that can be made concrete.
  • Both determinant cuts in §5 take a kernel vector against a basis of the component's own coordinate space, so the form they produce cannot vanish identically on that component. The split into mixed and pure equations is exhaustive, because the bidegree is never (0,0).
  • The Hilbert bounds are bounds on the variety actually present. Random-point evaluation ranks modulo a prime equal the paper's complete-intersection series exactly, with no mismatch, in three families: the bicone of Lemma 5.1 (10 bidegrees, d = 4 and 5), a saturated first-cut component (5 bidegrees), and three examples of Proposition 7.1's pair image under five weightings (15 runs). In two of those three examples (10 of the 15 runs), and for the first-cut component, the unsaturated weight would have given the wrong count. So the saturation step is needed, and it is right.
  • The surface case analysis of §8.1 (an a-image of degree ≥ 3, 2 or 1) is exhaustive. In the plane case both alternatives the paper rules out are genuinely impossible.
  • Uniformity in moving equations, coordinate changes and boxes is argued at every place it is used.
• M2 on the quintic set (Proposition 8.2). An exact resultant computation finds exactly 25 normalised quintics with critical values (1, i, −1, −i). It finds 25 again for a reordering and 25 for generic values (0, 1, 3, 7): the Hurwitz count 5⁵⁻³. The roots of x⁴+1 and x⁴+2 reduce to (1, i, −1, −i) after scaling. The critical values are the roots of f, fixed before any box, curve or prime is chosen. So the set of their integer values, O(X^1/5) of them, is one global set, and deleting it once is legitimate. The paper says only "finitely many"; stating 25 would let a reader check it.
• M2 on §12 (the worked example n⁴+1) found it consistent with the general argument. Its enlarged-cell certificate passes in exact arithmetic (gap − 4τ = 1941/10⁵), ℤ[ζ₈] is norm-Euclidean by the rounding argument given, and the Pell estimate holds.
• One GAP, in Corollary 1.3 only. For d = k+1 the proof cites Reuss's Lemma 3, its proof and his §6 for the triple count. W graded this a GAP. Reuss's §§2–3 work in ℤ[θ] with θ integral, that is, for monic f. The paper applies them to a primitive, possibly non-monic g without the standard reduction (substitute y = cn, so that c^d−1g(y/c) is monic). W adds that Reuss's statement is for general irreducible f, so the citation is defensible. M1 checked the same citation for a different point: the estimate is assembled from Reuss's proof text rather than stated, which M1 graded EXPOSITION; it did not examine the monic reduction. The gap is fillable, it touches only Corollary 1.3, and Corollary 1.3 has no Lean.
• Smaller points.
  • Booker–Browning 2016 is not cited for the k = 2 case of Corollary 1.3 (W).
  • The Erdős history omits [Er81h] (W).
  • Xiao's Theorem 9.1 needs no primitivity step, and the estimate taken from Xiao's §9 sits inside a proof sketch; Browning 2011 is the primary source (M1, W).
  • W could not fetch Browning 2011 itself. Its range r ≥ (3d+1)/4 rests on three secondary statements (Xiao, Heath-Brown 2013, Reuss), which agree.

Numbers (computer-assisted, label (d); they test nothing about the theorem). For f = x⁴+2, ρ(p²) is 2 for p ≡ 3 mod 8, either 4 or 0 for p ≡ 1 mod 8, and 0 otherwise. Our July report proves this, and checks the formula by brute force for p ≤ 10⁴. The predicted density is c ≈ 0.7566840, enclosed rigorously in July between 0.75668370 and 0.75668401. For x⁴+1 it is c₈ = ∏_{p≡1 (8)}(1 − 4/p²) ≈ 0.9808175. The counts:

Each count was made twice, by different methods.

• By factoring every n⁴+w in PARI/GP. Our July run covered n⁴+2 to 10⁵, with its factorisations certified by a separate program. Today we ran both polynomials to 10⁵ and to 2·10⁵, and seat M2 ran both to 10⁶.
• By a sieve that factors nothing. It runs over every prime p ≤ 10⁶, marking the classes n ≡ r mod p² for each root r of x⁴+w lifted from p to p².

The two agree at every checkpoint. A version of the sieve with the lift removed gives 65,353 at 10⁵, so the agreement is not automatic.

The large-prime tail that Proposition 1.4 is about is tiny here. Factoring every value up to 10⁶ (M2's run; ours to 10⁵ agrees) finds only two n with p² | n⁴+2 for a prime p > n: n = 2 (p = 3) and n = 97 (97⁴+2 = 179²·2763). For n⁴+1 there are none. The sieve is exact for N ≤ 10⁶ only because of this census: a prime p > 10⁶ with p² | f(n) and n ≤ 10⁶ would have p > n, and none does.

Sources and the world.

• Erdős's three sentences are quoted above from the page images of [Er53] (users.renyi.hu/~p_erdos/1953-02.pdf), [Er65b] (1965-17.pdf) and [Er81h] (1981-33.pdf), read by seat W. The paper cites the first two, not [Er81h].
• The two earlier claims did not hold up.
  • Zapata Ceballos and Jalalvand (arXiv 2608.10335, v1 11 August 2026) claimed positive squarefree density for monic irreducible polynomials of degree 2q, q prime, with squarefree fixed divisor, whose field contains a degree-q Galois subfield. Their Corollary 2.4 covers every monic quartic whose Galois group is neither S₄ nor A₄ (with squarefree fixed divisor), and so x⁴+2 as well. The paper cites v1 as a claim it does not use, and says it "includes n⁴+1"; it included n⁴+2 too. The authors withdrew it on 15 October: "The proof of Proposition 2.3 is incomplete. The argument does not provide the estimate needed to control the contribution of square divisors arising from prime ideals of large norm." That is the large-prime tail, the step Proposition 1.4 is about.
  • Carella (arXiv 2310.16952, 2023, math.GM, one version, unrefereed) claims n⁴+1 and n⁴+2 with a power saving. Our July report found a sign error in its decisive fractional-part estimate, and noted that its constant 0.757159 lies outside our enclosure of the true density. Seat W adds that its constant for n⁴+1 is also wrong (0.981003 against 0.980817), and so is its Theorem 1.3 constant (0.9638 where the density is 0.9006).
• Uncited prior work. Booker and Browning (Discrete Analysis 2016:8, Theorem 1.2) already proved the k = 2 case of Corollary 1.3 for factors of degree at most 3, by the same factor-by-factor tail.
• The record elsewhere.
  • The teorth database still lists #978 as open (last update 31 August 2025).
  • The problem page was last edited on 31 March 2026. It does not mention OpenAI, lists no proof claims, and has suspended comments.
  • Formal Conjectures marked parts ii and iii solved in PR #6898 (Moritz Firsching, merged 11 October). Its stated checks are a build of FC's own changed files, resolution of the link, a grep of the release for sorry, and inspection of the comparator configuration. It did not build or replay OpenAI's proof. FC's status-mismatch bot issue #7135 is open.
  • A preprint of 21 October on random polynomials (arXiv 2610.29911) still says the squarefree asymptotic is known only up to degree 3 (Hooley), and does not cite OpenAI.
• The paper and its Lean have not changed since release. The manuscript, Main.lean and the whole PowerFree directory have the same git hashes at the initial commit (adc7f12, 6 October) and at the current head (1581d4c). FC's link (Main.lean#L144) points at allDegrees.

What this entry is. The theorem is OpenAI's, and its proof is OpenAI's model's. What is ours:

• the third kernel replay and its controls;
• the readings;
• the Lean bridge proving Formal Conjectures' parts.ii, parts.iii and variants.sub_two, plus the density form in FC's vocabulary;
• the numbers;
• a correction to our own July report.

Labels, as used on this site: (a) elementary; (b) rigorous modulo named cited theorems; (c) plausible, unverified; (d) computer-assisted. Theorem 1.1, Corollary 1.2 and the three FC statements are (d): Lean-verified, kernel-replayed here and twice before, unrefereed by any human. Corollary 1.3, §12, and the paper's own route through §§5–6, 8.2, 10 and Appendix A are (c): our AI seats read them, as reported above, nothing formal backs them, and Corollary 1.3 carries the one GAP found.

Where to look for a hole. In the formal claim, these are the places one could hide, and each can be read without trusting the rest:

1. the seven definitions in Model.lean, which the comparator repeats: are they the problem?
2. the Mathlib notions they use (tprod, Multipliable, IsLittleO, Nat.floor). Seat L checked the two tprod traps: a non-multipliable family has ∏' = 1, and a product diverging to 0 counts as multipliable. Both are closed by the statement's explicit Multipliable and 0 < conjuncts.
3. the statement of allDegrees;
4. the kernel: our replay, which took Mathlib's compiled files from its cache, the leanchecker --fresh pass, and the two earlier replays (one also with nanoda);
5. our bridge's 330 lines, against FC's text.

In the paper, the parts the Lean does not touch are the ones to read hardest:

• Lemma 4.2 and §§5–6;
• Proposition 8.2, and Proposition 8.1 and the §§7–9 thresholds as stated (the Lean only parallels them);
• the certificate of §10 and Appendix A;
• §11.1 in degrees d ≤ 8;
• the Browning/Xiao citation for d ≥ 9;
• Corollary 1.3 and §12.