[FOM] Talk on Formal Verification

[W.Taylor at math.canterbury.ac.nz]

Quoting "Timothy Y. Chow" <tchow at alum.mit.edu>:

> If Gowers has written anything else on this topic,

An interesting related bagatelle here is that, just as people are
astonished (as Gowers noted) by first seeing analysis used to prove
number-theoretic problems, it also goes the other way.

A simple little example of this is the anonymous theorem, (that Just-So-ly
*could* have been the first of its type), that log_2(3) is irrational.
It is startlingly cute to note that this "analytic" result boils down
to noting that 2^m = 3^n is impossible in the naturals, a basic number
theoretic result.

The trouble with all these cases is that it is very hard to re-cast
one's mind back to before one saw some "human-only" result, to try
to imagine whether a machine could do it.  In particular, Tim has
put his finger on a sore point:

> As a side comment, I think that if someone wanted to make a serious
> effort to get computers to come closer to doing research mathematics,
> a good first step might be to try to train a computer to solve
> International Mathematical Olympiad problems.  I'm guessing that
> within 50 years, computers will solve IMO problems better than most
> contestants.  I also predict that this will happen *not* by getting
> computers to be creative and insightful, but by convincing ourselves
> that solving IMO problems doesn't really require much creativity and
> insight.  (In fact I think there's a good chance that if computers
> eventually become better than humans at doing mathematical research,
> a byproduct will be that we'll become convinced that mathematical
> research doesn't require creativity or insight.)

I agree with his 50 year comment, and also especially with the last point,
that in effect we always think machines "haven't really done it", by
shifting the goalposts.  This has been seen with computers playing
world champ Chess, now very close to that with Go, and allegedly with
the "Jeopardy" game.

Tim is right to observe that we will undoubtedly shift the goalposts on
math creativity as well; we just cannot believe that any non-biological
machine will ever really "think like we do"!

Bill Taylor


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.