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.
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.
> 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.
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.
In fact you can encode any proof to a few hundred lines. Just write a program that brute forces through all possible proofs. If that counts, then no proof need be longer than it's conjecture plus a constant.
There's a lot of fine distinction, and a hell of a lot of study, of these kinds of questions. One thing you might ask of your proofs is that they are immediate—which is to say, they can be (a) grasped and (b) believed, at least in principle, after only a finite amount of work. Further, you should be able to prove that your proof has these properties.
Without these properties, it's hard to call something a proof since it might simply go on forever and never resolve the question in the way you wish it would. This is absolutely the realm of things like the Halting Problem.
So 200TB of data plus a short proof that the search completed could at least in principle be immediately checked in finite work. On the other hand, the mere program which generates this data could not be unless it also comes with a proof of its own termination. We have no general process to generate these, so you must create a specific one for your generation program.
If it's cheaper to just spit out 200TB than communicate why you're sure that your program won't spin, then the better proof is 200TB long.
---
As a side note, this is sort of odd sounding because we're implicitly saying that "small is better" in proofs. In an ultimate sense this is probably true---if I had before me all of the proofs of something I would want to order them and pick the smallest.
But in practice, we cannot enumerate proofs and must expend energy to achieve new ones. Thus, there are at least two kinds of energy optimization which prevail. The first is how much effort is required to achieve a proof and the second is how much effort is required to communicate/transmit the proof to someone else.
This 200TB proof might be well-optimizing the search question and it might also be failing on the communication question.
Depends on how you look at it. The 200TB seems to be the data required to prove that none of the possible combinations works.
If it had been temporary data to get to a simple proof of something, then I'd agree that this data was just a side-effect.
But if I'm understanding it correctly, as it stands even if you're told that it stops at 7,825, you'd still need all of this data to prove that it's true.
Correct. They didn't even know if there was a finite number where colouring became impossible, but it was strongly believed there was such a limit. Privately, people had their own ideas - sort of Fermi estimates. I don't know anyone who made such estimates public.
Is the data compressed and piped into a known compression algorithm, or is there some other technique used? I'd love to know how the actual program is run. Side note... the visual output is really interesting to see, and I'll admit I crossed my eyes at it to see if I could see some sort of pattern (read: there was no sailboat).
> Although the computer solution has cracked the Boolean Pythagorean triples problem, it hasn’t provided an underlying reason why the colouring is impossible, or explored whether the number 7,825 is meaningful, says Kullmann.
Kind of reminds me of why we were always taught to avoid proof by induction (the mathematical kind[0]) when possible.
Also, funny coincidence, but the shortest math paper published in a serious journal[1] was also a "no insight into why" kind of proof.
That's the problem with counterexample proofs, though. If something is only true for a large-but-finite range of numbers, there might not be a satisfying reason why.
If you verified the code performed the correct function, ensured it ran correctly and computed the result, then the code itself serves as most of the proof (not the 200TB). Really what you want to be peer-reviewed is the code, not the swathes of data.
> If you verified the code performed the correct function, ensured it ran correctly and computed the result, then the code itself serves as most of the proof
But then you have to trust their program doesn't have any bugs, and checking the proof requires a lot of computational power.
Instead, the authors produced a very large input file to a very small program. This way, instead of trusting the program they used to produce the input file, you only need to trust:
1) the input file corresponds to the theorem statement in their paper; and
2) the certificate checking program is correct
The benefit of this approach over the one you suggest are numerous:
* The effort of part 2 amortizes and isn't specific to any particular problem.
* The computational cost of re-checking their proof is considerably smaller than the cost of finding the proof certificate, allowing for the proof to be re-checked by anyone with a bit of spare computing power (as opposed to requiring a super computer in order to replicate the result).
Surely the value of this is that it provides a counterexample to a long-standing conjecture. The proof that it is a counterexample may not be too enlightening, but that's hardly the point.
A mathematician doesn't come up with a research where he says: "Ei look, we are now extremely confident that this theorem applies in every case... we don't have a full mathematical proof for it but I can show you all these cases where it holds true."
No, a mathematician proposes a result and then goes on to prove or disprove mathematically that it holds true under specific conditions in absolutely every case where those conditions are met.
Of course this is mathematics. Obviously, it would be nicer to have a real understanding of what's going on, but now that people know what to prove, such a proof might come along soon.
You are either completely oblivious to computer assisted/generated proofs or you have a niche definition of mathematics for yourself.
Also they are not saying "all these cases where it holds true," they are saying "in all the cases, it holds true," which is the definition for validity.
IANAMathematician, but, a brute force proof is still a proof though, isn't it?
If I have the theory, that all positive integers smaller than 5 are also smaller than 6, I would assume I'm mathematically allowed to 'brute force' the proof by enumerating all the numbers > 0 and < 5 and then testing for each that it's also < 6.
If I can prove I enumerated all the positive integers smaller than 5 and didn't find any exceptions, I guess I proved my theory...
It's a silly way to prove my silly theory, but it is a proof. (I have also a truly remarkable proof, which this comment is too small to contain. ;) )
[+] [-] CJefferson|9 years ago|reply
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.
[+] [-] nsimplexx|9 years ago|reply
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.
[+] [-] tluyben2|9 years ago|reply
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).
[+] [-] ifdefdebug|9 years ago|reply
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.
[+] [-] jacobolus|9 years ago|reply
[+] [-] curiousgal|9 years ago|reply
[+] [-] hatsunearu|9 years ago|reply
[+] [-] Aardwolf|9 years ago|reply
So in a sense, the code is the proof, and the 200TB is just something it generates as a side effect.
[+] [-] Houshalter|9 years ago|reply
[+] [-] tel|9 years ago|reply
Without these properties, it's hard to call something a proof since it might simply go on forever and never resolve the question in the way you wish it would. This is absolutely the realm of things like the Halting Problem.
So 200TB of data plus a short proof that the search completed could at least in principle be immediately checked in finite work. On the other hand, the mere program which generates this data could not be unless it also comes with a proof of its own termination. We have no general process to generate these, so you must create a specific one for your generation program.
If it's cheaper to just spit out 200TB than communicate why you're sure that your program won't spin, then the better proof is 200TB long.
---
As a side note, this is sort of odd sounding because we're implicitly saying that "small is better" in proofs. In an ultimate sense this is probably true---if I had before me all of the proofs of something I would want to order them and pick the smallest.
But in practice, we cannot enumerate proofs and must expend energy to achieve new ones. Thus, there are at least two kinds of energy optimization which prevail. The first is how much effort is required to achieve a proof and the second is how much effort is required to communicate/transmit the proof to someone else.
This 200TB proof might be well-optimizing the search question and it might also be failing on the communication question.
[+] [-] prof_hobart|9 years ago|reply
If it had been temporary data to get to a simple proof of something, then I'd agree that this data was just a side-effect.
But if I'm understanding it correctly, as it stands even if you're told that it stops at 7,825, you'd still need all of this data to prove that it's true.
[+] [-] unknown|9 years ago|reply
[deleted]
[+] [-] mafribe|9 years ago|reply
- D. Aspinall, C. Kaliszyk, Towards Formal Proof Metrics.
- G. Klein, Proof Engineering Considered Essential.
- G. Gonthier, Engineering Mathematics: The Odd Order Theorem Proof.
- T. Bourke, M. Daum, G. Klein, R. Kolanski, Challenges and Experiences in Managing Large-Scale Proofs.
[+] [-] JadeNB|9 years ago|reply
Towards formal proof metrics: http://link.springer.com/chapter/10.1007/978-3-662-49665-7_1...
Proof engineering considered essential: http://link.springer.com/chapter/10.1007/978-3-319-06410-9_2
Engineering mathematics: http://dl.acm.org/citation.cfm?id=2429071
Challenges and experiences …: http://link.springer.com/chapter/10.1007/978-3-642-31374-5_3
[+] [-] infruset|9 years ago|reply
[+] [-] cantagi|9 years ago|reply
So they didn't know in advance how long it was going to take or the size of the output?
[+] [-] ColinWright|9 years ago|reply
[+] [-] dmichulke|9 years ago|reply
Worse even, no one would know why it wouldn't halt...
In other words, you have to be lucky to find a counterexample to the given assumption otherwise you're stuck publishing an increased lower bound
[+] [-] userbinator|9 years ago|reply
http://www.links.org/?p=6
[+] [-] dylanz|9 years ago|reply
[+] [-] nrfc|9 years ago|reply
https://www.cs.utexas.edu/~marijn/drat-trim/
There are publications and examples on the website that explain how the compression the authors used works.
[+] [-] vanderZwan|9 years ago|reply
Kind of reminds me of why we were always taught to avoid proof by induction (the mathematical kind[0]) when possible.
Also, funny coincidence, but the shortest math paper published in a serious journal[1] was also a "no insight into why" kind of proof.
[0] https://en.wikipedia.org/wiki/Mathematical_induction
[1] http://www.openculture.com/2015/04/shortest-known-paper-in-a...
[+] [-] j2kun|9 years ago|reply
[+] [-] gsam|9 years ago|reply
[+] [-] nrfc|9 years ago|reply
But then you have to trust their program doesn't have any bugs, and checking the proof requires a lot of computational power.
Instead, the authors produced a very large input file to a very small program. This way, instead of trusting the program they used to produce the input file, you only need to trust:
1) the input file corresponds to the theorem statement in their paper; and
2) the certificate checking program is correct
The benefit of this approach over the one you suggest are numerous:
* The effort of part 2 amortizes and isn't specific to any particular problem.
* The computational cost of re-checking their proof is considerably smaller than the cost of finding the proof certificate, allowing for the proof to be re-checked by anyone with a bit of spare computing power (as opposed to requiring a super computer in order to replicate the result).
[+] [-] alimw|9 years ago|reply
[+] [-] jbmorgado|9 years ago|reply
A mathematician doesn't come up with a research where he says: "Ei look, we are now extremely confident that this theorem applies in every case... we don't have a full mathematical proof for it but I can show you all these cases where it holds true."
No, a mathematician proposes a result and then goes on to prove or disprove mathematically that it holds true under specific conditions in absolutely every case where those conditions are met.
[+] [-] auggierose|9 years ago|reply
[+] [-] mathetic|9 years ago|reply
Also they are not saying "all these cases where it holds true," they are saying "in all the cases, it holds true," which is the definition for validity.
[+] [-] BugsBunnySan|9 years ago|reply
If I have the theory, that all positive integers smaller than 5 are also smaller than 6, I would assume I'm mathematically allowed to 'brute force' the proof by enumerating all the numbers > 0 and < 5 and then testing for each that it's also < 6.
If I can prove I enumerated all the positive integers smaller than 5 and didn't find any exceptions, I guess I proved my theory...
It's a silly way to prove my silly theory, but it is a proof. (I have also a truly remarkable proof, which this comment is too small to contain. ;) )
[+] [-] gone35|9 years ago|reply
[1] https://en.wikipedia.org/wiki/Conjecture
[+] [-] infinidim|9 years ago|reply