Bridging Syntax and Semantics of Lean Expressions in E-Graphs

Marcus Rossel, Andrés Goens

Interactive theorem provers, like Isabelle/HOL, Coq and Lean, have expressive languages that allow the formalization of general mathematical objects and proofs. In this context, an…