theoriz3r is a wrapper for Z3 in python. The idea is to use Z3's model checking to do "exploratory theorem proving": an interaction style where the computer curates a giant list of automatically generated questions by eliminating questions that are answered as a trivial consequence of assertions that the user has already made.