Maintaining a library of formal mathematics. (English) Zbl 1455.68262
Benzmüller, Christoph (ed.) et al., Intelligent computer mathematics. 13th international conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12236, 251-267 (2020).
Summary: 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.
For the entire collection see [Zbl 1452.68005].
For the entire collection see [Zbl 1452.68005].
MSC:
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 68V30 | Mathematical knowledge management |
