Summary
My background is in algebraic number theory, although recently I have started to work in the area of formal proof verification. I believe that computers will be able to help humans with proofs within my lifetime, and I am actively trying to make this happen sooner by (a) helping to build a database of modern mathematical theorems and definitions and (b) trying to teach mathematics undergraduates how to use the software. See also Tom Hales' Formal Abstracts project.
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 lectures have been videoed. For example:
* What computers can't do (lay intro to P v NP at Royal Institution).
* The Future of Mathematics (2019 talk at Microsoft Research).
* Will Computers Outsmart Mathematicians? (2021 talk 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
Chapters
Buzzard KM, 2007, Eigenvarieties, L-Functions and Galois Representations, Editor(s): Burns, Buzzard, Nekovar, Cambridge University Press, Pages:59-120, ISBN:9780521694155
Conference
Buzzard K, Commelin J, Massot P, 2020, Formalising perfectoid spaces, POPL: Principles of Programming Languages, Association for Computing Machinery, Pages:299-312