5 ms·

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

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

by gsam 10y ago

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.