Mechanization of theorem proving in geometry and Hilbert’s mechanization theorem

Generally speaking, Euclid’s “Elements” is the origin of axiomatization of mathematics. However, from the viewpoint of rigor, it has many blemishes. This has been recognized for thousands of years. In the middle and late nineteenth century a critical movement attesting the very foundation of mathematics began. Mathematicians made a comprehensive analysis of the axioms besides the independence problem of the axiom of parallels in the “Elements.” This movement was initiated in Germany and Italy by Pasch and Peano, followed by others and epitomized later on by Hubert. He classified the axioms of Euclidean geometry into five groups (cf. Sect. 1.1) as the basis and starting point of all theorem proving so that Euclidean geometry has had a rigorous foundation ever since. However, even though there is a rigorous axiom system as the basis of all reasoning and proving, by using the Euclidean proof method for geometric theorems it is still impossible to reach an extent of rigor without flaws. This opposes all conventional understandings, as it seems that nobody has ever precisely pointed out or even recognized this fact. This section focuses on explaining this issue.