Hacker News Reader

Comment by CJefferson | Hacker News Reader

Darn, I had no idea one could get into the media with this kind of stuff.

I had a much larger "proof", where we didn't bother storing all the details, in which we enumerated 718,981,858,383,872 semigroups, towards counting the semigroups of size 10.

Uncompressed, it would have been about 63,000 terabytes just for the semigroups, and about a thousand times that to store the "proof", which is just the tree of the search.

Of course, it would have compressed extremely well, but also I'm not sure it would have had any value, you could rebuild the search tree much faster than you could read it from a disc, and if anyone re-verified our calculation I would prefer they did it by a slightly different search, which would give us much better guarantees of correctness.

View on HN

I have a question about computer-generated proofs, as I am doing something similar.

When you encode the search tree as a proof, is there a technical name for that technique?

In my situation I encoded the proof as a sequence which is just the depth-first linear labelling of the tree. Then I proved why the sequence represents a proof. But if there is a most standard terminology/literature on this step, it would make it easier for me to talk about.

I've had a similar problem, there is nothing that useful I'm afraid. Probably best to look into general discussions of trees.

One thing worth trying to do (if you can) is separate the generation of the tree from the tree itself -- hopefully you can imagine the tree existing as a complete object (even though you never store it all), and formulate proofs based on that.

Proof by exhaustion?

In the community of the theorem prover Coq, a proof obtained by running a proven correct decision procedure is called a "proof by reflection".

There is also the "proof by certificate" approach. You generate a potentially large proof certificate by an unverified program. Then you run a proven correct (small) checker on the certificate to concude that the theorem is correct.

> Darn, I had no idea one could get into the media with this kind of stuff.

With the right spin anything can get into the media. It helps if no-one used that before; your 63000 are far more impressive but won't get much traction after this. However it is summer now so the coming months it'll be quite easy to get mostly anything in the news(paper).

I don't understand your objection. Couldn't you have published just the algorithm of your proof - an deterministic algorithm to reproduce those terabytes of data is arguably a compressed version of the data itself, and thus of the proof.

This problem has much more than just a search tree. They had to check 10 to 2300 possibilities to proof their counter example, so a simple search tree was no option and they had to boil it down to "just under 1 trillion". So lots of maths involved here.

I don't understand why you think CJefferson could have published their algorithm but the people in the news somehow couldn't. I guarantee you they did not write a 20-terabyte algorithm.

Maybe they had a lot of typewriters and then visited a zoo

Hey, we did lots of maths too! (Well not me personally, but lots was done).

There is actually 12,418,001,077,381,302,684 semigroups of size 10. We only had to find 718,981,858,383,872 by brute force search (which still involved a whole bunch of maths and case splitting), which is 0.006% of the total. There is a whole PhD in the maths involved.

Of course, we could (and have) just published the search which has to be redone, and the maths which is required to prove the piece of search to be done.

OK, sounds interesting enough. So maybe your publication didn't make it into the news because the problem you solved didn't have Pythagoras in it's name :)

He didn't get into the news because he didn't solve a problem for which a famous mathematician (Ronald Graham) had offered a prize. Also, it's somewhat more exciting to use a huge calculation to answer a yes-or-no question that anyone can understand, rather than to count a huge number of fairly obscure gadgets: semigroups of size 10.

(Personally I love semigroups, and I think it's cool that you counted all the ones of size 10. But any story about them in the popular press would focus on the sheer size of the calculation rather than what it actually achieved.)

Once you have a full explicit list of all the semigroups of a particular size, is there anything else interesting you can do with it?

They are useful for exploratory maths. If someone has an idea for a theorem "All semigroups with properties X and Y are of type Z", while an automated proof might be major work, a simple check of all semigroups up to a certain size is trivial, and a counter-example doesn't require a complex proof.

However, for numbers of the size I was looking at, storing them is impossible. We were just interested in how many there were (which wasn't known, and we don't know how to calculate without enumerating them through search).

Where the f did you store all of that?!

Oh, nowhere, just dumped it as we generated it. In my experience storing these kinds of things often isn't that useful anyway, when proving correctness of the answer it's as easy to start from scratch as go through a trace of what I did previously.

Ah, the benefits of having your problem in PSPACE...

If you can reduce a proof of a theorem to a finite number of operations, then I'd argue (and you'd agree) that the scheme + program (or just the scheme) is sufficient proof.

Reply on news.ycombinator.com