Bridging Syntax and Semantics of Lean Expressions in E-Graphs

Explore a 28-minute video presentation from the EGRAPHS 2024 workshop that delves into bridging the gap between Lean's expression semantics and syntactically driven e-graphs in equality saturation. Discover how Marcus Rossel and Andrés Goens from Technische Universität Dresden and the University of Amsterdam tackle the challenge of implementing proof automation for equational reasoning in Lean. Learn about their approach to handling bound variables, implicit typing, and Lean's definitional equality, which encompasses α-equivalence, β-reduction, and η-reduction. Gain insights into the challenges they face and their ongoing development efforts, including their partially unsound techniques that remain sound due to Lean's proof checking. Access the active development of this project on GitHub and understand its potential impact on reducing the time and effort required for theorem proving in interactive theorem provers like Isabelle/HOL, Coq, and Lean.

[EGRAPHS24] Bridging Syntax and Semantics of Lean Expressions in E-Graphs