Thank you for your thoughtful response, Marshall. Just one question for now: Has any of this helped you develop your own theorem prover? It all seems quite removed from the world of "real" mathematics. (Group axioms with unbounded quantifiers? What next?)