Clarification of Skepticism

[Timothy Y. Chow]

Harvey Friedman wrote:
> Serious mathematics generally involves major intellectual JUMPS. I see 
> no evidence that these JUMPS can be simulated by any proof technologies.

Thanks for the clarification.  I agree with your main point that the 
hypothetical achievements you talk about are still relatively far in the 
future.

However, I want to remark that it is easy to overlook, or underestimate, 
the communal nature of mathematical research.  There can be a tendency to 
think of mathematical research as being carried out by a solitary thinker, 
conquering intellectual hurdles by dint of sheer thought.  Some research 
is carried out this way, but any significant mathematical achievement must 
at minimum stand on the shoulders of giants, and most achievements involve 
non-trivial, real-time interactions between human beings.

The term "automated theorem prover" has a strong connotation that a 
computer has to come up with a proof *by itself*.  Let me point out that 
we never judge human mathematicians that way.  We don't regard it as 
cheating to enroll as a graduate student and take courses at a university, 
to talk to other mathematicians, or to search the literature.  If a small 
group of mathematicians has a healthy collaboration, they don't waste 
effort arguing about whether a JUMP was made by a single individual or by 
the group talking it out together.

Suppose programs get to the point where they can really *interact* with 
humans at the level where they use human language to ask questions, give 
lectures, and even carry on live conversations about an open research 
problem with the same fluency that human colleagues can.  You might argue 
that at that point, they are no longer proving theorems "by themselves." 
But so what?  If JUMPS are being made that wouldn't have happened 
otherwise, who cares how exactly we slice and dice the credit for the 
JUMP?

Even today, I would submit that it may be misleading to ask whether 
programs can perform solo JUMPS a la Evel Knievel.  The more relevant 
question is whether JUMPS are being made that would not be made without 
the program.

Tim