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.

Opinions of Doron Zeilberger