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.
Show HN: Theoriz3r, minimal proof of concept exploratory theorem prover | Heykuki News