Kevin Buzzard is professor for pure mathematics at Imperial College London.
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:
Last revised on June 13, 2023 at 18:01:41. See the history of this page for a list of all contributions to it.