>Anonymous comments are cowardly; please show yourself. If you stay anonymous I am not aware of power dynamics, and I cannot adjust my response accordingly. Yeah no thanks, I would rather not be the subject of…
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…
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…
>Anonymous comments are cowardly; please show yourself. If you stay anonymous I am not aware of power dynamics, and I cannot adjust my response accordingly. Yeah no thanks, I would rather not be the subject of…
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…
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…