Skip to main content
Proof Assistants Beta
Kevin Buzzard's user avatar
Kevin Buzzard's user avatar
Kevin Buzzard's user avatar
Kevin Buzzard
  • Member for 2 years, 10 months
  • Last seen more than a week ago
Profile Activity
Stats
2,560
reputation
21k
reached
18
answers
2
questions
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
This user doesn’t have any gold badges yet.
12
silver badges
21
bronze badges
Top tags
View all tags
87
Score
3
Posts
15
Posts %
85
Score
2
Posts
10
Posts %
52
Score
2
Posts
10
Posts %
47
Score
2
Posts
10
Posts %
43
Score
10
Posts
50
Posts %
14
Score
5
Posts
25
Posts %
Top posts
View all questions and answers
answer
59
Are some proof assistants better suited for given areas of math than others?
Feb 9, 2022
answer
45
Proof assistants for beginners - a comparison
Feb 9, 2022
answer
28
Why haven't all of the "hundred greatest theorems" been formalized yet?
Feb 9, 2022
answer
26
Usage and Importance of Proof Assistants
Feb 8, 2022
question
20
Examples of formalisation of abelian categories
Apr 12, 2022
answer
14
What games are there?
Feb 13, 2022
answer
14
What games are there?
Feb 13, 2022
question
12
auto-generating the proof of infinitude of primes
May 13, 2022
answer
10
Lean: problems with visually indistinguishable instances
Feb 19, 2022
answer
7
How did the meaning of "lifting" in proof assistants arise?
Feb 12, 2022
Top network posts
View all network posts
156
Proofs shown to be wrong after formalization with proof assistant
139
Which mathematical definitions should be formalised in Lean?
135
what mistakes did the Italian algebraic geometers actually make?
124
Etale cohomology -- Why study it?
121
Extent of “unscientific”, and of wrong, papers in research mathematics