8 ms·

Wikipedia-size maths proof too big for humans to check

39 points by graeham 13y ago

ColinWright 13y ago
https://hn.algolia.com/?q=proof#!/story/past_week/0/maths%20proof https://hn.algolia.com/?q=proof#!/story/past_week/0/maths%20...
- Dylan16807 13y ago
  Those submissions never got traction or comments, why link them?
  - ColinWright 13y ago
    Because sometimes older submissions end up getting some discussion, even when more recent submissions have more comments.
saurik 13y ago
http://www.reddit.com/r/math/comments/1y5v15/if_no_human_can_check_a_proof_of_a_theorem_does/ http://www.reddit.com/r/math/comments/1y5v15/if_no_human_can...
archgrove 13y ago
So, to me, proofs have two purposes. The first is to just say "This theorem is true". The second is to give some insight into the problem. I have no problem with such a proof satisfying purpose one; I may not be able to check it myself, but I can build a chain of trustworthiness all the way back to a program that I can check myself. In such a chain, the truth of the final result is not, to me, in dispute. Alas, such a proof throughly fails the second test. I can't see how to gain insight into the problem from such a proof, beyond just it validating previous thought chains of the form "If X were true, then I could deduce Y". It doesn't reveal more about the structure of the problem, or other results in the space. It's no doubt useful (and all credit to the authors), but in terms of generating new mathematics, I'm dubious. Perhaps people more versed in this specific sub-field can tell me if I'm wrong?
- dragontamer 13y ago
  It is a field of AI, not a field of Mathematics. Automated Theorem Proving is a very old field, one of the earliest fields of Artificial Intelligence. The first proof of this nature was the Four Color Theorem, proven by an automated reasoner as opposed to a mathematician. At which point, the insight into the matter is understanding the AI algorithm and how the AI searches for a solution. And finally... how we can be sure that the AI itself is provably correct. http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_com...
  - deleted 13y ago
    [deleted]
  - ColinWright 13y ago
    I would be interested to see why you claim that the FCT was proven by an automated reasoner. My understanding is that Haken and Appel created techniques to create unavoidable configurations, and techniques to prove that a given configuration is reducable. They then programmed a computer to find an unavoidable set of reducable configurations. In Haken and Appel's proof there was no automated reasoning. Similarly in this case. The theorem claims that for every C there is an N such that a sequence of length at least N has a sub-configuration of discrepancy at least C. In this case the researchers created a program to show that in a sequence of length at least 1161 there is always a sub-sequence of discrepancy of at least 2. To the best of my understanding there is no automated reasoning, so I would be interested to see why you claim otherwise.
    - dragontamer 13y ago
      All Automated Reasoning is... is programming a computer to search a space automatically. In First Order Logic, you use the Resolution Rule to generate the search space for example. But at the end of the day... Automated Reasoning is nothing more than a glorified graph traversal. The FCT was solved with a hybrid method. Yes, you mention that there was significant human input in reducing the problem. However, a computer program was used to find (and prove) a huge number of those configurations. Search and verification. That is all "automated reasoning" is. In AI circles the FCT is considered to have been solved by Automated Reasoning methods. http://en.wikipedia.org/wiki/Automated_theorem_proving#Related_problems http://en.wikipedia.org/wiki/Automated_theorem_proving#Relat...
adiM 13y ago
From the linked Wikipedia article: > All experiments were conducted on PCs equipped with an Intel Core i5-2500K CPU running at 3.30GHz and 16GB of RAM. Why are these experiments not being conducted on a more powerful computer or a cluster?
- IsTom 13y ago
  Because it only took 6 hours anyway.
- alephnil 13y ago
  As already mentioned, it only took six hours. To make it run on a cluster or supercomnputer, you must parallelize the algorithm, which will take considerably longer time, even if it is easy. Then they likely have to apply for access, which also take time. Then it is easier to just run it on an available computer.
- csense 13y ago
  For the same reason you don't see word processors using a more powerful computer or cluster to render text for display as pixels. - It would be awfully inconvenient to program - It would require buying, building or obtaining access to such a machine - It'd require investing some amount of time and/or money -- obviously completely unnecessarily -- because whatever desktop or laptop happened to be within reach is perfectly adequate to the task
twocows 13y ago
"Wikipedia-sized" Is it really? They say in the article that the text of Wikipedia is a 10GB download, but that has to be compressed (and compression on plaintext, which comprises most of Wikipedia, is extremely efficient). I'm guessing (but have no proof) that their 13GB file was raw data. A minor thing, but comparisons like this always drive me nuts. Just say "13GB proof too big for humans to check." Then there's no confusion.</sillyrant>
- deleted 13y ago
  [deleted]
- VLM 13y ago
  A lot of its name games. 10 gigs of possibilities tested is actually pretty short for something like OGR-27. We're probably going to prove OGR-27 in a few weeks (or has it already been announced?) and I'm fairly certain a list of all possible rulers checked would exceed 10 gigs. Yet you can report OGR-26 in only 26 small numbers, or I guess you could draw a graphic pix using 492 pixels or whatever. So is OGR-27 merely 27 numbers aka a 1-d pixel "graph" probably around five hundred something pixels, or is it really zillions of gigs of rulers all of which are longer than the OGR?
deleted 13y ago
[deleted]
snird 13y ago
"The set-theoretical axioms that sustain modern mathematics are self-evident in differing degrees. One of them – indeed, the most important of them, namely Cantor's axiom, the so-called axiom of infinity – has scarcely any claim to self-evidence at all". John P. Mayberry
judk 13y ago
"Wikipedia" is displacing "encyclopedia" and "Library of Congress" as a unit of measure!
- wlievens 13y ago
  Clearly there is a defent "yo mamma" joke in there.
