数学形式化语言综述
A Survey of Languages for Formalizing Mathematics
摘要：
为了在计算机系统中处理数学内容，有必要用形式语言来表示它。理想情况下，这些都是由工具来支持的，这些工具可以验证内容的正确性，允许使用它进行计算，并生成人类可读的文档。这些目标很难组合，最先进的工具通常必须做出艰难的妥协。在本文中，我们讨论了已创建的语言，为此目的，包括证明助手和其他形式系统的逻辑语言，半形式语言，中间语言交换数学知识，语言框架，允许建立定制的语言。我们评估其优势的基础上，我们的经验，设计和应用语言和工具的形式化数学。我们得出的结论是，没有现有的语言是真正足够好的，并得出可能的未来改进的想法。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
