Skip to main content
MathOverflow
Kevin Buzzard's user avatar
Kevin Buzzard's user avatar
Kevin Buzzard's user avatar
Kevin Buzzard
  • Member for 15 years, 1 month
  • Last seen more than a week ago
Profile Activity
Stats
41,399
reputation
1.1m
reached
218
answers
65
questions
#59 overall
Communities
View all
About

Kevin Buzzard. Algebraic number theorist in London. Interested in formal theorem proving.

My blog aimed at teaching undergraduates to use Lean, a formal proof verification system: https://xenaproject.wordpress.com/

Badges
View all badges
13
gold badges
166
silver badges
245
bronze badges
Top tags
View all tags
1,410
Score
144
Posts
51
Posts %
482
Score
41
Posts
14
Posts %
350
Score
30
Posts
11
Posts %
191
Score
21
Posts
7
Posts %
149
Score
20
Posts
7
Posts %
149
Score
17
Posts
6
Posts %
Top posts
View all questions and answers
answer
194
What programming languages do mathematicians use?
Jan 8, 2010
answer
156
Proofs shown to be wrong after formalization with proof assistant
Oct 12, 2018
question
139
Which mathematical definitions should be formalised in Lean?
Sep 21, 2018
question
135
what mistakes did the Italian algebraic geometers actually make?
Mar 26, 2010
answer
124
Etale cohomology -- Why study it?
Nov 19, 2009
answer
121
Extent of “unscientific”, and of wrong, papers in research mathematics
Feb 1, 2020
question
107
solving $f(f(x))=g(x)$
Mar 9, 2010
question
86
What are the local Langlands conjectures nowadays, for connected reductive groups over a $p$-adic field?
Feb 9, 2010
answer
80
What would you want to see at the Museum of Mathematics?
Dec 25, 2010
answer
73
How do I check if a functor has a (left/right) adjoint?
Nov 18, 2009
Top network posts
View all network posts
59
Are some proof assistants better suited for given areas of math than others?
45
Proof assistants for beginners - a comparison
28
Why haven't all of the "hundred greatest theorems" been formalized yet?
26
Usage and Importance of Proof Assistants
20
Examples of formalisation of abelian categories