Kevin Buzzard, Massó, and Kamlin began drafting a blueprint listing the definitions needed to define a perfectoid space in Lean.

“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.”