I believe this example may qualify. It is open whether Thompson's group $F$ is amenable. 

We may present $F$ as $\langle A,B\mid [AB^{-1},A^{-1}BA]=[AB^{-1},A^{-2}BA^2]={\rm id}]\rangle$.

*Amenability* of a finitely presented group $G$ with finite generating set $\Gamma$ is equivalent to the finiteness of the *Følner function* $$ Føl_{G,\Gamma}(n)=\min(|X|\mid X\subseteq G,\text{ $X$ is ($1/n$)-Følner with respect to $\Gamma$} ), $$ where $X$ is $\varepsilon$-Følner with respect to $\Gamma$ iff $$ \sum_{\gamma\in\Gamma}|(X\cdot\gamma)\triangle X|<\varepsilon|X|. $$
Here, $\triangle$ denotes symmetric difference, as usual.

Justin Moore [proved][1] recently the following:

**Theorem.** For every finite symmetric generating set $\Gamma\subseteq F$ there is a constant $C>1$ such that if $X\subseteq F$ is a $C^{-n}$-Følner set with respect 
to $\Gamma$, then $X$ contains at least $exp_n(0)$ elements.

Here, $exp_0(n)=n$ and $exp_{m+1}(n)=2^{exp_m(n)}$. 

This means that either $F$ is not amenable, or its amenability is not provable in primitive recursive arithmetic.


----------

On the recent arguments about amenability or not of $F$, see this nice [answer][2] by Mark Sapir.


  [1]: http://www.math.cornell.edu/~justin/Ftp/tower.pdf
  [2]: https://mathoverflow.net/questions/26821/is-thompsons-group-f-amenable/29065#29065