Tarski Lecture: Formalizing mathematics

Lecture | April 24 | 4-5 p.m. | 4 LeConte Hall

 Thomas Hales, University of Pittsburgh

 Department of 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.