← All papers
The Lean mathematical library
cs.LO
Oct 21, 2019 · v2
TL;DR
Describes the architecture, design, and social organization of Lean's mathlib library.
Abstract
This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. 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.
Problem
Building a unified, community-driven library of formalized mathematics requires careful architectural decisions about foundations, structure hierarchies, automation, and social organization.
Approach
Mathlib is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. It uses dependently typed foundations, focuses on classical mathematics, employs an extensive hierarchy of structures, and leverages both large-scale and small-scale automation with distributed organization.
Results
The paper describes the architecture, design decisions, and social organization that produced mathlib as a comprehensive formal mathematics library used by the Lean community.