Are there any interesting theorems of first-order group theory I've heard that theoremhood in first-order group theory is uncomputable, so there should be some theorems that are difficult to prove. However the few theorems of group theory I know are about subgroups, exponents and such, so they don't seem to be formalizable in first-order logic (for each $n\in\mathbb{N}$ we can write $\forall_x x^n=e$ for "the group has exponent $n$" but this doesn't seem to help much).
Are there any cool theorems or conjectures that are naturally stated in the first-order language of group theory?
 A: It is proved in [1] that a finite group is soluble if and only if it satisfies the following first order sentence, which states that no non-trivial element $g$ is a product of $56$ commutators of pairs of conjugates of $g$:
$$
\forall g\ \forall x_1 \dotsm \forall x_{56}\ \forall y_1 \dotsm \forall y_{56}\ \bigl(g = 1 \vee g \not= [g^{x_1}, g^{y_1}] \dotsm [g^{x_{56}}, g^{y_{56}}]\bigr)
$$
[1] J. S. Wilson – Finite axiomatization of finite soluble groups, J. London Math. Soc. (2) 74 (2006), 566–582.
A: There are actually many model-theoretic questions related to groups. You might be interested in the following questions (and even more by their answer) from this site

*

*Model theory in group theory

*Is there a finite theory of groups whose models are all torsion-free?
and from MathOverflow

*

*A question concerning model theory of groups

*Applications of logic to group theory?

*Why are model theorists so fond of definable groups?
Since you are looking for difficult theorems, let me mention the solution to Tarski's conjectures.
Quoting Wikipedia,

Around 1945, Alfred Tarski asked whether the free groups on two or
more generators have the same first-order theory, and whether this
theory is decidable. Sela [2] answered the first question by
showing that any two nonabelian free groups have the same first-order
theory, and Kharlampovich & Myasnikov [1] answered both questions,
showing that this theory is decidable.
A similar unsolved (as of 2011) question in free probability theory
asks whether the von Neumann group algebras of any two non-abelian
finitely generated free groups are isomorphic.

[1] O. Kharlampovich and A. Myasnikov, Elementary theory of free non-abelian groups, Journal of Algebra 302 no 2,‎ 2006, p. 451–552.
[2] Z. Sela, Diophantine geometry over groups. VI. The elementary theory of a free group, Geom. Funct. Anal. 16 (3), 2006, 707–730
This is a very active research topic. See for instance this recent paper:
[3] S. André, J. Fruchter, Formal solutions and the first-order theory of acylindrically hyperbolic groups
