  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.
