search

leanprover / lean3

Lean Theorem Prover
http://leanprover.github.io/
Apache License 2.0
2.15k stars 217 forks source link

Import Isabelle theorems #1979

Closed mrmartin closed 6 years ago

mrmartin commented 6 years ago

This is not an issue, but 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.

Kha commented 6 years ago

Hi,

Please use the mailing list or chat room (which is much more active these days) for discussions around Lean.