Kevin Buzzard believed that formalizing perfectoid spaces in Lean would prove that Lean could express any mathematics.

“Perfectoid spaces are truly state-of-the-art objects in, in math. And Kevin says, "All right, if we can formalize them, if we can show Lean is capable, capable of expressing perfectoid spaces, we'll have indisputable proof that it can do anything."”