I was very interested in this as well for learning purposes. Without an instructor it's fairly easy to accidently make logical jumps and come up with wrong proofs. I figured that math is effectively a somewhat formal language for communicating concepts, so a compiler that checks errors (or even suggests corrections) could work well.
Tools like coq are great, but difficult to use (even as a programmer used to languages like Haskell) and they don't have a large set of existing proofs to work off of.
My opinion is that we need a good intermediate representation for proof tools (to share results; each new tool now needs a huge base built up to start being useful) and simpler tools to work with. It would be an enormous benefit to mathematicians and the world at large.
That'd be great, but I think the hard part about sharing representations is that many of the proof tools are based on different underlying type theories, which make it hard to go back and forth. For example Coq is based on the calculus of inductive constructions whereas Isabelle is based on HOL. Though, I'm guessing it's possible once a type scheme is fixed. Just poking around briefly, here's an SO question and answer on some of the differences between CIC and HOL (https://stackoverflow.com/questions/30152139/what-are-the-st...)
This should be possible when the underlying logics are similar (e.g. Isabelle/HOL and HOLight) but can be tricky if the logics are far apart (e.g. Isabelle/HOL and Coq).
Tools like coq are great, but difficult to use (even as a programmer used to languages like Haskell) and they don't have a large set of existing proofs to work off of.
My opinion is that we need a good intermediate representation for proof tools (to share results; each new tool now needs a huge base built up to start being useful) and simpler tools to work with. It would be an enormous benefit to mathematicians and the world at large.