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 important goal is to reduce the time and effort needed to prove theorems. A significant means of achieving this is by improving proof automation. We have implemented an early prototype of proof automation for equational reasoning in Lean by using equality saturation. To achieve this, we need to bridge the gap between Lean's expression semantics and the syntactically driven e-graphs in equality saturation. This involves handling bound variables, implicit typing, as well as Lean's definitional equality, which is more general than syntactic equality and involves notions like $\alpha$-equivalence, $\beta$-reduction, and $\eta$-reduction. In this extended abstract, we highlight how we attempt to bridge this gap, and which challenges remain to be solved. Notably, while our techniques are partially unsound, the resulting proof automation remains sound by virtue of Lean's proof checking.

翻译：交互式定理证明器，如Isabelle/HOL、Coq和Lean，拥有表达力强的语言，能够形式化一般的数学对象和证明。在此背景下，一个重要的目标是减少证明定理所需的时间和精力。实现这一目标的一个关键手段是改进证明自动化。我们通过使用等式饱和，在Lean中实现了一个用于等式推理的证明自动化早期原型。为此，我们需要弥合Lean的表达式语义与等式饱和中语法驱动的e-图之间的差距。这涉及处理绑定变量、隐式类型以及Lean的定义相等性，后者比语法相等性更一般，并包含$\alpha$-等价、$\beta$-归约和$\eta$-归约等概念。在这篇扩展摘要中，我们重点介绍了如何尝试弥合这一差距，以及仍待解决的挑战。值得注意的是，尽管我们的技术部分不健全，但由于Lean的证明检查机制，最终得到的证明自动化仍然是健全的。