Solution (source code)

= Solution

Let $L=\{0^m1^n:m,n\geq0,\ m\ne n\}$, and suppose it were a <regular language>. The <formal language> $B=0^*1^*$ is a <regular language>. By closure of <regular languages> under <set difference>,
$$
B\setminus L=\{0^n1^n:n\geq0\}
$$
would be a <regular language>. But the <pumping lemma for regular languages> rules this out: for pumping length $p$, every permitted pumped block in $0^p1^p$ consists of $k>0$ zeros, and deleting it produces $0^{p-k}1^p$, with unequal counts. This contradiction proves
$$
\boxed{\{0^m1^n:m\ne n\}\text{ is not regular}.}
$$
The closure step can also be realized by a <product automaton> accepting when the automaton for $B$ accepts and the automaton for $L$ rejects. If the exponents are instead required to be positive, use $B=0^+1^+$; the same argument applies.