5 ms·

I think articles like this are hilarious because they act like written down proofs are a gold standard of unassailable logic. Of course they aren't - what const

I think articles like this are hilarious because they act like written down proofs are a gold standard of unassailable logic. Of course they aren't - what constitutes proof to one person (or in one age) may or may not constitute proof to others. Look at Mochizuki's work - someone so convinced they are right, and yet no one else can understand it: https://www.nature.com/news/the-biggest-mystery-in-mathematics-shinichi-mochizuki-and-the-impenetrable-proof-1.18509 https://www.nature.com/news/the-biggest-mystery-in-mathemati... Another good example: Euler's proofs in his day would be failed in even a basic real analysis class now. Having known many many pure mathematicians, I believe that they don't want to use computers for the simple reason that many of them don't know how to, and thus denying the legitimacy of computer-generated (or assisted) proofs protects their livelihood/careers.

tacomonstrous 8y ago
>denying the legitimacy of computer-generated proofs protects their livelihood/careers. While this might be an issue, the bigger problem is that there are no interesting new theorems that were obtained in this way yet. What is true is that there is still serious prejudice against theorems verified by reducing to a finite (yet large) number of concrete cases, which are then verified by an algorithm. This is the case even after the whole brouhaha over and resolution of the 4 colors theorem by Hales.
- dannykwells 8y ago
  Good catch on the generated vs. assisted - I edited my comment.
- auggierose 8y ago
  Hales didn't resolve the 4 colors theorem, Gonthier did that. Hales proved the Kepler Conjecture and afterwards facilitated its formal verification via the Flyspeck project.
  - wolfgke 8y ago
    > Hales didn't resolve the 4 colors theorem, Gonthier did that. Gonthier didn't resolve the 4 colors theorem, Appel and Haken did that. Gonthier just created the first computer-checked proof for the Four-color theorem.
  - tacomonstrous 8y ago
    Yes, thank you. Mixed up machine assisted proofs.
- dwheeler 8y ago
  >> denying the legitimacy of computer-generated proofs protects their livelihood/careers. > While this might be an issue, the bigger problem is that there are no interesting new theorems that were obtained in this way yet. I think the issue is that there is a need for computer verified proofs, not necessarily computer generated proofs. It's much easier to create a proof verifier than a proof generator, and verifiers can give us much greater confidence that the proofs are correct (regardless of whether a human or computer generated them).
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.
AlexCoventry 8y ago
Most mathematicians would love for a machine to check their proofs. The problem, as Buzzard says, is that is much too expensive. Another way to put is, at the moment the math you can do with machine-checkable proofs is a bit boring, compared to math on the cutting edge outside formal methods.
throwawaymath 8y ago
> Look at Mochizuki's work - someone so convinced they are right, and yet no one else can understand it: I don't think this is a good characterization of Mochizuki or his Inter-universal Teichmuller theory. The vast majority of new results in both pure and applied mathematics are accepted by the mathematics community without incident - this applies to extremely sophisticated and groundbreaking work as well. For example, if you look at the work of almost any Fields medalist in the last century, you'll see that it was contemporaneously well-received. What you're citing is one example of 1) an extremely complicated proof, 2) delivered to the mathematics community in a very unorthodox manner, 3) by an author who has demonstrated significant reluctance to refine their work to make it more comprehensible to others. This is very uncommon and doesn't actually support your point (not that your point doesn't have merit, but this just isn't really applicable). I feel your framing of Mochizuki's IUT could be interpreted as saying that he somehow developed a robust proof which is, for a variety of reasons, not accepted by the community at large. This is not the case - his proof is not robust! There is significant evidence that it doesn't actually work. Furthermore, if your attempt at a proof does not agree with the general consensus of the mathematics community, it makes more sense to conclude that your proof is likely in error than it does to use it as an example of how proofs are subjective, and different people could require different levels of rigor. That's almost never the case in real world peer review - you're more likely to have your math paper dinged for a subjective assessment of how interesting or useful it is than because the reviewer actually finds it to in error. I'm also going to have to strongly disagree with you in regards to Euler's proofs. Analysis as a discipline is far more mature than it was in Euler's time, but Euler still clearly proved the things we attribute to him. I'm not really sure what your expectation is here - we have more sophisticated means of articulating proofs, and likewise much more mathematical scaffolding to support new theories. But Euler's work is rigorous. > Having known many many pure mathematicians, I believe that they don't want to use computers for the simple reason that many of them don't know how to, and thus denying the legitimacy of computer-generated (or assisted) proofs protects their livelihood/careers. Trading anecdote for anecdote: I've never known a single mathematician who felt that computer-generated proofs posed a threat to their careers. I don't mean to call your experience into question, but frankly I'm a little shocked that this is your interpretation of their reluctance to use computers. In my experience mathematicians are loathe to use computers not because they feel threatened by them, but because they just don't need to and never learned to. That's a very different attitude! As for my own opinion: the legitimacy of computer-generated proofs and the work of professional mathematicians are independent of each other. It would be naive to think that computer-assisted proofs would actually threaten a mathematician's livelihood. From the discussions I've had with mathematicians both in person and online (such as on /r/math), I'm fairly sure most of them would consider this idea incoherent and not actually be concerned about it. In fact, most mathematicians I know (myself included) would be thrilled to have more computer-assisted proofs available.

