Tag Archives: perfectoid space

The Sphere Eversion Project

Patrick Massot has written a blueprint for sphere eversion. This marks the beginning of a community formalisation project. Continue reading

Posted in Imperial, Learning Lean, Type theory | Tagged , , , , , , , | 2 Comments

A computer-generated proof that nobody understands

Computers can find 1000 page proofs about simple things. Why not Shimura varieties? Continue reading

Posted in General | Tagged , , , , , , , , , , | 7 Comments

Perfectoid spaces!

Patrick Massot, Johan Commelin and I finished our definition of a perfectoid space in Lean! Patrick and Johan are professional mathematicians like me, not Imperial undergraduates, but I am sufficiently excited about the project that I couldn’t stop myself blogging … Continue reading

Advertisement

Posted in Uncategorized | Tagged , , , , , | 4 Comments