Yes. https://arxiv.org/abs/1412.8091 details a translation from OpenTheory to Metamath, and https://arxiv.org/abs/1910.10703 has a translation from Metamath -> MM0 -> Lean + HOL. You have to map every axiom and inference rule of the source system to a theorem of the target system, and since most of these systems have a similar idea about what math is this is usually possible, modulo some axiomatic strength mismatches, which can usually be addressed by adding (reasonable, idiomatic) axioms to the target system to make up the difference. For example if translating set.mm to HOL light, you have to add the axioms of ZFC to HOL light because the standard axioms of HOL light are only strong enough to prove the existence of ordinals up to omega*2. When targeting lean, the axioms are already strong enough in the target system that nothing has to be added.
The second stage of the translation is "alignment" of concepts, and this can be harder because it depends on the size of the libraries; in principle you want to align all concepts in the intersection of both libraries, but this is a lot of work and needs maintenance, to track progress in both libraries, and moreover it's not clear who should be responsible for that maintenance since it sits in the DMZ between completely separate proof ecosystems. If you want to target a particular statement, you just need to align everything in the definitional stack leading up to the theorem statement. I did this in the MM0 paper with the statement http://us.metamath.org/mpeuni/dirith.html , which has an advanced proof but contains only relatively simple concepts of primality, divisibility and infinitude that were easily located in lean's mathlib, resulting in the translated statement https://github.com/digama0/mm0/blob/master/mm0-lean/mm0/set/post.lean#L539-L540 . Mario Carneiro On Thu, Feb 11, 2021 at 11:53 PM [email protected] <[email protected]> wrote: > > I'm just curious: has there ever been any serious effort to make a > translator between Metamath and another unrelated proof language(such as > HOL Light, Mizar, Coq etc)? What would be the biggest challenges facing > such an effort? > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/3e2185a8-dd68-4376-b616-ea033f9d9590n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/3e2185a8-dd68-4376-b616-ea033f9d9590n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvKtr9aAiaTaps0fno66JTZw005Dt4cfVYWCFYO3z_4pA%40mail.gmail.com.
