Lean is an open-source, functional programming language that brings new levels of rigor, collaboration, and accessibility to mathematical sciences. Developed in 2013 to tackle complex mathematical problems, Lean is bridging the gap between automated and natural theorem proving. In this talk, I will introduce Lean, trace its FOSS story, and explore adoption case studies that are going to impact the future of machine-assisted mathematics.
Through demos, I will illustrate Lean's programming ecosystem, fundamental components of its interactive workflow, and how proofs are generated and verified. We will survey Mathlib, Lean's open-source formalized mathematics library maintained by a large community of mathematicians and students who actively contribute to the project and have already formalized over 200 thousand theorems.
By the end of the session, attendees will have a clear picture of Lean's capabilities and how formal theorem proving can accelerate research and pedagogy in STEM. The session also aims to show how Lean's open, collaborative model makes advanced mathematics accessible to a large audience and motivate individuals to participate and contribute to this growing open-source community.
How the formalization of mathematical proofs can accelerate collaborative research
Why is FOSS-driven effort crucial for open mathematics
Resources to get started with formalization and machine-assisted theorem proving
Navigation through an open-source mathematical library and contribution guidelines
The proposal doesn't explicitly justify the need for Theorem Prover, and given the relatively niche topic, it'll be good to spend a few minutes introducing why Theorem Provers are necessary in the first place.
The proposal doesn't mention this explicitly, but it'll be valuable to show a few examples of theorems proved using Lean, from beginner to intermediate and advanced.
It'll be great if the proposer also highlights how newcomers could contribute theorem proofs to the community, because the proposer already highlighted the fact that an active community has created a significant number of theorem proofs.
P.S. A call out to Terry Tao and some of his Lean theorem proofs might be appreciated.
Sounds like a niche and fun OSS project. No one is complaining about learning a new language.