As was pointed out in the comments, for nice formal systems, you can in principle derive "all" theorems (in the sense that any theorem will come up in a finite amount of time) with a naïve algorithm.
There are a few problems with this approach :
The naïve algorithm is very (very very....) inefficient : you have to go through all proof trees of length $\leq n$; and there is an explosion of possibilities.
All in all you have infinitely many theorems so you will never get done : you will never have a finished list of theorems (in particular any given theorem can appear very very late, later than the survival of humans, which makes for a poor algorithm for practical purposes)
I think the most important point : the naïve algorithm cannot make a difference between theorems; any two theorems look alike to it. But us humans are interested in very specific theorems, and the amount of theorems we're interested in is probably ridiculous when compared to all theorems. That is, the naïve algorithm spits out tons of theorems of the form "$Q\implies (P\implies Q)$" for tons of already complex formulas $P,Q$, whereas we're not interested in them. And even more complex theorems we'd have to first decypher them in order to see if they're interesting : imagine the computer spits out a $160000$ character long theorem, written out in fully formalized form [note that usually our theorems can be short because we use abbreviations, abuse of notations, etc. that we understand among ourselves]; and you have to understand it to see if it's of any interest !
All these make a naïve approach such as "I have axioms and rules of inference so I can just use these to derive all theorems" untractable and most likely uninteresting. That's why there has to be a lot of work when trying to use computers to help us with proofs, to come up with clever solutions to the issues mentioned above.
Automated theorem proving, proof-assistants and related fields have come a long way, but still have a long way to go.