A formalization of the concept of a perfectoid space in the Lean formal proof verification system.
By Johan Commelin, Patrick Massot and Kevin Buzzard
This is a project whose first goal is to create a type in a certain computer language. The language is Lean, which is some version of dependent type theory. Dependent type theory is another foundation for mathematics, and in this type theory you can do all the things that mathematicians are used to doing in ZFC set theory.
The name of the type we're constructing is perfectoid_space. One could define a perfectoid space to be a term of this type. Hence any computer program which outputs a term of this type could be said to be a program which computed a perfectoid space. My initial goal is to finish formalising the definition, and after that one could imagine proving basic results about perfectoid spaces within Lean. Is this sort of thing feasible? I don't know. I think so though, and I'm not really sure if anyone has tried this sort of thing before. Let's find out!
This project is not yet finished. It usually compiles, or mostly compiles, with Lean 3.4.1 and Mathlib Head. When we've finished it I'll put up a more coherent description of how to compile it. In the mean time, you can find a precompiled Lean binary for most operating systems here. Once you have Lean up and running you can download the project as a zip file here and extract it into a directory, or just go to the project home page and clone or download the repository. Once you have unpacked the repository into a directory then change into the directory and run
$ leanpkg upgradeand this will download mathlib. Typing leanpkg build will build the repository, which will take a while, but will ultimately make things run more quickly.
If you are considering contributing then you will want to use an IDE, and the two standard ones for Lean are VS Code and emacs. Instructions for setting these editors up for Lean are here in the Lean reference manual.
I read theorem proving in Lean and then I did a whole bunch of undergraduate level mathematics (I basically took a basic course which I teach, and tried to solve the problem sheets in Lean). Do note however that this whole thing is all very beta at the minute. I think Tom Hales describes it best.
Because I think that this idea is really interesting, and I want to see where it leads. And because I like computing examples of mathematical objects, especially complex ones like eigencurves and so on.
You're welcome to ask questions at
Chat : https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Perfectoid.20spaces
Perfectoid rings and spaces formalised, modulo the entire theory of adic spaces.
Brian Conrad's learning seminar.
Scholze etale cohomology of diamonds (ArXiv).