Kevin Buzzard, Massó, and Kamlin began a three-person project to blueprint the Lean definitions needed to define a perfectoid space.

“And so he and Massó and Kamlin start this effort, just the three of them, to create a blueprint, essentially a kind of, um, a guide to the things they would need to define in Lean in order to be able to-- in or- in order to be able to write the definition of a perfectoid space.”