New record bound on the irrationality measure of ζ(2), μ ≤ 5.0495243, released as a 92k-line Lean proof written by Claude; beaten by a human paper a week later
On Sept 25, 2026 Jonathan Kleid published a machine-checked Lean 4 proof that the irrationality measure of ζ(2) = π²/6 is at most 5.0495243, improving Zudilin's 2014 record of 5.095412. Kleid found the parameters, (13, 11, 9, 15; 26) in Zudilin's construction, with his own computer-algebra system qedbook. Per the repository, "the Lean text was written by Claude (Anthropic) sessions directed by Jonathan Kleid". The development has 166 hand-structured modules (91,672 lines) plus 559 generated certificate modules, with no sorry and only Lean's three standard axioms. On Oct 2 David Niedbala Giraudin posted a 6-page human paper (arXiv 2610.02912) lowering the bound to 5.0193784; it cites Kleid's bound as the previous record.
Key facts
- Theorem (Lean): ¬ LiouvilleWith 5.0495243 ζ(2), plus the explicit rational-approximation form C/n^5.0495243 ≤ |ζ(2) − m/n| for large n; certified value of the construction 5.04952429053…
- Previous records: 5.441243 (Rhin–Viola, 1996), 5.095412 (Zudilin, Ann. Math. Québec 2014)
- Provenance (README): 'The Lean text was written by Claude (Anthropic) sessions directed by Jonathan Kleid, who also designed the search program and the verification discipline (every gate proven able to go red before its green was accepted)'
- Size: 166 modules / 91,672 lines, plus 559 generated modules holding a creative-telescoping certificate as exact integer data; full build ~12.6 CPU-hours, ~13 GB disk, assembly modules peak near 18 GB RAM
- Fills Mathlib gaps: explicit complex Binet bound for log Γ, a linear-forms criterion for ¬LiouvilleWith, Poincaré-type growth bounds for three-term recurrences, p-adic analysis of the common factor; the PNT comes from the vendored PrimeNumberTheoremAnd project (Kontorovich, Tao et al.)
- Repository qedbook/zeta2-irrationality-measure created 2026-09-25 (Apache-2.0); no accompanying paper
- Superseded Oct 2, 2026: Niedbala Giraudin, arXiv 2610.02912, μ(ζ(2)) < 5.0193784, using Zudilin's two hypergeometric constructions at new parameters without creative telescoping, constants checked by ball arithmetic; no AI disclosure. The same author's arXiv 2609.26980 (Sept 22) improved the 25-year-old ζ(3) record to μ(ζ(3)) < 5.5138800 (from 5.513891), also with no AI disclosure
Science result
- Field
- mathematics / number theory / Diophantine approximation
- Problem
- Irrationality measure (exponent) of ζ(2) = π²/6 (open since 2014)
- Result
- μ(ζ(2)) ≤ 5.0495243 (from 5.095412), fully formalized in Lean 4; later improved by humans to < 5.0193784
- AI system
- Claude
- Human role
- Human-led: Kleid ran the parameter search in his own CAS and directed the work; Claude wrote the Lean formalization
- Verification
- Formal proof in Lean 4 (no sorry, standard axioms only); not peer-reviewed
- Status
- confirmed
- Why surprising
- A record in classical Diophantine approximation was published as a ~92k-line AI-written Lean proof with no paper at all.
What happened
Kleid searched the parameter space of Zudilin's Mellin–Barnes construction with qedbook, his own computer-algebra system, using Marcovecchio's pairing theorem to make each candidate tractable. He found a member whose growth rates give the exponent 1 + (42.034 + 15.019)/(29.108 − 15.019) ≈ 5.0495. He then had Claude write a complete Lean 4 proof. Every value computed in qedbook enters the proof as data that Lean's kernel re-checks. The repository says what is and is not proved: the sharper figure 5.04952429 printed by the search is not claimed.
A week later a human preprint beat the bound, citing Kleid's "machine-verified bound … published in September 2026" as the intermediate record.
Why it matters
It is a new way to publish: a record in analytic number theory released as a fully kernel-checked, AI-written formal proof rather than a paper. It also shows the pace of autumn 2026, when an AI-formalized record stood for only a week before a short human paper improved it. The open question is whether qedbook-style search plus AI formalization can now reach the human bound.
Changelog
- 2026-10-05: created (leads run; lead from arXiv 2610.02912)
Related events
- Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help (July–September catalogue) ★★★★
- ζ(5) proved irrational: Aabir Fauzan's Zenodo preprint, the first such result since Apéry's ζ(3) in 1978, is formally verified in Lean within a week, one formalization written by Claude ★★★★★
Sources (5)
- codeGitHub qedbook/zeta2-irrationality-measure: μ(ζ(2)) ≤ 5.0495243, machine-checked in Lean 4
- officialqedbook
- paperarXiv 2610.02912: A new upper bound for the irrationality exponent of ζ(2) (Niedbala Giraudin)
- paperarXiv 2609.26980: A new upper bound for the irrationality exponent of ζ(3) (Niedbala Giraudin)
- paperZudilin (2014): Two hypergeometric tales and a new irrationality measure of ζ(2)
id: 2026-09-25-zeta2-irrationality-measure-claude-lean · updated 2026-10-05 · open in the interactive timeline