A formal approach to logic and reasoning initiated by Frege in the late 19th and early 20th centuries marked a step function in the evolution of the subject. In the following decades, the foundations of modern mathematics and logic were cemented by the likes of Hilbert and Gödel. The developments in formal logic also spurred the revolution of computing that has shaped the world in the late 20th and early 21st centuries. However, most of us are only vaguely aware of the next revolution that is well on its way, the revolution of automated formal logic: applying the computing power of modern computers to the problem of logical reasoning. This area of research has been active for many decades and there has been significant progress in producing useful results for the larger community. Automated reasoning tools are already widely used in software and hardware verification tools, but they are still a long way from everyday use by computer scientists and mathematicians.

This paper marks a milestone in the steady progress of this field. It presents an automated system for reasoning about a significant portion of the mathematics of Euclidean spaces. The author describes the overall structure of the theory of higher-order logic (HOL), and points out a few key results that have been proved with it. The development focuses not just on proving a couple of “big-ticket” theorems, but also aims to make the reasoning tools relevant for more general and routine application. The author rightly emphasizes the activity of engineering a usable system for doing everyday work.

The paper itself does not do justice to the work underlying it. In the limited form of a journal paper, it can only give brief, and one could even argue superficial, descriptions of the formalization. The value however is in the fact that it may motivate the reader to actually download the HOL Light theorem prover and try to solve a problem using it. The approach will be validated if even a single application of the HOL Light system comes out of these trials.