4 ms·

How many professional mathematicians use Isabelle/HOL? Honest question!

• yummyfajitas 12y ago
  Close to none. Part of that is a social problem. People who do computer assisted proofs are not particularly well regarded, in my experience. Another big issue with those tools is that they don't work as well for analysis as they do for algebraic geometry and graph theory. This might be in part due to the fact that most of the folks constructing them are logicians, not analysts.