# Conjectures, Tests and Proofs: An Overview of Theory Exploration

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 28 references that are in the map.
- First posted on arXiv 7 Sep 2021.

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

- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [Proof-Pattern Recognition and Lemma Discovery in ACL2](https://mlsanity.com/paper/1308.1780/) (2013)
- [Hipster: Integrating Theory Exploration in a Proof Assistant](https://mlsanity.com/paper/1405.3426/) (2014)
- [Formalizing Graph Trail Properties in Isabelle/HOL](https://mlsanity.com/paper/2103.03607/) (2021)

## Abstract (arXiv)

A key component of mathematical reasoning is the ability to formulate interesting conjectures about a problem domain at hand. In this paper, we give a brief overview of a theory exploration system called QuickSpec, which is able to automatically discover interesting conjectures about a given set of functions. QuickSpec works by interleaving term generation with random testing to form candidate conjectures. This is made tractable by starting from small sizes and ensuring that only terms that are irreducible with respect to already discovered conjectures are considered. QuickSpec has been successfully applied to generate lemmas for automated inductive theorem proving as well as to generate specifications of functional programs. We give an overview of typical use-cases of QuickSpec, as well as demonstrating how to easily connect it to a theorem prover of the user's choice.