Technology for Which Mathematical Activities?/1

[Harvey Friedman]

The various postings expressing optimism about the use of technology
based on current developments have NOTHING TO DO with what I am
saying.

For various specialized tasks of interest, there has obviously been
more and more useful technology.

For certain other tasks of even greater interest, progress appears
totally unthinkable at the moment.

I really was only making my obvious point IN PASSING. I was setting
the stage for discussing what are the REALISTIC outcomes of proof
technology research that have been OVERLOOKED and that I do think are
FEASIBLE, although difficult.

I will by the way defend attacks against me for finding TEX a
disgusting nuisance. But I don't think that this is a useful
discussion for FOM.

As far as technology is concerned, music performance software of the
kind I had to master some of (say DP), makes Tex look like a
specialized joke, and is REALLY useful. I created a new kind of piano
recording based on thousands of hours of micro editing with this
splendid technology which makes tex output look like a minor ugly
eyesore in comparison. If you are interested in this path breaking
story in piano performance you can talk to me offline. I credit my use
of this performance software to my being well on the road to top
professional classical pianism in the ordinary sense with fingers. I
would be interested if the use of TEX can be credited for putting
people well on the road to top professional mathematics.

WE ALL KNOW THAT technology help for doing mathematics is around. The
real question is: for what kinds of things? Making completely
unsupportable claims of prospects that are totally unwarranted,
instead of FOCUSING ON the kinds of things that are realistic, is
rather counterproductive with the general mathematical community.

I suggest we compile and discuss a list of things, generally
explainable, which have yielded progress and we can expect more
progress. And say something new maybe about this. Here are some.

1. HELP IN formulating conjectures. NOW this is only realistic in
CERTAIN KINDS OF MATHEMATICS. Interesting to understand which kind it
is and which kind it is not. If it involves VISUALIZATION, hen of
course. Generating pictures on a screen can be a huge addition to
generating pictures in the mind or on paper. Would be interesting. And
obviously certain kinds of discrete mathematics, involving counting
finite sets, particularly when the challenges already surface in the
manageable finite, is another.

2. HOWEVER: help in formulating conceptual breakthrough conjectures is
another matter. Finding the right conjecture that explains some
mysterious phenomena, or yields a startling revelation about a field -
thee are crucially important endeavors. For instance, Goedel came up
with the precise statement that is now known as the COMPLETENESS
THEOREM FOR PREDICATE CALCULUS. Then proved it. Would he benefit from
technology to even think of the completeness theorem?

3. AND HOWEVER, help in formulating KEY DEFINITIONS. Frege invented
first order predicate calculus. Are we going to say that with the help
of computer technology, this would be facilitated?

4. Also tell me how computer technology is going to help Solovay and
Reinhardt lay out the fundamental large cardinal hierarchy based on
nontrivial elementary embeddings? And tell me how computer technology
is going to help Cohen discover forcing, or Goedel discover L?

5. ESTABLISHING ABSOLUTE RIGOR. That, like 1, is where the technology
has really made a difference. BUT doing this for a big theorem BEFORE
it has really been well understood? Like - I have a pretty good idea
of how to prove the Riemann Hypothesis maybe in about 50 pages using
this and that this way and that way. Before I really can understand
the details of how the subtle parts work together, I will use my proof
assistant. I AM VERY DOUBTFUL ABOUT THIS. After the big theorem has
been fleshed out and well understood, THEN with the technology doing
proof verification IS GENERALLY VIABLE, although it is still
INCREDIBLY TIME CONSUMING. WHAT ABOUT formally verifying FLT? I have
no doubt that this will be done by 2100, but WILL INVOLVE SERIOUS
REWORKING AND SIMPLIFICATIONS of the proof and a lot of serious time
commitments. And the key ideas in those preliminaries are just not
going to be using technology.

6. FINDING ERRORS. There are, as I understand it, some interesting
cases of this. I would like to HEAR MORE ABOUT THIS. Obviously very
unusual, but very interesting. ESPECIALLY if we can use this to help
us see SYMPTOMS OF where conventional acceptance of theorems can go
wrong.

7. NOW LET'S GET REAL. Instead of my making all this fun about this,
WHERE ARE THE UNUSUAL situations? What are they like?

I still haven't got to my main points about WHAT FOUNDATIONAL
INFORMATION CAN BE HOPE TO GET OUT OF THE TECHNOLOGY? I.e., Structural
Proof Theory.

Harvey Friedman