Skip to Main Content
Lightning Talk Intermediate

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

Approved
Session Description

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.

Key Takeaways

  • 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

References

https://lean-lang.org/
https://github.com/leanprover
https://leanprover-community.github.io/
https://leanprover-community.github.io/mathlib_stats.html
https://leanprover-community.github.io/mathlib4_docs/

Session Categories

Story of a FOSS project - from inception to growth
Contributing to FOSS
Introducing a FOSS project or a new version of a popular project
Community
Knowledge Commons (Open Hardware, Open Science, Open Data etc.)
Which track are you applying for?
FOSS in Science Devroom

Speakers

Sagnik Saha
Independent consultant / Researcher
https://thesagniksaha.com
Sagnik Saha

Sagnik is a mathematician and holds an MS in Mathematics and Biology. His academic work is centered around computational number theory, arithmetic geometry, and algorithmic bioimaging. As a consultant, he works on projects using multidisciplinary tools at the intersection of tech, research, art, and scicomm. Sagnik is a passionate advocate for math education, open-source tools, and communities around science and tech research. Beyond this, he also works in film and design production, partnering with organizations to amplify stories for science, tech, and community initiatives.

Reviews

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.

Reviewer #1 Approved

Sounds like a niche and fun OSS project. No one is complaining about learning a new language.

Reviewer #2 Approved
Reviewer #3 Approved