Yes but parsing theorems (at least at the syntactic level) should be no harder than parsing English, and we do lots of reasonably smart text mining, and even some reasonable natural language translation.
Math theorems are hard-going for many humans. Machines think differently—but may well find them challenging too. I’m not sure this area is particularly low-hanging.
Most theorems are not presented in a very machine-friendly format, I believe.
Yes but parsing theorems (at least at the syntactic level) should be no harder than parsing English, and we do lots of reasonably smart text mining, and even some reasonable natural language translation.
Math theorems are hard-going for many humans. Machines think differently—but may well find them challenging too. I’m not sure this area is particularly low-hanging.