The fall of the theorem economy
David Bessis @davidbessis · substack · 2026-04-21 · ★★★ · archived
An influential essay (cross-posted to LessWrong) arguing that AI theorem-proving exposes how mathematics has been misread as theorem production, and predicting an unintelligible 'Mathslop' layer beside Mathlib.
Summary
Bessis, a mathematician and author, argues that the real value of mathematics lies in building human intuition and concepts, and that theorems have served as a proxy for it. AI trained to prove theorems in Lean can win at the proxy while producing proofs that convey little insight. He expects formal mathematics to split into an intelligible layer (Mathlib) and an unintelligible one he calls "Mathslop": results known to be correct through proofs no human understands. Published 2026-04-21 (Substack metadata); Bessis's follow-up X post (Apr 25) had ~95k views.
Archived text
(blog post; summary only)
Related events
All posts · id: 2026-04-21-david-bessis-fall-of-the-theorem-economy