Imperial College London


Faculty of Natural SciencesDepartment of Mathematics

Professor of Pure Mathematics



k.buzzard Website CV




660Huxley BuildingSouth Kensington Campus





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. Three ways I do this:

* I help to build a database of modern mathematical theorems and definitions;

* I teach mathematics undergraduates how to use the software which can read the database;

* From October 2024 I will be leading a project to formalise a 21st century proof of Fermat's Last Theorem.

If you are a mathematician (or a future mathematician) interested in starting to learn about how to prove theorems using computers, you could try the natural number game! Want some more advanced mathematics? Read about how Commelin, Massot and I told a computer what a perfectoid space was!

Some of my recent talks:

* 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).

My personal website (papers, teaching etc) is here.

Selected Publications

Journal Articles

Buzzard K, Hughes C, Lau K, et al., 2021, Schemes in Lean, Experimental Mathematics, Vol:31, ISSN:1058-6458, Pages:355-363

Buzzard K, Verberkmoes A, 2018, Stably uniform affinoids are sheafy, Journal fur die Reine und Angewandte Mathematik, Vol:740, ISSN:0075-4102, Pages:25-39

Buzzard K, Ciere M, 2014, Playing simple loony dots and boxes endgames optimally, Integers: Electronic Journal of Combinatorial Number Theory, Vol:14, ISSN:1553-1732

Buzzard K, Gee T, 2014, The conjectural connections between automorphic representations and Galois representations, Automorphic Forms and Galois Representations, Vol 1, Vol:414, ISSN:0076-0552, Pages:135-187

Buzzard K, Diamond F, Jarvis F, 2010, ON SERRE'S CONJECTURE FOR MOD l GALOIS REPRESENTATIONS OVER TOTALLY REAL FIELDS, Duke Mathematical Journal, Vol:155, ISSN:0012-7094, Pages:105-161

Buzzard K, 2003, Analytic continuation of overconvergent eigenforms, Journal of the American Mathematical Society, Vol:16, ISSN:0894-0347, Pages:29-55

Buzzard, K., Taylor, R., 1999, Companion forms and weight one forms, Annals of Mathematics, Vol:149, ISSN:0003-486X, Pages:905-919


Buzzard KM, 2007, Eigenvarieties, L-Functions and Galois Representations, Editor(s): Burns, Buzzard, Nekovar, Cambridge University Press, Pages:59-120, ISBN:9780521694155


Buzzard K, Commelin J, Massot P, 2020, Formalising perfectoid spaces, POPL: Principles of Programming Languages, Association for Computing Machinery, Pages:299-312

More Publications