Tao's Equational Proof Challenge Accepted (Technical Report)

TL;DR

This paper presents Krympa, a proof minimization tool that significantly reduces complex equational proofs by combining brute force, heuristics, and multiple provers, demonstrated on proofs from Terence Tao's challenge.

Contribution

Introduction of Krympa, a novel proof minimization tool that effectively shortens complex equational proofs using combined strategies and multiple theorem provers.

Findings

Reduced a 62-step proof to 20 steps using Krympa.

Successfully minimized a 151-step proof to 10 steps in empirical tests.

Performed well on 1431 equational problems from the same project.

Abstract

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.