Comment by ColinWright | Hacker News Reader

Comment by ColinWright | Hacker News Reader

Parent Full thread

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.

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.

Using that context, I have no knowledge of the form the certificate takes, so I can't venture an opinion at all in this case. I suspect the answer is "no", but that's just on general principles.

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.

Reply on news.ycombinator.com