They don't do it because the technology just isn't there yet. Automated theorem checking is typically very difficult for any nontrivial theorem; automated theorem generation is so extraordinarily difficult, it's generally infeasible.

The steps to construct a proof of a theorem are as follows:

1. Formally define a language specification which will ostensibly contain the theorem statement and a proof.

2. Search the language space (the set of all strings of the language) for a proof of the theorem statement.

3. If step 2 fails, change the language specification to include prerequisite mathematics or an alternative statement of the theorem.

Even when you exploit clever structural properties of the theorem statement and the language definition, it's extremely easy to encounter a combinatorial explosion when you search for a proof.

On the other hand, suppose you already have a proof and simply want to verify it using a proof assistant. In order to do so, the language you define must be able to automatically verify all prerequisite mathematics which your proof depends on. Encoding that mathematics into a language is difficult and tedious, and dependency checking is itself vulnerable to combinatorial explosion.

It's a very active area of research in its own right, but it can't obviate this problem for the foreseeable future.