It is necessarily the case that you can eventually generate all possible finite proofs on a UTM. It also necessarily the case that you can eventually generate all possible theorems on a UTM. This follows trivially from the fact that both proofs and theorems are finite collections of characters from some finite alphabet. As a result, it is necessarily the case, that you can generate all proofs, and all theorems, given enough time.
In this view, where we mechanistically generate all theorems and proofs, being able to prove a theorem is being able to connect a given theorem to its proof, since as demonstrated, generating all possible theorems and proofs is trivial, given enough time on a UTM. At the same time, Gödel’s First Incompleteness Theorem states that it is not as a general matter possible to prove or disprove all statements within a formal system. Therefore, Gödel’s theorem implies that we cannot map every theorem to its proof, since that would be equivalent to being able to prove every theorem in the system, which is forbidden by the theorem.
As a corollary, it must be the case that there is no computable mapping from the set of theorems to the set of proofs. If you assume otherwise, then you can prove every theorem in the system using a computable function, which would certainly violate Gödel’s theorem.
Does Gödel’s theorem preclude the existence of any such mapping as a general matter?
Or, does it imply that such any such mapping is not computable?
Another way to think about this is if we have a given theorem, we generate all proofs, until we find the proof for the theorem in question. However, we don’t know how long the proof is, even if we’re told ex ante that the theorem is in fact true. As a result, mapping a theorem to its proof in this manner is not decidable, if you assume you can’t know the length of the proof ex ante. The intuition is that a short theorem, could have an extremely long proof. This is arguably the case for the Robertson–Seymour Theorem, which has fairly succinct statements, but an incredibly long and complex proof, that I do not claim to understand.
Taking this to its extreme, we can at least posit the idea of a finite theorem, that requires an infinite proof. This is obviously beyond the realm of human knowledge, since human beings can only write a finite number of symbols over a lifetime. But the point is, such a theorem could exist, and if it does, it would be unprovable.