I haven’t yet read all of them (75,000 words!), but I thought that Steven Strogatz’s idea was worth mentioning. With reference to the four-colour theorem, classification of simple groups, and sphere packing, he worries that mathematics might be getting too hard, that the use of computer programs in mathematical proofs leaves mathematicians with the ability to show something is true without understanding why.
Obviously the use of computers as an aid in proofs is relatively new. But, is it new that there are results where we dont really understand why they are true? I’ve always thought that on the frontiers things are usually not well understood; but, as the body of knowledge grows, new tools are developed and new insights achieved, and what was hard becomes easier. Computer proofs may have skewed this progression somewhat, but do they signal a more fundamental change? Is it worth speculating whether or not, without computers, mathematicians might have continued working on the four-colour theorem and we might have a “real proof” by now?
I don’t think I’m quite ready to accept the idea that we are now reaching the limits of the human brain.
Aside: Professor Strogatz mentions a recent article by Brian Davies, Whither Mathematics, which talks about similar issues. It also talks about using formal verification of computer programs when they are included in a mathematical proof. Until now I’ve not paid much attention to such things, but I guess that if mathematical proofs are requiring computer programs then we’ll need techniques to verify their correctness so they can be verified like more traditional proofs.