I think a large part of it may be that people are still inventing the languages and we haven't seen enough industry adoption to settle down on a handful of good ones.

We're still in the Cambrian explosion of new ideas and languages.

The best way to get to the future you want is to keep using them and convincing others to join you!

How about a "Rosetta Proof" wiki in the style of "Rosetta Code"? You wouldn't need to settle on one language, and it might help clarify the advantages of one language or another.

> Unfortunately, I've never seen enough momentum behind one proof language to give a wiki a chance of becoming something substantial.

It's probably not far from hoping for the "Wikipedia of programming" where a single programming is used for all programs. There's religious wars on the best approach to everything and even the proof for "1 + 1 = 2" is fundamentally different in different proof assistants.

Well according to https://deducteam.github.io/ HOL and Coq can be autotranslated to Dedukti (which is the language Logipedia uses)...

Because logic as a subject doesn't have a community in itself and a lot of noise instead of signal (can't find anyone who doesn't mention Gödel against science and maths)