What was already known
Lai proved that at least one of ζ₂(7), ζ₂(9), ζ₂(11), ζ₂(13) is irrational; the same maintainer’s earlier AI-produced theorem narrowed the alternative to ζ₂(7), ζ₂(9), ζ₂(11).
AI involvement
The maintainer reports that Claude agents produced the mathematical construction and informal proof as well as the Lean formalization under human direction; no task-only autonomy or human expert proof review is documented.
The maintainer credits Claude agents with the mathematical construction, informal proof and Lean formalization under human direction; no task-only autonomy is documented.
Importance
Further narrows the earlier alternatives to two values, using a different shifted well-poised construction, denominator argument and nonvanishing argument from the three-value proof.
Limitations
The project’s definition is identified with Kubota–Leopoldt ζ₂ by a cited theorem that is not formalized; the rational normalization does not affect irrationality. No human expert review is reported. The novelty search was incomplete, and an unrefereed earlier Long draft claims the stronger individual irrationality of ζ₂(7) but has an apparent large-prime gap. The same maintainer later proved ζ₂(7) individually, so this result is a historical intermediate step; it does not identify which of the two values is irrational.
Technical verification
The source reports a completed hypothesis-free Lean proof and Comparator matching for the exact Volkenborn-defined values. Identification with Kubota–Leopoldt ζ₂ is cited, not formalized; Formal applies to the project-defined values. AIProofWatch did not rerun the checks.
Formal checking
Repository reports a hypothesis-free theorem, no admitted proof in imported modules, Lean kernel and leanchecker checks, and successful Comparator checks.
- Checker
- Lean 4 kernel, leanchecker and Comparator, as reported by the maintainer and Palomar registry
- Scope
- For the project-defined Volkenborn-normalized 2-adic values, zeta2(7) and zeta2(9) cannot both be rational in Q₂. The Lean theorem also proves convergence of every J(s) limit used in the definitions and has no extra hypotheses.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
No human expert mathematical review or explanation of the AI-produced central construction is reported. Few is the evidence default, not a positive finding that experts cannot understand it.
Correction and publication history
Primary-source review of a historical intermediate AI mathematical advance, exact formal scope, proof construction, check report and later stronger results.
Read this published revision