[FOM] A speculative prediction about theorem-proving AI
Serguei Mokhov
serguei at gmail.com
Mon Jun 4 12:07:31 EDT 2018
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
More information about the FOM
mailing list