{"id":"arxiv:2609.24604","kind":"preprint","title":"Encoding Lean's Type Theory in Dedukti","authors":["Frédéric Blanqui","Rishikesh Vaishnav"],"author_count":2,"year":2026,"published":"2026-09-21","venue":"ICTAC 2026 - International Colloquium on Theoretical Aspects of Computing, Nov 2026, Bariloche, Argentina","cited_by":null,"doi":null,"arxiv_id":"2609.24604","nct_id":null,"source_url":"https://arxiv.org/abs/2609.24604","archive_url":"https://space-kitty.com/papers/arxiv:2609.24604","updated":"2026-09-21","pmid":null,"pmcid":null,"openalex_id":null,"pdf_url":"https://arxiv.org/pdf/2609.24604","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_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.LO"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[],"cited_in_dossiers":[]}