← All papers
Encoding Lean's Type Theory in Dedukti
cs.LO
Sep 21, 2026 · v1
TL;DR
Presents a Dedukti theory encoding Lean's type theory with a typability-preserving translation from a large subset of Lean.
Abstract
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.
Problem
Lean has a rich library of mathematical formalizations that users of other proof assistants would like to reuse. Translating this library requires a faithful encoding of Lean's type theory in an interoperable framework.
Approach
A theory is defined in the Dedukti logical framework capable of encoding Lean terms and types. A translation from a large subset of Lean into this Dedukti theory is constructed. The translation is designed to preserve typability.
Results
The work provides a Dedukti theory and a typability-preserving translation covering a large subset of Lean, enabling export of Lean formalizations toward other systems.