Comment by Kratacoa
3 days ago
And formalised mathematics are ignored in mathematical practice by most mathematicians, and even the ones that know of it often don't use that as a foundational language due to relative inconvenience.
3 days ago
And formalised mathematics are ignored in mathematical practice by most mathematicians, and even the ones that know of it often don't use that as a foundational language due to relative inconvenience.
I think at this stage, most mathematicians recognize that formal proof verification is a real and interesting thing. We have extremely prominent mathematicians like Scholze & Tao making a point of using these tools.
But in many cases, it's extra effort for not much reward. The patterns which most mathemematicians are interested in are (generally) independent of the particular foundations used to realize them. Whether one invests the effort into formal verification depends on how hard the argument is and how crucial the theorem.