8 ms·

> Mathematics is very strict science with axioms and following theorems. Mathematics textbooks would be intractably longer if they spelled out every step in ex

> Mathematics is very strict science with axioms and following theorems. Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail. And then the proofs wouldn't make sense to people because the core ideas would be obscured by the formality! A typical mathematics proof is intended to be read by a thinking human assumed to have some level of mathematical sophistication and knowledge. These assumptions make proofs far more implicit than proofs in a formal language, which essentially only assumes that the "reader", i.e. the computer, can push symbols around and compare them.

mrob 8y ago
Why can't textbooks use code-folding style display to hide unwanted detail? Paper books are basically obsolete except as a master copy for archival.
- wtallis 8y ago
  I participated in a discussion on /r/math about this a few months ago, and there was surprising resistance to ideas like this. Most of it fell into two categories. The first was people with a paper fetish who refuse to believe that there are now computer display technologies that provide adequate readability and resolution to be a full-time substitute for books. The second was people who can't imagine a usable way to typeset proofs that embed metadata about which lines are the key steps and which could be folded. This is probably influenced by the fact that LaTeX doesn't support this kind of semantic markup and it would be awkward to add.
  - yesenadam 8y ago
    people with a paper fetish who refuse to believe Maybe there was surprising resistance because you spoke like that?
    - wtallis 8y ago
      Nah. I'm only using language that harsh now because of how disappointingly irrational and weak the objections on reddit were. It's odd to see mathematicians resistant to quantifying what they believe to be inferior about computer displays, and improperly generalizing what seemed to be their experience with $500 laptops to also argue against high-quality eInk, OLED and IPS LCDs.
      - dogecoinbase 8y ago
        It's odd to see mathematicians resistant to quantifying what they believe to be inferior about computer displays They're mathematicians, not display interface experts. This is like demanding that someone explain to you why they don't like a particular kind of food -- people are allowed to dislike things without having a complete internal axiomatic system justifying it.
        wtallis 8y ago
        Dislike, sure. Personal preferences are acceptable. But claiming that it's impossible for a computer/tablet display to be as readable as paper and that all electronic displays cause more eyestrain is unreasonable. Especially when the person making that claim has already demonstrated that they are familiar with terms like resolution, contrast ratio and form factor, but they fail to even propose a hypothesis for what might still be inferior about the best computer display technologies.
        captain_perl 8y ago
        Mathematicians are happy to use computers for typesetting papers, but not for the initial creative phase: 1) computer displays require you to scroll, which interrupts your mental flow 2) paper and pencil or pen is free-form 3) in advanced mathematics, results are rarely calculated in numerical form, so the computer isn't helpful 4) notebooks are permanent. No backups needed. I imagine the same is true for most cartoon artists.
      - Retra 8y ago
        Trying to do learn math with a computer is frustration. The computer eats up your desk space, you have to constantly move it around as you work on different things, a mouse and keyboard eat up even more space. You have to have power, and you have to drop your pen every other time you need something. Maybe you don't see the problem because you aren't doing any math?
  - groby_b 8y ago
    Except... it's not a fetish. Paper books have many advantages. It is easily annotable. (none of the current ebook types are easy). It provides tactile feedback, which can be used for organization - folded corners give you two types of indices (top/bottom outer corner). The entire structure of the book as a stack of pages gives you immediate visual feedback where you are, and it's effectively random-addressable. ("Yeah, it's roughly a third in, check there"). Heck, you can color page edges to make it even easier, and that gives you three spatial indices on top of the two tactile ones. It's not as unwieldy as screens. It is flexible, which makes it nicer to handle. It doesn't need to be charged. It doesn't break when you drop it. (Not to mention you can kill a fly with a paper book, ebooks don't work) Yes, e-books have other advantages - but calling it a paper fetish basically means you're making an uninformed call, because you're not even aware of the advantages. The second, you could have easily addressed by proposing a markup if it were easy to do so. The fact that you haven't, and aren't even aware why people think it's hard, means you're again coming from an uninformed position. And you thought the resistance was surprising?
    - nateburke 8y ago
      Paper math books also do not serve up distracting ads.
      - derangedHorse 8y ago
        Math ebooks shouldn't either lol
    - wtallis 8y ago
      The reddit thread in question was surprisingly lacking in discussion of the usability aspects you're focusing on. I think most of those issues make for a much more productive conversation, because there's real room for improvement in those areas—paper and current computer/tablet technology each have their own usability pros and cons. I'm not at all uninformed about those usability challenges. I was just surprised and disappointed at how many people assumed that paper had an unbeatable advantage on the purely visual aspects of presenting information, as if computers were still limited to 100dpi with really poor black levels. > The second, you could have easily addressed by proposing a markup if it were easy to do so. The fact that you haven't, and aren't even aware why people think it's hard, means you're again coming from an uninformed position. I didn't propose any specific markup because the specific syntax isn't the problem. The problem is that the predominant markup language for mathematical documents is LaTeX, which is a bit too presentation-oriented rather than semantic/structure-oriented for it to be really easy to use it to produce documents that can be interactively folded (especially when the output file format is almost always PDF). Something that used eg. MathML and an HTML/XML based overall document structure can trivially encode all the information necessary for rich interactive reading, and proposing specific tag or class names to indicate what lines of a proof should be collapsed by default only invites bikeshedding. I think you're quite unjustified in accusing me of being so thoroughly uninformed.
