This seminar series will consist of two talks: Theorem provers as tools for mathematicians by Associate Professor Scott Morrison from MSI and Mechanising computability and Kolmogorov complexity (in HOL) by Dr Michael Norrish, from Data61.
Theorem provers as tools for mathematicians
I'll look at the current state of theorem provers, in particular at how close (or otherwise!) they are to being useful for mathematicians. Famous early examples of successful use of theorem provers --- the four colour theorem, the Kepler conjecture, and the odd order theorem --- are impressive more for their immensity than their conceptual depth. As more mathematicians are using these systems, more modern examples are starting to appear.
Mechanising Computability and Kolmogorov Complexity (in HOL)
I’ll discuss how it is possible to recapitulate some classical 1930s maths in a theorem-prover, while forging a somewhat novel path that allows us to entirely avoid having to talk about Turing Machines. In the process, I’ll talk about how mechanised mathematics is simultaneously fun, useful, and harrowingly pedantic. Finally, last point notwithstanding, I will try to convince you that theorem-prover pedantry is a powerful tool, keeping track of details that otherwise threaten to derail understanding and correctness. The MSI/RSCS The Seminar Series is supported by the Mathematical Sciences Institute at the College of Science and the Research School of Computer Science at the College of Engineering & Computer Science at ANU.
This event is free and open to the public. It will be followed by wine and cheese in Level 3, Hanna Neumann Bldg.