translate lean to isabelle

Stream: lean4

[blah]

If I want to translate lean to isabelle to enrich the library of isabelle, is there some advice for me or if it’s a feasible job

[Henrik Böving]

Lean and Isabelle are based on very fundamentally different logics, partially orthogonal language constructs and more things. I would say what youre asking for would probably be a multi year research effort to automate. Doing some stuff by hand is doable as long as you don't venture out into the too dependently typed variants of lean.

[blah]

Henrik Böving 发言道：

Lean and Isabelle are based on very fundamentally different logics, partially orthogonal language constructs and more things. I would say what youre asking for would probably be a multi year research effort to automate. Doing some stuff by hand is doable as long as you don't venture out into the too dependently typed variants of lean.

So it’s impossible to translate the whole library of lean to isabelle? I found some ways of translation in lean and coq

[suhr]

Lean and Coq are both based on Calculus of Inductive Constructions (with some minor differences), while HOL is a very different kind of a theory. For example, there's no dependent types in HOL.

[Ruben Van de Velde]

That seems like somewhere between "many years of engineering" to "impossible", depending on how reliable you want it to be and how complex the lean can be

[Ruben Van de Velde]

And it would likely still not be connected to the existing development of mathematics in Isabelle

[Patrick Massot]

There is a lot of work in this direction. See https://deducteam.github.io/. It is already possible to translate a proof from Isabelle to Lean, going through Dedukti. The issue is that the result is unusable because the core mathematical types are not aligned.

[Ruben Van de Velde]

Fascinating