Abstract #
One of the most important questions in computer science is whether it is intrinsically more time-consuming to come up with an answer than to verify one. This is the so-called question: if they’re equal it’s as “easy” to come up with an answer as it is to verify the answer. That would be pretty weird: doesn’t coming up with answers require more creativity? So most computer scientists are pretty sure . But maybe not! It’s a big question. Just recently it seemed to me, maybe it doesn’t matter anymore?
1 A Magic Answer Box #
Imagine we had a machine that could answer any question. Better than that though, it gives you an incontrovertible proof backing its answer up.
A machine like that would be easy to build: It’s just a computer! It doesn’t even need any fancy AI. Here’s how it works: You give it a (mathematical) statement , and some ginormous number, . It tells you whether there is a proof of of length at most . If there is, it can hand you the proof.
And it’s easy! The magic answer box just generates all possible strings of length at most , and checks if any of them are valid proofs of . Voilà! Creativity is automated.
2 Complexity #
The only issue with the magic answer box is that it’s slow. The only general algorithm we know that is guaranteed to work is very, very slow. Sure, checking one is easier. But we don’t know an efficient algorithm for finding the proofs. It all sounds like the question!
As one famous meat-mathematician once wrote to another:
“The mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine.”
So, being true would be crazy - we might then have an efficient algorithm for automating mathematics!
3 One Million Dollars #
With the recent smashing of Navier-Stokes by [OpenAI](https://openai.com/index/navier-stokes-solution/), I’ve had the
[Millennium Prize Problems](https://www.claymath.org/millennium-problems/) on my mind.
They serve as dramatic lighthouses for mathematical endeavour. These are the amazing, rock hard problems that you get a million dollars for settling (with a proof!).
The difficulty with having them on my mind though, is that I don’t know what any of them really mean. Except, of course for the question. That one, I know a little about. In recent weeks, I’ve heard people say that it is likely the hardest of them all. Even the magician mathematician Terence
Tao is on record saying that it would probably be the last problem to fall. So I’ve dared to wonder recently: maybe I’ll know for sure whether soon.
4 Brainworm #
Of course, you can guess the dreadful imposition that comes blacking in one’s mind: We have automated creativity. An AI has settled Navier-Stokes. I personally have had AIs answer many publishable questions in computer science. I can’t get it out of my head, it turns out, we live in the world!
5 Of Course Not Quite #
Now, sure, yes, . Or maybe not. And Gödel’s magic-answer-box machine is exhaustive, and AI is not. Maybe that makes all the difference. The AIs might fail on some problems, and the magic-answer-box would be guaranteed not to “miss” any proof. But it does make me wonder. Perhaps every natural mathematical question whose answer is within reach of human understanding is also within reach of AI. Maybe of course, and not perhaps at all.
6 I See a Darkness #
So why do I care if anymore? It feels like the only millennium problem I understood, is maybe just another curiosity now. Perhaps the funniest world would be the one where AIs automate creativity, and quickly prove , via an time algorithm for SAT.