# Has any previously unknown result been proven by an automated theorem prover?

Despite these theoretical limits, in practice, theorem provers can solve many hard problems...

However it is not clear whether these 'hard problems' are new. Do computer-generated proofs contribute anything to 'human-generated' mathematics?

I am aware of the four-color theorem but as mentioned on the Wikipedia page, perhaps it is more an example of proof-verification than automated reasoning. But maybe this is still the best example?

-
Of course. Turn on any theorem prover, and soon you will get a previously unknown (and totally uninteresting) result. So what we really want to know is interesting results obtained this way. That is what the answers show us. – GEdgar Aug 16 '12 at 15:42
Depending on what you mean by "theorem provers", there are a lot of interesting results in Computational Problems in Abstract Algebra, edited by John Leech. – MJD Aug 16 '12 at 21:57

Check out A Summary of New Results in Mathematics Obtained with Argonne's Automated Deduction Software. It lists many solved problems (even though it's an old page, it summarizes results obtained until 1995).

Some information is also here, section What has Automated Theorem Proving been Really Useful for?.

-

Robbins' conjecture that all Robbins algebras are Boolean algebras was first proved using EQP, after Tarski and others had tried and failed to prove or disprove it.

-

The Robbins Conjecture, which has already been mentioned, is probably the most interesting example for what automated theorem provers are capable of already. Another interesting piece of information I remember is that the Logic Theorist programme in the mid-fifties was able to prove much of the Principia Mathematica by itself and even managed to find a more elegant proof for the Isosceles Triangle Theorem than Russell himself.

However, I would like to clarify what you said about the Four Colour Theorem: what Wikipedia refers to is the proof of this theorem using Coq, which is an interactive theorem prover. The basic idea is that the user provides a step-by-step proof and the theorem prover proves the validity of each step itself. Different theorem provers have different levels of automation; the only one I am familiar with is Isabelle, which has quite powerful automation. A remarkable example is Cantor's theorem that there is no injective mapping from a set to its powerset, which can be proven completely automatically by one of Isabelle's many proof methods. However, this is more or less a coincidence, the system can't usually prove theorems like this on its own, but it handles things like tedious simplifications and case distinctions quite well and sometimes solves problems that are not immediately obvious to me automatically. Unfortunately, most often, it is the other way round.

-
Where you said "there is no injective mapping from a set to its powerset" I think you meant to say " there is no surjective mapping from a set to its powerset". – bof Sep 11 at 8:55

google for this "automated theorem proving in hardware design" (without the quotes). There are a lot of interesting hits, showing automated theorem proving being used for hardware design. The theorem then would be something like "Design X verifies the specified properties", certainly an interesting theorem in its way, but maybe not what the OP thought of?

-

Ken Kunen has some work on loops where original results were proved by theorem prover. He has this program of first proving results this way and then analyzing the result to get a good human understandable proof.

-
Could you give a reference? – Nate Eldredge Aug 16 '12 at 22:23

Bob Veroff has a few examples of results that I believe many would find interesting, first proved by a computer, such as relatively short single axiom bases for Boolean Algebra. Though, not all of what he proves there makes for a new result.

A perhaps better example consists of the proof of XCB as one of the shortest single axioms for the classical equivalential calculus under E-detachment (from, E$\alpha$$\beta, as well as \alpha, we may infer \beta). The proof of XCB, in effect, completed the solution of what one might think of as the larger problem. The larger problem here can get stated as: "Find all of the shortest axioms, up to re-lettering of variables, under E-detachment for the classical equivalential calculus." Many similar larger problems in logic (and probably also abstract algebra) remain open. I note that Ulrich's site doesn't have a complete list of these problems (this is not to get blamed on Ulrich)... for instance the problem of finding the set of the shortest single axioms for classical propositional calculus in disjunction "A", and negation "N" under A-N detachment "From AN\alpha$$\beta$, as well as $\alpha$, infer $\beta$", remains open.

-