Hacker News Reader

throwaway45434on Why is dependent type theory more suitable than set theory for proof assistants?

I agree with you that it's not obvious that Lean is the only or best option for formalizing "all" or at least most of mathematics. But I didn't get the impression that Kevin thinks that it's the best tool imaginable but rather the best tool that is currently available.

But that wasn't the point: He's right in that constructive/intuitionistic mathematics is so niche that it can be safely ignored when discussing formalization of the mathematics he and almost every other mathematician or scientist is interested in.

Kevin gets attention because he's an accomplished mathematician who tries to formalize his work, or at least what it's based on. I find it ridiculous to dismiss his opinion the way you do.

throwaway45434on Why is dependent type theory more suitable than set theory for proof assistants?

At least 99% of all mathematicians in academia work with classical logic only, and a good fraction hasn't even heard of anything else. So yeah, Lean might not be suitable for some of the remaining 1%, but that doesn't make Kevin's claim "sensationalist".