Comment by amluto

If you consider the statement that perfect play by both sides in checked results in a draw to be the statement of a theorem, then the proof is 237GB compressed :) And verifying it requires quite a lot of computation.

https://www.science.org/cms/asset/7f2147df-b2f1-4748-9e98-1a...