9 ms·

I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.

JadeNB 6y ago
Just pick a different one! There are definitely formalisation efforts out there that use constructive mathematics; for example Coq is so called after the logic, the calculus of constructions, that it uses (https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions).
- kevinbuzzard 6y ago
  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.
  - 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
Most are... like Coq, Agda, HoTT, etc.
zozbot234 6y ago
AIUI, the Lean system does support constructive mathematics. You can add axioms and reasoning principles that make the system non-constructive, but they're entirely optional.
- IngoBlechschmid 6y ago
  Yes, you are quite right, but the community around Lean's standard library heavily focuses on classical mathematics.
cjfd 6y ago
There does not seem to be any reason for mathematicians to be turned about by these engines using constructive mathematics. One can use excluded middle as an axiom and do all the classical mathematics one likes. What becomes much easier if the engine is constructive is telling which theorems depend on excluded middle and which do not.
- zozbot234 6y ago
  This is in fact how Lean works - the basic logic is constructive and excluded middle is an "extra" axiom. But even that is not as elegant as just writing non-constructive statements in the negative fragment of the logic, where (AIUI) one can already reason classically with no need for extra axioms.
  - kmill 6y ago
    I know we've discussed on HN before whether the elegance of the negative fragment extends to practice, but something about Lean is that it doesn't have LEM as an axiom. It's a theorem following from (a version of) the axiom of choice, the existence of quotient types, proof irrelevance (proofs of the same theorem are equal), and proposition extensionality (logically equivalent propositions are equal). Lean doesn't let you construct things that materially depend on LEM however -- you can only use it to prove that already constructed things have desired properties.
    - enricozb 6y ago
      In case anyone is curious, the proof of LEM from AC is: Diaconescu's Theorem [0] [0]: https://en.wikipedia.org/wiki/Diaconescu%27s_theorem#:~:text=In%20mathematical%20logic%2C%20Diaconescu's%20theorem,later%20by%20Goodman%20and%20Myhill https://en.wikipedia.org/wiki/Diaconescu%27s_theorem#:~:text....
Abhinav2000 6y ago
What is constructive mathematics for the layman?
- a1369209993 6y ago
  Roughly, that proving a statement of the form "For all a,b,c,..., there exists x,y,z such that some statement involving a,b,c,...,x,y, and z is true." requires actually constructing suitable x,y, and z given suitable a,b,c, etc to derive them from.
  - Abhinav2000 6y ago
    Thanks
  - zozbot234 6y ago
    With the proviso that the non-constructive statement '∃ x such that P(x)' can also be understood constructively as '¬∀ x ¬P(x)' which does not require constructing a suitable x, so classical proofs can be modeled without adding any extra axioms to the logic. (Clearly the two statements are classically, though not constructively equivalent). Similarly, all classical uses of LEM (A ∨ B) can be understood as constructive statements of the form ¬(¬A ∧ ¬B).
- kevinbuzzard 6y ago
  It's mathematics where certain kinds of proof by contradiction are not allowed -- if you want to prove that something exists because you want to use it, then you have to make it, you can't just say "let's assume it didn't exist and go on from there to deduce that 0 = 1 which is definitely wrong, so our assumption is wrong, so it exists, so let's use it". Here is the reason why it's obvious for mathematicians. If you're trying to prove a theorem (e.g. the theorem that class numbers of imaginary quadratic fields tend to infinity), and then someone comes up with a proof which assumes that a certain generalisation of the Riemann hypothesis is true, and then someone else comes up with a proof which assumes that the exact same generalisation is false, then we mathematicians say "great, the theorem is now proved". This actually happened. However if your boss asks you to write some code which does a calculation, and the next day you show up in their office with two USB sticks and say "this code is guaranteed to produce the correct answer if the Riemann hypothesis is true, and this other code is guaranteed to produce the correct answer if the Riemann hypothesis is false" then you are going to lose your job, because all you did was prove that the code exists, which is less helpful than it could be. For me one of the biggest problems with the area of formalisation of mathematics is that for decades it has been dominated by computer scientists, whose view of what is important and beautiful in mathematics does not really coincide with that of the working mathematician. This is what I am fighting to change.