tacomonstrous 8y ago

>denying the legitimacy of computer-generated proofs protects their livelihood/careers. While this might be an issue, the bigger problem is that there are no interesting new theorems that were obtained in this way yet. What is true is that there is still serious prejudice against theorems verified by reducing to a finite (yet large) number of concrete cases, which are then verified by an algorithm. This is the case even after the whole brouhaha over and resolution of the 4 colors theorem by Hales.

dannykwells 8y ago
Good catch on the generated vs. assisted - I edited my comment.
auggierose 8y ago
Hales didn't resolve the 4 colors theorem, Gonthier did that. Hales proved the Kepler Conjecture and afterwards facilitated its formal verification via the Flyspeck project.
- wolfgke 8y ago
  > Hales didn't resolve the 4 colors theorem, Gonthier did that. Gonthier didn't resolve the 4 colors theorem, Appel and Haken did that. Gonthier just created the first computer-checked proof for the Four-color theorem.
- tacomonstrous 8y ago
  Yes, thank you. Mixed up machine assisted proofs.
dwheeler 8y ago
>> denying the legitimacy of computer-generated proofs protects their livelihood/careers. > While this might be an issue, the bigger problem is that there are no interesting new theorems that were obtained in this way yet. I think the issue is that there is a need for computer verified proofs, not necessarily computer generated proofs. It's much easier to create a proof verifier than a proof generator, and verifiers can give us much greater confidence that the proofs are correct (regardless of whether a human or computer generated them).

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.

AlexCoventry 8y ago

Most mathematicians would love for a machine to check their proofs. The problem, as Buzzard says, is that is much too expensive. Another way to put is, at the moment the math you can do with machine-checkable proofs is a bit boring, compared to math on the cutting edge outside formal methods.

throwawaymath 8y ago

> Look at Mochizuki's work - someone so convinced they are right, and yet no one else can understand it: I don't think this is a good characterization of Mochizuki or his Inter-universal Teichmuller theory. The vast majority of new results in both pure and applied mathematics are accepted by the mathematics community without incident - this applies to extremely sophisticated and groundbreaking work as well. For example, if you look at the work of almost any Fields medalist in the last century, you'll see that it was contemporaneously well-received. What you're citing is one example of 1) an extremely complicated proof, 2) delivered to the mathematics community in a very unorthodox manner, 3) by an author who has demonstrated significant reluctance to refine their work to make it more comprehensible to others. This is very uncommon and doesn't actually support your point (not that your point doesn't have merit, but this just isn't really applicable). I feel your framing of Mochizuki's IUT could be interpreted as saying that he somehow developed a robust proof which is, for a variety of reasons, not accepted by the community at large. This is not the case - his proof is not robust! There is significant evidence that it doesn't actually work. Furthermore, if your attempt at a proof does not agree with the general consensus of the mathematics community, it makes more sense to conclude that your proof is likely in error than it does to use it as an example of how proofs are subjective, and different people could require different levels of rigor. That's almost never the case in real world peer review - you're more likely to have your math paper dinged for a subjective assessment of how interesting or useful it is than because the reviewer actually finds it to in error. I'm also going to have to strongly disagree with you in regards to Euler's proofs. Analysis as a discipline is far more mature than it was in Euler's time, but Euler still clearly proved the things we attribute to him. I'm not really sure what your expectation is here - we have more sophisticated means of articulating proofs, and likewise much more mathematical scaffolding to support new theories. But Euler's work is rigorous. > Having known many many pure mathematicians, I believe that they don't want to use computers for the simple reason that many of them don't know how to, and thus denying the legitimacy of computer-generated (or assisted) proofs protects their livelihood/careers. Trading anecdote for anecdote: I've never known a single mathematician who felt that computer-generated proofs posed a threat to their careers. I don't mean to call your experience into question, but frankly I'm a little shocked that this is your interpretation of their reluctance to use computers. In my experience mathematicians are loathe to use computers not because they feel threatened by them, but because they just don't need to and never learned to. That's a very different attitude! As for my own opinion: the legitimacy of computer-generated proofs and the work of professional mathematicians are independent of each other. It would be naive to think that computer-assisted proofs would actually threaten a mathematician's livelihood. From the discussions I've had with mathematicians both in person and online (such as on /r/math), I'm fairly sure most of them would consider this idea incoherent and not actually be concerned about it. In fact, most mathematicians I know (myself included) would be thrilled to have more computer-assisted proofs available.