7
$\begingroup$

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

$\endgroup$
  • 6
    $\begingroup$ Can you phrase the question as a question? $\endgroup$ – Dave Clarke Jun 22 '12 at 18:43
  • $\begingroup$ insert implicit words "What are some...?" or "Are there some...?" $\endgroup$ – vzn Jun 22 '12 at 20:31
  • $\begingroup$ Formal proof only makes sense with respect to a fixed proof system/theory. $\endgroup$ – Kaveh Jun 24 '12 at 4:57
  • $\begingroup$ you mean like PA or ZFC etc? any std/conventional/widely accepted proof systems are ok $\endgroup$ – vzn Jun 24 '12 at 14:46
  • $\begingroup$ The Knuth-Bendix paper is along the lines of the second bullet. You can find it in Selected Papers on Design of Algorithms, but I don't think it's online. $\endgroup$ – Radu GRIGore Jun 25 '12 at 12:13
11
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ thx, accepting this answer for now, but feel it doesnt really answer the question, even if you helpfully clarify basic terminology. disagree that the community does not have a criteria for "interesting" or significant theorems. interesting/significant theorems, are, obviously, at least those found in books and papers that mathematicians read & discuss. the problem with ATP for decades has been that it can only find somewhat trivial theorems in general so far. maybe my question is more simply, what is the most complicated proof that has yielded to ATP. $\endgroup$ – vzn Jun 27 '12 at 21:47
  • $\begingroup$ the field has its distinctions/definitions as you note, but they are often blurred somewhat in descriptions/presentations/overviews & are not strictly compartmentalized as you imply. for example in the wikipedia entry on ATP, it cites the four color graph thm as "related".... $\endgroup$ – vzn Jun 28 '12 at 15:03
  • 1
    $\begingroup$ "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." no I feel the response misses the point. proving significant theorems is trivial for a mathematician but still largely impossible for a computer. a simple example would be the euclidean proof of the infinitude of primes. can a computer prove it from the assertion alone? still, apparently, not. that shows theres still a massive gap in this field. but, some may choose to downplay or handwave it away. $\endgroup$ – vzn Jun 28 '12 at 15:06
  • $\begingroup$ I don't think we're downplaying it. There is something circular in your request that you need to see. If a computer has to prove a statement from the assertion alone, that statement has to sit within a decidable theory and we have to come up with the decision procedure. $\endgroup$ – Vijay D Jun 29 '12 at 2:56
  • $\begingroup$ respectfully think you are totally wrong about that, and that the theory you espouse has turned into the cart pushing the horse. think it is your own reformulation of my question that is circular which amounts to "only theorems in decidable theories can be proven or disproven" which is surely false. however, dont have an obvious counterexample at hand and fully admit the current theory justifies your perspective/perception. however, suggest you study the concept of a "semialgorithm". also suggest you look into the TPTP archive & see how it naturally applies to the question. $\endgroup$ – vzn Jun 29 '12 at 3:09
3
$\begingroup$

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.

$\endgroup$
  • 4
    $\begingroup$ The answer would be even more helpful if you would state what is in the linked paper. $\endgroup$ – Jan Johannsen Oct 15 '14 at 7:09
  • $\begingroup$ In what sense is this work unsupervised machine learning? $\endgroup$ – Martin Berger Oct 16 '14 at 7:16
  • 2
    $\begingroup$ In the sense that the authors just expressed their problem as a SAT instance and let the SAT solver discover the proof. IMO, their SAT encoding was rather straight forward. $\endgroup$ – Abhishek Anand Oct 16 '14 at 16:42
  • $\begingroup$ Calling reduction to SAT unsupervised machine learning is stretching the latter term. $\endgroup$ – Martin Berger Oct 18 '14 at 5:45
  • 1
    $\begingroup$ Firstly, as mentioned in the answer by Vijay D, automatic theorem proving (and not "unsupervised machine learning") is the term used by the theorem proving community for the kind of works the OP is looking for. I think this work is best classified as automated theorem proving (as opposed to interactive proving). Note that some amount of interaction is necessary in SPECIFICATION of the problem; we can't expect the machines to reliably read our minds. Perhaps you would be happier if the problem was specified in FOL and the SAT formulae were derived automatically? $\endgroup$ – Abhishek Anand Oct 18 '14 at 22:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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