|
|
|
|
|
|
by AtlasBarfed
1824 days ago
|
|
|
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. |
|
|