Perfectoid spaces are sophisticated objects in arithmetic geometry introduced
by Peter Scholze in 2012. We formalised enough definitions and theorems in
topology, algebra and geometry to define perfectoid spaces in the Lean theorem
prover. This experiment confirms that a proof assistant can handle complexity
in that direction, which is rather different from formalising a long proof
about simple objects. It also confirms that mathematicians with no computer
science training can become proficient users of a proof assistant in a
relatively short period of time. Finally, we observe that formalising a piece
of mathematics that is a trending topic boosts the visibility of proof
assistants amongst pure mathematicians.