Tag Archives: perfectoid space

The Sphere Eversion Project

Posted on June 5, 2020 by xenaproject

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 cap set, Johannes Hölzl, Patrick Massot, perfectoid space, Rob Lewis, Sander Dahmen, scheme, sphere eversion | 2 Comments

A computer-generated proof that nobody understands

Posted on July 6, 2019 by xenaproject

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

Posted in General | Tagged Bruck loop, David Stanovsky, Goro Shimura, J. D. Phillips, Michael Kinyon, perfectoid space, Pierre Deligne, Robbins conjecture, Shimura variety, Waldmeister, William McCune | 7 Comments

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 →

Posted in Uncategorized | Tagged Chris Hughes, Johan Commelin, Kenny Lau, Patrick Massot, perfectoid space, Ramon Fernandez Mir | 4 Comments

Tag Archives: perfectoid space

The Sphere Eversion Project

A computer-generated proof that nobody understands

Perfectoid spaces!

Categories

Recent Posts