Instead of struggling to write an abstract mathematical specification, developers can write a simple, inefficient, but correct version of their program. This 'naive' implementation can then be used as a formal spec for an AI to generate an optimized version, along with a proof of its equivalence.
Beyond its academic use for formal verification, Lean is a functional programming language used to build substantial software. Its own tooling is written in Lean, and AWS uses it for a half-million-line compiler for AI accelerators, treating its proof capabilities as a valuable bonus.
The primary barrier to adopting formal verification has been the immense cost (often 10x development time) of maintaining proofs as software changes. AI excels at this tedious and difficult task, rewriting and adapting proofs automatically, which is the key change making the practice scalable and mainstream.
A team successfully formalized and simplified a complex proof from Fields Medalist Peter Scholze using Lean. The tool's interactive feedback guided them, allowing them to refactor and improve the mathematics akin to how a programmer refactors code, even without a complete intuitive grasp of the subject.
Because Lean is written in Lean, it's highly extensible. Users can write metaprograms in the same file as their proofs to build custom automation, visualizations, or entire domain-specific languages (DSLs). One mathematician even created a point-and-click, English-like proof interface this way without modifying Lean's core.
Unlike systems with Higher-Order Logic, Lean's Dependent Type Theory allows types to depend on values. This enables creating functions that require a proof as an argument (e.g., a division function that takes x, y, and a proof that y != 0), baking critical invariants directly into the type system.
The act of creating a formal proof for a piece of software forces a level of rigor that surpasses even implementing it from scratch. This newfound confidence and clarity allows engineers to pursue aggressive optimizations without the fear of introducing subtle bugs, which they would otherwise avoid due to uncertainty.
Instead of writing code and then tests, developers could define precise mathematical properties. AI would then synthesize both the program and a formal proof that the program meets those specifications, ensuring correctness by design and flipping the current code-first paradigm.
A project demonstrated an AI successfully translating the zlib C library into the Lean language and proving its core compression/decompression property is correct. This shows AI's capability to handle real-world, complex codebases for formal verification, a task previously deemed infeasible.
Users describe working with Lean as playing their 'favorite computer game.' The process of incrementally solving small proof goals in an interactive environment provides a constant 'buzz' and sense of accomplishment, which makes the difficult task of formal verification highly engaging and addictive for problem-solvers.
Formal verification tooling must cater to two distinct proof shapes. Mathematical theorems (like Fermat's Last Theorem) have very small statements but incredibly deep, complex proofs. In contrast, software verification involves proving properties about massive statements (the code), but the proofs themselves are relatively shallow.