Theorem provers as tools for mathematicians
Scott Morrison, Associate Professor, MSI, ANU
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)
Michael Norrish, Principal Researcher, Data61
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.
This event is free and open to the public. It will be followed by wine and cheese in Level 3, Hanna Neumann Bldg.
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.