"not provable", what does this to do with unification?
They mean you can't use the rules in Figure 2 defining $\approx$ (and $\#$) to derive $\emptyset\vdash a.\!X\approx b.\!X$.  If you attempt to do it you'll use $\approx$-abstraction-2 followed by $\approx$-suspension at which point you'll not be able to satisfy the premise as $\nabla$ is empty but the disagreement set is $\{a,b\}$.  There are no other applicable rules, so there is no derivation.

Conceptually, though conceptual understanding is not needed to answer this question, what's happening is with an empty freshness environment we're free to replace $X$ with $a$ (or $b$) but $a.\!a \neq_\alpha b.\!a$. This is what it means in the sentences following that quote by $\alpha$-equivalence not being preserved by substitution.  The freshness constraints in $\nabla$ are what disallow such substitutions. So in an empty freshness environment $a.\!X$ and $b.\!X$ can't be unified as their instances need not be $\alpha$-equivalent.

I recommend getting more familiar with inductively defined judgements and derivations, as e.g. discussed in Chapter 2 of Robert Harper's Practical Foundations for Programming Languages. You should do the exercises there, and write out the complete derivations for the examples in the Nominal Unification paper. Ultimately, checking derivability like this should be as straightforward and mechanical as checking $(x+3)(x-1) = x^2+2x-3$.