ProfessorKevin Buzzard
Professor of Pure Mathematics
Department of Mathematics - Faculty of Natural Sciences
Orcid identifier0000-0002-7187-5109 (opens in a new tab)
- Professor of Pure MathematicsDepartment of Mathematics - Faculty of Natural Sciences
- 660, Huxley Building, South Kensington Campus, United Kingdom
BIO
My background is in algebraic number theory. Currently I work in the area of formal proof verification. I believe that within my lifetime, computers will be able to help human mathematicians to create proofs, and I am actively trying to accelerate this process. Examples of things I do:
- I help to maintain Mathlib, a formalized database of modern mathematical theorems and definitions;
- I teach mathematics undergraduates how to use Lean, the software which can read the database;
- I am leading a project to formalize a 21st century proof of Fermat's Last Theorem;
- I am managing a project to formalize the statements of recent theorems published in the top mathematics journals.
Some of my recent talks (see links on left):
- Oxford Strachey Lecture 2025 - Will computers prove theorems?
- Stanford MRC Public Lecture 2024 - Can AI do mathematics?
- The 2023 Bernays Lectures, ETH Zurich.
- The 2022 Plücker lectures, University of Bonn
- My plenary lecture at the 2022 International Congress of Mathematics.
- Will Computers Outsmart Mathematicians? (2021 talk for a general audience at Gresham College).
FACULTY
- Faculty of Natural Sciences
POSITION NAME
- Professor of Pure Mathematics