[FOM] A speculative prediction about theorem-proving AI

[Josef Urban]

This has been my program for the last 20 years. Indeed, in the recent years
the proportion of people who consider it crazy is going down significantly.
Some recent papers are:

https://arxiv.org/abs/1805.07563
https://arxiv.org/abs/1805.06502

Josef

On Mon, Jun 4, 2018, 06:23 Timothy Y. Chow <tchow at princeton.edu> wrote:

> Some of the recent discussion about formalizing mathematics has led me to
> the following speculative thought about the possibility of artificial
> intelligences outperforming mathematicians when it comes to proving new
> theorems.
>
> It has been rightly pointed out that current AI technology is very far
> away from being able to "come up with new ideas" or "think outside the
> box" in the way that seems to be necessary to produce truly novel and
> ground-breaking mathematical research.  What it is good at is crunching
> lots of data and codifying existing patterns.
>
> To me, this suggests the following possible avenue for theorem-proving
> AIs:
>
> 1. First, large swaths of existing mathematics are formally verified.  As
> FOM readers are well aware, this project is well underway even though it
> has a long way to go.
>
> 2. This body of formal mathematics is then treated as raw data for an AI
> algorithm to study.
>
> 3. The AI extracts patterns and uses those patterns to generate new
> formally verified theorems/proofs/conjectures.
>
> The point here is that this avenue does not require anyone to solve the
> problem of "creativity" or "thinking outside the box."  The artificial
> mathematicians remain "dumb" and "uncreative" but they have seen enough
> human mathematics to be able to mimic it, and generate new instances.  A
> key point is that a large body of formalized human mathematics potentially
> provides an enormous amount of information about what constitutes
> "interesting" mathematics.  We've long understood how to explain to a
> computer what a theorem is, but a big stumbling block has been explaining
> what an "interesting" theorem (or conjecture) is.  Giving the computer a
> huge amount of formalized human mathematics seems to be an excellent way
> to "explain" to it what "interesting" means.
>
> My speculative prediction is that this is the route by which we'll first
> arrive at AIs that prove interesting new theorems.  To me, it seems to be
> an easier route than trying to solve the age-old problem of getting AI to
> mimic human "creativity" and "originality."  As with many (most?) tasks,
> generating new and interesting mathematics may not require any
> "creativity" or "originality."
>
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180604/5dc858b2/attachment-0001.html>