There are computer generated proofs. They are also completely unreadable, much less understandable, by humans. In reality, most of mathematics is based on set theory, which makes it hard for computers to reason about proofs. There is currently an effort to rebase mathematics on type theory, which would allow computers to verify and create proofs much more easily. However, basically all of mathematics has to be reproved using this new foundation. To give an example, group theory as taught in undergraduate classes depends completely on sets. A group itself is a set with additional properties. Subgroups are defined in terms of set intersection and union. Type theory is still in its infancy, and this stuff is still being figured out. In terms of Mathematica, it doesn't know jack shit about complicated math theorems. Can it tell you if a group is solvable?

Yeah, classifying math aspects and creating relations between different proofs is probably one of the thornier issues I'd guess. It does feel however that mathematics is a domain where an AI should be able to train itself in some way

Why are types easier than sets? They are both computable.

Automated proof checking software has been around for a while, and they don't really require any capacity I'd describe as 'AI' as they simply verify logic: https://en.wikipedia.org/wiki/Automated_proof_checking

The trouble is that writing a proof in a format amenable to this verification is harder and much more tedious than writing it for a paper

Some time ago I started designing a system that would convert between automated checkers syntax and some simplified human-readable English. But failed, once realized the problem is bigger than me.

Here I just want to encourage anyone who thinks he's a good programmer to develop such a system. It would be extremely useful for education as well: students would get a tool that explains complex proofs, and professors would give assignments to put a theorem into the system (if student is able to enter the theorem into the system, then he/she definitely understands it up to the very foundations). The main problem to solve is good UX, not the math.

They who manage to make the system, the new verified Wikipedia for Math, would have their names inscribed for eternity, because Math is eternal.

yes, that's why I think something different than Automated proof checking for solving advanced theorems, you need to have an AI that can take "creative leaps" and break down proofs down to something humans can understand, and not just verify existing rules

You mean x amount of Fields medals. There is no Nobel for math.

Also, this is a lot harder than you think. "Extrapolating" from a learning set is relatively easy to do for statistical problems and prediction, but proofs are hard.

Ah sorry that's right, I always forget, maybe one in Economics then :)

This is an area of research: http://en.wikipedia.org/wiki/Automated_theorem_proving