cert-machine · report · ζ(7) · a claimed proof, audited · generated from the record

A claimed proof that ζ(7) is irrational: the inequality it rests on fails

A preprint posted on 23 September 2026 claims that ζ(7) is irrational, by adapting the Hankel-determinant argument that settled ζ(5) a week earlier. The proof rests on one number, A₂₀₀ + U, being negative; the paper prints −11.99. On 3 October a reader, GitHub user @huntrontrakkr, reported that one of its integrals does not follow from the paper's own formulas. We recomputed it in exact arithmetic, with code written here. The reader is right: the number is positive, under every reading of the paper and every correction in its favour that we could decide. That breaks this proof. It does not show that ζ(7) is rational — whether ζ(7) is irrational remains open.

tl;dr

The finding. The paper needs A₂₀₀ + U < 0 and prints −11.99. Computed from its own formulas, the outer integral is +1.576, not −15.28, and A₂₀₀ + U is +4.86. With every correction in the author's favour that we could decide, it is still +2.26, and no other cutoff M can bring it below zero. The proof route fails. Theorem 1.1 is not disproved: ζ(7) may well be irrational; this paper does not show it.
The mechanism. The paper's Table 5, the piecewise-linear function it integrates, does not come from its own exponent formula (59). Past y = 1 the paper itself sets the local exponent to zero, which leaves 37/20 − y ≥ 0; Table 5 prints −239/20 − 2y there. The local p-adic bound (59) is not the problem: on the paper's own polynomials at K = 40, 80, 120 it holds at every prime we tested, and holds with equality at most of them. The error is in integrating it.
Check it. python3 instruments/zeta7audit/battery.py re-derives every decided number, re-runs two of the paper's polynomials exactly, and fires 9 planted forgeries (42 checks, under a minute). instruments/zetahankel/.venv/bin/python instruments/zeta7audit/decide.py rewrites the record in seconds.

A₂₀₀ + U, as printed

−11.99

must be negative for the proof to work

A₂₀₀ + U, recomputed

+4.86

the paper's own formulas, its own A0 and U

smallest after any decided repair

+2.26

every reading, A0 and U corrected in the author's favour

outer integral I_out

+1.576

printed: −15.28 (122)

the family itself, n = 3

+0.88

log P(ζ(7))/K², measured exactly · a measurement, not the limit

the reader's report

4 / 4

points confirmed · issue #1 by @huntrontrakkr, a third party

Local working document, machine-derived, not peer-reviewed. Decided: the arithmetic of the paper's proof route, from its formulas as printed, as exact rationals or arb balls — the outer integral, the inner integral (121), the constants A0 and U's ingredients, the margins (117)–(119). Measured, not decided: the paper's own family at three sizes. Not decided: whether ζ(7) is irrational (open); Theorem 1.2 as a statement about large n; the inner estimate Proposition 4.4; Lemma 6.1's supremum; the Lean repository's own theorem, which was read, not built. Nothing was posted, commented or sent.

§1 · the claim and the report

What the paper claims, and what the reader found

