If these proofs really are like codebases, wouldn't we eventually expect these proofs to be written as software?
You'd install lemmas using a package manager and then import them into your proof.
You can then install updates to proofs. Maybe someone has found the proof to be wrong, in which case you either find a different proof or invalidate the lemma so all the dependents can be invalidated automatically.
You'd install lemmas using a package manager and then import them into your proof.
You can then install updates to proofs. Maybe someone has found the proof to be wrong, in which case you either find a different proof or invalidate the lemma so all the dependents can be invalidated automatically.