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.
| Popular series | |
|---|---|
 | The largest compilation of the best free and open source software in the universe. Each article is supplied with a legendary ratings chart helping you to make informed decisions. |
 | Hundreds of in-depth reviews offering our unbiased and expert opinion on software. We offer helpful and impartial information. |
 | The Big List of Active Linux Distros is a large compilation of actively developed Linux distributions. |
 | Replace proprietary software with open source alternatives: Google, Microsoft, Apple, Adobe, IBM, Autodesk, Oracle, Atlassian, Corel, Cisco, Intuit, and SAS. |
 | Awesome Free Linux Games Tools showcases a series of tools that making gaming on Linux a more pleasurable experience. This is a new series. |
 | Machine Learning explores practical applications of machine learning and deep learning from a Linux perspective. We've written reviews of more than 40 self-hosted apps. All are free and open source. |
 | New to Linux? Read our Linux for Starters series. We start right at the basics and teach you everything you need to know to get started with Linux. |
 | Alternatives to popular CLI tools showcases essential tools that are modern replacements for core Linux utilities. |
 | Essential Linux system tools focuses on small, indispensable utilities, useful for system administrators as well as regular users. |
 | Linux utilities to maximise your productivity. Small, indispensable tools, useful for anyone running a Linux machine. |
 | Surveys popular streaming services from a Linux perspective: Amazon Music Unlimited, Myuzi, Spotify, Deezer, Tidal. |
 | Saving Money with Linux looks at how you can reduce your energy bills running Linux. |
 | Home computers became commonplace in the 1980s. Emulate home computers including the Commodore 64, Amiga, Atari ST, ZX81, Amstrad CPC, and ZX Spectrum. |
 | Now and Then examines how promising open source software fared over the years. It can be a bumpy ride. |
 | Linux at Home looks at a range of home activities where Linux can play its part, making the most of our time at home, keeping active and engaged. |
 | Linux Candy reveals the lighter side of Linux. Have some fun and escape from the daily drudgery. |
 | Getting Started with Docker helps you master Docker, a set of platform as a service products that delivers software in packages called containers. |
 | Best Free Android Apps. We showcase free Android apps that are definitely worth downloading. There's a strict eligibility criteria for inclusion in this series. |
 | These best free books accelerate your learning of every programming language. Learn a new language today! |
 | These free tutorials offer the perfect tonic to our free programming books series. |
 | Linux Around The World showcases usergroups that are relevant to Linux enthusiasts. Great ways to meet up with fellow enthusiasts. |
 | Stars and Stripes is an occasional series looking at the impact of Linux in the USA. |