What was already known
Zudilin had proved that at least one odd zeta value in the longer list ζ(7), ζ(9), …, ζ(35) is irrational. Zudilin’s later very-well-poised linear forms suggested shorter lists, but his needed asymptotic lemma was unproved beyond three derivatives.
AI involvement
The maintainer credits Claude agents with the mathematical configuration, size and nonvanishing theorems, informal proofs and Lean formalization, while the human directed the work.
The maintainer explicitly credits Claude agents with the configuration, key size and nonvanishing theorems, informal proofs and Lean formalization under human direction.
Importance
Shortens a published odd-zeta irrationality window using a new configuration and a formal proof that avoids the missing asymptotic lemma.
Limitations
The mathematics and Lean proof were produced by Claude agents under human direction and have not been reviewed by a human expert. The author’s prior-work search did not include MathSciNet, so novelty beyond its stated search is not fully established. An unrefereed September 2026 preprint separately claims ζ(7) alone is irrational, which would imply this result, but its numerical constants are disputed in a project issue; no exclusive priority claim is made. The theorem gives no individual value or irrationality measure.
Technical verification
The theorem has no hypotheses and uses Mathlib’s riemannZeta directly. The source reports completed Lean proof checking, kernel-checked numerical certificates, leanchecker replay and Comparator matching of the Challenge and Solution statements. AIProofWatch did not rerun the checks.
Formal checking
Repository reports no admitted proofs in imported modules, Lean kernel checking and leanchecker replay.
- Checker
- Lean 4 kernel, leanchecker and Comparator as run by maintainer and Palomar registry
- Scope
- At least one Mathlib riemannZeta value at the eight specified odd integers is irrational; no individual identification
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The source says the AI-produced mathematical argument has not been reviewed by a human expert; no independent human explanation of the configuration and analytic estimates is documented. Few is an evidence default.
Correction and publication history
Primary-source review of exact Mathlib theorem, Zudilin baseline, AI-origin disclosure, checker scope and competing claim.
Read this published revision