Computer theorem proving in mathematics (Q704001)

This paper presents an overview of issues about computer theorem proving in standard pure-mathematics context. The autor begins with the basic reasons for mechanizing theorem verification and a history of computer theorem proving. Next, he deals with issues as: extra-mathematical considerations (format of the proof document, the basic programming code used to specify the syntax of the language, etc.), basic task (well-defined and machine-determinable meaning, the system of notation for the mathematical objects, etc.), a discussion about the system used (e.g., type theory as a basis for mathematical verification), several options for doing set theory and, finally, some perspectives of future developments of machine verified mathematics.