Comment by throwaway45434

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".