# DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs

arXiv: https://arxiv.org/abs/2602.18657 · HTML: https://mlsanity.com/paper/2602.18657/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Feb 2026.

## Built on by (most cited first, 1 of 1)

- [Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline](https://mlsanity.com/paper/2604.18882/) (2026)

## Abstract (arXiv)

Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and such DSLs is a tedious engineering chore. To simplify this task, we present DSLean, a framework for bidirectional translation between expressions in the Lean proof assistant and external syntax. DSLean requires only a specification of an external language and its Lean equivalents, abstracting away meta-level implementation details. We demonstrate DSLean's capabilities by implementing three new automation tactics, providing access to external solvers for interval arithmetic, ordinary differential equations, and ring ideal membership.