6 ms·

It certainly is a social construct, because what tools are at my disposal to convince someone who disagrees otherwise? In that sense everything is a social cons

It certainly is a social construct, because what tools are at my disposal to convince someone who disagrees otherwise? In that sense everything is a social construct. Apart from that, with the help of computers, it can be made absolutely precise and clear which statements follow from which axioms, and in that sense it is not a social construct at all. It also is much less cumbersome than it used to be, and will continue to improve quickly. I can sit down and prove something using a tool like Isabelle, and I will be as sure of its "truth" as I can possibly be, and it really doesn't matter what other people, mathematicians or not, think about it. That's the beauty of it. Of course, you could say my belief in Isabelle is also a social construct. Except it is not, I know exactly how Isabelle works. There could be issues with Isabelle, but these issues adding up to make my proof wrong are very unlikely, especially in addition to my independent understanding of the proof. But of course, it is much nicer if others can see the same truth that I do, and for this, computer-assisted proof is actually great, because it allows to understand and trust in the high-level structure of a proof without having to verify every little gritty low-level detail.

prmph 4y ago
> Apart from that, with the help of computers, it can be made absolutely precise and clear which statements follow from which axioms, and in that sense it is not a social construct at all. I think you are mistaken. The idea that math proofs are a social construct relates to, in my view, much deeper ideas than you seem to think [1]. It is not just that convincing other mathematicians that a proof is correct is a social process, but also that the reasoning on which any proof relies, even if it seems unassailable, even if built into an automated checker, is still a product of the human mind. Usually there is a level of logic that can challenge even what seems so basic as to be fool-proof. Take the proof that the square root of 2 is irrational. The proof relies on a contradiction that arises if one assumes the root is rational, but one can imagine a logic system where such a contradiction does not imply that the original assumption is false. How possible, you say? It's all math, where one is allowed any starting assumptions, and works out the implications of those. But, there is something deeply satisfying about thinking that contradictions are (or should be) impossible in our universe, and so this "proof" seems solid. 1. https://plato.stanford.edu/entries/intuitionism/ https://plato.stanford.edu/entries/intuitionism/
- qazxcvbnm 4y ago
  > It is not just that convincing other mathematicians that a proof is correct is a social process, but also that the reasoning on which any proof relies, even if it seems unassailable, even if built into an automated checker, is still a product of the human mind. Usually there is a level of logic that can challenge even what seems so basic as to be fool-proof. I think you are mistaken. I used to be very troubled by the notion that no single set of axioms really can be agreed on to do mathematics, but I have been convinced finally that the truth of the matter is a very subtle point; that the truth of mathematics is absolute; it merely is not finitely-axiomatisable. With a sufficiently weak proof system, clearly we can conceive of a system where the irrationality of the square root of 2 is not provably true, but no consistent proof system can prove that the square root of 2 is rational. Certain mathematical constructs, indeed most(*) of known mathematics, that which is constructible by constructivist methods, are irrefutably there in any consistent mathematical universe, and in that sense, true. Yet, no single axiom system can encompass all mathematical truth, as is well known from Goedel's theorems, but neither does that mean that the set of axioms to be worked with can be arbitrarily chosen. The chosen set of axioms must be consistent. The question, then, is whether consistency of axioms can possibly be an objective fact; and even though for any sufficiently strong set of axioms, its consistency cannot be proven in of itself, it consistency can in fact be objectively established - objectively established, but not finitely established. My evidence for this perspective is Scott Aaronson's construction of a Turing-Machine encoding of the ZFC axioms. What the construction of this encoding implies, is that the revelation of the uncomputable busy-beaver (BB) function for value 8000, which is a finite, well defined, and an objectively irrefutable, albeit unthinkably massive, number, constitutes a proof of the consistency of ZFC axioms. A similar procedure I believe can be applied to any set of axioms that one wishes to work with. The part where the magic occurs, I believe, is in the uncomputable nature of the BB function, by which it is possible to finally and objectively establish consistency of sets of axioms. Uncomputability amounts to the acknowledgement that though something may always be well-defined, there is no finite method to encompass its values; that is the nature I now take of mathematics as well.
  - auggierose 4y ago
    > Uncomputability amounts to the acknowledgement that though something may always be well-defined, there is no finite method to encompass its values That is kind of obvious, isn't it? But some people need more convincing than others :-)
soVeryTired 4y ago
> I can sit down and prove something using a tool like Isabelle, and I will be as sure of its "truth" as I can possibly be, and it really doesn't matter what other people, mathematicians or not, think about it. That's the beauty of it. But I guess the point is that almost no-one does this. I would guess that if someone tried to formally verify every published paper out there (or even every textbook), they would uncover a large number of gaps. Very few of those gaps would be unfixable, and very few results would turn out to be incorrect, but the possibility exists.
- auggierose 4y ago
  Not many do this currently, that is true. But this will change. In a hundred years every mathematician will do this. I think it will reach "mainstream" much much earlier than this, probably around 2030.
  - ChadNauseam 4y ago
    Probably by 2030 and by 2040 at the latest, you will be able to give a proposition to a machine learning model and the model will output a machine-verifiable proof of its truth or falsity at least as often as a human can.
    - auggierose 4y ago
      It's not that easy. Humans often work weeks, months, or even years towards proving a theorem. They need to build new theories for it, generalise the theorem, etc., before the proof becomes possible. I would not expect machines to be able to prove any of those theorems by 2030 automatically without human guidance (but maybe I am too pessimistic!) I definitely would expect machines to be able to do the sort of effortless small step reasoning that humans are capable of, and that's really all that is needed for proof assistants to go main stream. It is already possible to a certain extent now, but it needs to get a whole lot better.

