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 a

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/ https://xkcd.com/927/