Is there any way to easily translate proofs from one proof assistant to another? If so, how does it work?
Gaëtan Gilbert was able to translate Lean's library into Coq.
However, note that this is a translation at the level of proof terms, not proof scripts: in order to prove a theorem in Lean, you usually write a proof script using tactics (such as
cases), and Lean will compile it down to a proof term that can be checked by Lean's kernel.
The translation happens after the compilation phase, and will produce a proof term that can be checked by Coq's kernel, not a readable proof script for Coq.
So, how does this work? While Lean and Coq's tactics and idioms are quite different, it turns out that their proof terms are very similar, as their internal logics are both based on the Calculus of Inductive Constructions. There are some subtle differences, however: the universes are not handled in the exact same way, and Lean has definitional quotients as well as elimination rules for proof-irrelevant types that are not supported by vanilla Coq. But Coq can be modified to handle these, making it into a Lean type-checker.
Some impressive work was done a while ago by Chantal Keller, which translated the entirety of HOL Light's library into Coq.
On the face of it, HOL is close to being a subset of the underlying logic of Coq (with some classical axioms), but the technical challenges were non-trivial: because HOL systems usually do not keep proof objects, there can be a size explosion in the translation, which must create them.
Another interesting point is that a "naive" translation would give unintelligible statements from HOL, with its own natural numbers, quantifiers, etc, but Chantal came up with a way to send some definitions to their appropriate targets.
Mario Carneiro also has worked on this with Metamath Zero, which can directly translate proofs to Lean. As Loïc mentioned, though, this is a term-wise translation, which means that the code between the two libraries won't interact well; for example, the two ring types would be different, and won't work together directly without more glue.
A similar example is mathport, which attempts to copy proofs from Lean3 to Lean4. This is done at many levels, but the hope is that eventually only the tactic level is needed; however, for example, tactics need to be ported by hand, so this is far from automatic.
I would discourage people to do so, unless the proofs and theorems are super simple (like natural number properties). Reasons:
- In different systems, there are (nontrivially) different ways to represent certain things. For example, quotients in Lean and cubical Agda and Arend are all different from each other (they have different computation rules). It's very very hard for a translation algorithm to work across these differences.
- The type theories and design philosophy are mostly likely to be different. For instance, in Agda, the identity type lives in Type, but in Coq (and maybe Lean), the identity type lives in Prop (and note that Coq Prop and Lean Prop are different in strictness). This can make proofs in Agda to not work in other systems, or vice versa. Not to mention simple type theory proofs and dependent type theory proofs.
- A translated theorem can be hard to use, because the best practices of different systems can be different. For example, mathlib embraces classical math, so probably constructivists will not appreciate proofs translated from there. Also, the translated proofs can be hard to read.
What I do found useful, is to implement similar tactics among systems, then translate the tactics automatically and check them against manually translated theorems. By that we "translate" theorems but in a supervised manner. I think this should be useful, but people haven't done it as far as I know. I plan to do this in Aya.
So around 2003-2008 (approximately), there was one effort (not sure what happened to it), to have a common host/packaging system for sharing proofs between systems, with the working name "Logosphere". A bunch of talks and working notes seem to be around online, but the underlying effort seems to have evaporated. I suspect someone could message Carsten Schürmann and ask about it! (I met him Fall of 2005 and he was pretty cool)
Here's some related papers that come up!
I am aware of certain efforts of this nature within the Isabelle/HOL community.
(Automated translation of theorems from HOL4 to Isabelle/HOL)
- Immler F, Rädle J, Wenzel M. Virtualization of HOL4 in Isabelle. In: Harrison J, O’Leary J, Tolmach A, editors. Proceedings of the 10th International Conference on Interactive Theorem Proving. 2019.
(Automated translation of theorems from Isabelle/HOL to Isabelle/ZF)
- Krauss A, Schropp A. A Mechanized Translation from Higher-Order Logic to Set Theory. In: Kaufmann M, Paulson LC, editors. Proceedings of the First International Conference on Interactive Theorem Proving, ITP 2010, Edinburgh, UK, July 11-14, 2010. Heidelberg, Germany: Springer; 2010. p. 323–38. (Lecture Notes in Computer Science; vol. 6172).
(Involves translation of theorems from Mizar to HOTG = Isabelle/HOL + Tarski-Grothendieck Set Theory, but I am not certain about the status of this project and the level of automation that was used: it seems like this is an ongoing effort; I encourage you to correct me if you know more)
- Kaliszyk C, Pąk K. Semantics of Mizar as an Isabelle Object Logic. Journal of Automated Reasoning. 2019;63(3):557–95.
- Brown CE, Kaliszyk C, Pak K. Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. In: Harrison J, O’Leary J, Tolmach A, editors. 10th International Conference on Interactive Theorem Proving (ITP 2019). Portland, USA; 2019. p. 9:1-9:16.
"Is there any way to easily translate proofs from one proof assistant to another? If so, how does it work?"
From the Logopedia About webpage:
"Some proofs expressed in some Dedukti theories can be translated to other proof systems, such as HOL Light, HOL 4 , Isabelle / HOL , Coq , Matita , Lean , PVS ...".
Logipedia boils down to translating proofs into Dedukti.
Currently, this is possible for:
- Matita via Krajono
- OpenTheory and HolLight via Holide
- Coq with CoqInE
- FoCaLize, Zenon modulo, iProverModulo, TPTP problems
- more to come ... (using the OpenTheory standard)
Not always entirely automatic, and not yet complete, but it translates between several proof formats.
"Sharing a Library between Proof Assistants: Reaching out to the HOL Family" by François Thiré (July 5, 2018)
"Exporting an Arithmetic Library from Dedukti to HOL", by François Thiré (December 19, 2017)
"Experiences from Exporting Major Proof Assistant Libraries", by Kohlhase and Rabe (May 5 2020)