Abstract:

The Lean theorem prover is gaining increasing attention within the mathematical community as a robust tool for constructing precise, machine-checkable proofs. Supported by a growing ecosystem of users and a comprehensive library of formalized results, Lean is enabling new forms of collaboration and verification in mathematics. In this talk, I will introduce the Lean system and discuss its applications in formalizing modern mathematics, with a focus on the Mathlib library, a large and actively maintained repository of formalized theorems. I will also highlight recent developments in proof automation and AI-assisted formalization that make working in Lean more efficient. Finally, I will present the role of the Lean Focused Research Organization (FRO), a non-profit committed to supporting the development and long-term sustainability of the Lean ecosystem. This talk aims to provide a clear picture of how Lean is being used today and its potential to influence the future of mathematical research and education.

Abstract: The formal verification system Lean represents a remarkable convergence of mathematical logic, computer science, and artificial intelligence. This talk explores how Lean is transforming the way we think about mathematical proof, software correctness, and reasoning. At its core, Lean provides a precise language for expressing mathematical statements and proofs in a way that can be verified by computer. But it is much more than just a proof checker: it serves as a platform for collaborative mathematics, a framework for verified software development, and an experimental ground for AI-assisted theorem proving.

The presentation will demonstrate how the mathematical community is using Lean to formalize complex mathematical proofs, enabling unprecedented levels of collaboration and verification. In software development, examples will show how Lean's dependent type theory allows developers to write provably correct programs and implement aggressive optimizations with confidence. The discussion will conclude with exciting developments at the intersection of Lean and AI, including development of AI-powered proof automation. Throughout, these developments illustrate how Lean addresses long-standing challenges in mathematics, software reliability, and AI trustworthiness.