Formally Verified Mathematics

The article discusses how formal verification could become the new standard for rigor in mathematics with the help of computational proof assistants. Due to developments in computer science over the past few decades, it is now possible to achieve complete formalization in practice. Working with 'computational proof assistants,' users are able to verify substantial mathematical theorems, constructing formal axiomatic derivations of remarkable complexity. The notion of proof lies at the heart of mathematics. Although early records of measurement and numeric computation predate the ancient Greeks, mathematics proper is commonly seen as having begun with development of the deductive method, as exemplified by Euclid's Elements of Geometry.