3 ms·

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 b

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

tlringer 6y ago
It does. And if classical logic is what they like, they can use Isabelle/HOL just as nicely. It is classical. It has wonderful automation. Kevin gets attention because he is bold, not because he is correct. 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.
- JoeCamel 6y ago
  Saying Lean "rules out many kinds of mathematics" and not giving a single example, sounds more sensationalist to me. I also don't see what's wrong with anonymous comments as long as they are constructive and people are nice. I don't know Kevin as well as you do (apparently) but maybe he is just ignorant on the topics you know so much about. Why something gets attention of media (Quanta Magazine?) is complicated. From your comments, you also seem very "bold".
  - tlringer 6y ago
    I'm a woman though, and women rarely get positive attention for anything in CS. I'm bold because as a woman in the field you need to be bold to survive as a researcher. In the type theory and proof assistant worlds there are only a handful of us. A typical ratio at a conference for proof assistant research is 1 woman for every 40 men. Anonymous comments scare me because there are (a few, thankfully not many) abusive people in the PL community I am afraid of engaging with. I don't want to accidentally find myself arguing with one of them. I need to know when to exit the conversation. Proof relevant mathematics, higher category theory, lots of topology. Sorry. I don't spend all of time on HackerNews, I sometimes don't get around to responding to things. I am talking to Kevin about this framing so we can figure out how to make it healthier in the future. Some of my comments about Kevin were likewise out of line because I interpreted some of our previous interactions as rooted in a gender-based power dynamic when they were actually just rooted in something Kevin finds difficult and wants to do better at, and that is my honest mistake.
- throwaway45434 6y ago
  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.
  - tlringer 6y ago
    Lean is not classical. I don't know where the idea that Lean is classical is coming from. Lean is constructive. It is consistent with classical axioms, just like Coq is, and just like Cubical is in the propositional fragment. Isabelle/HOL on the other hand is classical, and is quite a natural choice if classical logic is what you want, which is why mathematicians have been using it for decades now. I know Kevin. He does good work. He also heckled every talk at ITP, including my own, in the middle to express his opinions. I have never met another researcher in my life who does that. Media outlets interview him and not the other 50 years of researchers doing work on proof assistants and using them both for mathematics and for verifying systems. I wrote a whole book about the history of program verification and for sure nobody has ever interviewed me about it. Kevin is loud and bold, that is why his opinions spread like fire. But they are just that, opinions.
    - lakecresva 6y ago
      It's because the mathlib authors don't really care about being constructive and frequently use things like choice/LEM, in contrast to Coq/math-comp. If there's a constructive and non-constructive version of something, the mathlib people will use whatever's easier or nicer to work with. There's some info here about how Lean does realizability with pervasive use of choice: https://github.com/coq/coq/issues/10871#issuecomment-546641216 https://github.com/coq/coq/issues/10871#issuecomment-5466412...
- throwaway45434 6y ago
  >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 discussion at your next lgbtqxyz-blm meetings.

tlringer 6y ago

It does. And if classical logic is what they like, they can use Isabelle/HOL just as nicely. It is classical. It has wonderful automation. Kevin gets attention because he is bold, not because he is correct. 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.

JoeCamel 6y ago
Saying Lean "rules out many kinds of mathematics" and not giving a single example, sounds more sensationalist to me. I also don't see what's wrong with anonymous comments as long as they are constructive and people are nice. I don't know Kevin as well as you do (apparently) but maybe he is just ignorant on the topics you know so much about. Why something gets attention of media (Quanta Magazine?) is complicated. From your comments, you also seem very "bold".
- tlringer 6y ago
  I'm a woman though, and women rarely get positive attention for anything in CS. I'm bold because as a woman in the field you need to be bold to survive as a researcher. In the type theory and proof assistant worlds there are only a handful of us. A typical ratio at a conference for proof assistant research is 1 woman for every 40 men. Anonymous comments scare me because there are (a few, thankfully not many) abusive people in the PL community I am afraid of engaging with. I don't want to accidentally find myself arguing with one of them. I need to know when to exit the conversation. Proof relevant mathematics, higher category theory, lots of topology. Sorry. I don't spend all of time on HackerNews, I sometimes don't get around to responding to things. I am talking to Kevin about this framing so we can figure out how to make it healthier in the future. Some of my comments about Kevin were likewise out of line because I interpreted some of our previous interactions as rooted in a gender-based power dynamic when they were actually just rooted in something Kevin finds difficult and wants to do better at, and that is my honest mistake.
throwaway45434 6y ago
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.
- tlringer 6y ago
  Lean is not classical. I don't know where the idea that Lean is classical is coming from. Lean is constructive. It is consistent with classical axioms, just like Coq is, and just like Cubical is in the propositional fragment. Isabelle/HOL on the other hand is classical, and is quite a natural choice if classical logic is what you want, which is why mathematicians have been using it for decades now. I know Kevin. He does good work. He also heckled every talk at ITP, including my own, in the middle to express his opinions. I have never met another researcher in my life who does that. Media outlets interview him and not the other 50 years of researchers doing work on proof assistants and using them both for mathematics and for verifying systems. I wrote a whole book about the history of program verification and for sure nobody has ever interviewed me about it. Kevin is loud and bold, that is why his opinions spread like fire. But they are just that, opinions.
  - lakecresva 6y ago
    It's because the mathlib authors don't really care about being constructive and frequently use things like choice/LEM, in contrast to Coq/math-comp. If there's a constructive and non-constructive version of something, the mathlib people will use whatever's easier or nicer to work with. There's some info here about how Lean does realizability with pervasive use of choice: https://github.com/coq/coq/issues/10871#issuecomment-546641216 https://github.com/coq/coq/issues/10871#issuecomment-5466412...
throwaway45434 6y ago
>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 discussion at your next lgbtqxyz-blm meetings.