Tao's Equational Proof Challenge Accepted (Technical Report)
计算机科学中的逻辑
2026-05-21 v1
摘要
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.
引用
@article{arxiv.2605.21200,
title = {Tao's Equational Proof Challenge Accepted (Technical Report)},
author = {Lydia Kondylidou and Jasmin Blanchette and Marijn J. H. Heule},
journal= {arXiv preprint arXiv:2605.21200},
year = {2026}
}
备注
18 pages. Extended version of a paper accepted at IJCAR 2026