Mathematics Colloquia and Seminars

Return to Colloquia & Seminar listing

Formal Proof

Distinguished Lecture Series

Speaker: Thomas Hales, University of Pittsburgh
Related Webpage: http://www.math.ucdavis.edu/seminars/thurston/
Location: 1147 MSB
Start time: Fri, May 11 2018, 4:10PM

This talk will discuss the design of formal proof assistants – computer programs that are used to check the correctness of mathematics.
Most mathematicians accept set theory as the foundation of mathematics, but many proof assistants are based on type theory instead. What is type theory, and why does it replace set theory?
This talk will also discuss the prospects of moving all mathematical publications into a proof assistant.



Part of the Thurston Lecture Series.