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.

Frankl’s union-closed conjecture — a possible Polymath project?

Although it was from only a couple of people, I had an enthusiastic response to a very tentative suggestion that it might be rewarding to see whether a polymath project could say anything useful about Frankl’s union-closed conjecture. A potentially worrying aspect of the idea is that the problem is extremely elementary to state, does not seem to yield to any standard techniques, and is rather notorious. But, as one of the commenters said, that is not necessarily an argument against trying it. A notable feature of the polymath experiment has been that it throws up surprises, so while I wouldn’t expect a polymath project to solve Frankl’s union-closed conjecture, I also know that I need to be rather cautious about my expectations — which in this case is an argument in favour of giving it a try.

A less serious problem is what acronym one would use for the project. For the density Hales-Jewett problem we went for DHJ, and for the Erdős discrepancy problem we used EDP. That general approach runs into difficulties with Frankl’s union-closed conjecture, so I suggest FUNC. This post, if the project were to go ahead, could be FUNC0; in general I like the idea that we would be engaged in a funky line of research.

Gil Kalai starts Polymath10

I’ve already mentioned this on Google Plus, but my readership there is different from my readership here, so it seems a good idea to write a similar post here, to give what publicity I can to the fact that Gil Kalai has started a new Polymath project. The problem he would like solved (and I would very much like to see it solved too) is the famous delta-systems or sunflower conjecture of Erdős and Rado.

The problem, as with many problems in combinatorics, is easy to state, but fascinatingly hard to solve. It is a classic extremal problem, in that it asks how big some combinatorial object needs to be before it is guaranteed to contain a subobject of some particular kind. In this case, the object is a –uniform hypergraph, which just means a collection of sets of size . The subobject one would like to find is a sunflower of size , which means a collection of sets such that we can find disjoint sets with the disjoint and with for each . I have used the letters and to stand for “head” and “petal” — is the head of the sunflower and are the petals.

Whither Polymath?

Over at the Polymath blog, Gil Kalai recently proposed a discussion about possible future Polymath projects. This post is partly to direct you to that discussion in case you haven’t noticed it and might have ideas to contribute, and partly to start a specific Polymathematical conversation. I don’t call it a Polymath project, but rather an idea I’d like to discuss that might or might not become the basis for a nice project. One thing that Gil and others have said is that it would be a good idea to experiment with various different levels of difficulty and importance of problem. Perhaps one way of getting a Polymath project to take off is to tackle a problem that isn’t necessarily all that hard or important, but is nevertheless sufficiently interesting to appeal to a critical mass of people. That is very much the spirit of this post.

Before I go any further, I should say that the topic in question is one about which I am not an expert, so it may well be that the answer to the question I’m about to ask is already known. I could I suppose try to find out on Mathoverflow, but I’m not sure I can formulate the question precisely enough to make a suitable Mathoverflow question, so instead I’m doing it here. This has the added advantage that if the question does seem suitable, then any discussion of it that there might be will take place where I would want any continuation of the discussion to take place.

Polymath6: A is to B as C is to ???

The Polymath experiment is still very much in its infancy, with the result that we still have only a rather hazy idea of what the advantages and disadvantages are of open online multiple collaboration. It is easy to think of potential advantages and disadvantages, but the more actual experience we can draw on, the more we will get a feel for which of these plausible speculations are correct.

In my last post but one I outlined a few thoughts about the cap-set problem. Although this wasn’t meant as the beginning of a Polymath project (as I said in the post, it was modelled more on Gil Kalai’s notion of an “open discussion”), it had something in common with such projects, to the point where one of the worries people have about the Polymath approach actually occurred: I suggested a line of attack that was, unbeknownst to me, actively being pursued by somebody.

I do not know exactly what calculations went on in the minds of Michael Bateman and Nets Katz when they decided to go public with their ideas before they had fully worked them out, but my guess is that they wanted to establish that they had got there first. This they did by the very effective method of explaining that the simple observations that I had made were much weaker than what they already knew how to prove. As it happens, the story has had a happy ending for them, since they managed, soon after posting their comments, to push their ideas to the point where they have obtained the first improvement to the Roth/Meshulam bound, something that many people have wanted to do for a long time.

Polymath3 now active

After a long initial discussion period, Polymath3, a project on Gil Kalai’s blog that aims to solve the polynomial Hirsch conjecture, has now started as an active research project. There is already quite a lot of material on his blog, and soon some of it should have migrated to a wiki, which will be a good place to get up to speed on the basics. I will update this post from time to time with news of how the project is going.

