We investigate the computational complexity of the Boolean Isomorphism problem (BI):
on input of two Boolean formulas F and G decide whether there exists a permutation of
the variables of G such that F and G become equivalent.

Our main result is a one-round interactive proof for $\overline{BI}$, where the Verifier
has access to an NP oracle. To obtain this, we use a recent result from learning theory
by Bshouty et.al. that Boolean formulas can be learned probabilistically with equivalence
queries and access to an NP oracle. As a consequence, BI cannot be $\Sigma_2^p$ complete
unless the Polynomial Hierarchy collapses. This solves an open problem posed in Borchert
et.al.

Further properties of BI are shown: BI has And- and Or-functions, the counting version,
#BI, can be computed in polynomial time relative to BI, and BI is self-reducible.