A Natural Formalized Proof Language
Lihan Xie, Zhicheng Hui, Qinxiang Cao
TL;DR
This work tackles the challenge of converting informal natural-language proofs into formal proofs by introducing a natural-language-like formal proof language and an automated checker, ProofGrader. The design blends human-readable structure with formal rigor through constructs like partial proofs and forward/backward reasoning, supported by a semantic framework and static analysis to resolve context-dependent semantics and notation overloading. A modular ProofGrader architecture comprises a parser, static analyzer, and a solver-manager-driven proof checker, enabling configurable solvers and educational use. Evaluated on 52 proofs across multiple domains, the system demonstrates reasonable performance and comparative advantages in readability and expressiveness, offering a practical path toward AI-assisted formalization and automated proof grading with explicit justification for each step.
Abstract
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.