8 ms·

Two-hundred-terabyte math proof is largest ever

166 points by tokenadult 10y ago

Aardwolf 10y ago
Probably the code used to generate the 200TB was not 200TB itself, right? So in a sense, the code is the proof, and the 200TB is just something it generates as a side effect.
- deleted 10y ago
  [deleted]
- prof_hobart 10y ago
  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.
- Houshalter 10y ago
  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.
  - poppingtonic 10y ago
    Hooray for proof search techniques. How much data would the Godel-numbering process generate, though? I'm assuming such a search would use this, unless I'm mistaken about my mathematical logic.
  - timlyo 10y ago
    And then if we get enough monkeys/children in a room tapping away, eventually they'll write enough programs to solve every problem. That's it, maths is solved.
    - firethief 10y ago
      I don't know, they tried that with Windows Phone apps...
  - ifdefdebug 10y ago
    I'm not sure: doesn't the halting problem apply to this? In other words, can you write such a brute force program that is guaranteed to halt after a finite number of steps, providing a yes or no? I guess not.
    - Ar-Curunir 10y ago
      You just look for all proofs of a certain length. This is equivalent to checking if a Turing machine halts within a bounded number of steps. This is a NP problem.
    - hyperpape 10y ago
      It doesn't, and it's interesting why. You can enumerate all possible proofs. If there is a proof of a given statement, you will eventually find it. But if there is no proof, you will never know, because it always could be the next proof you haven't looked at. For the same reason, for any program that halts, you can run it long enough, and see that it halts. But (unless you are lucky enough to detect a loop), if it doesn't halt, you will never witness that, you will only be able to say "it hasn't halted yet". It definitely can take a while until that kind of asymmetry becomes intuitive.
      - jerf 10y ago
        There's also the problem of identifying a proof when you have it. Hooray, after running a super-exponential number of steps in the real universe somehow it turns out Turing Machine #38,384,768,209,040,100 halts after fifteen googleplex and change steps. What does that mean? (This is not criticism, this is elaboration. The approach is useless in practice, but deeply understanding all the reasons why is a good exercise in computer science.)
      - ifdefdebug 10y ago
        > But if there is no proof, you will never know, because it always could be the next proof you haven't looked at. But that's exactly what I meant. So the brute force program proposed in the post I replied to doesn't exist, right? Let's say, you have proposition A. You write a program to brute force proofs for A. If it finds a proof, it will halt and output Yes, if it finds a disproof it will halt and output No, otherwise it will check the next proof. So if you say that your brute force program can proof/disproof proposition A (and A1, A2, A3, ... for that matter), you will have to proof that your program will halt for sure after a finite number of steps. Now that's proposition B. If you find a clever proof for proposition B, then you can claim that you wrote a program that can proof or disproof proposition A - maybe in a zillion years, but it can. If you can't find such a proof for proposition B, you can always try to write a brute force program to proof/disproof proposition B... then C, D, E, etc. :) And here comes the halting problem: you may be able to proof that a specific program will halt on a specific input, but it can be very hard to proof. But you can't proof that a specific program will halt on every input. This is directly related to Godel's incompleteness of formal systems.
  - edko 10y ago
    I'm not sure about that. Those "all possible proofs" will be an infinite numerable set. To pick a specific proof from the set, you will need an arbitrarily large number as the index, so your few hundred lines will not be enough (assuming line sizes are finite).
    - rspeer 10y ago
      I think the "plus a constant" here refers to a bound on the size of the proof. So you don't need the exact index, just a really rough upper bound. (This would, of course, be unreasonably inconvenient to check.)
- tel 10y ago
  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.
  - Dylan16807 10y ago
    Once you know the answer, you say "Take this program and run it with n=7825". That is your compact finite proof, not the untested program. You'd don't have to meta-prove halting, you just give it the required CPU hours.
    - tel 10y ago
      While I think what your saying is true, it's frowned upon. It's saying "I've discovered a truly marvelous proof and its at the bottom of this cave". We've dodged the infinity risk, but not the resources involved in communication risk. So it's kind of just crap UI at this point. I think that given that proofs are essentially social objects, this is a pretty big negative on that style of proof even if it doesn't totally sink the ship.
dylanz 10y ago
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).
- nrfc 10y ago
  The authors used this tool: https://www.cs.utexas.edu/~marijn/drat-trim/ 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.
CJefferson 10y ago
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.
- tluyben2 10y ago
  > 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).
  - deleted 10y ago
    [deleted]
- jacobolus 10y ago
  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?
  - CJefferson 10y ago
    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).
