Lean 4 formalization of the ζ(5) irrationality proof completed and open-sourced
AlexKontorovich · x · 2026-09-24
Mathematician Moritz Firsching reports completing a Lean 4 formalization of the recent preprint claiming ζ(5) is irrational, with the Zeta5 repo now public.
- The project formalizes Irrational (riemannZeta 5), following A. Fauzan's September 2026 preprint, via an Apery-style rational approximation construction
- The prime number theorem estimate (θ id) is imported from the PrimeNumberTheoremAnd library
- Solution.lean discharges the benchmark statement from Formal Conjectures; CI runs Comparator to verify the proof only depends on propext, Classical.choice, and Quot.sound
- Toolchain: Lean v4.34.0-rc1, pinned Mathlib commit, Apache 2.0 license
The result moves ζ(5) irrationality from a fresh preprint claim to machine-verified fact.
Related event: Zeta(5) Proven Irrational, Formalized in Lean Within Hours(4 posts)→
More from Research
- Autonomous agent edits just 1,024 weights to lift Qwen3.5 0.8B from 7.4% to 37.4% on MATH-500 — VictorSanh · 2026-11-12
- Gait dataset labeled by encounter, spanning pre-op to 3 months post-TKA — zawthet · 2026-11-12
- Walking alignment measured 2.5-3.1° more neutral than X-ray, iPad gait study finds — zawthet · 2026-11-12
- MIT's Tegmark coins 'formal-washing': Signal protocol proof is far from complete — tegmark · 2026-11-12
- Signal formal verification hits 80%, Tegmark says Wired overstated completion — tegmark · 2026-11-12
- Category-theoretic framework asks: when does a physical system actually compute? — neurovium · 2026-11-12