They actually have different enough use cases and abilities that it is rare to consider them as competitors.
The logic of Coq is vastly more expressive and it's proof process is vastly more controllable.
All of this comes at the cost of level of expertise required and ease and scale of automation.
I'm a big fan of Z3 clearly, but there are entire realms of human thought that can be clearly encoded into Coq that basically cannot in Z3.
You can in principle be fairly expressive in Z3Py if you use quantifiers freely and python as kind of a macro system but it is clunky and Z3 won't actually be able to solve convoluted quantifier usage, at which point you're sunk. You may at that point start to try to split up your theorem into pieces, but then you are building an ad hoc theorem prover that isn't quite just Z3.
In Coq, there is always the ability to appeal to the effort and ingenuity of the programmer/prover.
Coq has a much better ability to deal with the infinite, induction, and symbolic manipulation. It is also an entire programming language in its own right that you can run or extract to OCaml.
Another difference is the de Bruijn criterion. Proofs from a prover are only as trusted as the code of the prover itself. The "trusted core" of Coq is small, a few thousand lines of code. Whereas Z3 is not designed with this in mind, and there is no trusted core of Z3. You have to trust basically all of it. This point does not personally bother me that much, but other people find it important
One of the Coq downsides is the speed. Partially because of the higher level computations, but also partially because of the OCaml. I hope, OCaml Multicore will help the cause significantly.
The logic of Coq is vastly more expressive and it's proof process is vastly more controllable.
All of this comes at the cost of level of expertise required and ease and scale of automation.
I'm a big fan of Z3 clearly, but there are entire realms of human thought that can be clearly encoded into Coq that basically cannot in Z3.
You can in principle be fairly expressive in Z3Py if you use quantifiers freely and python as kind of a macro system but it is clunky and Z3 won't actually be able to solve convoluted quantifier usage, at which point you're sunk. You may at that point start to try to split up your theorem into pieces, but then you are building an ad hoc theorem prover that isn't quite just Z3.
In Coq, there is always the ability to appeal to the effort and ingenuity of the programmer/prover.
Coq has a much better ability to deal with the infinite, induction, and symbolic manipulation. It is also an entire programming language in its own right that you can run or extract to OCaml.
Another difference is the de Bruijn criterion. Proofs from a prover are only as trusted as the code of the prover itself. The "trusted core" of Coq is small, a few thousand lines of code. Whereas Z3 is not designed with this in mind, and there is no trusted core of Z3. You have to trust basically all of it. This point does not personally bother me that much, but other people find it important