The paper. P. Anand, Zeta 7 is Irrational, Zenodo 10.5281/zenodo.22920911, v1 (the record's only version), 2026-09-23, 42 pages, CC-BY-4.0. Theorem 1.1: ζ(7) is irrational. The route is Fauzan's for ζ(5): integer polynomials Q built from Hankel determinants of a moment functional that is positive at ζ(7), with lim sup K⁻² log Q(ζ(7)) ≤ A_M + U (117). A_M collects the arithmetic (the primes that can be divided out), U the size of the determinant. The proof needs the sum negative; (118) states A₂₀₀ + U < −11, and Theorem 1.2's rate exp(−19000 n²) comes from it.

The report. On 2026-10-03 GitHub user @huntrontrakkr — a third party, not this lab — opened issue #1 on gmDevi/zeta-7-21-lean, a repository whose README cites the paper, because the paper gives no contact address. The report makes four points: the outer integrand on (1, 37/20] is 37/20 − y, not Table 5's −239/20 − 2y, which alone moves A₂₀₀ + U to +0.95; integrating the paper's (54), (58), (59), (62) gives I_out = 453803/288000, not −11002997/720000; the constant A0 is Fauzan's entire ζ(5) constant; and with all of it, A₂₀₀ + U ≈ +4.86. It says plainly that it concerns only the v1 argument, not whether ζ(7) is irrational. As fetched on 2026-10-05 the issue is open with 0 comments.

What we did. We recomputed each of those points from the paper's printed formulas, with code written here that shares nothing with the paper or with the report's script, and checked it by reproducing a published value that is right: Fauzan's own outer integral, 127751/96000. We also computed the paper's own polynomials exactly at three sizes. The author's Zenodo note mentions a rounding issue in the decay constant, to be fixed in a v2; no v2 has been posted.

§2 · the verdicts

The reader is right on every point we checked

Each line is decided from the paper as printed, except the last two, which are its finite statements checked at three sizes. CERTIFIED means the statement holds exactly; REFUTED means it does not; REFUSED means the paper does not establish it, which is not the same as false; PARTIAL means checked only where stated. The kind of defect, where there is one, is an arithmetic slip.

claim	verdict	the number
the reader's point 1: the last piece alone moves A₂₀₀ + U to +0.95	CERTIFIED	+0.9484
the reader's point 2: I_out = 453803/288000 from the formulas	CERTIFIED	453803/288000
the reader's point 3: A0 is Fauzan's whole ζ(5) constant; (85) bounds that tail by ≈ −0.057	CERTIFIED	−2069/36000
the reader's total: A₂₀₀ + U ≈ +4.86, or ≈ +3.49 with A0 replaced	CERTIFIED	+4.865 · +3.490
(122) I_out = −11002997/720000 follows from the paper's formulas	REFUTED	it is Table 5's integral
Table 5, last row: −239/20 − 2y on [1, 37/20]	REFUTED	it is 37/20 − y
(118) A₂₀₀ + U < −11, the inequality the proof rests on	REFUTED	+4.865
(119) A₁₀₀₀₀₀ + U < −12, used for the irrationality measure	REFUTED	+4.824
Theorem 1.2, the decay exp(−19000 n²): its proof	REFUTED	proof only; see §5
Theorem 1.1: ζ(7) is irrational	REFUSED	not proved here; open
Corollary 1.3: \|ζ(7) − a/b\| > b⁻²⁷⁰	REFUSED	rests on (119)
(121) the inner integral, from (64)–(69)	CERTIFIED	exact, as printed
(96) U = 44/25 bounds λM0 − I(ρ) + C*	CERTIFIED	holds; the printed I(ρ) is mis-summed
Proposition 4.6, the local bound (59), at K = 40, 80, 120	PARTIAL	holds at every prime tested
Proposition 6.3, the real bound, at K = 40, 80, 120	PARTIAL	holds

§3 · where it breaks

Table 5 is not the integrand the paper defines

The outer primes, K/3 < p ≤ 2h, enter through an exponent L_p = v_p(S_K) + γ_p^out (60): the factorials of the normalisation (62) and the local bound (59). In the variable y = p/K, −L_p/K tends to a piecewise-linear function T(y), and I_out is its integral over [1/3, 37/20]. The paper's Appendix A.2 gives T as Table 5 and its integral as (122).

Past y = 1 there is nothing to compute. The paper sets γ_p^out = 0 for p > K (§5.1); K!, N! and 4 are units at such p; only the factorials (2i)! of S_K carry p, and they carry it in the denominator. So L_p = −(2h − p − 1) < 0 and T(y) = 37/20 − y, which is positive. Table 5 prints −239/20 − 2y, about −14. That one row is worth +12.94 in I_out. Across the rest of the range the table is wrong as well, by +3.92.

The outer integrand T(y): solid, decided from the paper's own formulas; dashed, the claim as printed in its Table 5. The steep vertical segments are jumps in the functions. The signed area under each line is I_out. Hover for values.

Table 5 interval	Table 5 gives	formulas, reading R2	formulas, reading R1
[1/3, 37/100]	−0.2406	+0.1679	+0.1569
[37/100, 37/80]	−0.5286	+0.3022	+0.2839
[37/80, 29/60]	−0.0993	+0.0460	+0.0454
[29/60, 1/2]	−0.0732	+0.0360	+0.0360
[1/2, 37/60]	−0.6621	+0.4233	+0.4233
[37/60, 37/40]	−1.0175	+0.3083	+0.3083
[37/40, 77/80]	−0.0445	−0.0333	−0.0333
[77/80, 1]	−0.0361	−0.0361	−0.0361
[1, 37/20]	−12.5800	+0.3613	+0.3613
[1/3, 37/20]	−15.2819	+1.5757	+1.5457

two readings, both decided

The paper defines R0 twice, inconsistently: (71) makes it the limit of −γ/K, while §5.3 and the proof of Proposition 5.4 say −γ = K(R0 − d) + O(1), so that R0 − d is that limit. R2 follows the proof: the integrand is the limit of the exponents the normalisation (61) actually uses, and its integral is 453803/288000, the reader's value. R1 takes (71) and (73) literally and subtracts d(y) a second time, which lowers I_out by 3/100 and favours the author. It gives 445163/288000. Neither is close to −11002997/720000, which is exactly the integral of Table 5.

§4 · what it does to the proof

A₂₀₀ + U is positive, and no repair we could decide brings it back

A₂₀₀ = A0 + I_out + ∫₃²⁰ R/x³ + (cutoff terms) (88)–(89), and the proof needs A₂₀₀ + U < 0. We recomputed it in every combination: I_out as printed, with only Table 5's last row fixed, and from the formulas under each reading; A0 and U as printed, or corrected in the author's favour where this audit can decide the correction. Two such corrections exist. The paper's A0 (≈ +1.318) is larger than the paper's own tail bound (85) for the quantity it stands for, −2069/36000. And the paper's U overstates its own bound, because (110) sums the comparison measure's energy with the wrong logarithm; correctly summed, λM0 − I(ρ) + C* = +0.5563, not 1.7514.

I_out	A0, U as printed	A0 → (85), U → 0.556	A0 → (85), U → measured	best any cutoff can do
I_out as printed (122)	−11.993	−14.572	−15.853	−14.613
Table 5 with only its last row corrected	+0.948	−1.630	−2.912	−1.672
from the formulas, reading R2	+4.865	+2.286	+1.005	+2.245
from the formulas, reading R1	+4.835	+2.256	+0.975	+2.215

Read across a row. With I_out from the formulas, every entry is positive, and the smallest decided one is +2.256. The third column goes further than the audit can decide: it replaces U with the measured value, at n = 3, of the quantity U bounds, −0.725. Even then the entry stays positive. The last column is B0 + U, the floor that A_M + U approaches as the cutoff M grows. A_M > B0 for every M, because (89)'s cutoff terms form a quadratic with negative discriminant, so no choice of M rescues (118). (119), the input to the irrationality measure, fails the same way.

the reader's point 1, read carefully

Correcting only the last row moves A₂₀₀ + U from −11.99 to +0.9484, exactly as reported. But that keeps the paper's A0 and U, which are both too large. With them corrected too, the last row alone would leave −1.63 < 0. So the last row does not break the proof by itself. What breaks it is the whole of Table 5, and the formulas decide every row of it.

§5 · the bounds, or the route?

The paper's own polynomials do not get small at n ≤ 3

A failed inequality could mean the bounds are loose while the polynomials are still small. To check, we computed the paper's own determinant exactly: K = 40n, N = 3n, D_N⁸/D_K, h = 37n, with our Hankel engine (its functional at k = 7 is the paper's (5)–(6)). We then divided out every common factor. What is left, P_K, is the smallest integer polynomial any normalisation can give. The paper's B.3 says its Q_K,M is a positive-integer multiple of P_K. Theorem 1.2 would need log P_K(ζ(7))/K² below −11.87 for large n.