kmill 6y ago
After working with Lean for a while, I've started to appreciate that there is a wider range of what it means to be constructive -- being "fully constructive" seems to me to be like fanatical efforts to make everything X, for example "everything is a function" or "everything is an object" and so on. In the Lean approach, anything not marked `noncomputable` in the Type universe and above needs to be constructible, in the sense that there is a program that can compute such an object using a functional programming language (where the function is guaranteed to terminate), but proofs don't need to be constructible in the same way. Proofs are still functions, but they're free to use things like the axiom of choice in the course of a proof. The way things are set up, even if you use non-computable things while making your inferences, this "forbidden" data will not leak out. It seems eminently reasonable to me that you can argue a program computes the correct thing because it doesn't compute the wrong thing, and unless you're specifically studying different toposes/logics, I'm not sure what constructive logic would really give you (and it's not like mathematicians slavishly keep track of where they used the axiom of choice or its consequence the LEM). How this all looks in Lean practice is that it's stronger to give a definition and prove it satisfies a property than to prove a "there exists" statement. mathlib authors tend to go for the first, unless the result is inherently noncomputable. There's also a facility for lifting propositions up to boolean values, which more or less amounts to giving a constructive proof -- this is used pervasively, for example with finite sets, which are constructive in the sense that if you have one there's an actual finite list backing it. I guess in short: it's a useful middle ground being able to prove something exists without having to construct it, but if you want to "have" the thing that purportedly exists you need to construct it.

JadeNB 6y ago

Just pick a different one! There are definitely formalisation efforts out there that use constructive mathematics; for example Coq is so called after the logic, the calculus of constructions, that it uses (https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions).

kevinbuzzard 6y ago
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.
- 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

Most are... like Coq, Agda, HoTT, etc.

zozbot234 6y ago

AIUI, the Lean system does support constructive mathematics. You can add axioms and reasoning principles that make the system non-constructive, but they're entirely optional.

IngoBlechschmid 6y ago
Yes, you are quite right, but the community around Lean's standard library heavily focuses on classical mathematics.

cjfd 6y ago

There does not seem to be any reason for mathematicians to be turned about by these engines using constructive mathematics. One can use excluded middle as an axiom and do all the classical mathematics one likes. What becomes much easier if the engine is constructive is telling which theorems depend on excluded middle and which do not.

zozbot234 6y ago
This is in fact how Lean works - the basic logic is constructive and excluded middle is an "extra" axiom. But even that is not as elegant as just writing non-constructive statements in the negative fragment of the logic, where (AIUI) one can already reason classically with no need for extra axioms.
- kmill 6y ago
  I know we've discussed on HN before whether the elegance of the negative fragment extends to practice, but something about Lean is that it doesn't have LEM as an axiom. It's a theorem following from (a version of) the axiom of choice, the existence of quotient types, proof irrelevance (proofs of the same theorem are equal), and proposition extensionality (logically equivalent propositions are equal). Lean doesn't let you construct things that materially depend on LEM however -- you can only use it to prove that already constructed things have desired properties.
  - enricozb 6y ago
    In case anyone is curious, the proof of LEM from AC is: Diaconescu's Theorem [0] [0]: https://en.wikipedia.org/wiki/Diaconescu%27s_theorem#:~:text=In%20mathematical%20logic%2C%20Diaconescu's%20theorem,later%20by%20Goodman%20and%20Myhill https://en.wikipedia.org/wiki/Diaconescu%27s_theorem#:~:text....

Abhinav2000 6y ago

What is constructive mathematics for the layman?

a1369209993 6y ago
Roughly, that proving a statement of the form "For all a,b,c,..., there exists x,y,z such that some statement involving a,b,c,...,x,y, and z is true." requires actually constructing suitable x,y, and z given suitable a,b,c, etc to derive them from.
- Abhinav2000 6y ago
  Thanks
- zozbot234 6y ago
  With the proviso that the non-constructive statement '∃ x such that P(x)' can also be understood constructively as '¬∀ x ¬P(x)' which does not require constructing a suitable x, so classical proofs can be modeled without adding any extra axioms to the logic. (Clearly the two statements are classically, though not constructively equivalent). Similarly, all classical uses of LEM (A ∨ B) can be understood as constructive statements of the form ¬(¬A ∧ ¬B).
kevinbuzzard 6y ago
It's mathematics where certain kinds of proof by contradiction are not allowed -- if you want to prove that something exists because you want to use it, then you have to make it, you can't just say "let's assume it didn't exist and go on from there to deduce that 0 = 1 which is definitely wrong, so our assumption is wrong, so it exists, so let's use it". Here is the reason why it's obvious for mathematicians. If you're trying to prove a theorem (e.g. the theorem that class numbers of imaginary quadratic fields tend to infinity), and then someone comes up with a proof which assumes that a certain generalisation of the Riemann hypothesis is true, and then someone else comes up with a proof which assumes that the exact same generalisation is false, then we mathematicians say "great, the theorem is now proved". This actually happened. However if your boss asks you to write some code which does a calculation, and the next day you show up in their office with two USB sticks and say "this code is guaranteed to produce the correct answer if the Riemann hypothesis is true, and this other code is guaranteed to produce the correct answer if the Riemann hypothesis is false" then you are going to lose your job, because all you did was prove that the code exists, which is less helpful than it could be. For me one of the biggest problems with the area of formalisation of mathematics is that for decades it has been dominated by computer scientists, whose view of what is important and beautiful in mathematics does not really coincide with that of the working mathematician. This is what I am fighting to change.

kmill 6y ago

After working with Lean for a while, I've started to appreciate that there is a wider range of what it means to be constructive -- being "fully constructive" seems to me to be like fanatical efforts to make everything X, for example "everything is a function" or "everything is an object" and so on. In the Lean approach, anything not marked `noncomputable` in the Type universe and above needs to be constructible, in the sense that there is a program that can compute such an object using a functional programming language (where the function is guaranteed to terminate), but proofs don't need to be constructible in the same way. Proofs are still functions, but they're free to use things like the axiom of choice in the course of a proof. The way things are set up, even if you use non-computable things while making your inferences, this "forbidden" data will not leak out. It seems eminently reasonable to me that you can argue a program computes the correct thing because it doesn't compute the wrong thing, and unless you're specifically studying different toposes/logics, I'm not sure what constructive logic would really give you (and it's not like mathematicians slavishly keep track of where they used the axiom of choice or its consequence the LEM). How this all looks in Lean practice is that it's stronger to give a definition and prove it satisfies a property than to prove a "there exists" statement. mathlib authors tend to go for the first, unless the result is inherently noncomputable. There's also a facility for lifting propositions up to boolean values, which more or less amounts to giving a constructive proof -- this is used pervasively, for example with finite sets, which are constructive in the sense that if you have one there's an actual finite list backing it. I guess in short: it's a useful middle ground being able to prove something exists without having to construct it, but if you want to "have" the thing that purportedly exists you need to construct it.