Cannonballs and Uber

Automated Theorem Proving is a blossoming area of mathematical research. Fields medalists like Terrance Tao, Maxim Kontsevich and Vladimir Voevodsky have all commented publicly on the impending machine-proof paradigm shift. Functionally, it provides a mechanism to totally verify mathematical statements and computer algorithms. For example, formal proofs methods have been successful in cryptography, unmanned aircraft systems, discrete geometry and autonomous-vehicle engineering. In this talk, we attempt to look at the mathematical, computer-scientific and philosophical sides of this subject. Resources will be supplied to help one get started using proof assistants.