What is Lean?

Lean is an interactive theorem prover used for formalizing mathematics and verifying proofs. The material tracks its role in automated formalization and its perceived relevance to AI progress.

• Jun 2026 - Karina Hong noted that Lean’s auto-formalization process caught an implicit assumption in a 50-year-old economic theorem by Robert Aumann, which had never been made explicit.
• Jun 2026 - Grant Sanderson stated that Lean ‘just doesn’t matter that much for the current level of progress in AI.’
• Jun 2026 - Luke Bailey described ‘this new era of verified intelligence’ in connection with Lean.