A Natural Formalized Proof Language

TL;DR

This paper introduces a new formal proof language designed to better convert natural language proofs into formal representations, supporting proof checking, static analysis, and partial proofs to bridge the gap between informal and formal mathematics.

Contribution

It proposes a novel proof language with an abstract syntax tree, enabling easier conversion from natural language and improved proof verification capabilities.

Findings

Developed a proof checking tool for the new language

Created a corpus of formal proofs from natural language

Enhanced expressiveness with partial proof structures

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.