A Review on Mechanical Proving and Formalization of Mathematical Theorems
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 pa...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2025-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/10930874/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849388566397845504 |
|---|---|
| author | Si Chen Wensheng Yu Guowei Dou Qimeng Zhang |
| author_facet | Si Chen Wensheng Yu Guowei Dou Qimeng Zhang |
| author_sort | Si Chen |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-2e9e35d79f404c51b5a458f82d7bcfb9 |
| institution | Kabale University |
| issn | 2169-3536 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj-art-2e9e35d79f404c51b5a458f82d7bcfb92025-08-20T03:42:15ZengIEEEIEEE Access2169-35362025-01-0113506725068610.1109/ACCESS.2025.355263410930874A Review on Mechanical Proving and Formalization of Mathematical TheoremsSi Chen0Wensheng Yu1https://orcid.org/0000-0002-3832-2748Guowei Dou2Qimeng Zhang3Beijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing, ChinaBeijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing, ChinaBeijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing, ChinaBeijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing, ChinaThe 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.https://ieeexplore.ieee.org/document/10930874/Artificial intelligenceCoqformalizationmechanical provingMorse-Kelley axiomatic set theorytheorem provers |
| spellingShingle | Si Chen Wensheng Yu Guowei Dou Qimeng Zhang A Review on Mechanical Proving and Formalization of Mathematical Theorems IEEE Access Artificial intelligence Coq formalization mechanical proving Morse-Kelley axiomatic set theory theorem provers |
| title | A Review on Mechanical Proving and Formalization of Mathematical Theorems |
| title_full | A Review on Mechanical Proving and Formalization of Mathematical Theorems |
| title_fullStr | A Review on Mechanical Proving and Formalization of Mathematical Theorems |
| title_full_unstemmed | A Review on Mechanical Proving and Formalization of Mathematical Theorems |
| title_short | A Review on Mechanical Proving and Formalization of Mathematical Theorems |
| title_sort | review on mechanical proving and formalization of mathematical theorems |
| topic | Artificial intelligence Coq formalization mechanical proving Morse-Kelley axiomatic set theory theorem provers |
| url | https://ieeexplore.ieee.org/document/10930874/ |
| work_keys_str_mv | AT sichen areviewonmechanicalprovingandformalizationofmathematicaltheorems AT wenshengyu areviewonmechanicalprovingandformalizationofmathematicaltheorems AT guoweidou areviewonmechanicalprovingandformalizationofmathematicaltheorems AT qimengzhang areviewonmechanicalprovingandformalizationofmathematicaltheorems AT sichen reviewonmechanicalprovingandformalizationofmathematicaltheorems AT wenshengyu reviewonmechanicalprovingandformalizationofmathematicaltheorems AT guoweidou reviewonmechanicalprovingandformalizationofmathematicaltheorems AT qimengzhang reviewonmechanicalprovingandformalizationofmathematicaltheorems |