[FOM] A speculative prediction about theorem-proving AI

[Timothy Y. Chow]

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