Automated theorem proving via unsupervised approaches

Question

This question Where and how did computers help prove a theorem? considers some automated theorem proving successes.
However they seem to be mostly supervised approaches, such as with the 4 color graph theorem, the researcher did/does the hard conceptual, non-automatable work of narrowing the conjecture to a finite (but large) set of computer-checkable cases.
Also, in other cases/examples the computer may have found an "infinite" type proof but have been obtained largely by the researcher closely intervening/guiding the overall theorem proving process.

Are there any significant examples of what could be called unsupervised theorem proving successes?

This would generally come in two forms:

• only the theorem statement/conjecture, which refers to infinite cases, is given to the computer and the computer manages to find it (ie prove it) without any human intervention/assistance.

• the computer searches all theorems and lists "interesting" ones based on some algorithmic criteria/rating, and later after browsing through the list, the researcher recognizes "mathematically significant" proof(s) that are standard or can be found in the literature.

^{(Note: I have some possible example(s) of the above & depending on response may answer with them.)}

Answer 1

Clarification on terminology

The theorem proving community does not use the terms supervised and unsupervised. They use the terms interactive theorem proving or automated theorem proving. If you give a conjecture to the prover and it always comes back with a yes or no answer, such a prover is a decision procedure for a logical theory or simply called a decision procedure.

Proving statements of an infinite nature

The intuition that a theorem that involves an infinite number of cases will be difficult for a machine is misleading. Consider the statement below.

The sum of two even numbers is an even number.

If you were do prove this by enumerating even numbers, there are infinitely many cases to consider. This statement is expressible in Presburger arithmetic. Presburger arithmetic is the first-order theory of the Natural numbers with the constants zero, one, addition, and equality. Presburger in his 1929 Masters thesis showed this theory to be decidable. There are other facts of an 'infinite' nature that can be expressed in Presburger arithmetic and proved algorithmically.

Fully Automatic Theorem Proving

In asking for a machine that works with no assistance, you are asking for a decision procedure. It does not make much mathematical sense to ask for a decision procedure for one conjecture. If the conjecture is either true or false, there is a a trivial decision procedure. What we do in practice is try to find a logic that can express a conjecture we care about and try to prove the logic is decidable.

There are many many logical theories that are known to be decidable. Presburger arithmetic is a standard example. Another famous example is the first-order theory of real closed fields. The axiomatization provided by Tarski and his collaborators is sufficient to express statements of Euclidean geometry without measurement of angles or trignometric functions. This theory is decidable though the complexity is non-elementary.

Observe again that the intuition that complexity of proving a statement depends on the cardinality of the underlying domain is quite misleading. The intuition that the complexity of automatically proving a statement corresponds with how late in our education we meet that idea is also misleading.

The theory of the natural numbers with addition and multiplication is undecidable. The first order theory of real-closed fields is decidable but the proof is quite complex. The first-order theory of algebraically closed fields, which includes facts about complex numbers is also decidable. The proof for algebraically closed fields takes one or two pages in logic textbooks.

To summarise, you are asking about decision procedures for logical theories. There are many of them.

Interest

Success of a tool and interest of the theorems are highly subjective. The value of a theorem changes over time. Theorems proved at a certain time are forgotten and rediscovered a few decades later when they are celebrated by the community. It is easy to claim a theorem significant in retrospect and put it in a textbook, but it is not easy to recognise the significance of a theorem when it is proved. There is also the matter of relevance. There is much in a model theory text book I find boring and much in an automated deduction book that a model theorist would find boring, even though we both work in the field of logic.

There are decision procedures that can prove statements in textbooks. Tarski's decision procedure can prove the statements in Euclid's Elements. There are some statements in elementary number theory and linear algebra that decision procedures can prove.

The company TheoryMine sells theorems. (Yes, you can now proudly go to a medieval market and barter two theorems about list reversal for a kilo of unwashed potatoes.) The techniques they use to identify interesting theorems may answer your question.

Success

There are many ways to define success of a theorem prover. If you're asking whether a fully automatic theorem prover has ever, entirely by itself, proved a statement that mathematicians wanted to prove, I believe there might be stray examples, but they are not considered major successes.

Asking if a piece of technology can achieve the same things a human being finds interesting misses the point. It's interesting for a human being to hike up a mountain but trivial for a helicopter.

The major success of automated theorem provers is proving theorems about machines. Reasoning about the correctness of a cache coherence protocol, a floating point multiplication algorithm, a device driver are all highly non-trivial problems of a scale and intricacy that our limited monkey brains cannot deal with.

There is a theorem prover in the production flow of an Intel chip. There is a theorem prover shipping with Windows 7 and Windows 8 device driver kits. These theorem provers and the theorems they prove save more money and affect the daily lives of more people than most of our manually derived proofs ever will. That reeks of success to me.

On The Capabilities of Theorem Provers

This is in response to a question about whether there is an automatically generated proof of the infinitude of the primes (automatic, not computer assisted).

I am not aware of such a proof. However, one should ask what the consequences of such a proof are. If a human being can prove this statement, I think we can conclude they know something about numbers and about proofs. The consequences of an automatic proof would be very significant. The automatic procedure would also be able to solve open problems in mathematics. The problem is that difficulty and capability are very different for human beings and for machines.

To summarise, we have absolutely no illusions about what can be proved completely automatically. The goal of the field is not to replace or compete with human mathematicians. It is not surprising that a machine cannot prove what a human being can prove. It is insightful to understand that the consequences of a human being proving something are quite different from a machine automatically proving something.

Answer 2

Here is a recent one: http://link.springer.com/chapter/10.1007%2F978-3-319-09284-3_17 You can get the fulltext here: http://arxiv.org/abs/1402.2184

It uses some state-of-the-art SAT solvers (see http://fmv.jku.at/lingeling/) to solve a member of a family of problems called "Erdős Discrepancy Conjecture". They encoded the problem as SAT instances and the SAT solver discovered proofs that there is a solution of certain length, and also a that there is no solution of a greater length.

An interesting fact about the latter part is that the proof runs into gigabytes. Proofs of non-existence of solutions to SAT problems are usually huge. At the time this work was presented, it was (and perhaps it still is) an open problem to convert that gigabyte sized proof to a few paragraphs that can appeal to human intuition.