5 ms·

Hi! Yes! Just pick a different one! The problem is that constructivists have been formalising mathematics for decades and have not really managed to break throu

Hi! Yes! Just pick a different one! The problem is that constructivists have been formalising mathematics for decades and have not really managed to break through into the mainstream mathematical community with their efforts. The difference with Lean's maths library is that we absolutely reject constructivism, which makes Lean far less suitable for certain kinds of computations but conversely far far better equipped for proving all the theorems in an undergraduate mathematics curriculum and then going on to tackle research level mathematical questions of the kind which most mathematicians recognise as "normal mathematics". My argument (I should say that I am the author of the blog post) is that this resolutely non-classical approach is far more likely to arouse the interest of mainstream mathematicians, who rejected constructivism 100 years ago and have never looked back. I can certainly see a role for constructive mathematics, however I know from experience that most working mathematicians reject it and hence the pragmatic approach is to reject it when formalising if we are to start appealing to the mathematical masses.

guerrilla 6y ago
The Four Colour Theorem in Coq seems pretty mainstream I'd say... Also I guess you know that you don't personally have to reject LEM to use Agda or whatever, you just can't do everything in it or at least everything the classical way.
- kevinbuzzard 6y ago
  This is a milestone result, and its formalisation taught us many things, for example that the systems are capable of handling long proofs about elementary objects. However finite graph theory is not remotely mainstream mathematics. Take your favourite super-prestigious maths prize, for example the Abel Prize or the Fields Medal. Now look at everyone who has won this prize in the last 10 years. That is the definition of mainstream mathematics. And as you will see if you do this, the areas which these people are working on are a million miles away from finite graph theory. This is precisely the problem. Computer scientists sometimes have a very twisted view of exactly what kind of mathematics is regarded as important in 2021. The experiment I outline above will give you some idea of what is mainstream, and believe me, it's not the four colour theorem.
  - kmill 6y ago
    I suppose it's not exactly mainstream, but Kronheimer and Mrowka are among those trying to prove the four color theorem using instanton homology and gauge theory. It's certainly not finite graph theory, though (their idea of a 3-regular graph is the singular locus of a certain kind of orbifold!)
  - QuesnayJr 6y ago
    Finite graph theory is completely mainstream mathematics. There's a kind of elite provicialism that you sometimes see, where only the mathematics that's done at Harvard or wins the big prizes counts, and this is a good example. There are probably more people employed in math departments working on finite graph theory than there are working on the Langlands Program. Robertson and Seymour were too old to be eligible, but the fact that someone like them could never win the Fields Medal, while someone in other fields could, is a statement about who is well-connected with the prize committee, and not a general statement about mathematics. And I say this as someone with no interest in graph theory, or combinatorics in general.
    - spekcular 6y ago
      Buzzard's post suggests to me that when he says "mainstream," he means what the community at large thinks of as important and field-defining (cf. the sentence with important in it). He is totally correct here; in this sense finite graph theory is not mainstream mathematics. Further, I don't think it is "elite provincialism" to point out this readily verifiable fact. Besides looking at the big prizes, we can look at any of the top journals (Annals, IHES, Inventiones, Journal of the AMS, Acta, whatever). You're not going to find a lot of finite graph theory there. Now, I think we should separate the question whether it is the case that he's right about what mathematicians value from the question of whether it ought to be the case that the world is this way. As I just said, the answer to the first question is yes. I'd argue that the answer to the second question is also yes, but that's a whole different discussion.
      - QuesnayJr 6y ago
        Pointing to the top journals is again a statement about who is well-connected, so if anything it is further proof of my claim of elite provincialism. Mathematics has politics, like any other field, and it's politics that determine that the proof of the Robertson-Seymour Theorem appeared in the "Journal of Combinatorial Theory" and not JAMS. The irony is that I suspect every single mathematician, elite or not, knows what the four-color theorem is, far more than could tell you what chromatic homotopy is, or state anything about the Langlands program beyond "Uh, it's something about number theory? And groups? Maybe?"
