Announcing an automatic theorem proving project

I am very happy to say that I have recently received a generous grant from the Astera Institute to set up a small group to work on automatic theorem proving, in the first instance for about three years after which we will take stock and see whether it is worth continuing. This will enable me to take on up to about three PhD students and two postdocs over the next couple of years. I am imagining that two of the PhD students will start next October and that at least one of the postdocs will start as soon as is convenient for them. Before any of these positions are advertised, I welcome any informal expressions of interest: in the first instance you should email me, and maybe I will set up Zoom meetings. (I have no idea what the level of demand is likely to be, so exactly how I respond to emails of this kind will depend on how many of them there are.)

I have privately let a few people know about this, and as a result I know of a handful of people who are already in Cambridge and are keen to participate. So I am expecting the core team working on the project to consist of 6-10 people. But I also plan to work in as open a way as possible, in the hope that people who want to can participate in the project remotely even if they are not part of the group that is based physically in Cambridge. Thus, part of the plan is to report regularly and publicly on what we are thinking about, what problems, both technical and more fundamental, are holding us up, and what progress we make. Also, my plan at this stage is that any software associated with the project will be open source, and that if people want to use ideas generated by the project to incorporate into their own theorem-proving programs, I will very much welcome that.

DBD2 — success of a kind

Yesterday, as I was walking to my office in the morning, I planned to write a post in which I was going to say that Polymath9 had basically been a failure, though not a failure I minded about, since it hadn’t had any significant negative consequences. Part of the reason I wanted to say that was that for a few weeks I’ve been thinking about other things, and it seems better to “close” a project publicly than to leave it in a strange limbo.

When I got to my office, those other things I’ve been thinking about (the project with Mohan Ganesalingam on theorem proving) commanded my attention and the post didn’t get written. And then in the evening, with impeccable timing, Pavel Pudlak sent me an email with an observation that shows that one of the statements that I was hoping was false is in fact true: every subset of can be Ramsey lifted to a very simple subset of a not much larger set. (If you have forgotten these definitions, or never read them in the first place, I’ll recap them in a moment.)

How much of a disaster is this? Well, it’s never a disaster to learn that a statement you wanted to go one way in fact goes the other way. It may be disappointing, but it’s much better to know the truth than to waste time chasing a fantasy. Also, there can be far more to it than that. The effect of discovering that your hopes are dashed is often that you readjust your hopes. If you had a subgoal that you now realize is unachievable, but you still believe that the main goal might be achievable, then your options have been narrowed down in a potentially useful way.

Is that the case here? I’ll offer a few preliminary thoughts on that question and see whether they lead to an interesting discussion. If they don’t, that’s fine — my general attitude is that I’m happy to think about all this on my own, but that I’d be even happier to discuss it with other people. The subtitle of this post is supposed to reflect the fact that I have gained something from making my ideas public, in that Pavel’s observation, though simple enough to understand, is one that I might have taken a long, or even infinite, time to make if I had worked entirely privately. So he has potentially saved me a lot of time, and that is one of the main points of mathematics done in the open.

DBD1 — initial post

This post is intended as a launch of Polymath9. I have no idea how the project will go, but I think it may be rather short lived, since the difficulties I am having at the moment look as though they could turn out to be serious ones that rule out any approach along the lines I have been thinking about. However, it is difficult to say that with any certainty, because the approach is fairly flexible, so even if the precise statements I have been trying to prove are false, it might be possible to come up with variants that are true. In a way I find that a good state of affairs, because it increases the chances of proving something interesting. Obviously it increases the chances of proving that PNP if one has more ways of attacking the problem. (I’m not claiming that it increases the probability to one that is not small — just that it increases it.) But it also increases the chances of what I would regard as a very nice consolation prize if, as expected, the approach does not work, namely a new barrier to proving that PNP. I don’t think it would be as fundamental a barrier as the three main barriers discovered so far, since it would not be showing that existing methods cannot work. Rather, it would be saying, “Here’s something we could try. Oh dear, it doesn’t work.” But as long as that something was reasonably general, I think its failure to work could be interesting enough to publish.

