> These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites.
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.
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.
It would be much stranger to me if there was only one.
These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites.
Where programming languages can be based on procedures, objects, or functions, proof systems can be based on set theory, on simple type theory, or on dependent type theory.
In his comparison of formal systems [1], Freek Wiedijk identifies no less than seven ways to represent mathematics.
[1] https://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf