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

Link. Using Lean, an environment for mathematical proofs.