- danharaj 8y ago
  Why can they? You can't assume fully explicit proofs are practical just because they're plausible. The justification of practicality will be highly nontrivial. If its impractical to write such a textbook then code folding gets you nothing.
  - mrob 8y ago
    If it is impractical now, that simply means the software needs improvement. If mathematicians stop being so accepting of informal proofs then there is a very strong incentive to improve the software.
    - danharaj 8y ago
      > that simply means The point is that it's not simple. It will require significant advances in computer science.
- rocqua 8y ago
  In all of my papers, I have attempted to include an indent-based hierarchy of the argument. Adding code-folding to this would allow for so much more detail here. I don't think we should have papers being nothing but folds, but there is definite value in presenting proofs in this way. One potential downside is that there is no longer an order that guides the reader through the paper. Because it isn't quite clear how deep the author expected you to unfold an argument.
  - stallmanite 8y ago
    Maybe a default path through the document could be specified by the author or by convention
  - mannykannot 8y ago
    I think the idea is that you go deeper only if you are stuck or unsure about something at your current level.
- S4M 8y ago
  Is code-folding necessary? Instead you could put the demonstration in an appendix, and the authors would be free to decide what goes in the core of the article and what goes into the appendix. This could be made automatically where trunks of article would move back and forth from the core to the article and vice-versa, depending of what the reader chose to, and in each case a corresponding pdf could be generated.
zbobet2012 8y ago
This is a common objection from mathematicians, that is very understandable. I think both Lamport and Voevodsky’s have made important contributions here [1]. Namely in presenting idea from software that we use to manage _exactly_ your complaint. The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The question is then to develop languages which encompass these modern methods. This is really the goal of the homotopy type theory project, to provide a language which is both machine checkable and easy to use informal reasoning with. [1]https://www.microsoft.com/en-us/research/publication/write-21st-century-proof/?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fum%2Fpeople%2Flamport%2Fpubs%2Fproof.pdf https://www.microsoft.com/en-us/research/publication/write-2... https://www.youtube.com/watch?v=kOY-XE29_d8 https://www.youtube.com/watch?v=kOY-XE29_d8
- zbobet2012 8y ago
  It's also important to note that this situation is _precisely_ what Voevodsky wanted to prevent: For nearly a decade, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people. “The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes,” Voevodsky said. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error. [1] Most mathematicians still think of machine check for dealing with a large _number_ of cases; but Homotopy Type Theories goal is to manage abstract complexity not just size. [1]https://www.quantamagazine.org/univalent-foundations-redefines-mathematics-20150519/ https://www.quantamagazine.org/univalent-foundations-redefin...
- danharaj 8y ago
  I own a copy of the HoTT book :) > Namely the way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The problem is that the required structure for writing sophisticated mathematical proofs is much more demanding than even a piece of software as complex as the Linux kernel. Part of that is because software as such, when interpreted as proofs, don't verify properties nearly as strong as a real theorem. The difference between a proof of `Integer -> Integer` and `Integer -> Odd Integer` is already a gulf the vast majority of software does not bridge. We're just not there yet. Voevodsky's program is a great first step but just that: A first step. No one really knows what the next thousand steps will be. It's not straightforward at all.
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."
derangedHorse 8y ago
You could say the same thing about code, yet we're able to build upon our abstractions to make something both high level and able to be broken down to the foundations.
ur-whale 8y ago
There is a big difference between explaining / teaching a proof and verifying its correctness. We're talking about the latter here.
czei002 8y ago
Can't you make the formal proof software "smart" enough to prove a theorem given sufficient intermediate steps and hints about what other theorems/defs to use? i.e. basically what a book does? This would makes writing formal proof much easier, wouldn't it?

