论文标题
对形式化数学的语言的调查
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.