Something that is maybe worth pointing out is that although the problem looks at first as though you need to know all sorts of facts about convexity, there is a very nice purely combinatorial statement (about set systems) that would imply the conjecture. So there is no excuse not to think about it …

Polymath news

If you haven’t already spotted this, you might like to know that Scott Aaronson has just posed a very interesting unsolved combinatorial problem and invited Polymath-style thoughts on it. I’ll give a quick and I hope appetite-whetting account of the problem here, but you could skip it if you want and jump straight to his posts on his blog and at Mathoverflow.

The problem is completely elementary, but it has consequences of great interest to theoretical computer scientists. As Scott says, it also seems to be at a realistic level of difficulty and highly suitable for a Polymath approach. (The first assertion is a coded way of saying that it isn’t a notorious “impossible” complexity assertion in disguise.) It asks this. Suppose you colour the points of with two colours in such a way that the origin is red and each of the coordinate axes contains at least one blue point. Do there exist constants , independent of , such that there must be a point that has at least neighbours that are coloured differently from ? At the moment, it seems that there isn’t even a proof that for sufficiently large there must be a point with 100 neighbours of the other colour. There is a non-trivial but not hard example that shows that cannot be more than . (Scott presents this in his Mathoverflow post.) A very brief remark is that if you just assume that not all points are coloured the same way, then the assertion is false: a counterexample is obtained if you colour a point red if its first coordinate is positive and blue otherwise.

Erdős’s discrepancy problem as a forthcoming Polymath project

This is an emergency post, since the number of comments on the previous post about Erdős’s discrepancy problem has become unwieldy while I’ve been away enjoying a bit of sunshine in Luxor. My head is full of amazing details from the walls and columns of ancient Egyptian tombs and temples. The main thing I didn’t see, or at least not until I finally saw them sticking up through the mist from my plane window yesterday morning, was the pyramids, since those are near Cairo. However, I didn’t feel too bad about that as my guide book, the Lonely Planet guide to Egypt, assured me that the pyramids never fail to disappoint (which was just one of many little gems of bad writing in that book).

For the first time for ages, I was completely away from all email and internet for a week, but just before I left, the results of the polls, as they then stood, about the next Polymath project were already suggesting that the Erdős discrepancy problem was the clear favourite, so I couldn’t help thinking about it a certain amount while I was in Egypt. I said that the process of choosing the next problem was not going to be fully democratic, but the fact is that I love the Erdős discrepancy problem and am currently somewhat grabbed by it, so I see no reason to go against such a clear majority, especially as it also has a clear majority of people who say that they are ready to work on it.

The next Polymath project on this blog: some polls

For reasons that I have already gone into, I do not think that the origin-of-life project is suitable as the next Polymath project on this blog, though there seems to be enough enthusiasm for it that I am quite serious about giving it a try at some point in the not too distant future. The complexity-related project also no longer seems such a great idea for now. That leaves three candidates from amongst the problems that I have posted about recently: the project related to the polynomial-DHJ problem, the project related to the Littlewood problem, and the project to solve Erdős’s discrepancy problem. My impression is that for each of these three projects there is already a small group of highly interested people, and certainly my level of enthusiasm for each of these three problems is enough for me to be ready to devote plenty of time to it. (A theory I want to test is that if I post regularly and am not completely stuck, then that will be enough to keep the project feeling active and attracting contributions from other people as well, even if a proof does not appear to be round the corner.)

To help me decide which of the above three problems to go for, here are four polls.

Erdős’s discrepancy problem

I’ve been pretty busy over the last month or so — hence my blog silence — and continue to be busy. But here is one more discussion of a problem that was on my earlier list of possible future Polymath projects. The problem in question is sometimes known as Erdős’s discrepancy problem. This will be a shortish post, because I don’t have much of a programme for solving the problem: if it were adopted, then we would be starting almost from scratch, but that could be an interesting experiment.

Here is the question.

Problem. Is it possible to find a -valued sequence and a constant such that for every and every ?

With the help of a little terminology we can ask this question in a slightly different way. If is a collection of subsets of a set and , define the discrepancy of to be the maximum value of over all . In our case, is the collection of all arithmetic progressions of the special form , and the question is whether there is any function that has bounded discrepancy for this . I say “bounded” rather than “finite” because one can define the function to be the discrepancy of with respect to all those sets in that are subsets of . Then the question is equivalent to asking whether there is any function for which is a bounded function of .