I’ve thought a little about what phrase to attach to the project (the equivalent of “density Hales-Jewett” or “Erdős discrepancy problem”). I don’t want to call it “P versus NP” because that is misleading: the project I have in mind is much more specific than that. It is to assess whether there is any possibility of proving complexity lower bounds by drawing inspiration from Martin’s proof of Borel determinacy. Only if the answer turned out to be yes, which for various reasons seems unlikely at the moment, would it be reasonable to think of this as a genuine attack on the P versus NP problem. So the phrase I’ve gone for is “discretized Borel determinacy”. That’s what DBD stands for above. It’s not a perfect description, but it will do.

What I did in my summer holidays

This post is intended to accomplish several things at once. First and foremost, I want to explain (not just in the post) why I have been interested in Borel determinacy and in the natural proofs barrier. Roughly speaking (or should I say tl;dr?) I think that Martin’s proof of Borel determinacy has features that might just conceivably offer a way past that barrier.

As long-term readers of this blog will be aware, the P versus NP problem is one of my personal mathematical diseases (in Richard Lipton’s sense). I had been in remission for a few years, but last academic year I set a Cambridge Part III essay on barriers in complexity theory, and after marking the essays in June I thought I would just spend an hour or two thinking about the problem again, and that hour or two accidentally turned into about three months (and counting).

The trouble was that I had an idea that has refused to die, despite my best efforts to kill it. Like a particularly awkward virus, it has accomplished this by mutating rapidly, so that what it looks like now is very different from what it looked like at the beginning of the summer. (For example, at that stage I hadn’t thought of trying to model a proof on the proof of Borel determinacy.) So what am I to do?

Razborov and Rudich’s natural proofs argument

Introduction

The purpose of this post is to add some rigour to what I wrote in the previous post, and in particular to the subsection entitled “Why should we believe that the set of easily computable functions is a ‘random-like’ set?” There I proved that if the Rubik’s-cube-like problem is as hard as it looks, then there can be no polynomial-time-computable property that distinguishes between a random composition of 3-bit scramblers and a purely random Boolean function. This implies that there can be no polynomial-time-computable “simplicity” property that is satisfied by all Boolean functions of circuit complexity at most that is not satisfied by almost all Boolean functions.

I personally find the assumption that the Rubik’s-cube-like problem is hard very plausible. However, if you disagree with me, then I don’t have much more I can say (though see Boaz Barak’s first comment on the previous post). What Razborov and Rudich did was to use a different set of random polynomial-time-computable functions that has a better theoretical backing. They build them out of a pseudorandom function generator, which in turn is built out of a pseudorandom generator, which is known to exist if the discrete logarithm problem is hard. And the discrete logarithm problem is hard if factorizing large integers is hard. Since many people have tried hard to find an algorithm for factorizing large integers, there is some quite strong empirical evidence for this problem’s being hard. It’s true that there are also people who think that it is not hard, but the existence of a pseudorandom generator does not depend on the hardness of factorizing. Perhaps a more significant advantage of the Razborov-Rudich argument is that any pseudorandom generator will do. So the correctness of their conclusion is based on a weaker hypothesis than the one I used earlier.

How not to prove that P is not equal to NP

This is the first of two posts about the difficulty of proving that PNP. The next post will contain yet another discussion (there are many of them online) of the famous paper Natural Proofs, by Razborov and Rudich. This one will set the scene by describing a couple of related but less rigorous arguments. I’m writing them because I’ve been fascinated by the natural proofs result ever since I heard about it on a car journey with Michael Saks about twelve years ago, but up to now I’ve been too lazy to follow its proof in detail. I’m now determined to put that right and writing a couple of blog posts seems a good way of forcing myself to read it properly. Although the proof is short, it has certain aspects that have made it hard for me to get my head round it, so I’ll try to write something considerably longer than what Razborov and Rudich write. I’ll assume knowledge of basic definitions such as Boolean functions, circuits, P, and NP. Also, throughout the posts I’ll write as though is a fixed large integer, when what I’m really talking about is a sequence of integers that tends to infinity. (For instance, I might say that a function can be computed in polynomial time. If is a fixed integer, then that is a meaningless statement, but one can easily convert it into a meaningful statement about a sequence of Boolean functions on larger and larger domains.)

