Progress on automated mathematical theorem proving?

There's apparently an annual automated theorem proving competition, looking at the kinds of problems there might be useful.

The space of theorems that are "very routine and not requiring any ideas" is actually pretty interesting. In particular, compilers do quite a lot of theorem-proving of the "these functions are equivalent" variety, and it's way more elaborate than most people imagine.

|A kind of counter-example to your claim is the following: http://www.math.rutgers.edu/~zeilberg/GT.html It is an automated reasoning system for Euclidean geometry. Starting from literally nothing, it derived all of the geometric propositions in Euclid's Elements in a matter of seconds. Then it proceeded to produce a number of geometric theorems of human interest that were never noticed by any previous Euclidean geometers, classical or modern.

This is simply to point out that there are some fields of math that are classically very hard but computers find trivial. Another example is the verification of random algebraic identities by brute force.

On the other hand, large fields of mathematics have not yet come to be dominated by computers. For those I think this paper is a good introduction to some state-of-the-art, machine-learning based techniques: http://arxiv.org/abs/1108.3446 One can see from the paper that there is plenty of room for machine learning techniques to be ported from fields like speech and vision.

Progress in machine learning in vision and speech has recently been driven by the existence of huge training data-sets. It is only within the last few years that truly large databases of human-made proofs in things like set theory or group theory have been formalized. I think that future progress will come as these databases continue to grow.

The only novel theorem I can recall being solved by a general artificial theorem prover is the Robbins conjecture. I'm sometimes surprised this area doesn't attract more attention, since proving theorems is very similar to writing programs and automated program writers would be extremely useful.

It's easy to give an algorithm that generates a proof of a mathematical theorem that's provable: choose a formal language with definitions and axioms, and for successive values of n, enumerate all sequences of mathematical deductions of length n, halting if the final line of a sequence is the statement of the the desired theorem. But the running time of this algorithm is exponential in the length of the proof, and the algorithm is infeasible to implement except for theorems with very short proofs.

Yes this approach is valid, but modern theorem provers more commonly reduce theorem proving to a sequence of SAT problems. Very roughly, for a first order sentence P, the idea is to search for counterexamples alternately to P and ~P in models of size 1,2,... . SAT solvers have improved rapidly over the past decade (http://www.satcompetition.org/), though they are still not good enough to facilitate theorem provers that can solve interesting math problems.

I highly recommend the concise and excellent "Handbook of Practical Logic and Automated Reasoning" http://www.cl.cam.ac.uk/~jrh13/atp/

Current theorem provers don't have a "sense of direction".

From the description of Polya's Mathematics and Plausible Reasoning: Vol. II: Patterns of Plausible Inference:

This is a guide to the practical art of plausible reasoning, particularly in mathematics but also in every field of human activity. Using mathematics as the example par excellence, Professor Polya shows how even that most rigorous deductive discipline is heavily dependent on techniques of guessing, inductive reasoning, and reasoning by analogy. In solving a problem, the answer must be guessed at before a proof can even begin, and guesses are usually made from a knowledge of facts, experience, and hunches. The truly creative mathematician must be a good guesser first and a good prover afterward; many important theorems have been guessed but not proved until much later. In the same way, solutions to problems can be guessed, and a good guesser is much more likely to find a correct solution...

Current theorem provers search for a proof, and even contain some ad hoc heuristics for exploring their search trees. (For example, Paulson's book ML for the working programmer ends with a chapter on theorem proving and offers "We have a general heuristic: never apply universal:left or existential:right to a goal if a different rule can usefully be applied.) However, Polya's notion of being a good guesser has been formalised as Bayesian reasoning. If a theorem prover, facing a fork in its search tree, uses Bayes Theorem to pick the most likely branch first, it may find much deeper results.

I don't think there is currently much overlap between those working on theorem proving and those working on Bayesian statistics. There is perhaps even a clash of temperaments between those who seek absolute certainty and those who seek an edge in the messy process of muddling through. Nevertheless I foresee great possibilities of using Bayesian reasoning to guide the internal search of theorem provers, thus giving them a sense of direction.

Reasoning "X hasn't been progressing recently, therefore X is unlikely to progress in the near future." is good reasoning if that is really all that we know. But it is also weak reasoning which we should be quick to discard if we see a relevant change looming. The next ten or twenty years might see the incorporation of Bayesian reasoning as a guiding principle for tree search heuristics inside theorem provers and lead to large advances.

The Ganesalingam-Gowers project is not about the cutting edge of automated theorem proving and there is no reason to expect that blog post to talk about the cutting edge. The contribution of that project is to make the input theorem and output proof be human-readable.

If somebody was able to write a program that's able to find proofs [involving substantive ideas], I would consider that to be strong evidence that there's been meaningful progress on general artificial intelligence. In absence of such examples, I have a strong prior against there having been meaningful progress on general artificial intelligence.

That strikes me as like saying, "Until this huge task is within a hair's breadth of being complete, I will doubt that any progress has been made." Surely there are more intermediate milestones, no?

Given that I think that capturing the ingenuity of human mathematicians is one of the last things I'd expect to see before seeing human-level-or-smarter AI, the poor state of automated theorem proving doesn't seem to me like much evidence on how far away GAI might be.

The Prover company is working on the safety of train signalling software. Basically, they seek to prove that a given program is "safe" along a number of formal criteria. It involves the translation of the program in some (boolean based) standard form, which is then analysed.

The formal criteria are chosen manually, but the proofs are found completely automatically.

Despite the sizeable length of the proofs, combinatorial explosion is generally avoided, because programs written by humans (and therefore their standard form translation) tend to have shapes that lend them amenable to massive cuts in the search tree.

It doesn't always work: first, the criteria are simple and bounded. Second, combinatorial explosion sometimes does occur, in which case human-devised tweaks are needed.

Oh, and it's all proprietary. Maybe there's some related academic papers, though.

If you expand your net outside of pure symbolic manipulation, there has been a lot of progress in general artificial intelligence. There is no evidence that a practical mathematical theorem prover, if ever created, will work using pure symbolic manipulation approaches.

EDIT: I'm curious to know why the person who down-voted me did so.

It's easy to give an algorithm that generates a proof of a mathematical theorem that's provable: choose a formal language with definitions and axioms, and for successive values of n, enumerate all sequences of mathematical deductions of length n, halting if the final line of a sequence is the statement of the the desired theorem.

Nitpick: This only works if the chosen formal system only contains rules that produce longer theorems.

Edit: Oops, looks like I misread the quote. This method will enumerate all theorems, but not (as I first interpreted it) decide if a given string is a theorem in finite time.