Some thoughts about "automated theorem searching"

Jun 27 2016, 01:02

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.