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.
Follow
@alexaltair I had the vague impression that they aren't yet great for the domains of math that people actually work in.
