What was already known
Lai proved that at least one of ζ₂(7), ζ₂(9), ζ₂(11), ζ₂(13) is irrational. Irrationality of ζ₂(3) and ζ₂(5) was already known.
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
Removes ζ₂(13) from Lai’s four-value alternative with a new AI-produced construction and a completed formal 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 maintainer’s novelty search was incomplete, and an unrefereed earlier Long draft claims all odd values 3–29 but has an apparent large-prime gap. The same maintainer later proved the stronger pair alternative and then ζ₂(7) individually, so this result is a historical intermediate step; it does not identify which of three 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, at least one of zeta2(7), zeta2(9), zeta2(11) is not 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