# Encoding Lean's Type Theory in Dedukti

Preprint · Frédéric Blanqui, Rishikesh Vaishnav

- Archive id: arxiv:2609.24604
- Published: 2026-09-21
- Venue: ICTAC 2026 - International Colloquium on Theoretical Aspects of Computing, Nov 2026, Bariloche, Argentina
- arXiv: https://arxiv.org/abs/2609.24604
- Source URL: https://arxiv.org/abs/2609.24604
- PDF: https://arxiv.org/pdf/2609.24604
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.