> Suppose that's the case, the problem is that the resulting language of all the finite proofs can still be infinite and we again cannot enumerate and check all the solutions (since the final set is infinite).

The set of all strings in the language is only countably infinite (= same size as tne natural numbers), which means you will reach the solution string after a finite time (just count 1, 2, 3, ... until you reach the corresponding natural number).

What I'm saying is that if each individual problem has a solution in the form of an individual finite proof (the premise of your second point), then the above gives you a general algorithm for finding the proof for any given of those individual problems (contradicting the premise of your first point).

What this doesn't give you is a way to prove that a proof exists for all individual prohlems, because that indeed would take infinite time.

Ykonstant is correct in that your use of "undecidable" was confused; I just ignored that.