Mathlib3
Lean 3's obsolete mathematical components library: please use mathlib4
> [!WARNING] > Lean 3 and Mathlib 3 are no longer actively maintained. > It is strongly recommended that you use [mathlib4](https://github.com/leanprover-community/mathlib4) for Lean 4 instead. The project is written primarily in Lean, distributed under the Apache License 2.0 license, first published in 2017. It has gained significant community traction with 1,665 stars and 290 forks on GitHub. Key topics include: formal-mathematics, formal-methods, formal-proofs, lean, proof-automation.
Lean 3's mathlib
[!WARNING]
Lean 3 and Mathlib 3 are no longer actively maintained.
It is strongly recommended that you use mathlib4 for Lean 4 instead.
(If you need to read the old README.md, please see OLD_README.md.)
Contributors
Showing top 12 contributors by commit count.
Related Repositories
lean-dojo/LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
google-deepmind/formal-conjectures
A collection of formalized statements of conjectures in Lean.
LogicalAtomist/principia-rewrite
The Principia Rewrite
eric-wieser/lean-matrix-cookbook
The matrix cookbook, proved in the Lean theorem prover
leanprover-community/LeanProject
A template for blueprint-driven formalization projects in Lean.
YuanheZ/lean-stat-learning-theory
[ICML2026] The first comprehensive Lean 4 formalization of statistical learning theory, featuring Gaussian Lipschitz concentration and Dudley's entropy integral-establishes a reusable foundation for formalizing ML theory.