Maintaining a library of formal mathematics

Floris van Doorn, Gabriel Ebner, Robert Y. Lewis*

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review


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.

Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings
EditorsChristoph Benzmüller, Bruce Miller
Number of pages17
ISBN (Electronic)9783030535186
ISBN (Print)9783030535179
Publication statusPublished - 2020
Event13th International Conference on Intelligent Computer Mathematics, CICM 2020 - Bertinoro, Italy
Duration: 26 Jul 202031 Jul 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12236 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference13th International Conference on Intelligent Computer Mathematics, CICM 2020


The first author is supported by the Sloan Foundation (grant G-2018-10067). The second and third authors receive support from the European Research Council (ERC) under the European Union?s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka) and from the Dutch Research Council (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

FundersFunder number
Alfred P. Sloan FoundationG-2018-10067
Horizon 2020 Framework Programme713999
European Research Council
Nederlandse Organisatie voor Wetenschappelijk Onderzoek016


    • Formal mathematics
    • Library development
    • Linting


    Dive into the research topics of 'Maintaining a library of formal mathematics'. Together they form a unique fingerprint.

    Cite this