Clarification of Skepticism
Timothy Y. Chow
tchow at math.princeton.edu
Thu Mar 4 22:07:25 EST 2021
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
More information about the FOM
mailing list