In this week’s theory seminar, we will host a talk by Kevin Buzzard.

Abstract

I am currently involved in a project to teach a computer proof assistant a proof of Fermat’s Last Theorem. In this talk I’ll explain what a computer proof assistant is, and I’ll try and explain something about the nature of the task, how I ended up doing it, and why I think it’s interesting and important. The talk will be suitable for both computer scientists and mathematicians, and you don’t need any specialized knowledge in computer proof assistants, AI or number theory to follow it.