[FOM] A speculative prediction about theorem-proving AI
Timothy Y. Chow
tchow at princeton.edu
Sat Jun 2 21:28:50 EDT 2018
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
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
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."
More information about the FOM