3 ms·

Why do you insist mathematicians become programmers? They have different skills, have different ways of thinking, and solve different problems. As an analogy, p

by smadge 8y ago

Why do you insist mathematicians become programmers? They have different skills, have different ways of thinking, and solve different problems. As an analogy, plenty of famous musicians were obviously very musically talented but didn’t know how to read or write musical notation. Proofs are just a medium to convey mathematical ideas to other mathematicians. I bet if Erdos were required to publish his ideas in a theorem prover language his mathematical output would have at least halved.

dwheeler 8y ago
> Why do you insist mathematicians become programmers? No one is insisting that. We're insisting that proofs actually be correct, something that demonstrably cannot be done (to an adequate level) when we depend only on humans. Humans get tired and make mistakes such as failing to notice missing or invalid steps. Humans are still really good at coming up with proofs - but not so good at verifying them. > Proofs are just a medium to convey mathematical ideas to other mathematicians. I disagree. For example, claiming that a^n + b^n = c^n for any integer value of n greater than 2 when all values are integer is clearly a mathematical idea. But that idea is not a proof of Fermat's Last Theorem; it is simply an idea. A proof should establish, beyond doubt, that a claim is actually true. > I bet if Erdos were required to publish his ideas in a theorem prover language his mathematical output would have at least halved. I'm not sure about that, Erdos was pretty smart. There's relatively little investment in theorem prover languages; a little investment would go a long way. For example, today you have to prove lots of little things that really should be in libraries and tools, but the lack of investment holds things back. This also assumes that "mathematical output" is acceptable if it is not computer-verified. At some point in the future I think a "proof" that is not computer-verified will be viewed as an unproven claim. Humans simply aren't very good at verifying proofs - and computers are extremely good at it.
- smadge 8y ago
  Well, I guess what I meant is that proofs are for convincing other mathematicians. If someone is unconvinced by the proof they’ll try to fill in the gaps or further specify certain parts of the proof themselves. If that doesn’t work, they might ask for clarification. Eventually a consensus on the validity of the proof will be reached. I agree if the proof were presented in a machine verifiable format to begin with we wouldn’t need this process. I think though, that the reason it isn’t done this way is partly because the effort required isn’t worth it yet. My professor would actually get annoyed if I am too specific in my proofs because it overall makes the proof more difficult for a human to understand, which as I said is ultimately the purpose of a proof. Additionally the proof itself sometimes conveys an interesting idea that isn’t captured in the theorem. Some theorems have many different proofs that use different methods to prove the same theorem. These different proofs provide different perspectives that lead to a better understanding of the topic. I have a background in both computer science and pure math and am very interested in highly formal methods, I just don’t think we should disparage mathemicians for doing more human oriented math.
  - dwheeler 8y ago
    > Some theorems have many different proofs that use different methods to prove the same theorem. These different proofs provide different perspectives that lead to a better understanding of the topic. Agreed, but there's no conflict. You can create multiple formal proofs, each of which provide different perspective that can lead to a better understanding. > Well, I guess what I meant is that proofs are for convincing other mathematicians. Not everyone agrees with this claim, and this disagreement is the essence of the "crisis". Is the purpose of a proof (1) to show that something is actually true, or (2) to convince another mathematician that it's true (whether or not it's actually true)? Historically the two were conflated, but that is no longer the case. Now we must ask if #1 or #2 is the real goal of a proof, because we now can choose between those alternatives. In short, I disagree with you. I believe that the purpose of a proof is to show that something is actually true (#1). Whether or not you can convince a human - any human - is historically how we determined #1, but increasingly this alternative (#2) is no longer an adequate measure of anything. Mathematicians are humans. They can be fooled, fail to see errors due to fatigue, or simply be overwhelmed because they have limited time. When humans were the only way to verify proofs, we had to live with those limitations - because there were no alternatives. But computers today can verify proofs. They can do it far more accurately than humans, they don't get tired, and they can do it 24x7. Computers aren't as good (today) at creating proofs, but they don't need to create proofs to verify proofs. We can take a number of actions that make computer-verified proofs far far more reliable than proofs merely checked by humans. As I stated earlier, it's odd that we make humans do the verification job, because a computer is much better at doing it. The question now is: should we continue to accept proofs that are only human-verified? Why? Why is it acceptable if "other mathematicians" can be convinced, if the proofs are invalid? Do we really believe mathematicians can't make mistakes? It's certainly useful to show "summary proofs" so that humans can see the big picture. But once you have the details, they can be summarized. If only "summaries of proofs" are available that aren't computer-verified, that means that errors may lurk that would have been countered by a formal proof. Large proofs are easily shared via the Internet, so size is no longer a serious concern. I don't disparage mathematicians for doing more "human oriented math". Indeed, we should honor the work of past math giants, who had no alternatives available. But we need to move beyond "human oriented math" because it is not trustworthy enough and we have a better alternative available. I'm not saying we can instantly do that today, by the way. There are tools that make it possible, but it's hard. It will take persistent work over many years to transition to a world where proofs are routinely computer-verified. There will need to be decisions on what to prioritize on formalization. Different approaches will need to tried, and I doubt there will be a single approach everyone uses. People with different skills will need to work together. Libraries and tools will need creation and refinement. But the first step in that journey is to have a general agreement that it's a journey worth taking. Do mathematicians and those who fund them care about truth, or do they care about merely convincing other mathematicians? We must now choose between those two options. I choose truth.

by smadge 8y ago

dwheeler 8y ago

> Why do you insist mathematicians become programmers? No one is insisting that. We're insisting that proofs actually be correct, something that demonstrably cannot be done (to an adequate level) when we depend only on humans. Humans get tired and make mistakes such as failing to notice missing or invalid steps. Humans are still really good at coming up with proofs - but not so good at verifying them. > Proofs are just a medium to convey mathematical ideas to other mathematicians. I disagree. For example, claiming that a^n + b^n = c^n for any integer value of n greater than 2 when all values are integer is clearly a mathematical idea. But that idea is not a proof of Fermat's Last Theorem; it is simply an idea. A proof should establish, beyond doubt, that a claim is actually true. > I bet if Erdos were required to publish his ideas in a theorem prover language his mathematical output would have at least halved. I'm not sure about that, Erdos was pretty smart. There's relatively little investment in theorem prover languages; a little investment would go a long way. For example, today you have to prove lots of little things that really should be in libraries and tools, but the lack of investment holds things back. This also assumes that "mathematical output" is acceptable if it is not computer-verified. At some point in the future I think a "proof" that is not computer-verified will be viewed as an unproven claim. Humans simply aren't very good at verifying proofs - and computers are extremely good at it.

smadge 8y ago
Well, I guess what I meant is that proofs are for convincing other mathematicians. If someone is unconvinced by the proof they’ll try to fill in the gaps or further specify certain parts of the proof themselves. If that doesn’t work, they might ask for clarification. Eventually a consensus on the validity of the proof will be reached. I agree if the proof were presented in a machine verifiable format to begin with we wouldn’t need this process. I think though, that the reason it isn’t done this way is partly because the effort required isn’t worth it yet. My professor would actually get annoyed if I am too specific in my proofs because it overall makes the proof more difficult for a human to understand, which as I said is ultimately the purpose of a proof. Additionally the proof itself sometimes conveys an interesting idea that isn’t captured in the theorem. Some theorems have many different proofs that use different methods to prove the same theorem. These different proofs provide different perspectives that lead to a better understanding of the topic. I have a background in both computer science and pure math and am very interested in highly formal methods, I just don’t think we should disparage mathemicians for doing more human oriented math.
- dwheeler 8y ago
  > Some theorems have many different proofs that use different methods to prove the same theorem. These different proofs provide different perspectives that lead to a better understanding of the topic. Agreed, but there's no conflict. You can create multiple formal proofs, each of which provide different perspective that can lead to a better understanding. > Well, I guess what I meant is that proofs are for convincing other mathematicians. Not everyone agrees with this claim, and this disagreement is the essence of the "crisis". Is the purpose of a proof (1) to show that something is actually true, or (2) to convince another mathematician that it's true (whether or not it's actually true)? Historically the two were conflated, but that is no longer the case. Now we must ask if #1 or #2 is the real goal of a proof, because we now can choose between those alternatives. In short, I disagree with you. I believe that the purpose of a proof is to show that something is actually true (#1). Whether or not you can convince a human - any human - is historically how we determined #1, but increasingly this alternative (#2) is no longer an adequate measure of anything. Mathematicians are humans. They can be fooled, fail to see errors due to fatigue, or simply be overwhelmed because they have limited time. When humans were the only way to verify proofs, we had to live with those limitations - because there were no alternatives. But computers today can verify proofs. They can do it far more accurately than humans, they don't get tired, and they can do it 24x7. Computers aren't as good (today) at creating proofs, but they don't need to create proofs to verify proofs. We can take a number of actions that make computer-verified proofs far far more reliable than proofs merely checked by humans. As I stated earlier, it's odd that we make humans do the verification job, because a computer is much better at doing it. The question now is: should we continue to accept proofs that are only human-verified? Why? Why is it acceptable if "other mathematicians" can be convinced, if the proofs are invalid? Do we really believe mathematicians can't make mistakes? It's certainly useful to show "summary proofs" so that humans can see the big picture. But once you have the details, they can be summarized. If only "summaries of proofs" are available that aren't computer-verified, that means that errors may lurk that would have been countered by a formal proof. Large proofs are easily shared via the Internet, so size is no longer a serious concern. I don't disparage mathematicians for doing more "human oriented math". Indeed, we should honor the work of past math giants, who had no alternatives available. But we need to move beyond "human oriented math" because it is not trustworthy enough and we have a better alternative available. I'm not saying we can instantly do that today, by the way. There are tools that make it possible, but it's hard. It will take persistent work over many years to transition to a world where proofs are routinely computer-verified. There will need to be decisions on what to prioritize on formalization. Different approaches will need to tried, and I doubt there will be a single approach everyone uses. People with different skills will need to work together. Libraries and tools will need creation and refinement. But the first step in that journey is to have a general agreement that it's a journey worth taking. Do mathematicians and those who fund them care about truth, or do they care about merely convincing other mathematicians? We must now choose between those two options. I choose truth.