This is essentially a follow-up to this previous discussion on how, in the absence of choice, the "invariant mean" and "Folner set" characterizations of amenability are no longer equivalent. Recently I've been wondering about, essentially, the opposite direction of the one in the link.

It's well known that, given an invariant mean on a group, one can deduce the existence of Folner sets. But the only proof of this that I know invokes the Hahn-Banach theorem or something similar.

This suggests that there might be groups where choice principles at least as strong as the Hahn-Banach theorem can prove that they have Folner sets, but for which one *cannot* prove the existence of Folner sets otherwise. In other words, groups which are support an invariant mean but for which we cannot give an explicit Folner set construction. This would be in stark contrast to the situation with, say, $\mathbb{Z}$, which has many very explicit Folner sequences but which, again, does not support an invariant mean in ZF.

Does anyone know if this can ever happen? I've tagged reverse mathematics because this seems like the sort of question its tools might be able to answer, even though it's outside of my expertise.

EDIT: as YCor points out, it obviously makes no sense without some choice to define amenable groups to be groups which support an invariant mean. "Do there exist groups with solvable word problem which support an invariant mean without a computable Folner sequence" would certainly be a good specification of my question.