|Time:|| 12 - 1:30 p.m.
Wean Hall 7220
|Speaker:|| Thomas Hales
Department of Mathematics
University of Pittsburgh
|Title:|| Formal Proofs in Geometry w/ HOL
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 HOL-Light. Particular attention will be
given to recent work, which has been focused on verifications about
topological spaces, metric spaces & Euclidean geometry.