I have a secondary motivation for the posts, which is to discuss a way in which one might try to get round the natural-proofs barrier. Or rather, it’s to discuss a way in which one might initially think of trying to get round it, since what I shall actually do is explain why a rather similar barrier seems to apply to this proof attempt. It might be interesting to convert this part of the discussion into a rigorous argument similar to that of Razborov and Rudich, which is what prompts me to try to understand their paper properly.

But first let me take a little time to talk about what the result says. It concerns a very natural (hence the name of the paper) way that one might attempt to prove that P does not equal NP. Let be the set of all Boolean functions . Then the strategy they discuss is to show on the one hand that all functions in that can be computed in fewer than steps have some property of “simplicity”, and on the other hand that some particular function in NP does not have that simplicity property.

Determinacy of Borel games V

This post is a kind of postscript to the previous four. It consists of miscellaneous observations that shed some light on the proof of Borel determinacy. I’m writing it mainly for my own benefit, but there seems to be no harm in posting it, just in case anyone else finds it interesting.

An attempt to lift that sort of works and sort of doesn’t

One way to get some further insight into the proof of Borel determinacy is to look at some auxiliary games that don’t work as lifts. A particularly natural candidate is this. Let be an infinite (pruned) tree, let and let be the game . Now define a game as follows. Player I plays a move of the form , where is a strategy for with first move . Player II plays a move of the form , where is a strategy for and . Thereafter, the two players must play the strategies and .

Clearly the outcome of this game is decided after the first two moves: if beats then Player I wins and otherwise Player II wins.

Determinacy of Borel games IV

To recap briefly, we have defined a notion of lifting from one game to another and embarked on a proof that every Borel game can be lifted to a clopen game. The stages of that proof are to show that every closed game can be lifted to a clopen game, and that the set of games that can be lifted is closed under countable unions. It is straightforward to show that it is also closed under taking complements, so that will prove that all Borel games can be lifted to clopen games. As we saw earlier, if a game can be lifted to a determined game, then it is itself determined. Since clopen games are determined, this will be enough.

We are in the middle of the proof that closed games can be lifted to clopen games. We have defined the game to which we will lift, and shown how to map Player I strategies for the auxiliary game to strategies for the original game . So the first thing to do in this post is to show how to map Player II strategies for to Player II strategies for .

Determinacy of Borel games III

My aim in this post (if I have enough space) is to prove that every closed game can be lifted to an open (and therefore, by continuity, which is part of the definition of lifting, clopen) game. Since I am discussing a formal proof, I shall be a little more formal with my definitions than I have been so far. Much of what I write to begin with will be repeating things I have already said in the two previous posts.

Trees and paths

Recall the definition of a pruned tree. This is an infinite rooted tree such that from every vertex there is at least one directed infinite path. (Less formally, if you are walking away from the root, you never get stuck.) Given such a tree , we write for the set of infinite directed paths in . If we are working in , then the tree we will work with has finite sequences as its vertices, with each sequence joined to its extensions . Then .

Determinacy of Borel games II

By the end of the previous post, I had said what a Borel subset of was, and what a determined subset was. Martin’s theorem is the statement that all Borel sets are determined.

I also commented that an intersection of two determined sets does not have to be determined, which suggests that in order to prove that all Borel sets are determined, we will need to find a clever inductive hypothesis. This hypothesis should be of the form, “All Borel sets of index less than have property P,” where having property P implies that you are determined, and it is also preserved when you take countable intersections and unions.

Since the property of being determined is quite a strange property, it seems rather unlikely that we will be able to find a much simpler property that does the job. So it is natural to look for a property that is itself related to games and determinacy. But what might such a property be?