5 ms·

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

54 points by ur-whale 6y ago

ur-whale 6y ago
An amazing theorem because - reportedly - no single human holds its overall proof in his head.
- QuesnayJr 6y ago
  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"
  - newprint 6y ago
    I see his point, but explaining this proof to people outside of this group becomes a challenge and rightfully so.
    - JadeNB 6y ago
      > I see his point, but explaining this proof to people outside of this group becomes a challenge and rightfully so. That's probably true for any interesting proof, maybe all the more so for less famous proofs than this one where it's not clear the effort invested to understand it will be worth it!
- JadeNB 6y ago
  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. :-)
newprint 6y ago
Friend of mine is older Russian mathematician - algebraist, in his late 70's. He has small picture of John G. Thompson on his work table. Thompson made an enormous contribution to the proof. From what I remember reading, part of the proof was formally verified. It is intersecting to think, that we have proofs that are impossible to grasp in a lifetime. Though, it would be possible to use the results ! Imagine, sometime in a future, humanity would loose the original proof due to some catastrophic event, but it would be know that theorem still holds true.
- raincom 6y ago
  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. “
Koshkin 6y ago
The author's picture at the bottom does not look like a good advertisement for benefits of mathematical learning.
- _Microft 6y ago
  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.
infruset 6y ago
Here is a Coq mechanized proof of the Odd order theorem, a (huge) step towards the classification: https://github.com/math-comp/odd-order https://github.com/math-comp/odd-order The paper is here: https://hal.archives-ouvertes.fr/hal-00816699/ https://hal.archives-ouvertes.fr/hal-00816699/
dwheeler 6y ago
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/ 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 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 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.
- 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

54 points by ur-whale 6y ago

ur-whale 6y ago

An amazing theorem because - reportedly - no single human holds its overall proof in his head.

QuesnayJr 6y ago
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"
- newprint 6y ago
  I see his point, but explaining this proof to people outside of this group becomes a challenge and rightfully so.
  - JadeNB 6y ago
    > I see his point, but explaining this proof to people outside of this group becomes a challenge and rightfully so. That's probably true for any interesting proof, maybe all the more so for less famous proofs than this one where it's not clear the effort invested to understand it will be worth it!
JadeNB 6y ago
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. :-)

newprint 6y ago

Friend of mine is older Russian mathematician - algebraist, in his late 70's. He has small picture of John G. Thompson on his work table. Thompson made an enormous contribution to the proof. From what I remember reading, part of the proof was formally verified. It is intersecting to think, that we have proofs that are impossible to grasp in a lifetime. Though, it would be possible to use the results ! Imagine, sometime in a future, humanity would loose the original proof due to some catastrophic event, but it would be know that theorem still holds true.

raincom 6y ago
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. “

Koshkin 6y ago

The author's picture at the bottom does not look like a good advertisement for benefits of mathematical learning.

_Microft 6y ago
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.

infruset 6y ago

Here is a Coq mechanized proof of the Odd order theorem, a (huge) step towards the classification: https://github.com/math-comp/odd-order https://github.com/math-comp/odd-order The paper is here: https://hal.archives-ouvertes.fr/hal-00816699/ https://hal.archives-ouvertes.fr/hal-00816699/

dwheeler 6y ago

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

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