Time:  12  1:30 p.m. 
Room: 
Wean Hall 7220

Speaker:  Thomas Hales Mellon Professor Department of Mathematics University of Pittsburgh 
Title:  Formal Proofs in Geometry w/ HOL

Abstract: 
HOL is a computer program that is used to give formal verifications of
theorems. This lecture will report on the experiences that I have had
with a version of HOL called HOLLight. Particular attention will be
given to recent work, which has been focused on verifications about
topological spaces, metric spaces & Euclidean geometry.
