This comment does nothing other than demonstrate your own ignorance of research mathematics.
Please keep going.
Why bother?
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.
Please don't post snarky dismissals to Hacker News. I'm dismayed to see this from you here.
Unfortunately, coq can’t parse just anything.
Unfortunately at this juncture, it's extremely difficult and time-consuming to place an arbitrary proof in the language of proof assistants. It's a very noble goal and much respect to those who do it, but even fully formalizing something like the four-color theorem is a major accomplishment.