7 ms·

This is why we need to move away from depending on just humans to verify proofs. The goal shouldn't be "does a human fully understand the whole thing" but "is i

• cg505 6y ago
  It is interesting, though, that a portion of the article is dedicated to discussing how it's important to make the proof simpler and more generally available. Although machine-verifiability is surely a good goal, it can't replace humans being able to comprehend the proofs as well. In this world where proof can all be verified, we may be more confident in our mathematical knowledge, but we'll also be unable to generate new knowledge.
• raincom 6y ago
  Human understanding is critical. See what Bill Thurston said:"The rapid advance of computers has helped dramatize this point, because computers and people are very different. For instance, when Appel and Haken completed a proof of the 4-color map theorem using a massive automatic computation, it evoked much controversy. I interpret the controversy as having little to do with doubt people had as to the veracity of the theorem or the correctness of the proof. Rather, it reflected a continuing desire for human understanding of a proof, in addition to knowledge that the theorem is true." From Bill Thurston: “On Proof and Progress in Mathematics”, Bulletin of the American Mathematical Society, 30(2), 161-177 https://arxiv.org/pdf/math/9404236 https://arxiv.org/pdf/math/9404236
  • deleted 6y ago
    [deleted]
  • dwheeler 6y ago
    Some mathematicians think that human understanding of every step is critical. That doesn't actually make it critical. At one time it was very important to have humans weave cloth. Now we generally expect machines to do that. Computers will not eliminate the need for human mathematicians. It will merely change what they do. In many ways it will be more freeing, because no one will need to review a proof to see if its steps are correct. Mathematicians will still need to develop definitions and determine what is important to prove, and at least in the short-term they will need to do much of the proving since machines are not yet very good at that. Many other fields have changed with computers, there's no reason to believe mathematics cannot be changed.
    • raincom 6y ago
      Well, if you think knowledge is same as truth, computer verifications can do. Today, at least the consensus in philosophy of science is not centered on truth. It is true that a falsity can't be knowledge. There is more to knowledge than truth.
      • dwheeler 6y ago
        But that is the problem: we are claiming that we "know" things are absolutely true, but we are using methods that are known to be inadequate for that purpose. Mathematicians are smart, but they are human. They make mistakes and miss others'. Math has increasingly become too complex to entrust mere human verification as being adequately trustworthy. Human verification has already been repeatedly demonstrated as inadequate. We must choose between truth or easier-to-understand claims that are sometimes false because we depend on fragile human verification. I think we should choose truth. Where we can get human understandability as well as truth, great! But formal verification should become the minimum over time, because truth should be the minimum. We can't do that all at once right now. But knowing the goal is the first step.
• pmiller2 6y ago
  > The goal shouldn't be "does a human fully understand the whole thing" but "is it proven to be true?" > [...] > But no one needs to "understand everything". Coming from a pure math background, I have to respectfully disagree. There is a serious debate in the philosophy of mathematics about what, precisely, is a proof. My own, and many others' view is roughly this: > Proofs are stories that convince suitably qualified others that a certain statement is true. > If I present you with a proof, and you have the appropriate background knowledge and ability, you can – usually with some time and effort – as a result of reading my story, become convinced that what I claim is true. > But if you take that as your working definition of proof, you have to acknowledge it is fundamentally about communication, not truth. In particular, whether an argument classifies as a proof depends as much on the intended reader as on its creator. [0] Many mathematicians do not consider a theorem to be "proved" until they understand why it is true. The four color theorem is a prime example of this. By now, literally every graph theorist considers the statement to be logically correct, but there are quite a few who would say that the computer verifications that are out there don't quite constitute "proof" for them. The problem is that these computer-based verifications are simply not conceptually accessible to the majority of working graph theorists who might want to know how the proof works. I haven't personally looked at any of them, but, I, as both a working SWE and someone with several graduate courses in graph theory, including topological graph theory, cannot honestly can't say that they would be accessible to me. The "story," to reference the Keith Devlin quote above, is written in a language that mathematicians simply do not understand. There are other issues, but this is the most fundamental. For instance, mathematicians highly value proofs that themselves offer insight into why the theorem should be true. They value proofs that offer new techniques to solve other problems (i.e. abstraction). While one can get this from a computer proof, it is far, far more difficult to extract these things from code than it is from traditional proofs one would see in a journal. The bottom line is that no, that is not "where we need to go," because that is simply not how mathematics functions. --- [0]: https://www.mathvalues.org/masterblog/what-is-a-mathematical-proof https://www.mathvalues.org/masterblog/what-is-a-mathematical...
  • ur-whale 6y ago
    >Coming from a pure math background, I have to respectfully disagree. Coming from an engineering background, I have to respectfully disagree. What matters to me most with Math is its predictive power When a theorem is proven, it is something I can build on: it won't crumble, and any edifice resting on that foundation is guaranteed to be stable. Whether I am convinced at a gut level that the proposition is true is basically poetry and matters very little. If the four color theorem was proven by machines, it actually is better than if a bunch of humans feel good about the proof, the likelihood of it delivering predictable behavior is all that matters, and for this I trust the machine way more that a bunch of poets feeling good about themselves.
