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.
leanprover-community/lean-perfectoid-spaces
Perfectoid spaces in the Lean formal theorem prover.
LeanApache-2.0