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?
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!
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.
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?