I have never seen a theorem prover applied to even basic 100-year-old results in Algebraic Number Theory. I think you underestimate the difficulty in translating a mathematical idea into a format a computer program can understand.

Why bother?