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
- OpenRSI calls for contributors: turn your research into benchmark tasks for frontier agents — ChengleiSi · 2026-09-24
- PosteriorBench: better reconstruction accuracy can mean worse posterior recovery — AnimaAnandkumar · 2026-09-24
- Third Unitree G1 Humanoid Soccer Demo in One Day Shows Sustained Dribbling With Onboard LiDAR — Darpinian · 2026-09-24
- 30 annotations with GEPA prompt optimization boost lead scorer accuracy 43%, cut cost 5x — CShorten30 · 2026-09-24
- Anthropic biologists: Claude's biology progress in a year is breathtaking, from hypothesis to lab confirmation — Flomerboy · 2026-09-24
- IROS 2026 plenary debate pits 8 experts on robots: generalists vs specialists — siddhss5 · 2026-09-24