Mathlib

Mathlib is an open-source mathematics library for the Lean theorem prover, built by a community of mathematicians and developers. It contains definitions and theorems from algebra, analysis, topology, number theory and other fields, written as formal proofs that Lean can check.

Because it lets authors of formal proofs reuse definitions and theorems that are already verified, it is widely used in the formalization of mathematics and in research on AI-based theorem proving.

This entry is based on AIPOST articles and widely known facts. If something is wrong, please send us a correction request.