I was trying to come up with a example where a theorem prover would have to be extended or rewritten in order to handle new types of mathematics. My imaginary scenario is a theorem validator built by mathematicians from pre-Cantor days, where I conjecture that it would be hard to encode transfinite proofs. As I know nothing about how theorem provers work, this is purely conjectural.

In more concrete terms .. and I am so far outside my knowledge that I barely know what I am saying ... I read in the Coq FAQ that "The axiom of unique choice together with classical logic (e.g. excluded-middle) are inconsistent in the variant of the Calculus of Inductive Constructions where Set is impredicative. As a consequence, the functional form of the axiom of choice and excluded-middle, or any form of the axiom of choice together with predicate extensionality are inconsistent in the Set-impredicative version of the Calculus of Inductive Constructions."

In other words, proofs involving "axiom of unique choice together with classical logic" cannot be expressed in at least Coq. While it might be possible to use a machine to check tools which assume the axiom of unique choice, it would no doubt take a lot of work if one needs to build such a system from scratch.

And that is the scenario - where it's much more difficult to develop a mechanical tool than to come up with a proof that enough for humans - that I am contemplating.