Encoding leans math library into dedukti logical framework
Encoding Lean's Type Theory in Dedukti
Logic in Computer Science
Summary
Proof assistants like Lean help people write and check complex math on computers, but different proof assistants use different languages. The authors created a way to translate much of Lean's math work into another system called Dedukti without breaking the meaning or types of the math statements. This translation helps different proof assistant users share and build on each other's work more easily. It makes Lean's large library more accessible to users of other proof systems.
What this means in practice
- •For proof assistant developers: Enable integration of Lean's mathematical libraries into Dedukti-based proof systems to expand reusable formal proofs.
- •For software verification engineers: Improve compatibility between proof tools by translating Lean proofs, facilitating verification of software across platforms.
Authors
Frédéric Blanqui, Rishikesh Vaishnav
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.