  In the paper we characterize the class of finite solvable groups by
two-variable identities in a way similar to the characterization of finite
nilpotent groups by Engel identities. More precisely, a sequence of words
$u_1,...,u_n,... $ is called correct if $u_k\equiv 1$ in a group $G$ implies
$u_m\equiv 1$ in a group $G$ for all $m>k$. We are looking for an explicit
correct sequence of words $u_1(x,y),...,u_n(x,y),...$ such that a group $G$ is
solvable if and only if for some $n$ the word $u_n$ is an identity in $G$.
  Let $u_1=x^{-2}y\min x$, and $u_{n+1} = [xu_nx\min,yu_ny\min]$. The main
result states that a finite group $G$ is solvable if and only if for some $n$
the identity $u_n(x,y)\equiv 1$ holds in $G$. In the language of profinite
groups this result implies that the provariety of prosolvable groups is
determined by a single explicit proidentity in two variables.
  The proof of the main theorem relies on reduction to J.Thompson's list of
minimal non-solvable simple groups, on extensive use of arithmetic geometry
(Lang - Weil bounds, Deligne's machinery, estimates of Betti numbers, etc.) and
on computer algebra and geometry (SINGULAR, MAGMA) .
