The Lean mathematical library, mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant.
Mathlib is a user maintained library for the Lean theorem prover. It contains both programming infrastructure and mathematics, as well as tactics that use the former and allow to develop the latter. This project is very active, with many contributors and daily activity.
This is free and open source software.
Website: leanprover-community.github.io
Support: GitHub Code Repository
Developer: Many contributors
License: Apache License 2.0
mathlib4 is written in Lean. Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming.
A proof assistant is a piece of software that provides a language for defining objects, specifying properties of these objects, and proving that these specifications hold. The system checks that these proofs are correct down to their logical foundation.
These tools are often used to verify the correctness of programs. But they can also be used for abstract mathematics, which is something of interest to the mathlib community. In a formalization, all definitions are precisely specified and all proofs are virtually guaranteed to be correct.
Related Software
| Proof Assistants | |
|---|---|
| Coq | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Agda | Interactive system for writing and checking proofs |
| Lean | Programming language and theorem prover |
| Matita | Experimental, interactive theorem prover |
Read our verdict in the software roundup.
 Explore our comprehensive directory of recommended free and open source software. Our carefully curated collection spans every major software category.This directory is part of our ongoing series of informative articles for Linux enthusiasts. It features hundreds of detailed reviews, along with open source alternatives to proprietary solutions from major corporations such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. You’ll also find interesting projects to try, hardware coverage, free programming books and tutorials, and much more. Discovered a useful open source Linux program that we haven’t covered yet? Let us know by completing this form. |