What can be proven in Peano arithmetic but not Heyting arithmetic?

The first example that occurs to me is (a formalization in the language of arithmetic, via coding, of) "For every Turing machine M and every input x, the computation of M on input x either terminates or doesn't terminate." With classical logic, this is trivially provable, as an instance of the law of the excluded middle. But it's not intuitionistically provable because the halting problem is undecidable. (In a bit more detail, if it were provable, then it would be recursively realizable, and the realizer would be an index for an algorithm that solves the halting problem.)

First, since Peano Arithmetic (PA) is simply Heyting Arithmetic (HA) with the Law of Excluded Middle, everything provable in HA is provable in PA. The negative translation can be used to transform every statement $\phi$ into a statement $\phi^N$ such that (1) PA proves that $\phi$ and $\phi^N$ are logically equivalent, and (2) PA proves $\phi$ if and only if HA proves $\phi^N$. So PA and HA are relatively close to each other.

For a statement provable in PA but not in HA, consider the classically valid statement $\forall \bar{x}(p(\bar{x}) \neq 0) \lor \exists \bar{x}(p(\bar{x}) = 0)$, where $p(\bar{x})$ is a polynomial in the variables $\bar{x} = x_1,\dots,x_n$. In order for this to be provable in HA, we must have either a proof of $\forall \bar{x}(p(\bar{x}) \neq 0)$ or a proof of $\exists \bar{x}(p(\bar{x}) = 0)$. A proof of the former would show that the problem $p(\bar{x}) = 0$ has no solution, and a proof of the latter would show that the problem $p(\bar{x}) = 0$ has a solution. Since proofs are finite, this gives an effective procedure to decide whether the Diophantine equation $p(\bar{x}) = 0$ has a solution. Because of the negative solution to Hilbert's Tenth Problem, we know that there is some polynomial $p(\bar{x})$ such that $\forall \bar{x}(p(\bar{x}) \neq 0) \lor \exists \bar{x}(p(\bar{x}) = 0)$ is not provable in HA.

According to Harvey Friedman, the following theorem is provable in PA but not HA:

Every polynomial $P:\mathbb{Z}^n \to \mathbb{Z}^m$ with integer coefficients assumes a value closest to the origin.

That is, there is a value which is at least as close to the origin, in the Euclidean distance, than any other value. This is unprovable in HA even when $m=1$.