Lisa is a proof assistant embedded in Scala 3. Proofs are written with a domain-specific language (DSL) and checked at runtime. It allows general-purpose programming and external Java or Scala libraries to be mixed with proof construction to implement powerful proof automation.

We also present how Lisa’s implementation as a Scala library enables key design features. We present two particular applications that make use of this design: a proof interface for functional programming students, and a tool to import and recheck proofs from the HOL Light proof assistant.