A survey of languages for formalizing mathematics

Kaliszyk C, Rabe F (2020)

Publication Type: Conference contribution

Publication year: 2020

Journal

Lecture Notes in Computer Science Springer Verlag

Publisher: Springer

Book Volume: 12236 LNAI

Pages Range: 138-156

Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Event location: Bertinoro IT

ISBN: 9783030535179

DOI: 10.1007/978-3-030-53518-6_9

Abstract

In order to work with mathematical content in computer systems, it is necessary to represent it in formal languages. Ideally, these are supported by tools that verify the correctness of the content, allow computing with it, and produce human-readable documents. These goals are challenging to combine and state-of-the-art tools typically have to make difficult compromises. In this paper we discuss languages that have been created for this purpose, including logical languages of proof assistants and other formal systems, semi-formal languages, intermediate languages for exchanging mathematical knowledge, and language frameworks that allow building customized languages. We evaluate their advantages based on our experience in designing and applying languages and tools for formalizing mathematics. We reach the conclusion that no existing language is truly good enough yet and derive ideas for possible future improvements.

Authors with CRIS profile

Florian Rabe Professur für Wissensrepräsentation und -verarbeitung

Involved external institutions

Leopold-Franzens-Universität Innsbruck / University of Innsbruck AT Austria (AT)

How to cite

APA:

Kaliszyk, C., & Rabe, F. (2020). A survey of languages for formalizing mathematics. In Christoph Benzmüller, Bruce Miller (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 138-156). Bertinoro, IT: Springer.

MLA:

Kaliszyk, Cezary, and Florian Rabe. "A survey of languages for formalizing mathematics." Proceedings of the 13th International Conference on Intelligent Computer Mathematics, CICM 2020, Bertinoro Ed. Christoph Benzmüller, Bruce Miller, Springer, 2020. 138-156.

BibTeX: Download