cantagi 10y ago
"but when you reach 7,825, it is impossible for every Pythagorean triple to be multicoloured" So they didn't know in advance how long it was going to take or the size of the output?
- ColinWright 10y ago
  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.
- dmichulke 10y ago
  Exactly, the program would have never halted if it were possible to colour all triples. 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
infruset 10y ago
A relevant article on large proofs: http://gallium.inria.fr/blog/large-proofs/ http://gallium.inria.fr/blog/large-proofs/
userbinator 10y ago
I think "brute force math" would be a good name for this technique --- that diagram reminds me of finding hash collisions: http://www.links.org/?p=6 http://www.links.org/?p=6
gsam 10y ago
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.
- nrfc 10y ago
  > 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).
  - umanwizard 10y ago
    > But then you have to trust their program doesn't have any bugs This is no different from a typical math paper. Proofs can have "bugs", too; and sometimes they're fatal. That's -- in theory -- one of the points of peer review.
    - nrfc 10y ago
      > This is no different from a typical math paper It's substantially different from a typical math paper. First because programs are typically much larger than even large mathematical proofs (more on this below). Second, because even after you trust the program, you then still have have to run the program to make sure the paper's result is correct. Far better to run the program once and then produce something you can check quickly than to require every peer reviewer to buy hundreds/thousands of dollars of compute time. Think P vs. NP: why force the reviewer to solve an NP problem when you can just as easily hand them a P problem. > Proofs can have "bugs", too But the reviewer's bug checking obligation is typically isolated to the paper at hand; i.e., the reviewer doesn't have to worry about the correctness of cited papers -- it's assumed those results are correct. By contrast, software implementations -- even for purely mathematical code -- often contain tens of thousands of lines of implicitly trusted code [1]. Reviewers therefore (rightly!) say of ad hoc programs submitted as a portion of a proof: "sorry, I can't possibly know whether there are any important bugs in these tens of thousands of lines of code upon when you depend". As a result, the SAT and theorem proving communities have developed highly trustworthy proof checkers so that the portion of code the reviewer has to trust can be meaningfully peer reviewed (and, more-over, peer reviewed apart from any particular theorem). [1] This is true even if you don't include things like the underlying operating system. Standard libraries, mathematics packages, compiler implementations, solver implementations, specialized software packages for the application domain, etc. etc. Some of this software a reasonable person will trust, but some of it really isn't interrogated well enough for the purpose of mathematical proof... and even just sorting out what's trustworthy and what's not can take a significant amount of time.
jbmorgado 10y ago
This isn't mathematics, this is data analysis. 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.
- mathetic 10y ago
  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.
- auggierose 10y ago
  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.
- BugsBunnySan 10y ago
  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. ;) )
  - dagw 10y ago
    Computer assisted proofs are historically frowned upon because you eventually end up in a black box you have to blindly trust. Can you verify that your code is correct according to the language spec? Can you verify that your compiler is bug free and follows the spec? Can you verify that your CPU is bug free and runs the output from your compiler correctly? Can you verify that your storage medium is correct and hasn't corrupted any of your intermediate results etc. etc. Practically people will eventually say that if your test has been run N times using M different compilers and P different computers and they all give the same answer then you're probably correct, but having a proof that humans can reason through from beginning to end makes people feel more comfortable. That being said computer assisted proofs are becoming more and more common and mathematicians are getting more and more comfortable with them as the verification tools surrounding them keep getting better. And even if computers aren't used for the final proof they are often used for intermediate tests. For example if you're making a statement about all primes it makes sense to quickly test the first few hundred million primes to make sure there aren't any obvious counter-examples.
mafribe 10y ago
There is an increasing appreciation that large proofs need "proof engineering" that is similar to software engineering. See e.g. - 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 10y ago
  Links, unfortunately non-free: Towards formal proof metrics: http://link.springer.com/chapter/10.1007/978-3-662-49665-7_19 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 http://link.springer.com/chapter/10.1007/978-3-319-06410-9_2 Engineering mathematics: http://dl.acm.org/citation.cfm?id=2429071 http://dl.acm.org/citation.cfm?id=2429071 Challenges and experiences …: http://link.springer.com/chapter/10.1007/978-3-642-31374-5_3 http://link.springer.com/chapter/10.1007/978-3-642-31374-5_3
infinidim 10y ago
I have discovered a truly marvelous demonstration of this proposition that this margin is too narrow to contain.
vanderZwan 10y ago
> 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. [0] https://en.wikipedia.org/wiki/Mathematical_induction https://en.wikipedia.org/wiki/Mathematical_induction [1] http://www.openculture.com/2015/04/shortest-known-paper-in-a-serious-math-journal.html http://www.openculture.com/2015/04/shortest-known-paper-in-a...
- j2kun 10y ago
  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.
