With some formal systems, it's possible to enumerate all the theorems.
This is the case for instance in propositional calculus or in some first-order theories with a recursively enumerable set of axioms (e.g. group theory, field theory, Peano arithmetic, etc.).
I'm looking for a software that would implement such an enumeration. Or more basically, a software that would produce random theorems (which may or may not be of interest). A software doing that in any of the formal systems listed previously would be acceptable.
I highly doubt you ever get any interesting theorem, even if you were to run such software for the remainder of your lifetime!
Let's take something like Peano Arithmetic (PA). How do we enumerate its theorems? Well, one obvious way is to systematically crank out strings of symbols, where the symbols are not just the symbols from the language of PA ($0$, $s$, $+$, and $\cdot$), but also those of FOL ... and while there are only finitely many logical operators (and only one open parenthesis and one close parenthesis), we'll need to deal with enumerably many variables. Any reasonable method of that cranks out all possible such strings will be such that the vast majority of strings are not FOL formulas but instead junk strings like $x_1 \to \forall ) + \forall s \to 0 ( 0 =$. Moreover, out of all the strings that actually are formulas, the vast majority will not be theorems, e.g. $s(0)=0$. And, even if you do get something that is a theorem, it is most likely uninteresting, e.g. $0+0=0$.
Even worse, while such an enumeration method will, for any theorem of PA, at some point produce that theorem (even if it is gazillion years from now), it may not be immediately clear to you that any such theorem is a theorem ... certainly if that theorem is an 'interesting' theorem.
So, instead of cranking out (what we hope will be) FOL formulas, what we really need to do is crank out proofs: proofs that have one or more of the Axioms of PA as its premises, and that has the theorem as its conclusion. So, you'll need to have strings that represent proofs ... avoiding proofs that have complicated subproof structures, you could use some Hilbert system ... i.e. you could crank out expressions that (hopefully!) embody sequences of sentences....all you'd need is to add a sentence separator symbol (e.g. $/$) ... a verification algorithm that determines whether every sentence in that sequence of statements is indeed an application of any of the axioms, or is the result of applying Modus Ponens to any two earlier sentences is written easily enough. Still, even with such simplifications, it should be clear that now the VAST majority of what such an enumeration method will out put is junk, and that even in the once in a blue moon case that it produces is an actual sequences of actual FOL formulas, the VAST majority of those does not constitute a proof, and even of those that do constitute a proof, the number of cases where it is a proof of something that is actually non-trivial will be extremely, extremely small.