Alex Kontorovich: 'WOW!! Zeta(5) is irrational! Here's a Lean formalization'
Alex Kontorovich @AlexKontorovich · x · 2026-09-23 · ★★★ · archived
Announces the complete Lean formalization (mo271/zeta5) of the ζ(5) proof (~74k views).
Summary
Kontorovich links github.com/mo271/zeta5 and adds "Amazing what we'll learn (with AI help)".
Archived text
WOW!! Zeta(5) is irrational! Here's a Lean formalization: https://t.co/QtqzxUu0fa Amazing what we'll learn (with AI help)
likes 496 · replies 23 (at fetch time)
Archived 2026-10-05 via syndication.
Related events
All posts · id: 2026-09-23-kontorovich-zeta5-lean-formalization