I think this discussion is a bit off, moving the root of trust from the mathematicians to the computers is the thing that will not only kill mathematics but al

I think this discussion is a bit off, moving the root of trust from the mathematicians to the computers is the thing that will not only kill mathematics but also our civilization (and I will try to argue this overstatement now). People have a hard time understanding things on extreme ends of the scale because they just assume everything is within some reasonable bounds of effort, this is a failure of imagination. Mathematics is not a reasonable amount of effort. What's more it is depended on by literally everything else we do (as a civilization). Theorem proving software (so far) makes the fatal mistake of just trusting; the machine it is running on, the operating system it is running in, and several other things that can subvert assumptions. The correctness of a proof is justified by the trust we place in the heavily audited kernel which will check the proof script outputted by compilers for the human (textual) interface but that kernel is just another program on your (mostly) proprietary platform. Mathematics is a religion that currently dominates the planet (and as with most religions, it is totally ambient to people in that they don't realize to what extent they base their behaviour on it) but it is not without competition and the thing we must realize is that this competition is as motivated, ruthless and mission-driven as anything else on the planet. Just as we have people sitting around learning to recite the qur'an or the bible from memory we also have universities full of mathematics students reciting proofs and theorems by memory, trying to keep the knowledge that brought us this far alive. Computer memory is inherently volatile and we do not have the same conventions and procedures in place as we do for safeguarding the legitimacy of written texts. These take time to develop and are usually motivated by tragedies (such as the loss of our "prehistory"). Try to imagine the amount of effort it would take to re-assess every piece of information that we have (at current time) because we accidentally let the entropy into our libraries.