Machine-Checked Proofs and the Rise of Formal Methods in Mathematics | Theoretically Speaking

Leonardo de Moura (AWS)
https://simons.berkeley.edu/events/ma...
Theoretically Speaking

The domains of mathematics and software engineering are witnessing a rapid escalation in complexity. As generative artificial intelligence emerges as a potential force in mathematical exploration, a pressing imperative arises: ensuring the correctness of machine-generated proofs and software constructs.

The Lean proof assistant addresses these challenges. Conceptualized as a nexus for mathematics and software, Lean functions as an integrated development environment in which mathematical proofs undergo interactive construction and verification. Concurrently, software undergoes mechanical verification. A salient feature of Lean is its inherent extensibility, permitting users to imbue it with bespoke extensions, crafted within Lean's own framework. This extensible design paradigm fosters an ethos of decentralized innovation, wherein practitioners are not merely users but active contributors.

In this presentation, Leonardo de Moura will describe Lean's contributions to the mathematical domain, its extensive mathematical library encapsulating over a million lines of formalized mathematics, its pivotal role in cutting-edge mathematical endeavors such as the Liquid Tensor Experiment, its impact on mathematical education, and its role in AI for mathematics.

Leonardo de Moura is a senior principal applied scientist in the Automated Reasoning Group at AWS. In his spare time, he serves as the chief architect of the Lean FRO, a nonprofit organization that he cofounded with Sebastian Ullrich. He also holds a position on the Board of Directors at the Lean FRO, where he actively contributes to its growth and development. Before joining AWS in 2023, he was a senior principal researcher in the RiSE group at Microsoft Research, where he worked for 17 years, starting in 2006. Prior to that, he worked as a computer scientist at SRI International. His research areas are automated reasoning, theorem proving, decision procedures, SAT, and SMT. He is the main architect of Lean, Z3, Yices 1.0, and SAL. Lean is an open-source theorem prover and programming language. Z3 and Yices are SMT solvers, and SAL (Symbolic Analysis Laboratory) is an open-source tool suite that includes symbolic and bounded model checkers, as well as automatic test generators. Z3 has been open-sourced (under the MIT license) since the beginning of 2015.