Formalising Perfectoid Spaces
summary
Formalisation of perfectoid spaces in Lean produces a dependency graph where the central definition sits atop reused mathlib plus new code for valuation theory, topological rings, completions and advanced sheaves. The perfectoid predicate itself is about 20 lines added on top of adic spaces, yields an embarrassingly trivial empty space example, and makes a nontrivial one-point example wildly expensive to build. Work requires fighting mathematicians’ abuse of notation, stretching the type class system, and heavy community support; no genuinely new theorems appear yet.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:05KEVIN BUZZARD AND PATRICK MASSOT
- 1:27SELECTING A TOPIC
- 2:19FASHIONABLE MATHEMATICS
- 2:47A PERFECTOID SPACE IS...
- 3:21A SOPHISTICATED DEFINITION?
- 6:47WE PORMALISED A DEFINITION
- 8:46THEOREMS UNDER THE HOOD
- 9:54ANSWERS TO OUR QUESTIONS
related talks
49mSemantic Foundations for Probabilistic Programming
20mFormalizing polynomial laws and the universal divided power algebra
20mFully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logica
25mLocally Nameless Sets
34mFormalizing the ∞-categorical Yoneda lemma
27mFunctorial Semantics for Partial Theories
19mCombining Dependency, Grades, and Adjoint Logic
14mAdequacy for Algebraic Effects Revisited