Return to Colloquia & Seminar listing
Formal Proof
William Thurston Lectures| 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.