nLab Kevin Buzzard

Kevin Buzzard is professor for pure mathematics at Imperial College London.

Selected writings

On Xena, formal proof and proof assistants (specifically Lean) in undergaduate mathematics courses:

Arguing that real applications of homotopy type theory have not even been looked into yet (at least as of 2020):

  • Univalent people, section in: Where is the fashionable mathematics? (Feb 2020) [blog post]

    “ I don’t want to hear protestations, I want to see the code.”

  • Is HoTT the way to do mathematics? (2020) [pdf]

    [slide 15:] “Nobody knows because nobody tried.”

On formalizing perfectoid spaces in Lean:

On equality:

category: people

Last revised on May 20, 2024 at 18:36:38. See the history of this page for a list of all contributions to it.