Kevin Buzzard
XenaProject
Random Fermat's Last Theorem observation: the bridge between analysis and algebra in it is nonconstructive. Chris Birkbeck, a post-doc at UCL, has been making modular forms in Lean. He
Read more
Isabelle/HOL has schemes! https://www.isa-afp.org/entries/Grothendieck_Schemes.html . The formalisation is due to Bordg, Paulson and Li. In this thread I will try to explain why this is a big deal. 1/n The
Read more
Ok so I claim that doing mathematics constructively obscures ideas which, to me at least, feel natural. Let me illustrate with a simple example: a locally open set is open.
Read more