The idea is that proof systems can be formulated as a grammar for a recursively enumerable language (Type 0 grammars in the Chomsky hierarchy):
https://en.wikipedia.org/wiki/Chomsky_hierarchy#Summary, such that if there is a proof of a particular statement a corresponding word can be derived by the corresponding grammar.
But this can easily be done by a Turing machine (either check through all possible derivations in the grammar or, more abstract, let the Turing machine let non-deterministically choose a possible derivation and use the fact that the expressiveness of non-deterministic Turing machines is the same as for deterministic Turing machines).