話変わるが4色問題の場合分けって大変と言ってもせいぜい数万通りくらいじゃなかったっけ。
十数人の数学者が数年がかりでチェックすれば出来るくらいの。

散在型有限単純群が26個しかないという定理の証明よりももしかして短いんじゃなかろうか。