Lean创始人访谈：Handwritten Math Will Change Dramatically

Dijkstra's quote emphasized the fundamental value of formal verification: tests can reveal bugs but cannot prove their nonexistence. Lean serves a dual purpose, functioning both as a programming language for writing code and as a proof system for verifying code properties with machine-checkable proofs. It provides absolute correctness guarantees and includes multiple independent checkers.

Lean's programming language and proof assistant nature stem from Dependent Type Theory-based proof assistants like Rocq/Coq and Lean. Software verification can follow two main paths: shallow embedding, where other languages are mapped into Lean for verification using tools like Rust-to-Lean translators, or deep embedding/semantic modeling, where languages like C are represented as data structures in Lean and their properties are stated and reasoned about.

The distinction between testing and proof is crucial: comprehensive test suites only cover limited scenarios and may miss edge cases, while formal proofs cover all possible situations, ensuring "bug nonexistence." An example is Zlib's compression library, where AI translated C code into Lean, proving the critical property that compressed data decompresses to the original data. This was completed in just one week, with further performance optimization possible without compromising existing proofs.

Specifying properties is discussed, with varying costs depending on the program. Writing a correct but inefficient specification can serve as a baseline, while AI can generate optimized versions that are proven equivalent. Companies like Jane Street have begun investing in formal verification for critical systems like the seL4 microkernel. However, the high cost of manual proof development has decreased significantly with AI, which excels at writing and maintaining formal proofs.

Lean is more than just a proof assistant; it's a production-level programming language. AWS runs an AI-optimized compiler with millions of lines of Lean code, providing additional proof benefits. Lean offers a near-native developer experience, with a build system similar to Rust's Cargo and an editor integrated with VS Code. Its unique Info View displays proof states in real-time, akin to a game's progress bar.

The core trust issue in Lean concerns trusting its core kernel. While the core is extensive and frequently changes, only a small kernel is essential to verify. Mario Carneiro implemented a "Lean for Lean" kernel in Lean, proving its consistency with Lean semantics. Other third-party kernels exist, also verified for consistency.

Formalizing mathematics has seen remarkable breakthroughs, including an IMO gold medalist AI-generated proof and a Unit Distance Conjecture formalized by AI in just two weeks. The Lean Mathematics Library (mathlib) has made significant strides, with Terence Tao using Lean to rediscover passion for mathematics. The key to Lean's appeal is its interactive, game-like proof experience, reminiscent of puzzle-solving, keeping enthusiasts deeply engaged.

AI can find new proofs but hasn't yet created new mathematical theories. While AI has discovered counterexamples refuting conjectures in Lean, proposing entirely new mathematical concepts remains beyond its current capabilities. Formalization is crucial for safety-critical systems or when human understanding is incomplete, providing confidence that "bug nonexistence" is assured.

In the next 3-5 years, formal verification and "handwritten math" will undergo significant transformation. Large language models are starting to integrate formal verification into their training pipelines, with promising results. Functional languages like Lean and Rocq are expected to become more mainstream, driven by AI-assisted coding and specification.

Handwritten math is likely to diminish as a dominant practice, replaced by AI-assisted, hybrid workflows where AI handles repetitive, non-creative tasks, and humans focus on defining specifications and intentions. Humans will remain essential in connecting mathematical formalisms to the real world, ensuring practical applications and usability.