[FOM] Talk on Formal Verification

[Timothy Y. Chow]

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