> It seems strange to me that there isn't one standard system.
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.