[tim_hutton]

Gödel's incompleteness isn't a practical obstacle to proof assistants - it will never stop us formalizing proofs and searching for new theorems. It's irrelevant to their operation and will continue to be for all time.

If Gödel's incompleteness applies to the theorem you are trying to prove then it means that the theorem has been very carefully set up with reference to the axioms that you are using in order to be unprovable. It's not something you will stumble across otherwise.

Think of it like this: imagine knowing that maths will stop working if a certain very specific enormous number appears in your calculation. This would keep mathematicians up at night with worry but it would have no practical effect on anyone else because the enormous number simply never appears.

[sva_]

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.