The Lean version of the theorem was 10,000s lines of code... With verifiers like this as a useful tool, I'm guessing in the coming years this LoC will be dwarf

The Lean version of the theorem was 10,000s lines of code... With verifiers like this as a useful tool, I'm guessing in the coming years this LoC will be dwarfed. I'm a bit surprised a theorem of major complexity reduced to that small a LoC count.