On the other hand, tech to verify formalized derivations will be cheaper than tech to generate falsely verifying formalized derivations (impossible unless one finds a bug in a verifier)

So we should move to formalization as a herd.