3 ms·

real currency on anonymous message boards is the quality and content of your ... I suggest to generalise this great insight: anonymity, and the require

real currency on anonymous message boards is the quality and content of your ... I suggest to generalise this great insight: anonymity, and the requirement that one's arguments must be valid independent from any reputation associated with the speaker, is the core essence of the scientific method. The edge case is mathematical proof: nobody would accept a mathematical theorem because it was from <famous person>. Instead it must be accompanied by a proof, a proof so detailed that everyone can verify it. Over 2000 years ago, Plato (in his Meno) use the slave boy as an example for "everyone", while today, we are even more stringent: even a machine (e.g. Isabelle/HOL, Agda, Coq, Lean), the prototypical mechanised slave, must understand a proof. Scholarly tools like anonymous peer review, double blind reviews, double blind experiemnts, anonymous grading etc all work precisely because of anonymity. A key mechanisim behind the positive qualities of anonymity is that the anonymous author no longer must fear punishment for the anonmous speech. The key invention here was the invention of writing, which enabled the separation (in space and time) between author and audience. This was amplified by the invention of the printing press (which amphified the audience), and later the internet. I'm not a historian of writing, but I suggest the following hypothesis: contemporary arguments against online anonymity (e.g. leads to trolling etc) are structurally somewhat similar to (but not idential with ) historical arguments against writing and the printing press.

deleted 8y ago
[deleted]
whatshisface 8y ago
>today, we are even more stringent: even a machine (e.g. Isabelle/HOL, Agda, Coq, Lean), the prototypical mechanised slave, must understand a proof. This is not quite true yet. An absolutely minuscule fraction of math papers published today involve machine proofs.
- MrEldritch 8y ago
  And indeed, this will likely always be the case, as the true purpose of proving a mathematical result is almost never to actually get the boolean true/false output, but to illustrate how to solve the problem in the first place and what methods were helpful for that. Which means that the proof doesn't have to be machine-checkable; in fact, it'd be less effective at doing its job if it included every trivial step. It's not code. It's pseudocode; the purpose is to communicate to humans.
  - IngoBlechschmid 8y ago
    > And indeed, this will likely always be the case, as the true purpose of proving a mathematical result is almost never to actually get the boolean true/false output, but to illustrate how to solve the problem in the first place and what methods were helpful for that. As a working mathematician, I wholeheartedly agree with the second part of the quoted sentence! But I think that the first part isn't quite right: The function of proofs to determine truth is extremely important, especially considering that, especially in pure mathematics, we often can't check our results in any other manner (like conducting physical experiments or checking many cases with the computer). Bad experiences with proofs which later turned out to be faulty led Voevodsky to initiate his univalent foundations program (also called homotopy type theory), where all results should be checked by the computer. (For the particular area he was working on, no existing theorem prover turned out to be sufficient. He made a breakthrough in finding a new foundation to base theorem provers on, which made it possible to formalize results in his area of mathematics not only in principle, but also in practice.) The hope is also that with computer-checked proofs, we can advance to new areas of mathematics which are currently inprenetable to our puny human minds. I'm very much looking forward to this future! You can learn more about Voevodsky's vision in slides of him and in a recorded lecture: https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundatio... https://www.youtube.com/watch?v=O45LaFsaqMA https://www.youtube.com/watch?v=O45LaFsaqMA
    - yesenadam 8y ago
      What do you think of Lamport's 'structured proofs'? https://www.microsoft.com/en-us/research/uploads/prod/2016/12/How-to-Write-a-Proof.pdf https://www.microsoft.com/en-us/research/uploads/prod/2016/1...
      - IngoBlechschmid 8y ago
        I love them! Done well, they can be extremely pleasant to read and understand. A good friend of mine creates those as a hobby: https://pwacker.com/ https://pwacker.com/
nsajko 8y ago
XKCDs relevant to the end of your comment: * https://xkcd.com/1227 https://xkcd.com/1227 * https://xkcd.com/1601 https://xkcd.com/1601

deleted 8y ago

[deleted]

whatshisface 8y ago

>today, we are even more stringent: even a machine (e.g. Isabelle/HOL, Agda, Coq, Lean), the prototypical mechanised slave, must understand a proof. This is not quite true yet. An absolutely minuscule fraction of math papers published today involve machine proofs.

MrEldritch 8y ago
And indeed, this will likely always be the case, as the true purpose of proving a mathematical result is almost never to actually get the boolean true/false output, but to illustrate how to solve the problem in the first place and what methods were helpful for that. Which means that the proof doesn't have to be machine-checkable; in fact, it'd be less effective at doing its job if it included every trivial step. It's not code. It's pseudocode; the purpose is to communicate to humans.
- IngoBlechschmid 8y ago
  > And indeed, this will likely always be the case, as the true purpose of proving a mathematical result is almost never to actually get the boolean true/false output, but to illustrate how to solve the problem in the first place and what methods were helpful for that. As a working mathematician, I wholeheartedly agree with the second part of the quoted sentence! But I think that the first part isn't quite right: The function of proofs to determine truth is extremely important, especially considering that, especially in pure mathematics, we often can't check our results in any other manner (like conducting physical experiments or checking many cases with the computer). Bad experiences with proofs which later turned out to be faulty led Voevodsky to initiate his univalent foundations program (also called homotopy type theory), where all results should be checked by the computer. (For the particular area he was working on, no existing theorem prover turned out to be sufficient. He made a breakthrough in finding a new foundation to base theorem provers on, which made it possible to formalize results in his area of mathematics not only in principle, but also in practice.) The hope is also that with computer-checked proofs, we can advance to new areas of mathematics which are currently inprenetable to our puny human minds. I'm very much looking forward to this future! You can learn more about Voevodsky's vision in slides of him and in a recorded lecture: https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundatio... https://www.youtube.com/watch?v=O45LaFsaqMA https://www.youtube.com/watch?v=O45LaFsaqMA
  - yesenadam 8y ago
    What do you think of Lamport's 'structured proofs'? https://www.microsoft.com/en-us/research/uploads/prod/2016/12/How-to-Write-a-Proof.pdf https://www.microsoft.com/en-us/research/uploads/prod/2016/1...
    - IngoBlechschmid 8y ago
      I love them! Done well, they can be extremely pleasant to read and understand. A good friend of mine creates those as a hobby: https://pwacker.com/ https://pwacker.com/

nsajko 8y ago

XKCDs relevant to the end of your comment: * https://xkcd.com/1227 https://xkcd.com/1227 * https://xkcd.com/1601 https://xkcd.com/1601