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]=\operatorname{id}\rangle$.

*Amenability* of a finitely presented group $G$ with finite generating set $\Gamma$ is equivalent to the finiteness of the *Følner function* $$ \operatorname{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)\mathbin\triangle X|<\varepsilon|X|. $$
Here, $\triangle$ denotes symmetric difference, as usual.

Justin Moore [proved](https://doi.org/10.4171/ggd/201) 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 a (rather) weak fragment primitive recursive arithmetic. See the related discussion in Justin's [paper](https://doi.org/10.4171/ggd/201), "Fast growth in the Følner function for Thompson's group $F$", particularly the comments surrounding Question 1.2. 

----------

On the recent arguments about amenability or not of $F$, see this nice [answer][2] by Mark Sapir to https://mathoverflow.net/questions/26821/is-thompsons-group-f-amenable


  [1]: https://ems.press/content/serial-article-files/6917
  [2]: https://mathoverflow.net/questions/26821/is-thompsons-group-f-amenable/29065#29065