[FOM] Talk on Formal Verification
Timothy Y. Chow
tchow at alum.mit.edu
Fri Feb 5 17:02:50 EST 2016
Colin McLarty wrote:
> I really doubt that Tim Gowers thought AI would never be able to think
> of factorials in the search for runs of composite numbers. What could
> be more paradigmatic of composite numbers than factorials, or a more
> convenient source of numbers with many factors?
>
> Much more likely he was thinking of the sort of results he has been
> getting lately, and much prominent work by others, on the distribution
> of prime gaps.
A couple of years ago, Gowers made some comments on this topic in the
context of a MathOverflow question:
http://mathoverflow.net/questions/48771/proofs-that-require-fundamentally-new-ways-of-thinking/48868#48868
At the time, Gowers was leaning towards the view that there is no
fundamental obstacle to teaching computers to be creative in the limited
domain of research mathematics. I quote:
The reason these proofs interest me is that they are the kinds of
arguments where it is tempting to say that human intelligence was
necessary for them to have been discovered. It would probably be
possible in principle, if technically difficult, to teach a computer
how to apply standard techniques, the familiar argument goes, but it
takes a human to invent those techniques in the first place.
Now I don't buy that argument. I think that it is possible in
principle, though technically difficult, for a computer to come up with
radically new techniques. Indeed, I think I can give reasonably good
Just So Stories for some of the examples above. So I'm looking for more
examples. The best examples would be ones where a technique just seems
to spring from nowhere -- ones where you're tempted to say, "A computer
could never have come up with *that*."
If Gowers has written anything else on this topic, I would be interested
in reading it.
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.)
Tim
More information about the FOM
mailing list