Formalising perfectoid spaces

TL;DR

This paper demonstrates the formalisation of perfectoid spaces, complex objects in arithmetic geometry, within the Lean proof assistant, showcasing the potential for formal verification in advanced mathematical research.

Contribution

It is the first formalisation of perfectoid spaces, illustrating that proof assistants can handle sophisticated mathematical concepts and are accessible to mathematicians without computer science backgrounds.

Findings

Proof assistant can formalise complex objects like perfectoid spaces

Mathematicians can learn proof assistants quickly

Formalising trending mathematical topics increases visibility of proof assistants

Abstract

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.