JadeNB 6y ago
> resolutely non-classical approach Calling this 'non-classical' is interesting—it's definitely non-classical from the point of view of formalisation, but I'm not sure formalisation has been around long enough to have classics …. As of course you know but non-mathematicians may not, from a non-formalising mathematician's point of view, it's the non-constructive logic that's classical, to the extent that it's actually sometimes called classical logic (https://en.wikipedia.org/wiki/Classical_logic https://en.wikipedia.org/wiki/Classical_logic).
- kevinbuzzard 6y ago
  :-) Yes, by assuming classical logic the Lean community is taking a non-classical approach to bringing formalisation to the masses :-)
Abhinav2000 6y ago
Dear Kevin, I am working on some hobby projects, similar but very much more elementary to what you are doing. May I please kindly get your e-mail address (or you may drop me a note at ashok dot khanna at hotmail dot com). I would love to connect and follow your work. I apologise as I was not able to find your e-mail address on your blog post - sorry if I missed it. Best wishes,
vcdimension 6y ago
AFAIK the advantage of constructivism is algorithms. Coq allows you to extract lisp/ML/Haskell programs. Perhaps we will be seeing the next generation of fully homomorphic encryption programs, or topological data analysis programs, automatically generated by Coq.
- auggierose 6y ago
  So what about an algorithm you verified in a non-constructive way?
  - vcdimension 6y ago
    You still need to construct the algorithm in the first place, which is what a constructive proof does.
    - auggierose 6y ago
      Sure, but you would not need to prove it in a constructive way. See, that is one of the problems with constructive mathematics. It not only requires you to write down the algorithm, but also to prove it constructively, although a non-constructive proof would be perfectly fine. In other words: constructivism is often overkill.
      - vcdimension 6y ago
        I think we're at cross-purposes; I am talking about mathematics for the purpose of real-life useful applications (e.g. cryptography, data analysis, etc), in which case you need algorithms.
        auggierose 6y ago
        Nope, we are not at cross-purposes. You just don't understand what I am saying. Let's say you need an algorithm for a real-life situation, and you manage to write one down. Ok then, you are good to go, just use it! But ... how do you know that the algorithm you have written down is correct? Now, a constructive mathematician would require you to also provide a constructive proof for your algorithm. A mainstream mathematician would additionally also be fine with a non-constructive proof for your algorithm. So, who is more real-life?

guerrilla 6y ago

The Four Colour Theorem in Coq seems pretty mainstream I'd say... Also I guess you know that you don't personally have to reject LEM to use Agda or whatever, you just can't do everything in it or at least everything the classical way.

kevinbuzzard 6y ago
This is a milestone result, and its formalisation taught us many things, for example that the systems are capable of handling long proofs about elementary objects. However finite graph theory is not remotely mainstream mathematics. Take your favourite super-prestigious maths prize, for example the Abel Prize or the Fields Medal. Now look at everyone who has won this prize in the last 10 years. That is the definition of mainstream mathematics. And as you will see if you do this, the areas which these people are working on are a million miles away from finite graph theory. This is precisely the problem. Computer scientists sometimes have a very twisted view of exactly what kind of mathematics is regarded as important in 2021. The experiment I outline above will give you some idea of what is mainstream, and believe me, it's not the four colour theorem.
- kmill 6y ago
  I suppose it's not exactly mainstream, but Kronheimer and Mrowka are among those trying to prove the four color theorem using instanton homology and gauge theory. It's certainly not finite graph theory, though (their idea of a 3-regular graph is the singular locus of a certain kind of orbifold!)
