After 8 years in AI formalization, Kaiyu Yang asks what happens when it gets cheap

KaiyuYang4 · x · 2026-09-25

Kaiyu Yang has worked on ML for formal theorem proving since 2018, building CoqGym, LeanDojo, and contributing to Goedel-Prover. This 25-minute essay is a personal reflection on those eight years.
The original hope: AI does the creative work while a rigorous formal system like Lean verifies it. The main obstacle was the cost of expressing everything precisely in Lean.
Coding agents like Codex and Claude Code are now collapsing that cost — formalizing results like Fermat's Last Theorem and building large software projects with specs and correctness proofs in Lean.
But that raises a harder question: once a claim is formalized and proven in Lean, how much of the original problem have we actually solved? Sometimes a great deal; sometimes the important part remains unresolved.
Given recent AI agent security incidents and debates on pacing frontier AI, formal verification looks attractive. Yang agrees it could help, but his experience makes him cautious about how much assurance to expect — focusing on the gap between what we can prove and what we need to trust.

More from AGI Musings