Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Wikipedia-size maths proof too big for humans to check

newscientist.com

Post reply on HN
Print view View original

11–20 of 65 posts

Re: Wikipedia-size maths proof too big for humans to check

#11

Post by alephnil »

adiM wrote: post #5

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?

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.

Re: Wikipedia-size maths proof too big for humans to check

#12

Post by ColinWright »

dragontamer wrote: post #7
archgrove wrote: post #4

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…

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…

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.

Re: Wikipedia-size maths proof too big for humans to check

#14

Post by Pxtl »

baddox wrote: post #10
archgrove wrote: post #4

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…

In this case, I don't see why the proof is considered to be the output of the program, but rather the entire program itself. If you can verify the soundness of the software and hardware involved (I certainly can't, but I presume the verification has been done), why should a human need to actually read the output?

and now we're into questions about homoiconicity. I think I see why Lisp was so popular in AI research.

Re: Wikipedia-size maths proof too big for humans to check

#15

Post by twocows »

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

Re: Wikipedia-size maths proof too big for humans to check

#16

Post by ColinWright »

Dylan16807 wrote: post #13
ColinWright wrote: post #2

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

Those submissions never got traction or comments, why link them?

Because sometimes older submissions end up getting some discussion, even when more recent submissions have more comments.

Re: Wikipedia-size maths proof too big for humans to check

#17

Post by ColinWright »

Someone wrote: post #9
archgrove wrote: post #4

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…

I don't claim to be better versed in this field, but a way forward could be to do common subexpression elimination on this proof. Then, try and give names to those common subexpressions. Finding common subexpressions in such a proof could be a separate field of research. It probably isn't a matter of looking for repeated strings.

I've re-drafted this several times and it always seems to come out snarky. Please believe me that it's not intended as such - my field is mathematics, not English. So please accept this at face value.

I have some expertise in this field. My PhD is in combinatorics, which is closely related, and one of the main results used computer search. More, it's closely related to the Four Colour Theorem.

To me, what you say makes no sense at all. Perhaps this is what the field needs - people who know absolutely nothing making suggestions that are so far outside the box that those who have spent decades studying it would never consider them.

On the other hand, maybe there's nothing in it. Have you thought it through more? Do you have more ideas? Do you have any actual concept of what "sub-expressions" might mean in this context? Having written compilers for food I feel that I have some knowledge of the concept, but in this case it seems not to mean anything.

Re: Wikipedia-size maths proof too big for humans to check

#18

Post by ColinWright »

baddox wrote: post #10
archgrove wrote: post #4

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…

In this case, I don't see why the proof is considered to be the output of the program, but rather the entire program itself. If you can verify the soundness of the software and hardware involved (I certainly can't, but I presume the verification has been done), why should a human need to actually read the output?

Because the output of the program is effectively a long list of cases of things that have been considered[0], and why they do or don't "work" in some sense. The output is independent of the program and, in principle, can be checked. In some ways it's like printing the search tree of chess to show that white has a forced win. It doesn't matter if the program is "correct" - you can check the output separately.

[0] EDIT: actually it's the certificate from a SAT solver

Re: Wikipedia-size maths proof too big for humans to check

#19

Post by ColinWright »

archgrove wrote: post #4

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…

Absolutely - you seem to have nailed every point.

The only thing you've missed is this - we now know that for C=2 the minimal length required to force a sub-sequence of discrepancy >=2 is 1161. The technique used gives a hint of how fast this dependency might grow, and that might give clues about techniques that probably won't work.

It also seems clear that a similar brute-force check of C>=3 won't be possible. Knowing these things gives clues as to how we might now proceed.

Re: Wikipedia-size maths proof too big for humans to check

#20

Post by dragontamer »

ColinWright wrote: post #12
dragontamer wrote: post #7

Earlier quoted context omitted.

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…

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 th…

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#Relat...

Post reply on HN