mrob 8y ago

Why can't textbooks use code-folding style display to hide unwanted detail? Paper books are basically obsolete except as a master copy for archival.

wtallis 8y ago
I participated in a discussion on /r/math about this a few months ago, and there was surprising resistance to ideas like this. Most of it fell into two categories. The first was people with a paper fetish who refuse to believe that there are now computer display technologies that provide adequate readability and resolution to be a full-time substitute for books. The second was people who can't imagine a usable way to typeset proofs that embed metadata about which lines are the key steps and which could be folded. This is probably influenced by the fact that LaTeX doesn't support this kind of semantic markup and it would be awkward to add.
- yesenadam 8y ago
  people with a paper fetish who refuse to believe Maybe there was surprising resistance because you spoke like that?
  - wtallis 8y ago
    Nah. I'm only using language that harsh now because of how disappointingly irrational and weak the objections on reddit were. It's odd to see mathematicians resistant to quantifying what they believe to be inferior about computer displays, and improperly generalizing what seemed to be their experience with $500 laptops to also argue against high-quality eInk, OLED and IPS LCDs.
    - dogecoinbase 8y ago
      It's odd to see mathematicians resistant to quantifying what they believe to be inferior about computer displays They're mathematicians, not display interface experts. This is like demanding that someone explain to you why they don't like a particular kind of food -- people are allowed to dislike things without having a complete internal axiomatic system justifying it.
      - wtallis 8y ago
        Dislike, sure. Personal preferences are acceptable. But claiming that it's impossible for a computer/tablet display to be as readable as paper and that all electronic displays cause more eyestrain is unreasonable. Especially when the person making that claim has already demonstrated that they are familiar with terms like resolution, contrast ratio and form factor, but they fail to even propose a hypothesis for what might still be inferior about the best computer display technologies.
        captain_perl 8y ago
        Mathematicians are happy to use computers for typesetting papers, but not for the initial creative phase: 1) computer displays require you to scroll, which interrupts your mental flow 2) paper and pencil or pen is free-form 3) in advanced mathematics, results are rarely calculated in numerical form, so the computer isn't helpful 4) notebooks are permanent. No backups needed. I imagine the same is true for most cartoon artists.
    - Retra 8y ago
      Trying to do learn math with a computer is frustration. The computer eats up your desk space, you have to constantly move it around as you work on different things, a mouse and keyboard eat up even more space. You have to have power, and you have to drop your pen every other time you need something. Maybe you don't see the problem because you aren't doing any math?
- groby_b 8y ago
  Except... it's not a fetish. Paper books have many advantages. It is easily annotable. (none of the current ebook types are easy). It provides tactile feedback, which can be used for organization - folded corners give you two types of indices (top/bottom outer corner). The entire structure of the book as a stack of pages gives you immediate visual feedback where you are, and it's effectively random-addressable. ("Yeah, it's roughly a third in, check there"). Heck, you can color page edges to make it even easier, and that gives you three spatial indices on top of the two tactile ones. It's not as unwieldy as screens. It is flexible, which makes it nicer to handle. It doesn't need to be charged. It doesn't break when you drop it. (Not to mention you can kill a fly with a paper book, ebooks don't work) Yes, e-books have other advantages - but calling it a paper fetish basically means you're making an uninformed call, because you're not even aware of the advantages. The second, you could have easily addressed by proposing a markup if it were easy to do so. The fact that you haven't, and aren't even aware why people think it's hard, means you're again coming from an uninformed position. And you thought the resistance was surprising?
  - nateburke 8y ago
    Paper math books also do not serve up distracting ads.
    - derangedHorse 8y ago
      Math ebooks shouldn't either lol
  - wtallis 8y ago
    The reddit thread in question was surprisingly lacking in discussion of the usability aspects you're focusing on. I think most of those issues make for a much more productive conversation, because there's real room for improvement in those areas—paper and current computer/tablet technology each have their own usability pros and cons. I'm not at all uninformed about those usability challenges. I was just surprised and disappointed at how many people assumed that paper had an unbeatable advantage on the purely visual aspects of presenting information, as if computers were still limited to 100dpi with really poor black levels. > The second, you could have easily addressed by proposing a markup if it were easy to do so. The fact that you haven't, and aren't even aware why people think it's hard, means you're again coming from an uninformed position. I didn't propose any specific markup because the specific syntax isn't the problem. The problem is that the predominant markup language for mathematical documents is LaTeX, which is a bit too presentation-oriented rather than semantic/structure-oriented for it to be really easy to use it to produce documents that can be interactively folded (especially when the output file format is almost always PDF). Something that used eg. MathML and an HTML/XML based overall document structure can trivially encode all the information necessary for rich interactive reading, and proposing specific tag or class names to indicate what lines of a proof should be collapsed by default only invites bikeshedding. I think you're quite unjustified in accusing me of being so thoroughly uninformed.
