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/