• wiz21c 6y ago
  I'm no mathematician but let's imagine you approach is followed. Computers do prove (or disprove) a lot of the open question (theorems we have no proof for). So far so good, the current math is "solved". But now, you have to make new math, discover/create new theorems. If you leave it to the computers, they'll generate millions of truth. But who will be able to understand and value those truths ? If you either leave it to humans, they'll first have to understand all the theorems proven above in order to be able to formulate new theorems. They'll have to deeply understand them, to abstract them to be able to use them as a foundation for new work. So my impression is that sooner or later, humans reenter the loop. However, if a computer proves that a new theorem is true, say with an impossible to understand proof then it means that's it's worth investing human time in that proof. So it'd be helpful.
  • bollu 6y ago
    In the above setting, we don't have computers _finding theorems_. We're using computers to _machine check_ our proofs; The process of verifying whether a proof is correct or not is mechanical when a proof is broken down to its smallest steps. The proof assistant simply assists us in making sure we haven't missed anything. If you are interested in humans and machines working together to find proofs, then boy do I have a story for you: http://math.iisc.ac.in/~gadgil/presentations/SummerCSIISc.html#/ http://math.iisc.ac.in/~gadgil/presentations/SummerCSIISc.ht...
    • wiz21c 6y ago
      Thx for pointing that presentation. I must admit the maths are way beyond what I can understand. But I get the general principle of the goals. That's quite inspiring, and a little crazy too :-) Thanks a lot, that was very interesting !
• ur-whale 6y ago
  Hear, hear, but the last time I suggested exactly this idea on HN (on a Mochizuki related article IIRC), my comment was downvoted into oblivion by folks who felt I was attacking the "purity" of their trade. To this day, I'm still trying to figure why math types seem to deeply hate the idea that a proper proof of a new theorem should be published in a formal, machine-verifiable language (e.g., Mochizuki's proof, which no one seem to understand, much less verify to be correct, could just be fed to a machine, end of story). I have some hypotheses: 1. Much like "traditional" artists, who saw the Photoshop-like tools as degrading to their art, they feel that using machines to help with proofs would somehow hinder, limit and dirty down their trade. 2. The existing tools are way too primitive to be any kind of useful. This, I can resonate with. I am not knowledgeable enough on current formal proof software, but last I looked at (~10 years ago), they made me feel like I was back to coding in assembly. If indeed the tools are still too primitive, then it's just a matter of making them better. And it seems to me like Math, if anything, really lends itself damn well to hierarchical building to reach better and better level of abstraction. 3. Many folks mix-up automated theorem proving (which is hard for machines, because it requires intuition leaps) and formal proof verification (which, unless I'm missing something, really lends itself well to mechanization). Anyhoo, I suspect that in spite of all the philosophical push-back, we will get there, if only because many modern proofs are so huge, they get to the point where they consume multiple mathematician-lifetimes worth of work. There's basically no other route.