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/
Top network posts
- 121 what mistakes did the Italian algebraic geometers actually make?
- 106 Which mathematical definitions should be formalised in Lean?
- 104 Etale cohomology -- Why study it?
- 96 solving $f(f(x))=g(x)$
- 83 Proofs shown to be wrong after formalization with proof assistant
- 76 What would you want to see at the Museum of Mathematics?
- 68 Smooth proper scheme over Z
- View more network posts →