- QuesnayJr 6y ago
  Finite graph theory is completely mainstream mathematics. There's a kind of elite provicialism that you sometimes see, where only the mathematics that's done at Harvard or wins the big prizes counts, and this is a good example. There are probably more people employed in math departments working on finite graph theory than there are working on the Langlands Program. Robertson and Seymour were too old to be eligible, but the fact that someone like them could never win the Fields Medal, while someone in other fields could, is a statement about who is well-connected with the prize committee, and not a general statement about mathematics. And I say this as someone with no interest in graph theory, or combinatorics in general.
  - spekcular 6y ago
    Buzzard's post suggests to me that when he says "mainstream," he means what the community at large thinks of as important and field-defining (cf. the sentence with important in it). He is totally correct here; in this sense finite graph theory is not mainstream mathematics. Further, I don't think it is "elite provincialism" to point out this readily verifiable fact. Besides looking at the big prizes, we can look at any of the top journals (Annals, IHES, Inventiones, Journal of the AMS, Acta, whatever). You're not going to find a lot of finite graph theory there. Now, I think we should separate the question whether it is the case that he's right about what mathematicians value from the question of whether it ought to be the case that the world is this way. As I just said, the answer to the first question is yes. I'd argue that the answer to the second question is also yes, but that's a whole different discussion.
    - QuesnayJr 6y ago
      Pointing to the top journals is again a statement about who is well-connected, so if anything it is further proof of my claim of elite provincialism. Mathematics has politics, like any other field, and it's politics that determine that the proof of the Robertson-Seymour Theorem appeared in the "Journal of Combinatorial Theory" and not JAMS. The irony is that I suspect every single mathematician, elite or not, knows what the four-color theorem is, far more than could tell you what chromatic homotopy is, or state anything about the Langlands program beyond "Uh, it's something about number theory? And groups? Maybe?"

JadeNB 6y ago

> resolutely non-classical approach Calling this 'non-classical' is interesting—it's definitely non-classical from the point of view of formalisation, but I'm not sure formalisation has been around long enough to have classics …. As of course you know but non-mathematicians may not, from a non-formalising mathematician's point of view, it's the non-constructive logic that's classical, to the extent that it's actually sometimes called classical logic (https://en.wikipedia.org/wiki/Classical_logic https://en.wikipedia.org/wiki/Classical_logic).

kevinbuzzard 6y ago
:-) Yes, by assuming classical logic the Lean community is taking a non-classical approach to bringing formalisation to the masses :-)

Abhinav2000 6y ago

Dear Kevin, I am working on some hobby projects, similar but very much more elementary to what you are doing. May I please kindly get your e-mail address (or you may drop me a note at ashok dot khanna at hotmail dot com). I would love to connect and follow your work. I apologise as I was not able to find your e-mail address on your blog post - sorry if I missed it. Best wishes,

vcdimension 6y ago

AFAIK the advantage of constructivism is algorithms. Coq allows you to extract lisp/ML/Haskell programs. Perhaps we will be seeing the next generation of fully homomorphic encryption programs, or topological data analysis programs, automatically generated by Coq.

auggierose 6y ago
So what about an algorithm you verified in a non-constructive way?
- vcdimension 6y ago
  You still need to construct the algorithm in the first place, which is what a constructive proof does.
  - auggierose 6y ago
    Sure, but you would not need to prove it in a constructive way. See, that is one of the problems with constructive mathematics. It not only requires you to write down the algorithm, but also to prove it constructively, although a non-constructive proof would be perfectly fine. In other words: constructivism is often overkill.
    - vcdimension 6y ago
      I think we're at cross-purposes; I am talking about mathematics for the purpose of real-life useful applications (e.g. cryptography, data analysis, etc), in which case you need algorithms.
      - auggierose 6y ago
        Nope, we are not at cross-purposes. You just don't understand what I am saying. Let's say you need an algorithm for a real-life situation, and you manage to write one down. Ok then, you are good to go, just use it! But ... how do you know that the algorithm you have written down is correct? Now, a constructive mathematician would require you to also provide a constructive proof for your algorithm. A mainstream mathematician would additionally also be fine with a non-constructive proof for your algorithm. So, who is more real-life?