Comment by KaiserPister

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?