[infruset]

I've seen the same reaction from people learning to program. Why are there thousands of programming languages? Why not put everything under one standard?

The main answer, as for many variations of this question (languages, laws, units of measure, programming languages), is history. Efforts to formalize mathematics have spawned in different universities, at different times, in different teams with different cultures and approaches. The mathematical theories underlying the software also vary greatly. There isn't one agreed upon formalization of mathematics. There's classical logic and there's intuitionistic logic, which wants to see every existence theorem backed by an actual witness and does not agree that `not (not A) = A`. (Speaking of which, different systems have (very) different notions of equality! In case you thought this one would at least be simple). Sometimes two pieces of software have nearly identical foundations, such as Lean and Coq to some extent; but one is decades old, and the other is a rewrite from scratch using other unification algorithms and a different programming language. Sometimes people just don't get along and start competing projects.

Note that some people have intended to unify various proof systems, which reminds me of the classical https://xkcd.com/927/