DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
Abstract
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.
Keywords
Cite
@article{arxiv.2602.18657,
title = {DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs},
author = {Tate Rowney and Riyaz Ahuja and Jeremy Avigad and Sean Welleck},
journal= {arXiv preprint arXiv:2602.18657},
year = {2026}
}
Comments
14 pages; code available at https://github.com/taterowney/DSLean