Cannonballs and Uber

Wednesday, February 1, 2017 - 15:00 to 15:50
703 Thackeray Hall
Speaker Information
Jacob Gross
Undergraduate Student
University of Pittsburgh

Abstract or Additional Information

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.