This wouldn't work because all theorems are trivially extensible. Either by adding extra theorems via conjunction, e.g. my new theorem C = previously-mined theo

This wouldn't work because all theorems are trivially extensible. Either by adding extra theorems via conjunction, e.g. my new theorem C = previously-mined theorems {A} ∪ {B}; or by adding garbage to the end, e.g my new theorem C = {A} ∪ {...arbitrary nonsense that cancels out}, e.g. (+ 0 + 0 + 0), or (- 1 + 1 - 1 + 1), or vastly more complex formulations. Logic isn't the study of merely finding out what's true, but what's true and interesting.