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 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 by Mark Sapir.
