4 ms·

Writing a formal proof in HOL Light is very much like writing a computer program. If the program run from start to finish without throwing errors, the proof is

by gghh 12y ago

Writing a formal proof in HOL Light is very much like writing a computer program. If the program run from start to finish without throwing errors, the proof is correct. Writing a proof takes forever, because you have to take into account all possible corner cases etc, but I'd be surprised if running (hence: verifying) the entire Hale's proof would take more than a few minutes.

bumbledraven 12y ago
I'd be surprised if running (hence: verifying) the entire Hale's proof would take more than a few minutes. I would have said the same thing before reading the announcement, but it says it took 5000 hours for some of the computations: The term the_nonlinear_inequalities is defined as a conjection of several hundred nonlinear inequalities. The domains of these inequalities have been partitioned to create more than 23,000 inequalities. The verification of all nonlinear inequalities in HOL Light on the Microsoft Azure cloud took approximately 5000 processor-hours. Almost all verifications were made in parallel with 32 cores, hence the real time is about 5000 / 32 = 156.25 hours Would those computations have to be repeated by every verifier? Or is theresome kind of certificate that can be verified faster?
- murbard2 12y ago
  Indeed there is, http://en.wikipedia.org/wiki/PCP_theorem http://en.wikipedia.org/wiki/PCP_theorem
  - bumbledraven 12y ago
    I suppose I was unclear. I should have asked, is the file ready for me to download? (Not, "does such a certificate exist, in the platonic sense")
- Strilanc 12y ago
  If there was a certificate that could be verified faster, then that would be used as the proof instead. For now we're stuck with the ~900K lines of code and 5K cpu hours. I wouldn't be surprised if there's probably a lot of room for improvement, though. A possible exception would be if the certificate was a probabilistic proof of some kind (someone mentioned the PCP theorem, which is an example of that), but I don't think mathematicians would be satisfied by that.
- dzdt 12y ago
  This computationally intensive step is proving a bunch of inequalities originally calculated by floating point numerical routines. It does a software floating point emulation inside the theorem prover with proofs of bounds on the rounding at each step. Software floating point in an inefficient high-level language is slow!

by gghh 12y ago

bumbledraven 12y ago

I'd be surprised if running (hence: verifying) the entire Hale's proof would take more than a few minutes. I would have said the same thing before reading the announcement, but it says it took 5000 hours for some of the computations: The term the_nonlinear_inequalities is defined as a conjection of several hundred nonlinear inequalities. The domains of these inequalities have been partitioned to create more than 23,000 inequalities. The verification of all nonlinear inequalities in HOL Light on the Microsoft Azure cloud took approximately 5000 processor-hours. Almost all verifications were made in parallel with 32 cores, hence the real time is about 5000 / 32 = 156.25 hours Would those computations have to be repeated by every verifier? Or is theresome kind of certificate that can be verified faster?

murbard2 12y ago
Indeed there is, http://en.wikipedia.org/wiki/PCP_theorem http://en.wikipedia.org/wiki/PCP_theorem
- bumbledraven 12y ago
  I suppose I was unclear. I should have asked, is the file ready for me to download? (Not, "does such a certificate exist, in the platonic sense")
Strilanc 12y ago
If there was a certificate that could be verified faster, then that would be used as the proof instead. For now we're stuck with the ~900K lines of code and 5K cpu hours. I wouldn't be surprised if there's probably a lot of room for improvement, though. A possible exception would be if the certificate was a probabilistic proof of some kind (someone mentioned the PCP theorem, which is an example of that), but I don't think mathematicians would be satisfied by that.
dzdt 12y ago
This computationally intensive step is proving a bunch of inequalities originally calculated by floating point numerical routines. It does a software floating point emulation inside the theorem prover with proofs of bounds on the rounding at each step. Software floating point in an inefficient high-level language is slow!