# Twitch: Learning Abstractions for Equational Theorem Proving

arXiv: https://arxiv.org/abs/2603.06849 · HTML: https://mlsanity.com/paper/2603.06849/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 25 references that are in the map.
- First posted on arXiv 6 Mar 2026.

## Builds on (most cited first, 5 of 5)

- [Top-Down Synthesis for Library Learning](https://mlsanity.com/paper/2211.16605/) (2022)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [Finding Proofs in Tarskian Geometry](https://mlsanity.com/paper/1606.07095/) (2016)
- [Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures](https://mlsanity.com/paper/2505.12305/) (2025)

## Abstract (arXiv)

Several successful strategies in automated reasoning rely on human-supplied guidance about which term or clause shapes are interesting. In this paper we aim to discover interesting term shapes automatically. Specifically, we discover abstractions : term patterns that occur over and over again in relevant proofs. We present our tool Twitch which discovers abstractions with the help of Stitch, a tool originally developed for discovering reusable library functions in program synthesis tasks. Twitch can produce abstractions in two ways: (1) from a partial, failed proof of a conjecture; (2) from successful proofs of other theorems in the same domain. We have also extended Twee, an equational theorem prover, to use these abstractions. We evaluate Twitch on a set of unit equality (UEQ) problems from TPTP, and show that it can prove 12 rating-1 problems as well as yielding significant speed-ups on many other problems.