Lean creator Leo de Moura on the Collatz kernel exploit and AI-era formal verification
Machine Learning Street Talk · rss · 2026-09-30
Long MLST interview with Leonardo de Moura (creator of Lean, co-creator of Z3) covering: Lean's minimal trusted kernel and independent checkers; the Collatz incident where a purported proof was accepted by both Lean's kernel and nanoda via different bugs in each; reward hacking and safety-by-transparency; Kim Morrison's zlib proof with Claude; AlphaProof and why certificates still matter; Lean 4, dependent types, and Mathlib as infrastructure. 75 min with full timestamps and references.
More from AGI Musings
- Dev mocks AI CLI hype: stop learning to think, race to $1T valuations — arthurcolle · 2026-09-30
- Greg Cook: writing is stored energy, the act of writing is attempted transfer — GregCook2011 · 2026-09-30
- AI is the discipline of building minds, and mathematics is just getting started — burny_tech · 2026-09-30
- Computational functionalism faces the same problem it criticizes in biological naturalism — burny_tech · 2026-09-30
- 'Most People Just Want Slop': Techies Keep Misreading What Normies Want From AI — max_paperclips · 2026-09-30
- "AI will replace everything" takes come from people who never engage with the field — AndyMasley · 2026-09-30