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?