The Lean mathematical library
arXiv:1910.09336 · doi:10.1145/3372885.3373824
Abstract
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 us here.
References in corpus (5)
- Formalising perfectoid spaces
- A Formal Proof of the Independence of the Continuum Hypothesis
- A formal proof of Hensel's lemma over the p-adic integers
- Technologies for "Complete, Transparent & Interactive Models of Math" in Education
- Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
Cited by in corpus (20)
- Formalising perfectoid spaces
- MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
- Formalizing of Category Theory in Agda
- Maintaining a Library of Formal Mathematics
- A Formal Proof of PAC Learnability for Decision Stumps
- Schemes in Lean
- Formalizing the Ring of Witt Vectors
- Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
- Validating Mathematical Structures
- Formalizing Geometric Algebra in Lean
- Parallel Verification of Natural Deduction Proof Graphs
- Trocq: Proof Transfer for Free, With or Without Univalence
- Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
- Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms
- Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
- Computational Synthetic Cohomology Theory in Homotopy Type Theory
- Formalising the local compactness of the adele ring
- Derandomization with Pseudorandomness
- Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)
- On Planarity of Graphs in Homotopy Type Theory