Lean required 300 GB of RAM, 96 cores, and took hours to compile and check the formalization.

Now they have the perfect stress test to hill-climb and optimize.