But as I also understand it, Goedel's incompleteness theorem also implies that for any given axiomatic system, if you have any finite number of theorems/proofs,

But as I also understand it, Goedel's incompleteness theorem also implies that for any given axiomatic system, if you have any finite number of theorems/proofs, you can never know if these are all theorems/proofs possible in that system. Hence it isn't possible to "finish" any axiomatic system, in the sense that no number of theorems/proofs will ever "complete" it. I might be wrong though. But if I understand it correctly, that's not a bad thing at all. It means that there might always be more out there to discover. Some dub Goedel's incompleteness a 'bug' of mathematics, I think it's actually a feature.