Kevin Mark Buzzard (born 21 September 1968) is a British mathematician and currently a professor of pure mathematics at Imperial College London.
[3] He then received his Ph.D. under the supervision of Richard Taylor with a thesis titled The levels of modular representations in 1995.
From October to December 2002 he held a visiting professorship at Harvard University, having previously worked at the Institute for Advanced Study, Princeton (1995), the University of California Berkeley (1996-7), and the Institute Henri Poincaré in Paris (2000).
[6] In 2017, he launched an ongoing formalization project and blog involving the Lean theorem prover[7] and has since promoted the use of computer proof assistants in future mathematics research.
[10] In 2024, Buzzard and collaborators were handed a five-year ESPRC grant to begin formalising Fermat's Last Theorem in Lean.