In the theory of a set of axioms there are many boring logical consequences, and scattered among them there are a few interesting ones. The few interesting ones include those that are singled out as theorems by human experts in the domain. This paper describes the techniques, implementation, and results of a automated system that generates logical consequences of a set of axioms, and uses filters and ranking to identify interesting theorems among the logical consequences. It is capable of generating and identifying interesting theorems that have not been explicitly identified by human experts.