[raphlinus]

There is work on making proofs portable from one system to another. One effort is Dedukti, which is based on the idea that "lambda pi modulo" is a universal logic for theorem provers. A less ambitious effort is OpenTheory, which from what I can tell is mostly about being able to interoperate between different HOL flavors.

And one of the efforts I personally find most interesting is Metamath Zero, which attempts to be an interchange format among other things, with connections to HOL and Lean. See section 5 of: https://arxiv.org/abs/1910.10703

I think there are many provers which theoretically could be used for this effort, and am not convinced Lean is the absolute best, but I applaud the community for actually going ahead and doing it, instead of farting around with tools and hoping the library will magically happen (a valid critique of HoTT in my opinion).

[dddbbb]

The author of the Metamath Zero paper is actually one of the most active contributors to the project described in the article[0].

[0]: https://leanprover-community.github.io/mathlib_stats.html

[yaseer]

Thanks for sharing! I Remember seeing Dedukti a while back, but I haven't seen some of these newer translation efforts.

I do hope the translation systems are actively used to consolidate, rather than built as an academic exercise.

There seems to be a large gap between vision ('our project will encapsulate all of mathematics in one place') and reality ('our project will just proliferate another standard')

https://xkcd.com/927/