2-billion-line Lean proofs: mathematicians debate proof without understanding
Singularitarian · x · 2026-09-09
Aram Pell asks what we actually learn from a 2-billion-line Lean proof of the Riemann Hypothesis, contrasting FLT's 13M-line formalization that still has a human-readable spine. Mathematician Alex Kontorovich pushes back: he'd iterate with AI on Lean proofs to compress and understand them, arguing formalization opens new paths to human understanding.
Related event: Two-Billion-Line Lean Proof Sparks Debate: Does Proof Equal Understanding?(2 posts)→
More from AGI Musings
- Anthropic Researcher Puts AI Extinction Risk Above 10% This Decade, Admits No Alignment Plan — SIGKITTEN · 2026-09-09
- Prediction: Humanoid Robots Will Be Under 10% of Workers in Physical Jobs Even in 5 Years — scottleibrand · 2026-09-09
- Anthropic Researcher's >10% AI Extinction Claim Goes Viral on X — builderjaydub · 2026-09-09
- Satire Skewers AI Labs: 'Models Might Kill You' but First Fund the $1T IPO — zetalyrae · 2026-09-09
- Meme Take: The Archons Were the First AI Safetyists — SydSteyerhart · 2026-09-09
- 10,000 agents for 88 hours equal 100 PhD-years of math work — beffjezos · 2026-09-09