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

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.

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
PublisherSpringer
Pages251-267
Number of pages17
ISBN (Electronic)9783030535186
ISBN (Print)9783030535179
DOIs
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

Conference

Conference13th International Conference on Intelligent Computer Mathematics, CICM 2020
CountryItaly
CityBertinoro
Period26/07/2031/07/20

Keywords

  • Formal mathematics
  • Library development
  • Linting

Fingerprint

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

Cite this