Formalising perfectoid spaces

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.

Final version, with small additions requested by referees. 22 pages. See also https://leanprover-community.github.io/lean-perfectoid-spaces/

References in corpus (3)

• The Lean mathematical library
• A formal proof of Hensel's lemma over the p-adic integers
• Adic Spaces

Cited by in corpus (14)

• The Lean mathematical library
• Maintaining a Library of Formal Mathematics
• Schemes in Lean
• Formalizing the Ring of Witt Vectors
• Proof Artifact Co-training for Theorem Proving with Language Models
• Mathematical Proof Between Generations
• Automated Mathematics and the Reconfiguration of Proof and Labor
• A Formalization of Complete Discrete Valuation Rings and Local Fields
• Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
• Simplifying Casts and Coercions
• A logical framework with a graph meta-language
• Generating isospectral but not isomorphic quantum graphs
• A cost-aware logical framework
• Formalising the local compactness of the adele ring