Maintaining a library of formal mathematics

Floris van Doorn; Gabriel Ebner; Robert Y. Lewis

doi:10.1007/978-3-030-53518-6_16

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 proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	Intelligent Computer Mathematics
Subtitle of host publication	13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings
Editors	Christoph Benzmüller, Bruce Miller
Publisher	Springer
Pages	251-267
Number of pages	17
ISBN (Electronic)	9783030535186
ISBN (Print)	9783030535179
DOIs	https://doi.org/10.1007/978-3-030-53518-6_16
Publication status	Published - 2020
Event	13th International Conference on Intelligent Computer Mathematics, CICM 2020 - Bertinoro, Italy Duration: 26 Jul 2020 → 31 Jul 2020

Publication series

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

Conference

Conference	13th International Conference on Intelligent Computer Mathematics, CICM 2020
Country/Territory	Italy
City	Bertinoro
Period	26/07/20 → 31/07/20

Funding

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).

Funders	Funder number
Alfred P. Sloan Foundation	G-2018-10067
Horizon 2020 Framework Programme	713999
European Research Council
Nederlandse Organisatie voor Wetenschappelijk Onderzoek	016

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 4 Quality Education

Keywords

Formal mathematics
Library development
Linting

Access to Document

10.1007/978-3-030-53518-6_16

Persistent URL (handle)

Persistent link

Cite this

van Doorn, F., Ebner, G., & Lewis, R. Y. (2020). Maintaining a library of formal mathematics. In C. Benzmüller, & B. Miller (Eds.), Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings (pp. 251-267). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12236 LNAI). Springer. https://doi.org/10.1007/978-3-030-53518-6_16

van Doorn, Floris ; Ebner, Gabriel ; Lewis, Robert Y. / Maintaining a library of formal mathematics. Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings. editor / Christoph Benzmüller ; Bruce Miller. Springer, 2020. pp. 251-267 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{10b611dd105b435bb2675da1d0dc5e01,

title = "Maintaining a library of formal mathematics",

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.",

keywords = "Formal mathematics, Library development, Linting",

author = "\{van Doorn\}, Floris and Gabriel Ebner and Lewis, \{Robert Y.\}",

year = "2020",

doi = "10.1007/978-3-030-53518-6\_16",

language = "English",

isbn = "9783030535179",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "251--267",

editor = "Christoph Benzm{\"u}ller and Bruce Miller",

booktitle = "Intelligent Computer Mathematics",

note = "13th International Conference on Intelligent Computer Mathematics, CICM 2020 ; Conference date: 26-07-2020 Through 31-07-2020",

}

van Doorn, F, Ebner, G & Lewis, RY 2020, Maintaining a library of formal mathematics. in C Benzmüller & B Miller (eds), Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12236 LNAI, Springer, pp. 251-267, 13th International Conference on Intelligent Computer Mathematics, CICM 2020, Bertinoro, Italy, 26/07/20. https://doi.org/10.1007/978-3-030-53518-6_16

Maintaining a library of formal mathematics. / van Doorn, Floris; Ebner, Gabriel; Lewis, Robert Y.
Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings. ed. / Christoph Benzmüller; Bruce Miller. Springer, 2020. p. 251-267 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12236 LNAI).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Maintaining a library of formal mathematics

AU - van Doorn, Floris

AU - Ebner, Gabriel

AU - Lewis, Robert Y.

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

KW - Formal mathematics

KW - Library development

KW - Linting

UR - https://www.scopus.com/pages/publications/85089210017

UR - https://www.scopus.com/pages/publications/85089210017#tab=citedBy

U2 - 10.1007/978-3-030-53518-6_16

DO - 10.1007/978-3-030-53518-6_16

M3 - Conference contribution

AN - SCOPUS:85089210017

SN - 9783030535179

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 251

EP - 267

BT - Intelligent Computer Mathematics

A2 - Benzmüller, Christoph

A2 - Miller, Bruce

PB - Springer

T2 - 13th International Conference on Intelligent Computer Mathematics, CICM 2020

Y2 - 26 July 2020 through 31 July 2020

ER -

van Doorn F, Ebner G, Lewis RY. Maintaining a library of formal mathematics. In Benzmüller C, Miller B, editors, Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings. Springer. 2020. p. 251-267. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2020 Jul 17. doi: 10.1007/978-3-030-53518-6_16

Maintaining a library of formal mathematics

Abstract

Publication series

Conference

Funding

UN SDGs

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this