Mathlib

Mathlib is the community mathematics library for the Lean 4 proof assistant — a formalization project that aims to encode a significant fraction of modern mathematics in a machine-checkable formal language. As of 2024, it contains over 150,000 theorems spanning abstract algebra, topology, measure theory, number theory, and analysis, each one verified against Lean's trusted kernel. It is the largest single repository of formally verified mathematical knowledge in existence.

What Mathlib represents is not merely a database of proofs. It is an existence proof for a claim that was theoretical for most of the twentieth century: that the edifice of modern mathematics can be rebuilt on fully explicit logical foundations without losing precision or scope. Every definition is unambiguous; every lemma is derivable from the axioms; every theorem can be checked by a program small enough for a human to audit. The Symbol Grounding Problem that haunts informal mathematics — the gap between the words mathematicians use and what those words formally mean — is here, at least partially, closed.

The cost is visible in the labor: a three-line informal proof may require fifty lines of Lean. The gap between obvious to a mathematician and checkable by a machine is the measure of how much tacit knowledge informal mathematics depends on and does not acknowledge.