n	K	h	log P(ζ(7))/K²	per h²	log F(ζ(7))/K²	(59) exact at	v_p above K
1	40	37	+0.7965	+0.931	−0.655	4 / 6	9 primes · all 0
2	80	74	+0.8712	+1.018	−0.707	10 / 13	12 primes · all 0
3	120	111	+0.8839	+1.033	−0.725	13 / 18	17 primes · all 0

The margin is positive at every size and still rising: +0.796, +0.871, +0.884. Per h² it sits near +1.03, the same wall the Hankel-method measurement found for ζ(7) across 323 families. The paper's family was measured here, not assumed to share that wall. The local bound (59) holds at every outer prime tested, and with equality at most. At every prime between K and 2h the exact valuation of Δ_K is 0, where Table 5's last row would need about 15K.

a measurement, labelled

Three sizes do not decide a limit in n, and Theorem 1.2 is a limit statement. What the table shows is narrower: the paper's proof is refuted by its own arithmetic (§3–§4), and on these polynomials nothing suggests the theorem's rate. If the route can be saved, it will take a different family, not tighter bounds on this one.

§6 · what holds

Most of the paper's machinery checks out

The inner integral. (121), ∫₃²⁰ R(x)/x³ dx = +0.170349, follows exactly from the definitions (64)–(69). R was proved affine on 131 cells (the paper lists 192, unmerged).
The bookkeeping. A₂₀₀ and A₁₀₀₀₀₀ recompute exactly from the printed A0, I_out and (121). The arithmetic after I_out is consistent; the problem is the input.
The local estimate. Proposition 4.6 holds on the exact Δ_K at K = 40, 80, 120: 4 of 6, 10 of 13, 13 of 18 outer primes with equality. Lemma 2.3's leading coefficient is exact. Proposition 6.3, stated for every K, holds at all three.
Errors against the author. The energy slip in (110) makes U larger, not smaller. A0 is larger than the paper's own bound for the tail it stands for. Both are in §4's repairs, and neither changes the outcome.
The calibration. The same evaluator, applied to Fauzan's (4.10), (4.14) and (5.3), returns his printed 127751/96000. So do his printed (5.8)–(5.10) and his Table 4, whose last row is the 37/20 − y that Anand's Table 5 lacks. A0 equals Fauzan's A* (5.19) exactly, and equals his I_out + (5.18) + (5.16) exactly.

