It’s common for formal proof efforts about software and hardware to involve thousands to tens of thousands of small lemmas.

13M lines does seem extreme and there is probably a lot of inefficiency given the way the proof was developed. Cutting it down is probably a long road, but is also a very well defined problem that AIs can probably just go do with enough time and budget now.