prmph 4y ago

> Apart from that, with the help of computers, it can be made absolutely precise and clear which statements follow from which axioms, and in that sense it is not a social construct at all. I think you are mistaken. The idea that math proofs are a social construct relates to, in my view, much deeper ideas than you seem to think [1]. It is not just that convincing other mathematicians that a proof is correct is a social process, but also that the reasoning on which any proof relies, even if it seems unassailable, even if built into an automated checker, is still a product of the human mind. Usually there is a level of logic that can challenge even what seems so basic as to be fool-proof. Take the proof that the square root of 2 is irrational. The proof relies on a contradiction that arises if one assumes the root is rational, but one can imagine a logic system where such a contradiction does not imply that the original assumption is false. How possible, you say? It's all math, where one is allowed any starting assumptions, and works out the implications of those. But, there is something deeply satisfying about thinking that contradictions are (or should be) impossible in our universe, and so this "proof" seems solid. 1. https://plato.stanford.edu/entries/intuitionism/ https://plato.stanford.edu/entries/intuitionism/

qazxcvbnm 4y ago
> It is not just that convincing other mathematicians that a proof is correct is a social process, but also that the reasoning on which any proof relies, even if it seems unassailable, even if built into an automated checker, is still a product of the human mind. Usually there is a level of logic that can challenge even what seems so basic as to be fool-proof. I think you are mistaken. I used to be very troubled by the notion that no single set of axioms really can be agreed on to do mathematics, but I have been convinced finally that the truth of the matter is a very subtle point; that the truth of mathematics is absolute; it merely is not finitely-axiomatisable. With a sufficiently weak proof system, clearly we can conceive of a system where the irrationality of the square root of 2 is not provably true, but no consistent proof system can prove that the square root of 2 is rational. Certain mathematical constructs, indeed most(*) of known mathematics, that which is constructible by constructivist methods, are irrefutably there in any consistent mathematical universe, and in that sense, true. Yet, no single axiom system can encompass all mathematical truth, as is well known from Goedel's theorems, but neither does that mean that the set of axioms to be worked with can be arbitrarily chosen. The chosen set of axioms must be consistent. The question, then, is whether consistency of axioms can possibly be an objective fact; and even though for any sufficiently strong set of axioms, its consistency cannot be proven in of itself, it consistency can in fact be objectively established - objectively established, but not finitely established. My evidence for this perspective is Scott Aaronson's construction of a Turing-Machine encoding of the ZFC axioms. What the construction of this encoding implies, is that the revelation of the uncomputable busy-beaver (BB) function for value 8000, which is a finite, well defined, and an objectively irrefutable, albeit unthinkably massive, number, constitutes a proof of the consistency of ZFC axioms. A similar procedure I believe can be applied to any set of axioms that one wishes to work with. The part where the magic occurs, I believe, is in the uncomputable nature of the BB function, by which it is possible to finally and objectively establish consistency of sets of axioms. Uncomputability amounts to the acknowledgement that though something may always be well-defined, there is no finite method to encompass its values; that is the nature I now take of mathematics as well.
- auggierose 4y ago
  > Uncomputability amounts to the acknowledgement that though something may always be well-defined, there is no finite method to encompass its values That is kind of obvious, isn't it? But some people need more convincing than others :-)

soVeryTired 4y ago

> I can sit down and prove something using a tool like Isabelle, and I will be as sure of its "truth" as I can possibly be, and it really doesn't matter what other people, mathematicians or not, think about it. That's the beauty of it. But I guess the point is that almost no-one does this. I would guess that if someone tried to formally verify every published paper out there (or even every textbook), they would uncover a large number of gaps. Very few of those gaps would be unfixable, and very few results would turn out to be incorrect, but the possibility exists.

auggierose 4y ago
Not many do this currently, that is true. But this will change. In a hundred years every mathematician will do this. I think it will reach "mainstream" much much earlier than this, probably around 2030.
- ChadNauseam 4y ago
  Probably by 2030 and by 2040 at the latest, you will be able to give a proposition to a machine learning model and the model will output a machine-verifiable proof of its truth or falsity at least as often as a human can.
  - auggierose 4y ago
    It's not that easy. Humans often work weeks, months, or even years towards proving a theorem. They need to build new theories for it, generalise the theorem, etc., before the proof becomes possible. I would not expect machines to be able to prove any of those theorems by 2030 automatically without human guidance (but maybe I am too pessimistic!) I definitely would expect machines to be able to do the sort of effortless small step reasoning that humans are capable of, and that's really all that is needed for proof assistants to go main stream. It is already possible to a certain extent now, but it needs to get a whole lot better.