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

The Wikipedia page on automated theorem proving states:

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?

Solution 1:

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.

Solution 2:

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?.

Solution 3:

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.

Solution 4:

Recently I and many colleagues have been proving theorems in combinatorics on words using the Walnut prover written by Hamoon Mousavi. Some of these theorems are quite nontrivial and for some no other proof is currently known. It has also been used to correct slightly wrong results in the literature.

For more info about Walnut, see https://arxiv.org/abs/1603.06017 .

For some of my papers on this subject see https://cs.uwaterloo.ca/~shallit/papers.html .

Solution 5:

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?