ABSTRACT
Large language models like ChatGPT can do all sorts of things – including writing correct computer code. But how good are they at mathematics? Do mathematicians need to start worrying that they will be soon out of a job? More realistically, will we get to the stage where modern computer tools such as large language models and interactive theorem provers will be able to help working mathematicians to do their research? I'll give an overview of where we are and speculate about where we're going.
LECTURER
Kevin Buzzard is Professor of Pure Mathematics at the Imperial College, London. His expertise is in algebraic number theory and he is currently working in the area of formal proof verification.