I’m a computer programmer and mathematics aficionado. Have been reading your Opinions and the 51st inspired my response.
The computational/combinatorial complexity doesn’t seem to be a proper measure for ‘deepness’ of mathematical results. The discovery of irrational numbers by Pythagoras’s pupils is technically simple (no wonder it happened long ago) yet many would agree it’s ‘deep’. It may well be that the bulk of mathematical universe is made of ‘dark’ stuff in the spirit of Gregory Chaitin – random facts, inaccessible from any axioms, or undecidable, or in NP, requiring hopelessly (for any conceivable computer technology) long sequences of ad-hoc, unique logical steps to get themselves established. FLT called for a couple of hundred pages, not bad even for a computer. Yet FLT itself didn’t count as much as the ideas and methods developed along the way. Five years later they helped solving the (important?) Taniyama-Shimura-Weil conjecture. In my view revealing patterns and/or web of relationships in that sea of seemingly random mathematical truths is what deepness and significance are all about. The wider the pattern, the deeper the result. Some topics are even ‘inherently’ fundamental, e.g. the real numbers.
It’s hard to say if 4CT is worth scrutinizing with pencil and paper. Probably not if it appeared to be just “one-line proof modulo routine-checking”, which would be rather too bad. Going through a proof, a mathematician could stumble on unexpected associations, connections or revelations. One can program the computer to look for some side effects, set checkpoints etc., but what is really worth cannot be anticipated. And prospective computers will most probably remain blind enough to spot, let alone pursue, what is really worth.
The game of chess seems a good analogy. Simple rules and initial configuration explode into a huge search space. Discernible strategic patterns spring into existence and melt down into the vast void of ad-hoc, tactical, “eye-for-eye” variations spontaneously and seamlessly. The recent man-machine contests demonstrated the treachery of navigating such an environment for both sides. Yet chess is only a game. Mathematics is incomparably more ‘serious’ and diverse semantically and intractable computational domains abound ever since. Here the vision and insight are indispensable. Computational power could help a lot, obviously, but it still needs to be wisely guided. One can imagine an omnipotent intellect (self-learning neural networks, genetic algorithms etc.) capable of spotting any tiny hints of pattern or structure but what if the scope is featureless at larger scales? Going door-to-door mocking up doesn’t look like the best strategy. A software program might be able to exhaust a combinatorial domain, not necessarily humanly incomprehensible, and still not find significant patterns. Such an outcome would be depressing and not very helpful. What’s wrong with the extensive searches? Exactly the trait that every single case has to be verified but the outcome is unpredictable (otherwise no search would be needed). Potentially one could end up with choppy, messy result that defies any reason. Not much could be inferred from a bunch of strictly local, isolated, ad-hoc facts. The search tour de force certainly wouldn’t make them any deeper or non-trivial. Fortunately, most searches do unearth some patterns, whose ‘explanation’ or conceptualization are built in the search algorithm (hatched out by a human!) or come later, facilitated - no doubt about that - by the row search data.
My personal fear of a non-expert is that the mathematical universe could be chaotic and one would increasingly need to resort to monstrous combinatorial computations just to find out about some curious, unique, humanly inaccessible Platonic realities pointing to nowhere. The technical difficulty of (ultra) finite domains could be a clue to a lack of nice behavior. Yet the genome is a striking example of the order of complex organization finite systems can achieve. On the other side, the wonderful conceptual richness of the infinite makes us struggle with the proliferation of models and their consistency. The prospects for chaos seem infinite too.