A Review on Mechanical Proving and Formalization of Mathematical Theorems - Si Chen; Wensheng Yu; Guowei Dou; Qimeng Zhang (IEEE Access)
The field of artificial intelligence represents a frontier and a focal point of contemporary technological development. As an important embodiment of artificial intelligence applied to theoretical-level research, mechanical proving has been a subject of significant interest among researchers. The past few centuries have witnessed multiple periods of machine proof of mathematical theorems as computer technology has continued to evolve. From the initial proposal of “mechanization of human mental labor” being proposed to the present, the idea of “mechanization of mathematics” has been gradually being realized. Along with various formalization tools being developed, mechanical proving have ushered in a new era nowadays. This paper introduces and summarizes the history of mathematical formalization, the main formalization tools and the main theoretical achievements in different stages and fields. This paper also provides an overview of our group’s work in the formalization of a series of mathematical theorems using Coq, including Morse-Kelley axiomatic set theory and the foundations of analysis among others. Despite the considerable promise of formal tools in bolstering system reliability and mathematical rigorousness, it continues to encounter obstacles in practical applications. Although the formal tool holds considerable prospects in enhancing system reliability and mathematical rigorousness, it still meets with barriers in practical application. The paper concludes with a discussion of some of the current challenges associated with mechanical proving, as well as offers suggestions for future research directions.