alimw 10y ago
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.

166 points by tokenadult 10y ago

Probably the code used to generate the 200TB was not 200TB itself, right? So in a sense, the code is the proof, and the 200TB is just something it generates as a side effect.

deleted 10y ago
[deleted]
prof_hobart 10y ago
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.
Houshalter 10y ago
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.
- poppingtonic 10y ago
  Hooray for proof search techniques. How much data would the Godel-numbering process generate, though? I'm assuming such a search would use this, unless I'm mistaken about my mathematical logic.
- timlyo 10y ago
  And then if we get enough monkeys/children in a room tapping away, eventually they'll write enough programs to solve every problem. That's it, maths is solved.
  - firethief 10y ago
    I don't know, they tried that with Windows Phone apps...
- ifdefdebug 10y ago
  I'm not sure: doesn't the halting problem apply to this? In other words, can you write such a brute force program that is guaranteed to halt after a finite number of steps, providing a yes or no? I guess not.
  - Ar-Curunir 10y ago
    You just look for all proofs of a certain length. This is equivalent to checking if a Turing machine halts within a bounded number of steps. This is a NP problem.
  - hyperpape 10y ago
    It doesn't, and it's interesting why. You can enumerate all possible proofs. If there is a proof of a given statement, you will eventually find it. But if there is no proof, you will never know, because it always could be the next proof you haven't looked at. For the same reason, for any program that halts, you can run it long enough, and see that it halts. But (unless you are lucky enough to detect a loop), if it doesn't halt, you will never witness that, you will only be able to say "it hasn't halted yet". It definitely can take a while until that kind of asymmetry becomes intuitive.
    - jerf 10y ago
      There's also the problem of identifying a proof when you have it. Hooray, after running a super-exponential number of steps in the real universe somehow it turns out Turing Machine #38,384,768,209,040,100 halts after fifteen googleplex and change steps. What does that mean? (This is not criticism, this is elaboration. The approach is useless in practice, but deeply understanding all the reasons why is a good exercise in computer science.)
    - ifdefdebug 10y ago
      > But if there is no proof, you will never know, because it always could be the next proof you haven't looked at. But that's exactly what I meant. So the brute force program proposed in the post I replied to doesn't exist, right? Let's say, you have proposition A. You write a program to brute force proofs for A. If it finds a proof, it will halt and output Yes, if it finds a disproof it will halt and output No, otherwise it will check the next proof. So if you say that your brute force program can proof/disproof proposition A (and A1, A2, A3, ... for that matter), you will have to proof that your program will halt for sure after a finite number of steps. Now that's proposition B. If you find a clever proof for proposition B, then you can claim that you wrote a program that can proof or disproof proposition A - maybe in a zillion years, but it can. If you can't find such a proof for proposition B, you can always try to write a brute force program to proof/disproof proposition B... then C, D, E, etc. :) And here comes the halting problem: you may be able to proof that a specific program will halt on a specific input, but it can be very hard to proof. But you can't proof that a specific program will halt on every input. This is directly related to Godel's incompleteness of formal systems.
- edko 10y ago
  I'm not sure about that. Those "all possible proofs" will be an infinite numerable set. To pick a specific proof from the set, you will need an arbitrarily large number as the index, so your few hundred lines will not be enough (assuming line sizes are finite).
  - rspeer 10y ago
    I think the "plus a constant" here refers to a bound on the size of the proof. So you don't need the exact index, just a really rough upper bound. (This would, of course, be unreasonably inconvenient to check.)
tel 10y ago
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.
- Dylan16807 10y ago
  Once you know the answer, you say "Take this program and run it with n=7825". That is your compact finite proof, not the untested program. You'd don't have to meta-prove halting, you just give it the required CPU hours.
  - tel 10y ago
    While I think what your saying is true, it's frowned upon. It's saying "I've discovered a truly marvelous proof and its at the bottom of this cave". We've dodged the infinity risk, but not the resources involved in communication risk. So it's kind of just crap UI at this point. I think that given that proofs are essentially social objects, this is a pretty big negative on that style of proof even if it doesn't totally sink the ship.

dylanz 10y ago

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).

nrfc 10y ago
The authors used this tool: https://www.cs.utexas.edu/~marijn/drat-trim/ 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.

CJefferson 10y ago

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.

tluyben2 10y ago
> 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).
- deleted 10y ago
  [deleted]
jacobolus 10y ago
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?
- CJefferson 10y ago
  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).

cantagi 10y ago

"but when you reach 7,825, it is impossible for every Pythagorean triple to be multicoloured" So they didn't know in advance how long it was going to take or the size of the output?

