Correction: it is a proof assistant, not a theorem prover. Z3 (also from De Moura) is a theorem prover. EDIT: Main difference between the two is that with a pr

Correction: it is a proof assistant, not a theorem prover. Z3 (also from De Moura) is a theorem prover. EDIT: Main difference between the two is that with a proof assistant, you write a proof and the assistant checks its correctness, while a prover provides you with a proof of a proposition's correctness (or of its lack thereof).