Written: March 24, 2009
I just finished writing a 12 page article that may not be as deep as some of the better traditional articles, for example this one, but it is much more fun to read.
These two articles are very different, but they have (at least) one thing in common: they both will soon (in ≤ 50 years) be considered utterly trivial. The latter because it would be doable in a few nano-seconds on any small computer, and the former because the elaborate and tedious Maple programming, that I spent three months developing, will take a few minutes to program, using a much higher-level future analog of Maple, that will make the current package accompanying my article seem like machine-language programming.
But, for us who live today, and who want to get a rough idea of the style of future mathematical communication, my humble article offers a much better approximation than Wiles'. If you notice, there are hardly any theorems or proofs in the body of my article. Most of the article is a very informal chat about the main ideas that went into the software development, and are meant to convey a methodology for what I call rigorous experimental mathematics. In other words, this is "meta-mathematics". The mathematics itself, i.e. the computer-generated theorems and proofs, are not part of the article itself, but rather are given in the accompanying webpage.
David Ruelle once said that a typical human mathematical paper is "a dance around a formal proof". With computer-generated mathematics, we will no longer need to pretend to be formal. All the formal part will be done by computers, and for the next fifty years, the (formal) programming, by us humans. But since a computer program is meant to be understood by computers, we don't have to bother writing it in humanese. Instead, just like in my article, the human author describes informally the main ideas, that would hopefully lead the readers to tackle other problems with that approach, and write their own programs. And who knows, perhaps there exists someone who knows Maple well enough, and arithmetic algebraic geometry and modular forms well enough, to start computerizing Wiles' proof. I have no clue about the details, but it seems to me that there are lots of computations there, and, even today, I am willing to bet that it would be possible to shrink the 108 pages (and countless more pages of the many results that Wiles uses) to many fewer pages, modulo routine calculations that the computer can do, all by itself. Of course, if all this would do is shorten the proof of FLT, it wouldn't be worth the trouble, but I am sure that the effort, along the same lines as my own effort of computerizing the ingenious method of proof of Amleh, Grove, Kent, and Ladas, would be useful in trying to prove many still unsolved problems.
So learn Maple (or Mathematica, or Sage etc.) young people! Better still, try to develop a better, higher-level computer algebra system, and then try and teach the computer the nifty tricks of Wiles and company.