An enormous theorem: the classification of finite simple groups (2006)

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

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.

So it'd be helpful.

> 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...

If humanity were to loose the original proof of some theorem X in 3000 AD, the only fact is known to them is that X is true, how on earth one should believe it? Just because that theorem X was proved in the West?

Just reverse the case, and replace the West with Africa or China. Everyone in the West would laugh at claims that "Some Chinese/African proved a theorem in 300 BC, but that proof doesn't exist anymore".

That's why Bill Thurston says this: “There is another effect caused by the big differences between how we think about mathematics and how we write it. A group of mathematicians interacting with each other can keep a collection of mathematical ideas alive for a period of years, even though the recorded version of their mathematical work differs from their actual thinking, having much greater emphasis on language, symbols, logic and formalism. But as new batches of mathematicians learn about the subject they tend to interpret what they read and hear more literally, so that the more easily recorded and communicated formalism and machinery tend to gradually take over from other modes of thinking.

There are two counters to this trend, so that mathematics does not become entirely mired down in formalism. First, younger generations of mathematicians are continually discovering and rediscovering insights on their own, thus reinjecting diverse modes of human thought into mathematics. “

That article has a comment from someone involved in the proof who disagrees:

"This article is very well written, but I must object to the implications of the statement that "no-one in the world today completely understands the whole proof." Of course, complete understanding is a high benchmark to set. But I would argue that Thompson, Aschbacher and Lyons understand the proof at least as well as Danny Gorenstein did, and Steve Smith and I (and probably several others) come pretty close. See our book which received the AMS Steele Prize for Mathematical Exposition. Danny Gorenstein deserves enormous credit for conceiving and daring to articulate the strategy of the proof back in 1971-72. But his overall perspective did not die with him.

Ron Solomon"

If that's the bar for amazing-ness, then purely computer-verified proofs, like those of the Four-Colour Theorem and Kepler's Conjecture, are even more amazing. :-)

You may be downvoted because it sounds like an ad hominem.

I agree that it is an unflattering choice and do not understand what makes people use images like this to represent themselves to the largest audience possible (i.e. anyone with internet access). There is no easier way to positively influence what others imagine than by not choosing an unflattering image. If someone really does not like any image of themselves, they can still leave it away and let people's imagination run free instead.