Classification of finite simple groups, undoubtedly, is very long and consists of a number of works by many different mathematicians, but the difficulties prese

Classification of finite simple groups, undoubtedly, is very long and consists of a number of works by many different mathematicians, but the difficulties presented by that proof are of a qualitatively different nature than those presented by the proof of the Four-Color-Theorem. For the classification of finite simple groups, mathematicians comprehend the plan of attack broadly, are able to understand why it is true - and simpler second-generation and third-generation proofs are being published now (which of itself is evidence of improved understanding). The proof has resulted in new techniques broadly applicable to other problems, and new insights into the subject. It has led to the discovery of additional sporadic groups, and more connections between them. However, the issue with the four-color-theorem is different: It's a proof that simply goes through all the reduced cases one by one, and checks it. Even if one had a lot of time, no mathematician should really bother reading through it, as there is no technique or idea one could absorb, and one would not really come out with any understand of why true or any way to apply it outside the problem. It is just mindless brute-force checking. It's like reading a telephone directory. I am not against computational mathematics or computational proof by the way. I am also for proof-checkers. I don't dispute the validity of computational proofs, or question their philosophical status. I do think one core aspect of the practice of mathematics has been in increasing human understanding of it, not merely compute things with symbols. Human mathematics is an act of summary/compression, and of translation at once (from a vast number of mathematical facts to the human language). In this sense - in physics too, simple "laws of physics" like Maxwell's Equations or Newton's Laws are amazing because they compress so many different things one could observe and convey something essential about their nature in a way humans can comprehend and tinker with, to produce further artifacts - like the electric motor or the steam engine. Nature (mathematical or physical) already knows (and operates within) its own laws, it is humans that need to be looped in. Hence my dissatisfaction of computer-generated proofs that don't enhance human understanding much.