[FOM] A speculative prediction about theorem-proving AI

[Josef Urban]

I should at least add that we have been organizing the discussion-oriented
AITP conference (http://aitp-conference.org/) for the last three years on
these topics. This year the number grew to almost 60 participants - slides
and videos are linked. Anybody interested is very welcome (April 8-12,
2019, Obergurgl).

Josef

On Mon, Jun 4, 2018, 10:35 Josef Urban <josef.urban at gmail.com> wrote:

> 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/eb6e2bfc/attachment.html>