It's a bit difficult to tell what exactly you're asking, but I hope the following answer helps.
m : "a sentence whose Godel number is i is true"
(Simply, m' says that "I am true")
This is problematic, since by Tarski's undefinability theorem, there is no way to express the predicate "true" in ZFC (or any other sufficiently complicated formal system). This means that there is no formula $\phi(x)$ in ZFC such that $\phi(A)$ is true if and only if $A$ is a code for a true sentence of ZFC.
But there is a formula $\phi(x)$ is ZFC such that $\phi(A)$ is true if and only if $A$ codes a valid proof of a given sentence of ZFC. This is your automated proof-checking machine. It's important not to confuse "provable" and "true" here.
Now, I'm assuming that this question is motivated by the proof of Gödel's theorem, which involves concocting a sentence of ZFC whose meaning amounts to "This sentence is not provable". It's easy to see that such a sentence can't be proven or disproven if ZFC is consistent. But a natural question is to ask about a similar sentence which can be concocted by the same methods whose meaning amounts to "This sentence is provable." Is such a sentence actually provable, or not?
The answer is that it is provable. This is a consequence of Löb's theorem, which states that if ZFC can prove "If P is provable, then P", then ZFC can prove P. If P is a statement which is equivalent to "P is provable," then one can prove in ZFC that if "P is provable" then P (since this is what P means!) So Löb's theorem applies.
Edited following outside discussion:
First I want to make one point about the set-up here. I used the wording "returns yes if $A$ is a valid proof of a given sentence of ZFC" above, but I'd like to adjust that a little bit.
Our proof checking machine should actually take two inputs, $A$ and $B$. Then:
$M(A,B) = 0$ if $A$ codes a valid proof of the sentence coded by $B$
$M(A,B) = 1$ if $A$ does not code a valid proof of the sentence coded by $B$
Yes, we can "physically" build a machine - or write a computer program - which does this. It decodes $A$, then goes through it line by line checking that
1. Each line follows from the previous lines by one of the deduction rules of our system
2. The proof ends with a valid deduction of $B$
Now "$M(A,B) = 0$" means "$A$ is a proof of $B$" and "$M(A,B) = 1$" means "$A$ is not a proof of $B$". $M$ is guaranteed to return $0$ or $1$ on any input.
Notice that this machine $M$ doesn't address the question of whether $B$ is provable. It just answers the question of whether $A$ is a proof of $B$ (Of course if $A$ is a proof of $B$, then $B$ is provable, but if $A$ is not a proof of $B$, we still don't know whether $B$ is provable. It could have some other proof which is not $A$).
Now we can alter our machine a bit to a machine $M'$ which attempts to answer the question "is $B$ provable?", or equivalently "does there exist some $A$ which codes a proof of $B$?"
To evaluate $M'(B)$, $M'$ works as follows: it cycles one by one through all the possible codes $A$. For each one, it runs $M(A,B)$. If it gets the answer $0$, then $A$ codes a proof of $B$, so it returns $0$ ("Yes, $B$ is provable!"). If it gets the answer $1$ it moves on to the next code and repeats.
Now $M'$ is a very different sort of machine. If $B$ is provable, then $M'$ will eventually find the proof and return $0$. But if $B$ is not provable, $M'$ will keep cycling through all the codes (there are infinitely many of them) forever, looking for a proof. The algorithm will never terminate.
It is this $M'$ that we diagonalize against when we write down sentences like "I am provable" or "I am not provable".
So to answer your specific question, we have a sentence $B$ which means "$M'(B) = 0$" (i.e. $B$ is provable).
If you feed $B$ to our machine $M'$, $M'$ will actually terminate and return $0$, that is, it will find us a proof of $B$.
The proof of this, as I said above, is Löb's theorem,