一句话：将定理解释为条件重写规则，用 e-graph 等式饱和在 Lean 中实现纸笔风格的等式推理 tactic。
数学家在纸笔等式推理中常依据上下文省略等式成立的条件，而交互式定理证明器要求显式给出所有细节，阻碍了抽象层面的推理。本文提出将定理解释为条件重写规则，借助 e-graph 上的等式饱和（equality saturation）自动搜索并推导等式证明，并将无法自动证明的条件作为证明义务呈现给用户。作者处理了命题条件、类型类等超出简单语法重写的方面，刻画了可这样解释的一类重要定理。该方法在 Lean 中以 tactic 形式实现，复用 egg 库的等式饱和能力，并通过四个用例展示了这一更高抽象层次在等式推理中的有效性。
Equations are ubiquitous in mathematical reasoning. Often, however, they only hold under certain conditions. As these conditions are usually clear from context, mathematicians regularly omit them when performing equational reasoning on paper. In contrast, interactive theorem provers pedantically insist on every detail to be convinced that a theorem holds, hindering equational reasoning at the more abstract level of pen-andpaper mathematics. In this paper, we address this issue by raising the level of equational reasoning to enable pen-and-paper style in interactive theorem provers. We achieve this by interpreting theorems as conditional rewrite rules, and use equality saturation to automatically derive equational proofs. Conditions that cannot be automatically proven may be surfaced as proof obligations. Concretely, we present how to interpret theorems as conditional rewrite rules for a significant class of theorems. Handling these theorems goes beyond simple syntactic rewriting, and deals with aspects like propositional conditions and type classes. We evaluate our approach by implementing it as a tactic in Lean, using the egg library for equality saturation with e-graphs. We show four use cases demonstrating the efficacy of this higher level of abstraction for equational reasoning.
@article{RosselSKSG26,
title = {Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation},
author = {Marcus Rossel and Rudi Schneider and Thomas Kœhler and Michel Steuwer and Andrés Goens},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776667}
}