Why is it so difficult for a computer to prove something?
While there are plans to formalize Fermat's Last Theorem (see this presentation), I have never read or heard that a computer can prove even a "simple" theorem like Pythagoras'. 


In 1949 Tarski proved that almost everything in The Elements lies within a decidable fragment of logic, when he showed the decidability of the first-order theory of real closed fields. So the Pythagorean theorem in particular is not talked about much because it's not especially hard. 

In general, the thing that makes theorem proving hard is induction. First-order logic without induction has a very useful property called the subformula property: true formulas $A$ have proofs involving only the subterms of $A$. This means that it's possible to build theorem provers which can decide what to prove next based on an analysis of the theorem they are instructed to prove. (Quantifier instantiation can make the right notion of subformula a bit more subtle, but we have reasonable techniques to cope with this.) 

However, the addition of the induction schema to the axioms breaks this property. The only proof of a true formula $A$ may require doing a proof $B$ which is not syntactically a subformula of $A$. When we run into this in a paper proof, we say we have to "strengthen the induction hypothesis". This is quite hard for a computer to do, because the appropriate strengthening can require both significant domain-specific information, and an understanding of why you're proving a particular theorem. Without this information, truly relevant generalizations can get lost in a forest of irrelevant ones.