The Dennes Room

Event Detail

Wed Apr 24, 2019
4 LeConte Hall, 4–5 PM
Alfred Tarski Lectures
Thomas Hales (University of Pittsburgh)
Formalizing mathematics

This talk will describe a broad long-term research program to make formal proofs in mathematics a practical reality. A formal proof is a mathematical proof that has been checked exhaustively by computer, on the basis of the fundamental axioms of mathematics and the primitive inference rules of logic. The field has progressed to the point that it is now possible to give formal proofs of major theorems in mathematics.