Mathlib — Lean
Contributing to Mathlib, a worldwide collaborative effort to formalize all of mathematics in the Lean theorem prover.
Overview
Mathlib is the mathematical library for the Lean theorem prover — a massive, worldwide collaborative project to formalize all of mathematics in a language that a computer can verify. Every definition, lemma, and theorem is machine-checked, making errors impossible.
What is Mathlib?
Mathlib contains hundreds of thousands of formalized mathematical statements spanning algebra, analysis, topology, number theory, and more. It is one of the largest formalization efforts in the world, with contributions from mathematicians and computer scientists across the globe.
My Involvement
Building on my master’s thesis work in Lean 4, I contribute to Mathlib by formalizing results and improving existing proofs. Working in this codebase means writing mathematics that is both human-readable and machine-verified — a unique discipline that sharpens both mathematical and programming skills.