What are the theorems of mathematics proved by a computer so far? [duplicate]

According to this, Robbin's problem concerning whether a Robbin's Algebra is a Boolean algebra is an important example. This was proven in 1996 by the Automated Theorem Proving system EPQ. The link contains further information.

There is project Mizar that aims to develop a database of formally verified mathematic theorems. The Mizar Mathematical Library contains a lot of "standard" mathematical theorems (see the link for examples). However, the theorems are not really proved automatically, the proofs are written by a human in the Mizar language and then they're verified (which at the end doesn't matter that much, the most important thing is that we have a formal proof that can be verified and manipulated by a computer).

I think the most-cited example is from several years ago: pons asinorum. At least that was a genuine example where the programmers were surprised of the nice proof they had not known themselves and it was likely more elegant than Euclid's original—but it turned out, it was already known to Pappus.

One well known theorem that has been formally proven is the Jordan curve theorem.

Characterization of faithfully flat homomorphisms

limit of : $a_{n+2} =\frac{1}{a_n} + \frac{1}{a_{n+1}}$

Approximating $1/z$ by polynomials

Motivation for introducing algebraic topology?

For which $n$ is $ \int_0^{\pi/2} \frac{\mathrm{d}x}{2+\sin nx}= \int_0^{\pi/2} \frac{\mathrm{d}x}{2+\sin x}=\frac{\pi}{3\sqrt{3\,}\,}$?

Incredible Blackjack Hand

What allows us divide/multiply dx in calculus?

Prove that $\sin x+\sin y=1$ does not have integer solutions

Give example of two non-isomorphic groups that have same as sets.

Must a continuous, non-constant, and periodic functions have a smallest period?

Closed-form for $B=\lim_{n\to\infty}\sum_{a_1=1}^{\infty}\frac{1}{a_1^2}\sum_{a_2=1}^{a_1}\frac{1}{a_2^2}\cdots\sum_{a_n=1}^{a_{n-1}}\frac{1}{a_n^2}$?