One area I've been playing with is "theory exploration", which takes a set of definitions and produces lemmas that are 'interesting' (i.e. irreducible, via some scheme like Knuth-Bendix rewriting).

(Thanks to Curry-Howard, we can also view this as generating test suites/specifications for software libraries!)

Notable tools include Hipster, IsaScheme, IsaCoSy, QuickSpec and Speculate.