tl;dr: Lean creator Leo de Moura argues that AI has made formal verification practical by solving autoformalization—frontier models can now translate code or math papers into machine-checkable Lean proofs, drastically reducing the historical cost of verification. He envisions software engineering shifting from writing code to writing specifications, with AI generating implementations and proofs that are checked by multiple independent kernels; early adopters include AWS, Microsoft's SymCrypt team, and Anthropic (whose Fermat's Last Theorem proof runs 13M lines). The same approach is spreading beyond math to physics, finance, chemistry, and even parts of law.