ζ(5) Proven Irrational, with Lean Formalization Completed Within Hours

ctjlewis · x · 2026-09-24

Elliot Glazer announced that ζ(5) is in fact irrational, a notable advance on the zeta function's values. Mathematician Moritz Firsching completed a Lean formalization of the result within hours and published the repository. Full proof details are in the linked repository as discussion continues.

Related event: Zeta(5) Proven Irrational, Formalized in Lean Within Hours(4 posts)→

Original post →

More from Research

Research channel →