Is it possible to translate from one language to another (e.g. from Coq to Isabelle or Coq to Lean or Coq to HOL Light etc.) using an intermediate language (e.g. TPTP or whatever Hammers use)?
What I had in mind was that since most ITPs have some sort of ability to talk to ATPs/Hammers it should be possible to translate between languages automatically (e.g. TPTP or whatever Hammers use).
Motivation(s): This could increase the number of facts users, ATPs, etc have in their disposal for further proving more things etc. Also, removing the dependence on any specific ITP seems valuable as they are hard to learn, so one can just learn 1 and then get the benefits of all of them.