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 it proven to be true?"
There are a number of computer-based tools that can verify proofs, including HOL Light, Isabelle, Coq, Mizar, ProofPower and Lean. We should be working towards the day where running a proof through that kind of tool is what's required for publication: http://www.cs.ru.nl/%7Efreek/100/
I do a lot with Metamath. The largest Metamath database, which uses classical logic & ZFC set theory, can be seen here: http://us.metamath.org/mpeuni/mmset.html Every one of its proofs routinely verified by 5 different programs written in 5 different programming languages by more than 5 different people. Humans still need to check the axioms and definitions (to ensure they are "what is meant"), check that the claims are what is desired, and in general humans need to create at least part of the proofs. But no one needs to "understand everything". Instead, you can see whatever you want to see, and be confident that every step is thoroughly verified.
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
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.
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.
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.
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.
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.
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.
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.
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 :-)
> 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.
>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.
You don't care about mathematics in the sense that the word describes what mathematicians do, then. You care about physics. There's a distinct difference. Mathematics predicts nothing; it simply illuminates what is already there.
No, that's not what I meant. I am a computer engineer not a structural one.
When I talk about building, I mean code, and making sure it does what it's supposed to.
Unless you count algorithms and their behavior to fall under the umbrella of physics, of course.
Mathematics most certainly does help predict what the behavior of my code will be. It's really not about illumination, it's about taking monster shortcuts in my code because a solidly proved theorem allows me to.
> the word describes what mathematicians do,
I think you just described what you think mathematicians do. I do know a number of pure mathematicians who think of their trade rather differently, namely they are trying to build useful math.
> it simply illuminates what is already there.
Now, we're strictly entering the domain of faith-based thinking. Are things already there only to be discovered, or do we invent them? Does the tree make a noise when it falls in the forest when no one is there to hear it fall? Pick your religion.
Current mathematics is an untrustworthy flashlight. A claimed proof can be later found false, toppling all built on it.
If we want illumination, we need better. The standard for proof acceptance should become formal verification. Mathematicians are simply no longer emough if your goal is certainty.
I agree that there are mathematicians with this viewpoint.
However, I argue that this viewpoint is obsolete and should no longer be acceptable. Sure, it's great if a proof can be clearly understood completely by human. But humans are frighteningly limited creatures. Humans struggle to understand some things, and make mistakes all the time. Euclid's Elements was one of the most popular books of all time, and no one noticed an omission of an axiom for over two thousand years. Mathematicians are smart people, but they are merely people. They make mistakes all the time. Even published papers have had many mistakes found in them.
If the goal is to make up stories and communicate them, then sure, there's no need for computer verification. But that sounds like a fiction writer. I don't think that describes mathematics adequately. Science and engineering all depend on mathematics, and for that to work well, mathematics has to be rigorously correct.
If the goal is for absolute certainty that certain claims are true given certain assumptions, then we need to move beyond the traditional manual methods of verification. Mathematics has gotten too complex for that to work anymore with a reasonable level of confidence. It will be challenging and take time, but so are many other important endeavors.
Is mathematics about truth, or about something else? In many ways this discussion is basically an argument about what is mathematics. You can see where I land on that question. I think truth should be the goal.
There are a number of computer-based tools that can verify proofs, including HOL Light, Isabelle, Coq, Mizar, ProofPower and Lean. We should be working towards the day where running a proof through that kind of tool is what's required for publication: http://www.cs.ru.nl/%7Efreek/100/
I do a lot with Metamath. The largest Metamath database, which uses classical logic & ZFC set theory, can be seen here: http://us.metamath.org/mpeuni/mmset.html Every one of its proofs routinely verified by 5 different programs written in 5 different programming languages by more than 5 different people. Humans still need to check the axioms and definitions (to ensure they are "what is meant"), check that the claims are what is desired, and in general humans need to create at least part of the proofs. But no one needs to "understand everything". Instead, you can see whatever you want to see, and be confident that every step is thoroughly verified.
A Metamath-specific video overview is here: https://www.youtube.com/watch?v=8WH4Rd4UKGE
THAT is where we need to go. We aren't ready for it yet, but part of the problem is that we need to agree that this the proper destination.