> The most popular theorem provers (at least among computer scientists) are based on some form of Martin-Löf type theory.
Are they? Judging by posts on HN, I 100% agree. But judging by the number of users and the amount of verified mathematics and code, I'm not so sure.
Maybe things have changed recently, but I believe that systems based on simple type theory (HOL and Isabelle) and systems based on set theory (Mizar, Metamath) have much larger repositories of verified mathematics and verified programs than those based on dependent type theories.
I don't have hard numbers to prove it. But I think it's significant that https://deepspec.org/main, the largest recent formal verification project (at least in the US) chose to use Coq, which is based on type theory. There's also Coq-verified code in Chrome (http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP1...), a claim that can't be made for any other theorem provers (as far as I'm aware).
Are they? Judging by posts on HN, I 100% agree. But judging by the number of users and the amount of verified mathematics and code, I'm not so sure.
Maybe things have changed recently, but I believe that systems based on simple type theory (HOL and Isabelle) and systems based on set theory (Mizar, Metamath) have much larger repositories of verified mathematics and verified programs than those based on dependent type theories.