Automatic theorem proving is the branch of computer science devoted to trying to program computers to find proofs of theorems. For a long time the field appeared to reach a plateau, with even quite simple proofs (for humans) remaining stubbornly out of reach for computers, at least for programs that did not in some sense "cheat" by having problem-specific heuristics hard-coded in. More recently, machine learning has had a significant impact, and there are some researchers in that area who are optimistic that computers will surpass humans at mathematics within the next ten to twenty years.
The aim of this project is slightly counterintuitive: it is to go back to more old-fashioned methods and try to push them further. More precisely, the aim is to understand in detail how humans find proofs, and then to use that understanding to program computers to find proofs in the same way. We go into the project with our eyes open, in the sense that we are well aware that there may be important aspects of the proof-finding process that rely on the kind of pattern recognition that machine learning and statistical methods are much better suited to than deterministic rule-based algorithms. However, it is also clear that much of the proof-finding process also involves search methods that can be clearly explained and programmed in a rule-based way: one of the aims of the project is to design a theorem-proving program that makes minimal use of black boxes.
One reason for doing this is to try to improve our theoretical understanding of how mathematicians find proofs. It is easy to show that the general problem of determining whether a given mathematical statement has a proof of up to a given length is NP-complete. Since it is also an observable fact that human mathematicians are capable of finding long and complicated proofs, the question naturally arises of what the features are of the statements we prove and the proofs we find that make finding them more tractable than solving worst-case instances of the general problem. This seems like an obviously interesting and important problem, but it has received surprisingly little attention.
A second reason is that it is hard to predict at this point what mix of rule-based programming and machine learning is likely to be best suited for automatic theorem proving. Given that, it seems sensible to develop both approaches as far as we can. There are already several teams working on machine-learning approaches (which is not to say that they have no rule-based component, but simply that the emphasis is different), so the expected additional value of pursuing a different approach seems greater than that of trying to do something more similar to existing work.
A third reason is that even if this project reaches a point where it is hard to do without machine learning, it may be that that point will be in a different place from where it is now. One possible outcome that would count as a success for this project would be if we could design a prover that was not fully automatic but that instead required the user to make choices from time to time from some limited set of possibilities. That would open up the possibility of training a machine to make those choices instead. This would not be the first hybrid approach to the problem, but it might be an interestingly different one.