Comment by auntienomen
3 days ago
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.
No comments yet
Contribute on Hacker News ↗