lean-perfectoid-spaces

A formalization of the concept of a perfectoid space in the Lean formal proof verification system.

By Kevin Buzzard, Johan Commelin, and Patrick Massot.

See the project website.