§7 · the Lean repository

gmDevi/zeta-7-21-lean proves something else, and says so

The issue was filed on gmDevi/zeta-7-21-lean because its README cites the paper. The repository does not formalise the paper. Its theorem, at commit 4e48690, is

¬ ∀ k ∈ {7, 9, 11, 13, 15, 17, 19, 21}, ∃ q : ℚ, riemannZeta k = q

that is, at least one of ζ(7), ζ(9), …, ζ(21) is irrational, by Zudilin's very-well-poised forms. It does not say which one, and it does not imply that ζ(7) is irrational. Its README cites Anand's paper as background and says its own check could not confirm two constants in the final inequality; that matches what §3 finds.

Census, grep-level. 38 .lean files, 15,635 lines: 1 sorry (Challenge.lean:32, the intended statement stub for the Comparator check), 0 admit, 0 axiom declarations, 0 native_decide, 20 uses of decide +kernel. The main theorem has no hypotheses.
Not built here. It needs a full Mathlib cache at Lean v4.35.0-rc2. The README reports #print axioms = propext, Classical.choice, Quot.sound, and registration in the Palomar registry at commit a3b69fc. Neither claim was checked here.

§8 · why you can trust this

How each number was decided

Exact integrals, no sampling. Each integrand is written once, as code over an affine form on a cell. Every max, min and floor it takes is checked to keep the same branch across the whole cell. When a branch changes, the cell is cut at the exact rational point where it does. The integrand is therefore proved piecewise linear, and each integral is an exact rational. The battery re-checks every stored piece on its own cell.
Two routes that share nothing. The finite exponents L_p(K) are computed as integers straight from (54), (58), (59), (62). Summed over every integer p, they approach the limit at a clean 1/K rate (−8.8e-4, −8.8e-5, −8.8e-6 at K = 4,000, 40,000, 400,000). Weighted by log p over the 47,087 primes, they give the outer part of log m_K,M/K² itself: [1.573030, 1.573030] at K = 400,000, an arb ball.
Balls for the rest. I(ρ), C*, the potential and every logarithm are evaluated in arb, with endpoints rounded outward. The polynomials P_K are exact integer polynomials, and log P_K(ζ(7)) is a ball of relative radius below 2⁻⁶⁰.
Independent of the claimant. No line is taken from the paper or from the reader's script. The control that the method is right is Fauzan's value, which a wrong method would not reproduce.
The battery. 42 checks and 9 planted forgeries at this build, every forgery refused: a flipped bit in the paper, a tampered I_out, (59)'s constant 9 moved by 10⁻⁶, Table 5's last row "corrected", Fauzan's constant moved by 10⁻⁶, two affine pieces merged, (118) relabelled CERTIFIED, the theorem itself called refuted, a forged fingerprint.
Not decided. Whether ζ(7) is irrational. It is open; this audit refutes one proof route and says nothing else about it. Theorem 1.2 as a statement about large n: no finite computation decides it. Measured at n = 1, 2, 3 only. Proposition 4.4 (the inner range) and the limit (70): they need K ≥ 200M² and are not tested here; (121) is decided only as a consequence of (64)–(69). Lemma 6.1's potential bound (94) as a sup: measured on a grid, not certified; the paper's A.3 partition is not re-run. The Lean repository's own theorem (one of ζ(7), …, ζ(21) is irrational): read at the pinned commit, not built.

§9 · the records

Sources, records, context

the records

The audit record (every decided quantity as an exact rational or a ball, both readings, all 24 margin scenarios, the verdicts, the Lean census) · the measured family in certs/zeta7-anand/measure.json · the code in instruments/zeta7audit/ · the sources pinned by sha256 in instruments/zeta7audit/PROVENANCE.json: the paper (CC-BY-4.0, committed), the issue thread as fetched, and, git-ignored, Fauzan's paper and the Lean clone.

Context: the Hankel method, measured past ζ(5), where the same family shape shows a positive margin at ζ(7) across 323 families. That is a measurement, not a theorem. This page decides one paper's proof, which is a narrower thing. The issue is issue #1 by @huntrontrakkr; the credit for finding the error is theirs.