ζ(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

2026-09-17★★★★★after cutoffscienceAalto UniversityGoogle DeepMindAnthropicconfidence: high

On Sept 17, 2026 Aabir Fauzan (Aalto University) posted "ζ(5) is irrational" on Zenodo. It proves that the value ζ(5) is irrational, the first irrationality proof for a specific odd zeta value since Apéry's ζ(3) (1978). By Sept 23 a complete, sorry-free Lean 4 formalization by Google DeepMind's Moritz Firsching was checked by Comparator against DeepMind's Formal Conjectures statement. A second, independent formalization was written by Claude Opus 5/5.5 agents in Claude Code under Dan Romik. How much AI was used in the paper itself is disputed: the author discloses only supporting use, while Frank Calegari says it looks "almost entirely AI generated".

Key facts

Preprint: A. Fauzan, 'ζ(5) is irrational', Zenodo 10.5281/zenodo.22826419, Sept 17, 2026; posted on Zenodo, not arXiv (about 16.8k views and 2.4k downloads by Oct 5). The record calls it the initial presentation, with a full manuscript and arXiv version to follow
Method (abstract): integer polynomials Q_n of degree 37n with 0 < Q_n(ζ(5)) < exp(−139n²/5), built as rationally normalized Hankel determinants with a positive moment representation and logarithmic-energy estimates. It also gives the irrationality measure bound |ζ(5) − a/b| > b^−260
Before this: Ball–Rivoal (infinitely many odd zeta values are irrational) and Zudilin (at least one of ζ(5), ζ(7), ζ(9), ζ(11) is irrational), but no specific odd value beyond ζ(3)
Paper's AI disclosure: 'A generative AI tool was used in a supporting role for editing the exposition, proofreading, LaTeX preparation, and consistency checks of the arguments, calculations, and references'
Frank Calegari (Sept 24): 'The paper I saw gives me the impression of being almost entirely AI generated (if so, it then comes with a very dishonest disclosure), but never mind, thanks for the compute!' He traces the key ideas to Prévost and Prévost–Rivoal
Lean formalization 1 (github.com/mo271/zeta5, Moritz Firsching, Google DeepMind; first commit Sept 23): complete with no sorry, axioms only propext, Classical.choice and Quot.sound. CI runs Comparator against Formal Conjectures' RiemannZetaValues.irrational_five. It deviates from the paper in three local estimates (rank loss r, cutoff M = 400) but still proves irrationality. How it was produced is not stated
Lean formalization 2 (github.com/danromik/zeta5-irrationality): 70 files, about 29,400 lines, no sorry; the prime number theorem is assumed as an axiom. README: 'The Lean code and the documentation were written by Claude (Anthropic), using the models Claude Opus 5 and Claude Opus 5.5, working as multi-agent workflows in Claude Code directed by Dan Romik'. Its pre-formalization audit found one inequality (p. 10) stated without proof and supplied a proof
Other efforts: an 'autonomous' formalization project (long-mathematics/zeta5-irrationality, Christopher D. Long) and a copy in Vilin97/lean-pool. One write-up reports the method handles ζ(k) for k = 2, 3, 4, 5 with changed parameters
Reactions: Elliot Glazer (Sept 22, ~81k views): 'zeta(5) has very likely been proven irrational … I had Astra study the argument, and it fully vouches for its correctness'. Alex Kontorovich (Sept 23, ~74k views): 'WOW!! Zeta(5) is irrational! … Amazing what we'll learn (with AI help)'

Science result

Field: mathematics / number theory (irrationality of zeta values)
Problem: Irrationality of ζ(5) = Σ 1/n⁵ (open since Apéry's 1978 proof for ζ(3); Euler-era question) (open since 1978)
Result: ζ(5) is irrational, with integer polynomials Q_n of degree 37n satisfying 0 < Q_n(ζ(5)) < exp(−139n²/5), and irrationality measure at most 260.
AI system: Claude Opus 5, Claude Opus 5.5, Claude Code, unnamed generative AI tool (paper)
Human role: Paper by a single human author who discloses AI only for editing and consistency checks (disputed by Calegari). One Lean formalization was written by Claude agents directed by Dan Romik; the other, by Moritz Firsching, does not say how it was produced.
Verification: Formal proof in Lean 4/Mathlib (two independent sorry-free formalizations; one checked by Comparator against DeepMind's Formal Conjectures statement, the other assumes the prime number theorem as an axiom); not yet peer-reviewed
Status: confirmed
Why surprising: A decades-old problem on a famous constant fell to an unknown author posting on Zenodo, and within a week machines had checked the proof, before most experts had read it.

What happened

Apéry's 1978 proof that ζ(3) is irrational was the last time a specific odd zeta value was shown to be irrational. Later work (Rivoal, Ball–Rivoal, Zudilin) proved only statements about families, such as "at least one of ζ(5), ζ(7), ζ(9), ζ(11) is irrational". On Sept 17, 2026 Aabir Fauzan, giving an Aalto University address and with no earlier research papers, posted a 31-page proof for ζ(5) on Zenodo. Commentators guessed he had no arXiv endorsement.

Verification was unusually fast. Elliot Glazer publicised the paper on Sept 22. On Sept 23 Moritz Firsching (Google DeepMind, a maintainer of the Formal Conjectures benchmark) pushed a complete Lean 4 formalization, and Alex Kontorovich announced it. Comparator CI then confirmed that it proves exactly the benchmark statement irrational_five with only the standard axioms. A separate formalization by Dan Romik was, by its README, written entirely by Claude Opus 5 and Opus 5.5 agents in Claude Code. It was done without consulting the other formalization, and its audit filled one gap in the paper.

The AI role in finding the proof is unclear. The paper's disclosure is limited to editing, LaTeX and consistency checks. Frank Calegari wrote that the paper looks "almost entirely AI generated" and, if so, the disclosure is "very dishonest". He then used ChatGPT to trace where its ideas came from. Andreas Holmstrom classifies it as "Human + AI (supporting role)". No AI system has been named as the author of the argument, and Fauzan has made no public statement that we found.

Why it matters

It is the most famous number-theory result of the AI-assisted 2026 wave: a problem experts had worked on for about 48 years. It was settled in a non-traditional venue and machine-verified in Lean within a week, with AI agents doing at least one formalization. That pattern (preprint, then Lean, then expert reading) reverses the usual peer-review order. The paper has not been refereed, and the ZFC-level guarantee rests on the Lean checks, one of which assumes the prime number theorem.

Changelog

2026-10-05: created (21:30 full run, from the URGENT lead found while processing the ζ(2) lead; the dataset had missed it since Sept 17)

Related events

Sources (10)

id: 2026-09-17-zeta-5-irrational-fauzan-lean-verified · updated 2026-10-05 · open in the interactive timeline