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

31–40 of 65 posts

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

#31

Post by ColinWright »

peterderivaz wrote: post #23
ColinWright wrote: post #17

Earlier quoted context omitted.

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

I wonder if you misunderstood his comment as a suggested method to solve the mathematical problem? The way I read it, he was suggesting a possible way of reducing the size of the DRUP certificate from 13GByte by searching for common patterns, perhaps similar to the way bzip works.

The question then is whether there's any exploitable semantic structure in the certificate. I would guess not, but I don't have enough knowledge of the specifics of this problem and proof to be more certain. It just doesn't feel likely - any structure would emerge in the way the sub-sequences could be constructed, and lack of such structure is what makes this problem hard.

Just a guess.

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

#32

Post by jkarni »

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…

But what you think of when you say "insight into the problem" might be an antiquated notion. It may be that such a thing is a rough measure of (as you almost say) how much more likely you are to prove something else (or how much easier it would be) -- without computer assistance.

But the twist is that with computer-aided proofs, being well-versed in the ways of using computers to help prove things may begin to count as having insight; and Coq (or whatever) programs may come to be studied so that one may gain insight, just as human proofs are studied today.

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

#33

Post by ColinWright »

scott_s wrote: post #30
ColinWright wrote: post #17

Earlier quoted context omitted.

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

When he says "sub-expressions", he means it in the program-code sense. Really, he's saying: why don't we try to refactor the proof? And, since it's so large, we probably can't do it by hand. So we would need to develop techniques to do it automatically. (Or semi-automatically.)

But the proof isn't large, just the output of the search. Assuming my understanding of the problem and the result are correct, the reporting on this is so poor as to be meaningless and misleading. As such, the comments are well-meaning, but (to me) seem meaningless.

Of course, my "understanding" may be completely wrong.

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

#34

Post by ColinWright »

dragontamer wrote: post #20
ColinWright wrote: post #12

Earlier quoted context omitted.

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

Knowing the FCT as well as I do, I have to say that I and many of my colleagues do not consider the H-A proof to be anything like automated reasoning. The work that Gowers and associates are now doing is very much so, but programming a computer to conduct a specific search, and for every item found compute whether it has a specific characteristic is really just like getting a machine to carry out a factoring algorithm.

We run the risk of arguing past each other, and potentially being in "violent agreement," but consider this. If you take an 8x8 chessboard and remove any black square and any white square, the resulting mutilated chess-board is guaranteed to be exactly coverable by dominoes, each of which covers exactly two squares. We can program a computer to conduct an exhaustive search to show that this is true. Would you consider the program to be an automated reasoner?

With what I know of this recent result, the work seems equivalent. It's a big problem fed to a SAT solver.

Edit: See the last paragraph of section 1 in the paper: http://arxiv.org/pdf/1402.2184.pdf

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

#35

Post by baddox »

ColinWright wrote: post #18
baddox wrote: post #10

Earlier quoted context omitted.

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…

I get that, but all these articles are worried about the fact that no human could possibly read and verify the output of the program. So why even bother? Why not just verify the software and hardware that generates the output?

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

#36

Post by baddox »

brador wrote: post #22
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…

Imagine if we could program a computer with all known mathematical truths. What curiosities would it discover that we have yet to find?

That would prove to be insurmountably difficult:

http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_the...

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

#37

Post by dllthomas »

baddox wrote: post #35
ColinWright wrote: post #18

Earlier quoted context omitted.

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…

I get that, but all these articles are worried about the fact that no human could possibly read and verify the output of the program. So why even bother? Why not just verify the software and hardware that generates the output?

A CS prof I had held the position (in grading his tests - perhaps not generally) that "a proof is anything that convinces me you could write a proof". The program, along with an output saying "true", would seem to suffice under that metric.

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

#38

Post by ColinWright »

baddox wrote: post #35
ColinWright wrote: post #18

Earlier quoted context omitted.

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…

I get that, but all these articles are worried about the fact that no human could possibly read and verify the output of the program. So why even bother? Why not just verify the software and hardware that generates the output?

It's a certificate output by a SAT solver. More, you can't guarantee that there wasn't a bit flip caused by a cosmic ray. Verifying the hardware and software isn't enough.

And yes, the whole question is to ask to what extent we can trust this. Personally, it's just as likely that a human proof would have a subtle and hard-to-find error, missed by all the reviewers.

All the popular articles are claiming this humungous output is a proof. It's not a proof, it's a certificate from a SAT solver. There's a difference, and most comments people are making based on the popular accounts are misguided.

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

#39

Post by baddox »

ColinWright wrote: post #38
baddox wrote: post #35

Earlier quoted context omitted.

I get that, but all these articles are worried about the fact that no human could possibly read and verify the output of the program. So why even bother? Why not just verify the software and hardware that generates the output?

It's a certificate output by a SAT solver. More, you can't guarantee that there wasn't a bit flip caused by a cosmic ray. Verifying the hardware and software isn't enough. And yes, the whole question is to ask to what extent we can trust this. Personally, it's just as likely that a human proof would have a subtle and hard-to-find error, missed by all the reviewers. All the popular articles are claiming this humungous…

> More, you can't guarantee that there wasn't a bit flip caused by a cosmic ray.

Hmm. Are bit flips from cosmic rays more likely than a human making a mistake verifying a proof, or even a large number of humans making the same mistake?

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

#40

Post by ufo »

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.

These theorem provers receive as input a high level computer program that describes how to generate the proof and output a low level sequence of logical steps. I think looking at that high level input is going to be more helpful then trying to reconstruct it from the output.
Post reply on HN