Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
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?
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.
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?.
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.
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 .
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?
An other example would probably be the Kepler Conjecture proven by a team surrounding Tomas Hales. It was called Flyspeck Project. Although he claimed to have proved it before, people weren't sure whether the proof was correct. So this might fall into the "proof checking" category.
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.
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.
7 years later --
I am aware that a few important ($\color{red}{\text{named})}$ mathematical problems have had their proofs verified ($\color{red}{\text{-or had been proven})}$ using automated theorem proving or proof assistant software. For example a proof by Feit and Thompson of the Odd-Order theorem has been verified by the proof assistance COQ. And this Git-repository The formal proof of the Odd Order Theorem, reposits the code, written in COQ, and makes available to the public in order to reproduce the results. Going up the file directory I find several other results: (1) A Formal Proof of the Irrationality of $\zeta(3),$ Apery's Constant and (2) Formal proof of the Four Color Theorem.
