Artificial intelligence assisted mathematical proof has become a highly focused area nowadays. One key problem in this field is to generate formal mathematical proofs from natural language proofs. Due to historical reasons, the formal proof languages adopted by traditional theorem provers were not intended to represent natural language proofs. Therefore, they are not well-suited for the aforementioned tasks and proof-checking work for educational purposes. In this paper, we design a proof language and its corresponding abstract syntax tree and implement a proof checking tool for it. This language can be easily converted from natural language, thus providing a rich corpus of formal proof. Additionally, it supports the handling of issues in informal proofs through static analysis, and enhances the expressive power of the language by introducing the structure of partial proofs. This design combines the expressiveness of natural language and the accuracy of formal language, resulting in an improved mathematical proof language.

翻译：人工智能辅助数学证明已成为当今高度关注的领域。该领域的一个关键问题是如何从自然语言证明中生成形式化数学证明。由于历史原因，传统定理证明器采用的形式化证明语言并非旨在表示自然语言证明。因此，它们不适用于上述任务及教育目的的证明检查工作。本文设计了一种证明语言及其对应的抽象语法树，并为其实现了证明检查工具。该语言可易于从自然语言转换而来，从而提供丰富的形式化证明语料库。此外，它还支持通过静态分析处理非形式化证明中的问题，并通过引入部分证明结构增强语言的表达能力。这一设计结合了自然语言的表达力与形式语言的准确性，形成了一种改进的数学证明语言。