Uploaded February 2024 | Updated September 2026, 11 hours ago
Abstract: The domains of mathematics and software engineering witness a rapid increase 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. Lean functions as an integrated development environment wherein mathematical proofs undergo interactive construction and verification. Concurrently, software undergoes mechanical verification. A salient feature of Lean is its inherent extensibility, permitting users to craft their extensions within Lean's own framework. This extensible design paradigm fosters decentralized innovation, wherein practitioners are not merely users but active contributors.
In this presentation, we 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.
Bio: Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. In his spare time, he dedicates himself to serving as the Chief Architect of the Lean FRO, a non-profit organization that he proudly co-founded alongside Sebastian Ullrich. He is also honored to hold 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 several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. Leo's work in automated reasoning has been acknowledged with a series of prestigious awards, including the CAV, Haifa, and Herbrand awards, as well as the Programming Languages Software Award by the ACM. Leo's work has also been reported in the New York Times and many popular science magazines such as Wired, Quanta, and Nature News.
Abstract: The domains of mathematics and software engineering witness a rapid increase 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. Lean functions as an integrated development environment wherein mathematical proofs undergo interactive construction and verification. Concurrently, software undergoes mechanical verification. A salient feature of Lean is its inherent extensibility, permitting users to craft their extensions within Lean's own framework. This extensible design paradigm fosters decentralized innovation, wherein practitioners are not merely users but active contributors.
In this presentation, we 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.
Bio: Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. In his spare time, he dedicates himself to serving as the Chief Architect of the Lean FRO, a non-profit organization that he proudly co-founded alongside Sebastian Ullrich. He is also honored to hold 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 several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. Leo's work in automated reasoning has been acknowledged with a series of prestigious awards, including the CAV, Haifa, and Herbrand awards, as well as the Programming Languages Software Award by the ACM. Leo's work has also been reported in the New York Times and many popular science magazines such as Wired, Quanta, and Nature News.
