Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.



Consider applying for YC's Fall 2026 batch! Applications are open till July 27.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: