Kevin Buzzard believed that formalizing perfectoid spaces would prove indisputably that Lean could express anything.

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