It doesn't seem execution was a problem. From Kevin Buzzard's blog: I’ve compiled the code base and run comparator on it — it checks out. It is a gigantic proo

It doesn't seem execution was a problem. From Kevin Buzzard's blog: I’ve compiled the code base and run comparator on it — it checks out. It is a gigantic proof (over 13.4 million lines of code) and takes nearly 20 times as long to compile as Lean’s mathematics library (on a machine with 96 cores!). Lean can be sluggish when jumping from file to file on a repo of this size (even on a machine with 500G of ram, which Anthropic also gave me access to), but Anthropic also supplied me with some html documents which are easier in practice to explore (clone the repo and open with a web browser). 500G of RAM is not actually that huge tbh (I was looking to buy a used 1TB server blade for some personal stuff a while ago but it was too much hassle) so I don't guess there was too much potential for buffer overflows.