Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. It was unclear whether a proof assistant could handle the complexity of defining such objects, and whether mathematicians without computer science training could effectively use one.

The authors formalize enough definitions and theorems in topology, algebra, and geometry to define perfectoid spaces in Lean. This required building up substantial infrastructure including topological rings, valuations, adic spaces, and perfectoid rings before assembling the final definition. The project was carried out by mathematicians with no prior computer science training who learned to use Lean during the project.

The formalization confirms that Lean can handle the definitional complexity of perfectoid spaces. The project also demonstrates that mathematicians without CS training can become proficient proof assistant users in a relatively short period of time.