In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover. We introduce a proof minimization tool called Krympa. Using a combination of brute force and heuristics, and exploiting both Vampire and the Twee equational prover, the tool reduces the 62-step proof to 20 steps, each corresponding to a rewrite. In an empirical evaluation, it also performs well on 1431 equational problems originating from the same project, reducing in particular a 151-step proof to only 10 steps.

翻译：在方程理论项目背景下，陶哲轩提出了一项挑战：寻找由Vampire叠加证明器生成的复杂62步证明的替代方案。我们引入了一个名为Krympa的证明最小化工具。通过结合穷举搜索与启发式方法，并利用Vampire和Twee方程证明器，该工具将62步证明缩减为20步，每步对应一个重写规则。在实证评估中，该工具对源自同一项目的1431个方程问题表现良好，尤其将一段151步证明减少至仅10步。