**PLEASE NOTE UPDATED TIME**
In this lecture, I will provide a general overview of automated and interactive theorem proving. I will characterize the general projects and existing technology, and describe some recent landmarks and successes in these fields. These will include the verification of the Feit-Thompson theorem, the verification of the Kepler conjecture, the use of computers to establish results in algebraic topology, and the recent use of fast satisfiability solvers in connection with the Erdős discrepancy conjecture.
To participate in this seminar:
This lecture series will be available on the Internet via SeeVogh: you can download and install the client for free at www.seevogh.com. It is recommended that you try it out with the test meeting number which is 7532474432. To take part in the lectures, please email Andrew Danson, who will provide the meeting numbers for the sessions, or check the CARMA event website periodically.
