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

41–50 of 65 posts

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

#41

Post by dragontamer »

ColinWright wrote: post #34
dragontamer wrote: post #20

Earlier quoted context omitted.

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

Yes, although brute force would be "simple AI", but the basics of AI nonetheless.

One of the many "classic" problems given to students of Artificial Intelligence is the 8-Queens problem: http://en.wikipedia.org/wiki/Eight_queens_puzzle#Exercise_in...

It is a short step to go from "8-Queens Algorithm Design" to "8-Queens Logic Programming", and from there automated reasoning. After all, Logic Programming is purely based on automated reasoning using Horn Clauses. It just so happens to be one of the most optimized forms of automated logic, fast enough to be a general programming language (Prolog is one of the easiest languages to solve the 8-Queens problem)

Automated Reasoning covers new tricks, like tree pruning, different logic systems or methodologies (Tableau Logic)... but no matter how complicated it gets, it all comes back to the same methodology. Its simply a glorified search algorithm, defined over some space. (Prolog at its core is nothing more than a depth first search over the horn clauses specified by the programmer)

For an example that clearly demonstrates the search, here's a Wikipedia link to Tableau type automated reasoning:

http://en.wikipedia.org/wiki/Method_of_analytic_tableaux#Sea...

And of course, the Automated Conference on the Tableaux Automated Reasoning methodology:

http://en.wikipedia.org/wiki/International_Conference_on_Aut...

The "Art" of Automated Reasoning is not in the search methodology (which is almost always just depth-first search + heuristics), but in how to define those spaces. Horn Logic, Tableaux, First Order Logic / Resolution Rule, etc. etc.

So whenever a new "search space" is defined to solve a practical problem, it is always of great interest to the Automated Reasoning community.

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

#42

Post by ColinWright »

baddox wrote: post #39
ColinWright wrote: post #38

Earlier quoted context omitted.

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?

If one human makes the mistake, it's probably because it's a mistake that humans trained in this field are likely to make. Mistakes are not independent in this sense. Also, the number of humans capable of an in-depth analysis of the result is small, and they've mostly all got the same training, so if there's a subtle mistake, it's one to which they are all susceptible.

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

#43

Post by scott_s »

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…

If the certificate from the SAT solver does not count as a proof, you can't blame the popular accounts. That's the language the paper authors use:

The negative witness, that is, the DRUP unsatisfiability certificate, is probably one of longest proofs of a non-trivial mathematical result ever produced. Its gigantic size is comparable, for example, with the size of the whole Wikipedia, so one may have doubts about to which degree this can be accepted as a proof of a mathematical statement.

From http://arxiv.org/pdf/1402.2184v2.pdf

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

#44

Post by [deleted] »

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…

[deleted]

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

#45

Post by scott_s »

ColinWright wrote: post #33
scott_s wrote: post #30

Earlier quoted context omitted.

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.

Let's avoid the use of the word "proof", which I address above. Is it possible to do any analysis of the output of the SAT solver, the certificate, to gain any insight into the problem? That's what the poster was asking.

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

#47

Post by judk »

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…

What's the difference between a certificate and a proof?

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

#48

Post by judk »

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…

The case analysis demonstrates that the overall nontrivial strategy is correct.

The insight is in the strategy.

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

#49

Post by Igglyboo »

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.

You could just run the program and verify that the certificates match a few times, I guess you can't be 100% certain but the probability of a bit flip happening multiple times is extremely small.

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

#50

Post by ColinWright »

scott_s wrote: post #43
ColinWright wrote: post #38

Earlier quoted context omitted.

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…

If the certificate from the SAT solver does not count as a proof, you can't blame the popular accounts. That's the language the paper authors use: The negative witness, that is, the DRUP unsatisfiability certificate, is probably one of longest proofs of a non-trivial mathematical result ever produced. Its gigantic size is comparable, for example, with the size of the whole Wikipedia, so one may have doubts about to whi…

I think the problem is that the general public think of "proof" as the kind of thing that mathematicians sit and work out with a pencil on paper. To use the word "proof" to refer to a certificate is technically correct and appropriate in context, but deeply misleading when used outside of that context. It certainly gives the wrong impression.

I also suspect we're mostly in complete agreement.

Post reply on HN