3 ms·

Conway is listed as being negative about using computer verified proofs, but he is well known for trashing set theory (or at least strongly protesting the shack

Conway is listed as being negative about using computer verified proofs, but he is well known for trashing set theory (or at least strongly protesting the shackles of set theory). So I wonder what he thinks of this new univalent foundation.

auggierose 11y ago
I found a mistake in one of his proofs in his book "On Numbers and Games" using computer verified proofs. It was only a mistake in the proof, that is, the proof was easy to correct and the result was still true, but it shows that noone is above mistakes. So using a computer can certainly drastically reduce the probability of an error.
- bumbledraven 11y ago
  Good job. What proof, may I ask? What was the mistake, and what tool did you use? Is there a paper on this I can read?
  - auggierose 11y ago
    I was using Isabelle. There is indeed a paper about this: http://link.springer.com/chapter/10.1007%2F11921240_19 http://link.springer.com/chapter/10.1007%2F11921240_19, and the flaw is described on page 284.
otoburb 11y ago
>>So I wonder what he thinks of this new univalent foundation. The Homotopy Type Theory (HoTT) book[1] puts forth a possible interpretation of Conway's thoughts about univalent foundations in section 11.6 (look at the bottom of the page for the following very selective and paraphrased quote): "[...] Conway's point was not to complain about ZF in particular, but to argue against all foundational theories at once [...] One might respond that, in fact, univalent foundations is not one of the "standard foundational theories" which Conway had in mind, but rather the metatheory in which we may express our ability to create new theories, and about which we may prove Conway's metatheorem."[2] [1] http://homotopytypetheory.org/book/ http://homotopytypetheory.org/book/ [2] http://www.math.ntnu.no/~stacey/documents/HoTT-online/main126.xhtml http://www.math.ntnu.no/~stacey/documents/HoTT-online/main12... EDIT: I forgot to mention that Voevodsky's definition of "Univalent Foundations" seems to be used interchangeably with the term "Homotopy Type Theory", but in Voevodsky's mind there is a sharp distinction[3]. Voevodsky tried to make this clear in an HoTT Google Groups email thread with the following statement: "HoTT is the study of the type-theoretic approach to the meta-theory of the Univalent Foundations."[4] [3] http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalent_foundations http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalent_... [4] https://groups.google.com/forum/#!topic/homotopytypetheory/zEixM1M3ZDQ%5B1-25%5D https://groups.google.com/forum/#!topic/homotopytypetheory/z...
harryjo 11y ago
Conway's opposition was to computer-generated proofs (not computer-verified proofs), because the software of the time wasn't high quality (for accuracy), and because they were so complicated that people couldn't get confidence that they were debugged. Basically, humans can't comprehend what the computers are doing, even when they are right, and we aren't always building them well enough to be trustworthy without checking their work. However, Zeilberger and Shalosh B Ekhad have done some highly reputable work, albeit in a narrow area. (Zeilberger designs algorithms in combinatorics, which then computer-generate proofs for specific questions) http://www.nytimes.com/learning/teachers/featured_articles/20040406tuesday.html http://www.nytimes.com/learning/teachers/featured_articles/2...

auggierose 11y ago

I found a mistake in one of his proofs in his book "On Numbers and Games" using computer verified proofs. It was only a mistake in the proof, that is, the proof was easy to correct and the result was still true, but it shows that noone is above mistakes. So using a computer can certainly drastically reduce the probability of an error.

bumbledraven 11y ago
Good job. What proof, may I ask? What was the mistake, and what tool did you use? Is there a paper on this I can read?
- auggierose 11y ago
  I was using Isabelle. There is indeed a paper about this: http://link.springer.com/chapter/10.1007%2F11921240_19 http://link.springer.com/chapter/10.1007%2F11921240_19, and the flaw is described on page 284.

otoburb 11y ago

>>So I wonder what he thinks of this new univalent foundation. The Homotopy Type Theory (HoTT) book[1] puts forth a possible interpretation of Conway's thoughts about univalent foundations in section 11.6 (look at the bottom of the page for the following very selective and paraphrased quote): "[...] Conway's point was not to complain about ZF in particular, but to argue against all foundational theories at once [...] One might respond that, in fact, univalent foundations is not one of the "standard foundational theories" which Conway had in mind, but rather the metatheory in which we may express our ability to create new theories, and about which we may prove Conway's metatheorem."[2] [1] http://homotopytypetheory.org/book/ http://homotopytypetheory.org/book/ [2] http://www.math.ntnu.no/~stacey/documents/HoTT-online/main126.xhtml http://www.math.ntnu.no/~stacey/documents/HoTT-online/main12... EDIT: I forgot to mention that Voevodsky's definition of "Univalent Foundations" seems to be used interchangeably with the term "Homotopy Type Theory", but in Voevodsky's mind there is a sharp distinction[3]. Voevodsky tried to make this clear in an HoTT Google Groups email thread with the following statement: "HoTT is the study of the type-theoretic approach to the meta-theory of the Univalent Foundations."[4] [3] http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalent_foundations http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalent_... [4] https://groups.google.com/forum/#!topic/homotopytypetheory/zEixM1M3ZDQ%5B1-25%5D https://groups.google.com/forum/#!topic/homotopytypetheory/z...

harryjo 11y ago

Conway's opposition was to computer-generated proofs (not computer-verified proofs), because the software of the time wasn't high quality (for accuracy), and because they were so complicated that people couldn't get confidence that they were debugged. Basically, humans can't comprehend what the computers are doing, even when they are right, and we aren't always building them well enough to be trustworthy without checking their work. However, Zeilberger and Shalosh B Ekhad have done some highly reputable work, albeit in a narrow area. (Zeilberger designs algorithms in combinatorics, which then computer-generate proofs for specific questions) http://www.nytimes.com/learning/teachers/featured_articles/20040406tuesday.html http://www.nytimes.com/learning/teachers/featured_articles/2...