I've been reading a book on Gödel's incompleteness theorems and it makes the following claim regarding provability of statements in Peano arithmetic (paraphrased):
There exists a formula $A(x)$ such that the statements $A(0), A(1), A(2), \dots$ are all provable, but $\forall x\, A(x)$ is not provable.
It goes on to say that while Gödel's first incompleteness theorem guarantees its existence, it is not easy to find such a property for a theory as strong as PA.
Is there a specific example of such a formula or has none been found yet?