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