Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
4  
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
1  
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
add comment

5 Answers

up vote 14 down vote accepted

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

share|improve this answer
add comment

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.

share|improve this answer
add comment

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.

share|improve this answer
add comment

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.

share|improve this answer
1  
Could you give a reference? –  Nate Eldredge Aug 16 '12 at 22:23
add comment

google for this "automated theorem proving in hardware design" (without the quotes). There atre 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?

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.