Back

Why didn't interactive theorem provers catch on in professional mathematics?

I'm used to writing code, and now that I'm studying more math I keep wanting to "run the compiler" on my work. Software gives you such great, rapid feedback! And it's not like mathematicians would be hesitant to learn an esoteric, questionably useful language.