“To define a perfectoid space, the three mathematicians had to combine more than 3,000 definitions of other mathematical objects and 30,000 connections between them.“ Posted on October 11, 2020 by jgordon Link. Using Lean, an environment for mathematical proofs.