In this MO question, the OP asked for an example of a statement which was known not to be independent of ZFC, but for which the truth value was unknown. I immediately thought of a question I asked on math.SE: is $e^{e^{e^{79}}}$ an integer? This is apparently an open question, but I realized after some thought that I don't know how to prove it is decidable in ZFC.

In general, only $\Sigma^0_1$ statements have to be provable if they are true, and the claim that a certain definable series sums to an integer is $\Sigma^0_2$ rather than $\Sigma^0_1$.

Moreover, it's not hard to see that there are definitions of sequences $(a_n)$ in ZFC such that ZFC proves that $\sum a_n$ converges but ZFC doesn't prove this sum is an integer and ZFC doesn't prove it is not an integer. These sequences can be constructed using the incompleteness theorem in the usual way. In fact, we can make $0 \leq a_n \leq 2^{-n}$ for all $n$, so there is no issue with the rate of convergence.

But there must be something special about $e^{e^{e^{79}}}$ that means either ZFC can prove it's an integer, or can prove it's not an integer - right?