<p>Here is a recent one:
<a href="http://link.springer.com/chapter/10.1007%2F978-3-319-09284-3_17" rel="nofollow">http://link.springer.com/chapter/10.1007%2F978-3-319-09284-3_17</a>
You can get the fulltext here:
<a href="http://arxiv.org/abs/1402.2184" rel="nofollow">http://arxiv.org/abs/1402.2184</a></p>

<p>It uses some state-of-the-art SAT solvers (see <a href="http://fmv.jku.at/lingeling/" rel="nofollow">http://fmv.jku.at/lingeling/</a>) 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.</p>

<p>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.</p>

CC BY-SA 3.0
2014-10-15T07:09:18.187Z
The answer would be even more helpful if you would state what is in the linked paper.
Jan Johannsen
CC BY-SA 3.0
2014-10-16T07:16:21.763Z
In what sense is this work unsupervised machine learning?
Martin Berger
CC BY-SA 3.0
2014-10-16T16:42:58.157Z
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.
Abhishek Anand
CC BY-SA 3.0
2014-10-18T05:45:59.347Z
Calling reduction to SAT unsupervised machine learning is stretching the latter term.
Martin Berger
CC BY-SA 3.0
2014-10-18T22:44:51.123Z
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?
Abhishek Anand
CC BY-SA 3.0
2014-10-15T02:50:34.610Z
2014-10-19T15:04:45.117Z
2014-10-19T15:04:45.117Z
Abhishek Anand
<p><strong>Clarification on terminology</strong></p>

<p>The theorem proving community does not use the terms <em>supervised</em> and <em>unsupervised</em>. They use the terms <em>interactive theorem proving</em> or <em>automated theorem proving</em>. If you give a conjecture to the prover and it always comes back with a yes or no answer, such a prover is a <em>decision procedure for a logical theory</em> or simply called a <em>decision procedure</em>.</p>

<p><strong>Proving statements of an infinite nature</strong></p>

<p>The intuition that a theorem that involves an infinite number of cases will be difficult for a machine is misleading. Consider the statement below.</p>

<blockquote>
  <p>The sum of two even numbers is an even number. </p>
</blockquote>

<p>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.</p>

<p><strong>Fully Automatic Theorem Proving</strong></p>

<p>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.</p>

<p>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 <a href="http://en.wikipedia.org/wiki/Real_closed_field">real closed fields</a>. 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. </p>

<p>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.</p>

<p>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.</p>

<p>To summarise, you are asking about decision procedures for logical theories. There are many of them.</p>

<p><strong>Interest</strong></p>

<p>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.</p>

<p>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.</p>

<p>The company <a href="http://theorymine.co.uk/?go=products">TheoryMine</a> 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.</p>

<p><strong>Success</strong></p>

<p>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.</p>

<p>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. </p>

<p>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. </p>

<p>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.</p>

<p><strong>On The Capabilities of Theorem Provers</strong></p>

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

<p>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 <em>very significant.</em> The automatic procedure would also be able to solve <a href="http://en.wikipedia.org/wiki/Twin_prime">open problems in mathematics</a>. The problem is that difficulty and capability are very different for human beings and for machines.</p>

<p>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.</p>

CC BY-SA 3.0
2012-06-27T21:47:00.553Z
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.
vzn
CC BY-SA 3.0
2012-06-28T15:03:13.690Z
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](http://en.wikipedia.org/wiki/Automated_theorem_proving), it cites the four color graph thm as "related"....
vzn
CC BY-SA 3.0
2012-06-28T15:06:29.367Z
"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.
vzn
CC BY-SA 3.0
2012-06-29T02:56:19.683Z
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.
Vijay D
CC BY-SA 3.0
2012-06-29T03:09:03.070Z
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.
vzn
CC BY-SA 3.0
2012-06-29T03:15:01.593Z
the question is clear but uses nonstandard terminology. it rules out human-assisted. human-assisted/supervised are basically synonyms. your answer stands. a better answer awaits. a better answer may very well be beyond all current theory.
vzn
CC BY-SA 3.0
2012-06-29T07:53:21.533Z
My mistake. My comment on clarity was not referring to your question but to your comment about TPTP, which I confused with the archive of formal proofs (which contains human assisted proofs). I retract that comment.
Vijay D
CC BY-SA 3.0
2012-06-29T16:25:50.290Z
huh? was indeed referring to [TPTP](http://www.cs.miami.edu/~tptp/). TPTP title on that pg says its "for automated theorem proving". but it is often used for human assisted proofs. again, a typical sleight-of-hand in this field. as far as I know it is difficult to figure which proofs in the archive have yielded to "true" ATP vs which of those have yielded to human assisted machine proofs.
vzn
CC BY-SA 3.0
2012-06-29T16:32:35.027Z
"It is not surprising that a machine cannot prove what a human being can prove." to me, it is indeed surprising given that thms are basically about logic/symbols, the virtual raison d'etre of computers. but surprise is indeed in the eye of the beholder wink
vzn
CC BY-SA 3.0
2014-10-20T15:37:56.087Z
Not to derail the conversation, but there are a number of automated proof of the infinitude of prime numbers e.g. http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=NUM&File=NUM016-1.p . However, it obviously doesn't *start* with the peano axioms. Then again, humans don't either...
cody
CC BY-SA 3.0
2012-06-27T19:18:06.607Z
2012-06-29T03:09:53.447Z
2012-06-29T03:09:53.447Z
Vijay D
<p>This question <a href="https://cstheory.stackexchange.com/questions/82/where-and-how-did-computers-help-prove-a-theorem">Where and how did computers help prove a theorem?</a> considers some automated theorem proving successes.<br>
However they seem to be mostly <em>supervised</em> 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.<br>
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.</p>

<p>Are there any significant examples of what could be called <em>unsupervised</em> theorem proving successes?</p>

<p>This would generally come in two forms:</p>

<ul>
<li><p>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.</p></li>
<li><p>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.</p></li>
</ul>

<p><sup>(Note: I have some possible example(s) of the above &amp; depending on response may answer with them.)</sup></p>

CC BY-SA 3.0
2012-06-22T18:43:06.250Z
Can you phrase the question as a question?
Dave Clarke
CC BY-SA 3.0
2012-06-22T20:31:34.800Z
insert implicit words "What are some...?" or "Are there some...?"
vzn
CC BY-SA 3.0
2012-06-24T04:57:03.773Z
Formal proof only makes sense with respect to a fixed proof system/theory.
Kaveh
CC BY-SA 3.0
2012-06-24T14:46:34.550Z
you mean like PA or ZFC etc? any std/conventional/widely accepted proof systems are ok
vzn
CC BY-SA 3.0
2012-06-25T12:13:37.813Z
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.
Radu GRIGore
CC BY-SA 3.0
2012-06-27T14:50:55.847Z
ok thx for ref. here is a link to [intro to knuth-bendix completion](http://comjnl.oxfordjournals.org/content/34/1/2.full.pdf) by A.J.J.Dick. however it seems mainly concerned with the rather basic (toy?) example $a + -(-a) = 0$. does anyone have a less basic example? thx
vzn
CC BY-SA 3.0
2012-06-28T11:41:54.160Z
Doug Lenat's somewhat controversial AM program might fit under the second bullet. I'm only familiar enough with the work to point you to the [wiki](http://en.wikipedia.org/wiki/Automated_Mathematician) page though.
alto
CC BY-SA 3.0
2012-06-30T00:42:51.140Z
thx, had heard of Lenat. it says on that page DL claimed the program discovered the goldbach conjecture and proved the unique factorization of primes. apparently this has not ever been replicated or the community does not believe the claim. wonder if there is a reference that focuses on this particular claim, which would be nearly revolutionary if replicable & scalable to other problems.
vzn
<reference-request><lo.logic><proof-complexity><automated-theorem-proving>
Automated theorem proving via unsupervised approaches
vzn
# Automated theorem proving via unsupervised approaches

(Asked by: username_0 on 2012-06-22)

This question [Where and how did computers help prove a theorem?](https://cstheory.stackexchange.com/questions/82/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.)

**Tags:** reference-request, lo.logic, proof-complexity, automated-theorem-proving

> **Comments:**
> **username_1**: Can you phrase the question as a question?  
> **username_0**: insert implicit words "What are some...?" or "Are there some...?"  
> **username_2**: Formal proof only makes sense with respect to a fixed proof system/theory.  
> **username_0**: you mean like PA or ZFC etc? any std/conventional/widely accepted proof systems are ok  
> **username_3**: 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.  
> **username_0**: ok thx for ref. here is a link to [intro to knuth-bendix completion](http://comjnl.oxfordjournals.org/content/34/1/2.full.pdf) by A.J.J.Dick. however it seems mainly concerned with the rather basic (toy?) example $a + -(-a) = 0$. does anyone have a less basic example? thx  
> **username_4**: Doug Lenat's somewhat controversial AM program might fit under the second bullet. I'm only familiar enough with the work to point you to the [wiki](http://en.wikipedia.org/wiki/Automated_Mathematician) page though.  
> **username_0**: thx, had heard of Lenat. it says on that page DL claimed the program discovered the goldbach conjecture and proved the unique factorization of primes. apparently this has not ever been replicated or the community does not believe the claim. wonder if there is a reference that focuses on this particular claim, which would be nearly revolutionary if replicable & scalable to other problems.  

---

## 2 answers

### Answer by username_8 on 2012-06-27. Score: 12 | Accepted answer

**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](http://en.wikipedia.org/wiki/Real_closed_field). 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](http://theorymine.co.uk/?go=products) 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](http://en.wikipedia.org/wiki/Twin_prime). 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.

> **Comments:**
> **username_0**: 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.  
> **username_0**: 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](http://en.wikipedia.org/wiki/Automated_theorem_proving), it cites the four color graph thm as "related"....  
> **username_0**: "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.  
> **username_8**: 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.  
> **username_0**: 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.  
> **username_0**: the question is clear but uses nonstandard terminology. it rules out human-assisted. human-assisted/supervised are basically synonyms. your answer stands. a better answer awaits. a better answer may very well be beyond all current theory.  
> **username_8**: My mistake. My comment on clarity was not referring to your question but to your comment about TPTP, which I confused with the archive of formal proofs (which contains human assisted proofs). I retract that comment.  
> **username_0**: huh? was indeed referring to [TPTP](http://www.cs.miami.edu/~tptp/). TPTP title on that pg says its "for automated theorem proving". but it is often used for human assisted proofs. again, a typical sleight-of-hand in this field. as far as I know it is difficult to figure which proofs in the archive have yielded to "true" ATP vs which of those have yielded to human assisted machine proofs.  
> **username_0**: "It is not surprising that a machine cannot prove what a human being can prove." to me, it is indeed surprising given that thms are basically about logic/symbols, the virtual raison d'etre of computers. but surprise is indeed in the eye of the beholder wink  
> **username_9**: Not to derail the conversation, but there are a number of automated proof of the infinitude of prime numbers e.g. http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=NUM&File=NUM016-1.p . However, it obviously doesn't *start* with the peano axioms. Then again, humans don't either...  

---

### Answer by username_5 on 2014-10-15. Score: 3

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.

> **Comments:**
> **username_6**: The answer would be even more helpful if you would state what is in the linked paper.  
> **username_7**: In what sense is this work unsupervised machine learning?  
> **username_5**: 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.  
> **username_7**: Calling reduction to SAT unsupervised machine learning is stretching the latter term.  
> **username_5**: Firstly, as mentioned in the answer by username_8, 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?  

---

