Elamur Research⌕
☰
home / papers / 2019 / Formalising perfectoid spaces

Formalising perfectoid spaces

Paper · 2019 · Kevin Buzzard, Johan Commelin and Patrick Massot

Summary

The authors address whether a proof assistant can cope with the highly abstract objects of current research mathematics, rather than long proofs about elementary ones. Their test case is the perfectoid space, introduced by Peter Scholze in 2012 and central to his Fields Medal work. Using the Lean theorem prover and its community library mathlib, they built the full chain of prerequisites. This includes completions of topological groups and rings with their universal properties, continuous valuations, Huber rings and Huber pairs, adic spectra Spa(A), and enough sheaf theory to construct objects of a category CLVRS. Adic spaces and then perfectoid spaces are defined as spaces locally isomorphic to such spectra. The work adds no extra axioms to Lean's logic. It shows that dependent type theory can express these structures, and that pure mathematicians without computer science training can learn to use a proof assistant fairly quickly. Formalising a fashionable topic also drew mathematicians' attention to formal proof.

Key points

  • This is reported as the first formalisation of perfectoid spaces in any theorem prover. It relies on Lean's calculus of inductive constructions and builds on mathlib, which was split off from Lean's core library in 2017. Much of the general material is intended to be merged into mathlib.
  • The informal sources were Bourbaki's Elements of Mathematics for the classical topology and algebra, and Torsten Wedhorn's lecture notes on adic spaces. Huber and Scholze's original papers were consulted occasionally.
  • Constructing the local models, meaning the passage from a Huber pair to an object of CLVRS, made up most of the effort. At two points the definitions differ slightly from the literature, but unformalised standard theorems show they are equivalent.
  • Beyond the definition, the only example obtained is the empty perfectoid space. Future work includes specialisations of valuations and nontrivial examples.
  • The main practical obstacles were elaboration with heavily overloaded notation, strain on the type class system, and a lack of documentation aimed at mathematicians. Proving lemmas was not the hardest part.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🔬Centre National de la Recherche ScientifiqueParis · France173 works · 62,617 citations🎓Imperial College LondonLondon · United Kingdom56 works · 13,671 citations🎓University of FreiburgFreiburg im Breisgau · Germany8 works · 1,661 citations🎓Université Paris-SudOrsay · France11 works · 5,167 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksMathematics · 233 worksComputational Theory and Mathematics · 496 worksGeometry and Topology · 9 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Kevin Buzzard, Johan Commelin and Patrick Massot. 2019. Formalising perfectoid spaces. arXiv:1910.12320 (CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Pages 299-312).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1145/3372885.3373830 · arXiv 1910.12320

@misc{buzzard2019formalising,
  title = {{Formalising perfectoid spaces}},
  author = {Kevin Buzzard, Johan Commelin and Patrick Massot},
  year = {2019},
  doi = {10.1145/3372885.3373830},
  eprint = {1910.12320},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1145/3372885.3373830}
}

References

23 references, 2 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Kevin Buzzard, Ramon Fernández Mir, Chris Hughes, and Kenny Lau. Schemes in Lean, 2019. URL: https://github.com/ramonfmir/lean-scheme. ↗
  2. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A User-Friendly Library of Real Analysis for Coq. Mathematics in Computer Science, 9(1):41–62, Mar 2015. Nicolas Bourbaki. Elements of mathematics. General topology. Part 1. Hermann, Paris; Addison-Wesley Publishing Co., Reading, Ma… find
  3. Nicolas Bourbaki. Commutative algebra. Chapters 1–7. Elements of Mathematics (Berlin). Springer-Verlag, Berlin, 1998. Translated from the French, Reprint of the 1989 English translation. find
  4. Michael Beeson and Freek Wiedijk. The meaning of infinity in calculus and computer algebra systems. J. Symb. Comput., 39(5):523–538, 2005. doi:10.1016/j.jsc.2004.12.002. Thierry Coquand and Christine Paulin. Inductively defined types. In COLOG-88, International Conference on Computer Logic, Tallinn,… — [doi:10.1016/j.jsc.2004.12.002](https://doi.org/10.1016/j.jsc.2004.12.002) find
  5. Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the solution to the cap set problem. In 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pages 15:1–15:19, 2019. doi:10.4230/LIPIcs. ITP.2019.15. — [doi:10.4230/lipics](https://doi.org/10.4230/lipics) find
  6. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 378–388, 2015. find
  7. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A Machine-checked Proof of the Odd Order Theorem. In Inter… find
  8. François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging Mathematical Structures. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pages 327–342, 2009. Georges Gonthier. The Four Colour… find
  9. Sébastien Gouëzel and Vladimir Shchur. A corrected quantitative version of the Morse lemma. Journal of Functional Analysis, 277(4):1258 – 1268, 2019. find
  10. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef… — A formal proof of the Kepler conjecture
  11. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pages 279–294, 2013. Roland Huber. Continuous valuations. Math… find
  12. Roland Huber. Étale cohomology of rigid analytic varieties and adic spaces. Aspects of Mathematics, E30. Friedr. Vieweg & Sohn, Braunschweig, 1996. find
  13. Ioan James. Topologies and uniformities. Springer Undergraduate Mathematics Series. Springer-Verlag London, Ltd., London, 1999. Revised version of Topological and uniform spaces [Springer, New York, 1987; MR0884154 (89b:54001)]. find
  14. Robert Y. Lewis. A formal proof of Hensel’s lemma over the p-adic integers. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 15–26, 2019. find
  15. Paul-Nicolas Madeleine. Arithmetic and Casting in Lean, 2019. Internship report. URL: https://lean-forward.github.io/internships/arithmetic_and_casting_in_lean.pdf. ↗
  16. The mathlib Community. The Lean mathematical library, 2019. arXiv:1910.09336.
  17. Assia Mahboubi and Enrico Tassi. Mathematical Components, 2017. URL: https://math-comp.github.io/mcb/. ↗
  18. Álvaro Pelayo, Vladimir Voevodsky, and Michael A. Warren. A univalent formalization of the p-adic numbers. Mathematical Structures in Computer Science, 25(5):1147–1171, 2015. Michael Rapoport. The work of Peter Scholze. In Proceedings of the International Congress of Mathematicians—Rio de Janeiro 20… find
  19. Damien Rouhling. Outils pour la formalisation en analyse classique. PhD thesis, 2019. URL: http://www-sop.inria.fr/members/Damien.Rouhling/data/phd/thesis.pdf. ↗
  20. Peter Scholze. Perfectoid spaces. Publ. Math. Inst. Hautes Études Sci., 116:245–313, 2012. find
  21. Peter Scholze. Etale cohomology of diamonds, 2017. arXiv:1709.07343. — [arXiv:1709.07343](https://arxiv.org/abs/1709.07343) find
  22. Torsten Wedhorn. Adic Spaces, 2012. arXiv:1910.05934. — [arXiv:1910.05934](https://arxiv.org/abs/1910.05934) find
  23. Torsten Wedhorn. On the work of Peter Scholze, 2019. arXiv:1909.11510. — [arXiv:1909.11510](https://arxiv.org/abs/1909.11510) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/buzzard-2019-formalising-perfectoid-spaces/