Some thoughts about "automated theorem searching"

Let me begin by giving a spoiler warning. If you haven't watched "The Prisoner" you might be spoiled about one of the episodes. Not that matters, for a show from nearly 40 years ago, but you should definitely watch it. It is a wonderful show. And even if you haven't watched it, it's just one episode, not the whole show. So you can keep on reading.

So, I'm fashionably late to the party (with some good excuse, see my previous post), but after the recent 200 terabytes proof for the coloring of Pythagorean triples, the same old questions are raised about whether or not at some point computers will be better than us in finding new theorems, and proving them too.

My answer is a cautious yes, with the caveat that we can still end up regressing to the middle ages with a side of nuclear winter. Or some other catastrophe. But to quote Rick Sanchez, "That's planning for failure, it's even stupider than regular planning." and who am I to argue with the smartest man in the universe? (Although, granted, Rick doesn't care about humanity and he has his portal gun, so that's a solid backup plan...) But I digress.

Assuming that we continue on the path on which we are set, and we don't collapse under our own weight in the world, it is probable that in a few centuries computers can do mathematics better than people. They will probably be able to search for, and prove, theorems that we wouldn't even think about.

And here is where "The Prisoner" comes in. In the episode "The General", Number Two devises a plan for super-saturated-quick-learning through flickering TV statics or something. The plan is to educate everyone, and achieve a measure of uniformity in the general populous. Number Six retorts, however, that if you just transmit facts to people, what you get is still just a row of cabbages, and Number Two answers "Indeed, knowledgeable cabbages". Knowing a bunch of historical facts does not mean that you know history. You are devoid of context, intricacies, and you are only left with dry and meaningless facts. It is us, the people, who generate context, who weave the seams into the names, dates and numbers. We give history meaning, because it is meaningful to us, specifically. It has not meaning otherwise.

In a show about the struggle of the individual against the society that wants them to conform and be a subdued and productive member of society, this is one of the strongest episodes where this message was brought to the surface.

Now. Who writes all these lectures? Ah, that would be The General. A supercomputer which is capable of answering every question, from advanced mathematics to crop spraying. And before Number Two can feed into the computer a question which was driving part of the plot, the claim of the supercomputer's power is contested by Number Six, who then types a short question and feeds it into the computer.

The computer crashes, causing a bit a kerfuffle. As things cool down, the following dialogue ensues:

Number Two: What was the question?
Number Six: It's insoluble for man or machine.
Number Two: What was it?
Number Six: W, H, Y, question mark.
Number Two: "Why?"
Number Six: Why.
Number Two: ...why?

Setting the epistemological awesomeness of Number Six aside; this is what separates, in my opinion, self-aware creatures from robots. We are capable of wondering "why" something is, and why is it even important? And here we circle back to automated theorem searching and proving. Until we develop a conscious machine, that can appreciate the intricate beauty of mathematical questions, and actively select whether or not a theorem is worth searching for, based on past knowledge, and past interest and the likes of it (and any of this will have to be a learning algorithm, because there is just no rigid definition for what is a beautiful mathematical statement), until we can create machines that have this ability, automated searching for theorems is doomed to produced a row of cabbages, even if knowledgeable cabbages, rather than mathematical results that would have been produced by mathematicians.

Because mathematics is meaningful to us, as humans, more than it is meaningful in any other non-existent way. And until computers can endow their existence with the search for meaning, they cannot appreciate why something like coloring of Pythagorean triples is interesting, or why the proof of independence of the continuum hypothesis from the axioms of set theory is beautiful.

Until then, mathematics is a human activity, and a social one too.

(Note, by the way, I didn't say anything about computer verified proofs. That is a different story altogether, and I have different, albeit equally strong, opinions there.)