Zulip Chat Archive

Stream: general

Topic: Import HOL theorems


view this post on Zulip Martin Kolář (Nov 02 2018 at 14:43):

Hi, I'm new here, and I have a question regarding LEAN's versatility.

Is it possible to import Isabelle/HOL proofs into LEAN? How could this be achieved?

The benefit would be the availability of the archive of formal proofs within LEAN, which contains over 118'600 lemmas, many of which are very handy.

view this post on Zulip Johan Commelin (Nov 02 2018 at 15:03):

@Martin Kolář Welcome! I am certainly not an expert on Lean or Isabelle. There are others around who will have more to say on this. What I do know is that there is not currently any link between Lean and other theorem provers. Also, it seems that porting proofs would result in non-idiomatic Lean. (I am not enough of an expert to know if this is a big problem.)

view this post on Zulip Andrew Ashworth (Nov 02 2018 at 16:50):

Isabelle would be quite difficult. It is more feasible for a Coq-Lean bridge to be built since the logical foundations (CIC) are the same.

view this post on Zulip Andrew Ashworth (Nov 02 2018 at 16:52):

Also, in a sense, even if you were to model Isabelle/HOL in Lean, then transfer the proofs over - then to build on it you would necessarily need to keep working in that Isabelle/HOL world. So there would be no advantage to switching, I think.

view this post on Zulip Martin Kolář (Nov 08 2018 at 13:02):

@Johan Commelin Thanks for your quick reply. So we would need to add axioms to Lean to accept Isabelle proofs? That sounds inconvenient, but feasible.

view this post on Zulip Johan Commelin (Nov 08 2018 at 13:07):

No, I am not talking about adding axioms. I think you would need to write some sort of transpiler.

view this post on Zulip Johan Commelin (Nov 08 2018 at 13:07):

And I think that becomes very painful, and the results are usually even less readable then what we have in mathlib now.

view this post on Zulip Rob Lewis (Nov 08 2018 at 13:11):

This sort of proof import/translation is possible in principle, and there are people who have investigated/are investigating it. See e.g. http://logipedia.inria.fr/about/about.php which is based on Dedukti. It doesn't necessarily require extra axioms. The biggest problem, that keeps it from being usable in practice right now, is that e.g. Lean's current library and natural Lean style don't match Isabelle's current library and natural Isabelle style. If you could import the AFP and Isabelle standard library directly into Lean, you wouldn't get something that uses mathlib. You'd get an image of Isabelle in Lean, using Isabelle's nat, int, etc etc. It would have no connection to anything formalized in Lean and would be extremely hard to work with.

view this post on Zulip Rob Lewis (Nov 08 2018 at 13:13):

In principle, you can try to match Isabelle concepts to Lean concepts, and a good enough interpreter could produce a usable Lean development from elsewhere. This doesn't exist yet and would be extremely hard to do.


Last updated: May 09 2021 at 18:17 UTC