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

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.