PeopleofSuperintelligence

Researcher

Kevin Buzzard

Kevin Buzzard is a mathematician whose work connects formal proof with AI for mathematics. He wins an IMO gold medal with a perfect score, studies mathematics at Cambridge and builds a career in pure mathematics at Imperial. The Xena Project brings Lean to undergraduate mathematics, and his work with collaborators formalizes perfectoid spaces in Lean. Today, he helps maintain Mathlib and leads projects that make research mathematics machine-checkable; he advises the AI Mathematical Olympiad Prize and reviewed Claude's Lean formalization of Fermat's Last Theorem.

Works
60
Citations
1,059
h-index
18

Publication numbers from OpenAlex, as of 14 October 2026.

Photo of Kevin Buzzard

Timeline

  1. 1986–1990

    An Olympiad medal and Cambridge

    At the Royal Grammar School in High Wycombe, he wins bronze at the 1986 International Mathematical Olympiad and gold with a perfect score in 1987. He studies mathematics at Trinity College, Cambridge, and becomes Senior Wrangler in 1990.

  2. 1995–2008

    From research visits to Imperial

    After earning a PhD under Richard Taylor in 1995, he works at the Institute for Advanced Study in Princeton, UC Berkeley and the Institute Henri Poincaré in Paris. He joins Imperial as a lecturer in 1998, becomes a reader in 2002 and professor in 2004, and serves as a visiting professor at Harvard in 2002. The London Mathematical Society awards him the Whitehead Prize in 2002 for work in number theory and the Senior Berwick Prize in 2008.

  3. 2017

    Teaching Lean through games

    The Xena Project starts in 2017 as a way to turn undergraduate pure-mathematics questions into levels of the Lean computer game.

  4. 2019

    Formalizing perfectoid spaces

    With Johan Commelin and Patrick Massot, he formalizes enough topology, algebra and geometry in Lean to define perfectoid spaces.

  5. 2024

    Taking formal proof to Fermat

    The AI Mathematical Olympiad Prize appoints him to its advisory committee in 2024. From October 2024, he leads an Imperial-hosted Lean project to formalize Fermat's Last Theorem, funded by an EPSRC grant through September 2029.

  6. 2025

    Research theorems for AI

    He leads a two-year Imperial project funded by Renaissance Philanthropy through the AI for Math Fund. The project aims to build a public dataset of formalized statements from recent journal publications.

  7. September 2026

    Claude's proof reaches Lean

    Anthropic reports that Claude completes a computer-checked Lean formalization of Fermat's Last Theorem in 11 days. Buzzard reviews the proof and says autoformalization can help rigorously check language-model mathematics.

  8. As of October 2026

    A library for formal proof

    At Imperial, he is Professor of Pure Mathematics and works in formal proof verification. He helps maintain Mathlib, the community-maintained Lean library of formalized mathematical definitions and theorems.

Sources and credits

Photo: Paulabuzzard at en.wikipedia, via Wikimedia Commons. License: CC BY-SA 3.0. Source: commons.wikimedia.org. Cropped to a square and resized. Ask us to remove or replace this photo.

  1. Kevin Buzzard - Wikipedia en.wikipedia.org. Checked 14 October 2026.
  2. AIMO Prize Appoints Further Advisory Committee Members | AIMO Prize aimoprize.com. Checked 14 October 2026.
  3. What is the Xena project? | Xena xenaproject.wordpress.com. Checked 14 October 2026.
  4. Formalising perfectoid spaces arxiv.org. Checked 14 October 2026.
  5. FLT/README.md at main · ImperialCollegeLondon/FLT · GitHub github.com. Checked 14 October 2026.
  6. Generous Donation To Advance AI For Mathematics | Imperial News | Imperial College London imperial.ac.uk. Checked 14 October 2026.
  7. Formalizing Fermat's Last Theorem | Anthropic anthropic.com. Checked 14 October 2026.
  8. Kevin Buzzard | About | Imperial College London profiles.imperial.ac.uk. Checked 14 October 2026.
  9. Mathlib maintainers leanprover-community.github.io. Checked 14 October 2026.