Lem is a tool for lightweight executable mathematics, for writing, managing, and publishing large-scale portable semantic definitions, with export to LaTeX, executable code (currently OCaml) and interactive theorem provers (currently Coq, HOL4, and Isabelle/HOL, though the generated Coq is not necessarily idiomatic). It is also intended as an intermediate language for generating definitions from d

