> If you have to rely on the computer to validate a proof you then have to rely on the whole supply chain that generated the computer as well as the software fo

> If you have to rely on the computer to validate a proof you then have to rely on the whole supply chain that generated the computer as well as the software for the proof checker. This is true, but a similar problem plagues typical proofs. > Proofs need to be dense enough that we can discover them in a long lost tomb and eventually figure out what that collapsed civilization had learned. This is almost never the case for modern mathematical research. Case in point, some of my current work relies on the classification of finite simple groups. Therefore, in practice, it is impossible to validate my results from first principles.