[FOM] A speculative prediction about theorem-proving AI

[Serguei Mokhov]

Indeed, some "ancient" earlier work in the same vein:

Assels, Michael John (1991) Machine learning of logical inference
rules. Masters thesis, Concordia University.
https://spectrum.library.concordia.ca/3623/

-s

On Mon, Jun 4, 2018 at 4:35 AM, 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

-- 
Serguei Mokhov
http://www.cs.concordia.ca/~mokhov
http://cciff.ca | http://mdreams-stage.com
http://marf.sf.net | http://sf.net/projects/marf