Разница между Z3 и coq

Мне интересно, может ли кто-нибудь сказать мне разницу между Z3 и coq? Мне кажется, что coq является помощником проверки в том смысле, что он требует, чтобы пользователь заполнил шаги проверки, тогда как Z3 не имеет этого требования. Но похоже, что у coq тоже есть автоматическая тактика, похожая на то, что делает Z3? Или, может быть, возможность поиска доказательств в coq не такая мощная, как в Z3?