Translating between a proof assistant's internal representation and domain-specific languages used by external solvers is a tedious engineering chore with little reusable infrastructure, especially in the Lean ecosystem.

The authors present DSLean, a framework for bidirectional translation between Lean 4 expressions and external DSL syntax. DSLean requires only a specification of an external language and its Lean equivalents, abstracting away meta-level implementation details. Users declare equivalences between Lean objects and external syntax strings, including patterns with free variables that are iteratively filled during translation. The framework ensures type-correctness throughout. Three new automation tactics are implemented as demonstrations: interval arithmetic, ordinary differential equations, and ring ideal membership solvers.

DSLean enables three new Lean 4 automation tactics providing access to external solvers for interval arithmetic, ODEs, and ring ideal membership, each requiring only a declarative specification rather than bespoke translation code.