- igravious 13y ago
  Uh, and football field. The output of this proof if laid end to end would fill 37 regular sized football fields.

39 points by graeham 13y ago

https://hn.algolia.com/?q=proof#!/story/past_week/0/maths%20proof https://hn.algolia.com/?q=proof#!/story/past_week/0/maths%20...

Dylan16807 13y ago
Those submissions never got traction or comments, why link them?
- ColinWright 13y ago
  Because sometimes older submissions end up getting some discussion, even when more recent submissions have more comments.

saurik 13y ago

http://www.reddit.com/r/math/comments/1y5v15/if_no_human_can_check_a_proof_of_a_theorem_does/ http://www.reddit.com/r/math/comments/1y5v15/if_no_human_can...

archgrove 13y ago

So, to me, proofs have two purposes. The first is to just say "This theorem is true". The second is to give some insight into the problem. I have no problem with such a proof satisfying purpose one; I may not be able to check it myself, but I can build a chain of trustworthiness all the way back to a program that I can check myself. In such a chain, the truth of the final result is not, to me, in dispute. Alas, such a proof throughly fails the second test. I can't see how to gain insight into the problem from such a proof, beyond just it validating previous thought chains of the form "If X were true, then I could deduce Y". It doesn't reveal more about the structure of the problem, or other results in the space. It's no doubt useful (and all credit to the authors), but in terms of generating new mathematics, I'm dubious. Perhaps people more versed in this specific sub-field can tell me if I'm wrong?

dragontamer 13y ago
It is a field of AI, not a field of Mathematics. Automated Theorem Proving is a very old field, one of the earliest fields of Artificial Intelligence. The first proof of this nature was the Four Color Theorem, proven by an automated reasoner as opposed to a mathematician. At which point, the insight into the matter is understanding the AI algorithm and how the AI searches for a solution. And finally... how we can be sure that the AI itself is provably correct. http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_com...
- deleted 13y ago
  [deleted]
- ColinWright 13y ago
  I would be interested to see why you claim that the FCT was proven by an automated reasoner. My understanding is that Haken and Appel created techniques to create unavoidable configurations, and techniques to prove that a given configuration is reducable. They then programmed a computer to find an unavoidable set of reducable configurations. In Haken and Appel's proof there was no automated reasoning. Similarly in this case. The theorem claims that for every C there is an N such that a sequence of length at least N has a sub-configuration of discrepancy at least C. In this case the researchers created a program to show that in a sequence of length at least 1161 there is always a sub-sequence of discrepancy of at least 2. To the best of my understanding there is no automated reasoning, so I would be interested to see why you claim otherwise.
  - dragontamer 13y ago
    All Automated Reasoning is... is programming a computer to search a space automatically. In First Order Logic, you use the Resolution Rule to generate the search space for example. But at the end of the day... Automated Reasoning is nothing more than a glorified graph traversal. The FCT was solved with a hybrid method. Yes, you mention that there was significant human input in reducing the problem. However, a computer program was used to find (and prove) a huge number of those configurations. Search and verification. That is all "automated reasoning" is. In AI circles the FCT is considered to have been solved by Automated Reasoning methods. http://en.wikipedia.org/wiki/Automated_theorem_proving#Related_problems http://en.wikipedia.org/wiki/Automated_theorem_proving#Relat...

adiM 13y ago

From the linked Wikipedia article: > All experiments were conducted on PCs equipped with an Intel Core i5-2500K CPU running at 3.30GHz and 16GB of RAM. Why are these experiments not being conducted on a more powerful computer or a cluster?

IsTom 13y ago
Because it only took 6 hours anyway.
alephnil 13y ago
As already mentioned, it only took six hours. To make it run on a cluster or supercomnputer, you must parallelize the algorithm, which will take considerably longer time, even if it is easy. Then they likely have to apply for access, which also take time. Then it is easier to just run it on an available computer.
csense 13y ago
For the same reason you don't see word processors using a more powerful computer or cluster to render text for display as pixels. - It would be awfully inconvenient to program - It would require buying, building or obtaining access to such a machine - It'd require investing some amount of time and/or money -- obviously completely unnecessarily -- because whatever desktop or laptop happened to be within reach is perfectly adequate to the task

twocows 13y ago

"Wikipedia-sized" Is it really? They say in the article that the text of Wikipedia is a 10GB download, but that has to be compressed (and compression on plaintext, which comprises most of Wikipedia, is extremely efficient). I'm guessing (but have no proof) that their 13GB file was raw data. A minor thing, but comparisons like this always drive me nuts. Just say "13GB proof too big for humans to check." Then there's no confusion.</sillyrant>

deleted 13y ago
[deleted]
VLM 13y ago
A lot of its name games. 10 gigs of possibilities tested is actually pretty short for something like OGR-27. We're probably going to prove OGR-27 in a few weeks (or has it already been announced?) and I'm fairly certain a list of all possible rulers checked would exceed 10 gigs. Yet you can report OGR-26 in only 26 small numbers, or I guess you could draw a graphic pix using 492 pixels or whatever. So is OGR-27 merely 27 numbers aka a 1-d pixel "graph" probably around five hundred something pixels, or is it really zillions of gigs of rulers all of which are longer than the OGR?

deleted 13y ago

[deleted]

snird 13y ago

"The set-theoretical axioms that sustain modern mathematics are self-evident in differing degrees. One of them – indeed, the most important of them, namely Cantor's axiom, the so-called axiom of infinity – has scarcely any claim to self-evidence at all". John P. Mayberry

judk 13y ago

"Wikipedia" is displacing "encyclopedia" and "Library of Congress" as a unit of measure!

wlievens 13y ago
Clearly there is a defent "yo mamma" joke in there.
igravious 13y ago
Uh, and football field. The output of this proof if laid end to end would fill 37 regular sized football fields.