danharaj 8y ago
Why can they? You can't assume fully explicit proofs are practical just because they're plausible. The justification of practicality will be highly nontrivial. If its impractical to write such a textbook then code folding gets you nothing.
- mrob 8y ago
  If it is impractical now, that simply means the software needs improvement. If mathematicians stop being so accepting of informal proofs then there is a very strong incentive to improve the software.
  - danharaj 8y ago
    > that simply means The point is that it's not simple. It will require significant advances in computer science.
rocqua 8y ago
In all of my papers, I have attempted to include an indent-based hierarchy of the argument. Adding code-folding to this would allow for so much more detail here. I don't think we should have papers being nothing but folds, but there is definite value in presenting proofs in this way. One potential downside is that there is no longer an order that guides the reader through the paper. Because it isn't quite clear how deep the author expected you to unfold an argument.
- stallmanite 8y ago
  Maybe a default path through the document could be specified by the author or by convention
- mannykannot 8y ago
  I think the idea is that you go deeper only if you are stuck or unsure about something at your current level.
S4M 8y ago
Is code-folding necessary? Instead you could put the demonstration in an appendix, and the authors would be free to decide what goes in the core of the article and what goes into the appendix. This could be made automatically where trunks of article would move back and forth from the core to the article and vice-versa, depending of what the reader chose to, and in each case a corresponding pdf could be generated.

zbobet2012 8y ago

This is a common objection from mathematicians, that is very understandable. I think both Lamport and Voevodsky’s have made important contributions here [1]. Namely in presenting idea from software that we use to manage _exactly_ your complaint. The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The question is then to develop languages which encompass these modern methods. This is really the goal of the homotopy type theory project, to provide a language which is both machine checkable and easy to use informal reasoning with. [1]https://www.microsoft.com/en-us/research/publication/write-21st-century-proof/?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fum%2Fpeople%2Flamport%2Fpubs%2Fproof.pdf https://www.microsoft.com/en-us/research/publication/write-2... https://www.youtube.com/watch?v=kOY-XE29_d8 https://www.youtube.com/watch?v=kOY-XE29_d8

zbobet2012 8y ago
It's also important to note that this situation is _precisely_ what Voevodsky wanted to prevent: For nearly a decade, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people. “The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes,” Voevodsky said. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error. [1] Most mathematicians still think of machine check for dealing with a large _number_ of cases; but Homotopy Type Theories goal is to manage abstract complexity not just size. [1]https://www.quantamagazine.org/univalent-foundations-redefines-mathematics-20150519/ https://www.quantamagazine.org/univalent-foundations-redefin...
danharaj 8y ago
I own a copy of the HoTT book :) > Namely the way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The problem is that the required structure for writing sophisticated mathematical proofs is much more demanding than even a piece of software as complex as the Linux kernel. Part of that is because software as such, when interpreted as proofs, don't verify properties nearly as strong as a real theorem. The difference between a proof of `Integer -> Integer` and `Integer -> Odd Integer` is already a gulf the vast majority of software does not bridge. We're just not there yet. Voevodsky's program is a great first step but just that: A first step. No one really knows what the next thousand steps will be. It's not straightforward at all.

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

derangedHorse 8y ago

You could say the same thing about code, yet we're able to build upon our abstractions to make something both high level and able to be broken down to the foundations.

ur-whale 8y ago

There is a big difference between explaining / teaching a proof and verifying its correctness. We're talking about the latter here.

czei002 8y ago

Can't you make the formal proof software "smart" enough to prove a theorem given sufficient intermediate steps and hints about what other theorems/defs to use? i.e. basically what a book does? This would makes writing formal proof much easier, wouldn't it?