The lean mathematical library

By The mathlib Community. 2019

385 citations recorded by the source corpus.

This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led to its development.

Subfields: Artificial Intelligence, Information Systems, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

In Program Analysis & Verification

Citations in the corpus

Llemma: An Open Language Model For Mathematics (2023, methodology): “We extract a dataset of (tactic state, next tactic) pairs from Mathlib 4 (mathlib Community, 2020) using the lean-training-data (Morrison, 2023) tool.”
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics (2021, background): “4% pass rate on held-out test statements from mathlib , Lean’s mathematical library (mathlib Community, 2020).”
The Lean 4 Theorem Prover and Programming Language (2021, methodology): “In 2017, using Lean 3, a community of users with very different backgrounds started the Lean mathematical library project mathlib [13].”
Proof Artifact Co-training for Theorem Proving with Language Models (2021, background): “The primary repository of formalized mathematics in Lean is mathlib (mathlib, 2020).”
Mathematical Capabilities of ChatGPT (2023, background): “Finally, we would also like to mention the field of formalized mathematics, where large databases that encode advanced mathematical concepts exist, e.g., the Lean Mathematical Library [48].”
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, background): “Formal statements are expressed in the Lean 3 theorem prover [de Moura et al., 2015], and depend on Lean’s mathlib [mathlib Community, 2020].”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, background): “1 Bottom ): Given the current state, it generates a tactic conditioning on a small number of premises retrieved from Lean’s math library, mathlib [25].”
LLMSTEP: LLM proofstep suggestions in Lean (2023, methodology): “By default, LLMSTEP uses a Pythia 2.8b language model [4] fine-tuned on (state, next-tactic) examples extracted from Lean Mathlib [9] via the LeanDojo Benchmark 4 dataset [19, 18].”