In the long run creating a certificate that guarantees a certain probability of correctness will take much less energy. Right now we can run miller-rabin and show with 1-(1/10^100) certainty that the number is/isn't prime. Similar for hash collisions, after a certain point these can't happen in reality. If Anthropic can get their uptime from 1 9 to 9 9s (software isn't the bottleneck for 9 9s) then we don't need formally checked proofs.