The Lean mathematical library

Along with a number of other contributors, I have written a paper about the Lean mathematical library. The paper describes a large-scale, open project to which 68 people (and counting) have contributed. Rather than attribute the paper to some subset of this group, we decided to release it as a community effort. (Update, Nov 28: our paper has been accepted at CPP!)

A huge amount of work has gone into building mathlib and it’s great to see it documented. One aspect of the project that we emphasize in the paper is the collaboration between people with different academic backgrounds and interests. Using mathlib is pleasant because it’s designed to support many people doing different things. Mathematics is a heterogeneous field, and many practicing mathematicians (let alone computer scientists) see only a small fragment of it. If our aim is to develop a system, library, and environment to accommodate mathematics, broadly speaking, we need participants from all corners.