Formalizing Mathematics and Scientific Computing with an Open-Source Theorem Prover

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