Encoding Lean's Type Theory in Dedukti
In the authors' words
The Lean proof assistant has a rich library of mathematical formalizations that are interesting to users of other proof assistants. To help with the translation of this library to other systems, we present a theory in the Dedukti logical framework in which one can encode Lean terms and types, and define a typability-preserving translation from some large subset of Lean to that Dedukti theory.
Main resultLimitation the authors admit
Appeared: Tuesday, September 22. arXiv. Preprint with a published version.
Published version: ICTAC 2026 - International Colloquium on Theoretical Aspects of Computing, Nov 2026, Bariloche, Argentina