ColinWright 10y ago
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.
dmichulke 10y ago
Exactly, the program would have never halted if it were possible to colour all triples. 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

infruset 10y ago

A relevant article on large proofs: http://gallium.inria.fr/blog/large-proofs/ http://gallium.inria.fr/blog/large-proofs/

userbinator 10y ago

I think "brute force math" would be a good name for this technique --- that diagram reminds me of finding hash collisions: http://www.links.org/?p=6 http://www.links.org/?p=6

gsam 10y ago

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.

nrfc 10y ago
> 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).
- umanwizard 10y ago
  > But then you have to trust their program doesn't have any bugs This is no different from a typical math paper. Proofs can have "bugs", too; and sometimes they're fatal. That's -- in theory -- one of the points of peer review.
  - nrfc 10y ago
    > This is no different from a typical math paper It's substantially different from a typical math paper. First because programs are typically much larger than even large mathematical proofs (more on this below). Second, because even after you trust the program, you then still have have to run the program to make sure the paper's result is correct. Far better to run the program once and then produce something you can check quickly than to require every peer reviewer to buy hundreds/thousands of dollars of compute time. Think P vs. NP: why force the reviewer to solve an NP problem when you can just as easily hand them a P problem. > Proofs can have "bugs", too But the reviewer's bug checking obligation is typically isolated to the paper at hand; i.e., the reviewer doesn't have to worry about the correctness of cited papers -- it's assumed those results are correct. By contrast, software implementations -- even for purely mathematical code -- often contain tens of thousands of lines of implicitly trusted code [1]. Reviewers therefore (rightly!) say of ad hoc programs submitted as a portion of a proof: "sorry, I can't possibly know whether there are any important bugs in these tens of thousands of lines of code upon when you depend". As a result, the SAT and theorem proving communities have developed highly trustworthy proof checkers so that the portion of code the reviewer has to trust can be meaningfully peer reviewed (and, more-over, peer reviewed apart from any particular theorem). [1] This is true even if you don't include things like the underlying operating system. Standard libraries, mathematics packages, compiler implementations, solver implementations, specialized software packages for the application domain, etc. etc. Some of this software a reasonable person will trust, but some of it really isn't interrogated well enough for the purpose of mathematical proof... and even just sorting out what's trustworthy and what's not can take a significant amount of time.

jbmorgado 10y ago

This isn't mathematics, this is data analysis. 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.

mathetic 10y ago
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.
auggierose 10y ago
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.
BugsBunnySan 10y ago
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. ;) )
- dagw 10y ago
  Computer assisted proofs are historically frowned upon because you eventually end up in a black box you have to blindly trust. Can you verify that your code is correct according to the language spec? Can you verify that your compiler is bug free and follows the spec? Can you verify that your CPU is bug free and runs the output from your compiler correctly? Can you verify that your storage medium is correct and hasn't corrupted any of your intermediate results etc. etc. Practically people will eventually say that if your test has been run N times using M different compilers and P different computers and they all give the same answer then you're probably correct, but having a proof that humans can reason through from beginning to end makes people feel more comfortable. That being said computer assisted proofs are becoming more and more common and mathematicians are getting more and more comfortable with them as the verification tools surrounding them keep getting better. And even if computers aren't used for the final proof they are often used for intermediate tests. For example if you're making a statement about all primes it makes sense to quickly test the first few hundred million primes to make sure there aren't any obvious counter-examples.

mafribe 10y ago

There is an increasing appreciation that large proofs need "proof engineering" that is similar to software engineering. See e.g. - 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 10y ago
Links, unfortunately non-free: Towards formal proof metrics: http://link.springer.com/chapter/10.1007/978-3-662-49665-7_19 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 http://link.springer.com/chapter/10.1007/978-3-319-06410-9_2 Engineering mathematics: http://dl.acm.org/citation.cfm?id=2429071 http://dl.acm.org/citation.cfm?id=2429071 Challenges and experiences …: http://link.springer.com/chapter/10.1007/978-3-642-31374-5_3 http://link.springer.com/chapter/10.1007/978-3-642-31374-5_3

infinidim 10y ago

I have discovered a truly marvelous demonstration of this proposition that this margin is too narrow to contain.

vanderZwan 10y ago

> 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. [0] https://en.wikipedia.org/wiki/Mathematical_induction https://en.wikipedia.org/wiki/Mathematical_induction [1] http://www.openculture.com/2015/04/shortest-known-paper-in-a-serious-math-journal.html http://www.openculture.com/2015/04/shortest-known-paper-in-a...

j2kun 10y ago
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.

alimw 10y ago

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.