They definitely don’t all compile to the same thing. Some do, most don’t.
I meant to say they are all the same thing on logical level, all those fancy typed theories can be reduced to hol/fol, for some it is implemented, for others not.
That’s not true either. Coq’s logic is significantly different to HoL.
hol meaning higher order logic (https://en.wikipedia.org/wiki/Higher-order_logic) not the lang of hol prover.
and they all compile into the same fol/hol assembly (e.g. Isabelle translates its languages to fol and uses E for actual theorem proving, and E knows nothing about Isabelle language coolness), so in theory they should be able to integrate nicely.
My understanding is that the problem is they formalize in different mathematical foundations/axiomatic theories, but I am not an expert in this.