Kevin Buzzard

Kevin Buzzard is a number theorist and professor at Imperial College London. He is an early advocate of the Lean proof assistant, contributes to the Lean mathematical library Mathlib, and has discussed using formal proof tools in work with Peter Scholze.