Proof — Perfectoid spaces formalization (Lean)
Statement
Scholze's perfectoid spaces—a central object in p-adic geometry—fully formalized in Lean from first principles. Every definition and lemma verified by computer. Dependency graph: 3000+ nodes, 30000+ edges. Establishes that modern algebraic geometry is ZFC-derivable.
Formula
Perfectoid space = CLVRS with local Spa(A)
Proof sketch
Commelin, Buzzard, Massot: Lean-perfectoid-spaces project. Formalized topology, algebra, geometry to define perfectoid spaces. Scholze (2012) proposed; formal derivation completed 2020.
Source
Commelin et al., lean-perfectoid-spaces, 2020. Scholze, Perfectoid spaces, 2012.
Domains
mathematics, computer-science