Leonardo de Moura · 12 min read
When AI writes the world's software, who verifies it? (opens in new tab)
The chief architect of Lean argues that formal mathematical verification becomes essential infrastructure as AI generates more of the world's code. When proof is cheap, it becomes the stronger path to correctness.