4 ms·

> Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail. Just as an example, Russell & Whitehead's Princi

by FabHK 8y ago

> Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail. Just as an example, Russell & Whitehead's Principia Mathematica famously requires some 400+ pages to prove that 1+1=2 (well, they prove some other stuff, too, I suppose.) See the image and caption here to get a flavour: https://en.wikipedia.org/wiki/Principia_Mathematica https://en.wikipedia.org/wiki/Principia_Mathematica

Smaug123 8y ago
It's not so much to prove that 1+1=2; rather to set up the definitions and background entirely from scratch. If you had to define the grammar and vocabulary of English before you wrote a sonnet, your sonnets too would be exceedingly long.
- dwheeler 8y ago
  Exactly right. Most of those background steps do things like establish the basics of complex numbers, and you can reuse them for anything else involving complex numbers. The actual proof in metamath that two plus two is equal to 4 is at http://us.metamath.org/mpeuni/2p2e4.html http://us.metamath.org/mpeuni/2p2e4.html It is only 10 steps long. Yes, it is longer than an informal proof (such as one printed in a math journal), but it is not hard to follow. In this case this proof is rigorously verified by four different independent computer verifiers all the way back to the axioms of logic and set theory. It is already possible to have proofs that are completely computer verified. Up to this point, mathematicians often do not use them because it is simpler not to. But in the long-term, I think we should change our expectations to start requiring proofs to be verified by computer if we really want to believe in them. Humans make mistakes, and reviewers often miss them. Computer verification, especially when there are multiple independent verifiers, provide much greater confidence that the claimed proof is actually correct. The number of so-called proofs that are actually not proofs is very large. If you are curious about metamath, I have a video on YouTube that you might find interesting: https://m.youtube.com/watch?v=8WH4Rd4UKGE# https://m.youtube.com/watch?v=8WH4Rd4UKGE#
Jach 8y ago
Someone already linked metamath, it also gives a flavor of just how long some proofs can be when you fully formalize them and start from ZFC axioms. From the trivia page at http://us.metamath.org/mpeuni/mmset.html#trivia http://us.metamath.org/mpeuni/mmset.html#trivia "The complete proof of [(2+0i) + (2+0i) = (4+0i)] involves 2,863 subtheorems including the 189 above. These have a total of 27,426 steps—this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms of ZFC set theory."
antidesitter 8y ago
Depends on your starting point. You can prove 1+1=2 quite easily from the Peano axioms: 1+1=1+S(0) [definition of 1] 1+S(0)=S(1+0) [definition of addition, a+S(b)=S(a+b)] 1+1=S(1+0) [transitivity of equality] S(1+0)=S(1) [definition of addition, a+0=a] 1+1=S(1) [transitivity of equality] S(1)=2 [definition of 2] 1+1=2 [transitivity of equality]
vbezhenar 8y ago
It's like telling that there are thousands of machine instructions to be able to write printf("%.2f", x). It means that we should use the power of abstraction.
- kiriakasis 8y ago
  That was exactly the point, if you abstract then you are handwaving details (unless you abstract inside a formal system that itself defines methods for abstraction and then you are back to square one)

by FabHK 8y ago

Smaug123 8y ago

It's not so much to prove that 1+1=2; rather to set up the definitions and background entirely from scratch. If you had to define the grammar and vocabulary of English before you wrote a sonnet, your sonnets too would be exceedingly long.

dwheeler 8y ago
Exactly right. Most of those background steps do things like establish the basics of complex numbers, and you can reuse them for anything else involving complex numbers. The actual proof in metamath that two plus two is equal to 4 is at http://us.metamath.org/mpeuni/2p2e4.html http://us.metamath.org/mpeuni/2p2e4.html It is only 10 steps long. Yes, it is longer than an informal proof (such as one printed in a math journal), but it is not hard to follow. In this case this proof is rigorously verified by four different independent computer verifiers all the way back to the axioms of logic and set theory. It is already possible to have proofs that are completely computer verified. Up to this point, mathematicians often do not use them because it is simpler not to. But in the long-term, I think we should change our expectations to start requiring proofs to be verified by computer if we really want to believe in them. Humans make mistakes, and reviewers often miss them. Computer verification, especially when there are multiple independent verifiers, provide much greater confidence that the claimed proof is actually correct. The number of so-called proofs that are actually not proofs is very large. If you are curious about metamath, I have a video on YouTube that you might find interesting: https://m.youtube.com/watch?v=8WH4Rd4UKGE# https://m.youtube.com/watch?v=8WH4Rd4UKGE#

Jach 8y ago

Someone already linked metamath, it also gives a flavor of just how long some proofs can be when you fully formalize them and start from ZFC axioms. From the trivia page at http://us.metamath.org/mpeuni/mmset.html#trivia http://us.metamath.org/mpeuni/mmset.html#trivia "The complete proof of [(2+0i) + (2+0i) = (4+0i)] involves 2,863 subtheorems including the 189 above. These have a total of 27,426 steps—this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms of ZFC set theory."

antidesitter 8y ago

Depends on your starting point. You can prove 1+1=2 quite easily from the Peano axioms: 1+1=1+S(0) [definition of 1] 1+S(0)=S(1+0) [definition of addition, a+S(b)=S(a+b)] 1+1=S(1+0) [transitivity of equality] S(1+0)=S(1) [definition of addition, a+0=a] 1+1=S(1) [transitivity of equality] S(1)=2 [definition of 2] 1+1=2 [transitivity of equality]

vbezhenar 8y ago

It's like telling that there are thousands of machine instructions to be able to write printf("%.2f", x). It means that we should use the power of abstraction.

kiriakasis 8y ago
That was exactly the point, if you abstract then you are handwaving details (unless you abstract inside a formal system that itself defines methods for abstraction and then you are back to square one)