Papers With

← All papers
First page of Tao's Equational Proof Challenge Accepted (Technical Report)

Tao's Equational Proof Challenge Accepted (Technical Report)

Lydia Kondylidou, Jasmin Blanchette, Marijn J. H. Heule

cs.LO May 20, 2026 · v1
tooling tactic-automation algebra logic
Read PDF arXiv abstract Code
TL;DR
Krympa parses Lean theorems from the Equational Theories Project into TPTP and outputs minimized proofs as Lean calc-based or automation-based proofs checked by Lean.
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.
Problem

In the Equational Theories Project, Vampire produced an unintelligible 62-step superposition proof of the magma implication 650 ⇒ 448. Terence Tao challenged the community to find a simpler alternative proof.

Approach

Krympa converts Vampire refutation proofs into direct proofs. For each lemma it generates big-step, small-step, and abstracted problems and attempts them with both Vampire and Twee. It then assembles a three-segment proof through chosen departure and arrival lemmas, keeping the shortest combination. Results are emitted as Lean proofs, either step-by-step with calc or compactly using Lean automation, and inputs are parsed from the project's Lean files.

Results

The 62-step proof was reduced to 20 rewrite steps. On 1431 problems from the project's Lean files, average proof length fell from 6.6 to 4.5 steps, and one 151-step proof was cut to 10 steps.

FileNum. problemsAvg. beforeAvg. after (BS)
Proofs71137.211.8
Proofs91439.813.1
Proofs131035.39.1
Total11726.311.4
Selected rows: average proof lengths for problems with baseline proofs of at least 15 steps (BS = big+small-step variants)