← All papers
Maintaining a Library of Formal Mathematics
cs.PL
Apr 7, 2020 · v2
TL;DR
Describes tooling for maintaining mathlib including linters and documentation generators.
Abstract
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience.
Problem
The Lean mathematical library mathlib is developed by contributors with varied backgrounds and experience levels, making it challenging to maintain quality and lower the barrier to entry.
Approach
The authors develop tooling for the mathlib library that checks proof developments for subtle mistakes and generates documentation suited for a varied audience. These tools help review contributions and enforce coding standards.
Results
The tooling lowers the barrier of entry for contributors and lessens the reviewing burden for the mathlib community, supporting maintenance of a large-scale formal mathematics library.