From what I've figured
(a) converting mathematical theorems and proofs from English to formal logic is a straightforward job for mathematicians with sufficient background, except that it takes time.
(b) once converted to formal logic, computer verification of the proof becomes straightforward.
If we can automate (a), a lot of time and intellectual labour (that could be dedicated elsewhere) is saved in doing (b) on published research papers.
Note that if solving (a) in its entirety is hard, we could expect the mathematicians to meet the computer system halfway and avoid writing lengthy English paras that are hard to convert. If it becomes doable enough, submitting a formal logical version of your paper could even become a standard procedure that is expected.
Additional benefit of solving (a) would be to do the process in reverse: mathematicians could delegate smaller tasks and lemmas (both trivial and non-trivial tasks) to an automated theorem prover (ATP). Assisted theorem proving will become more popular and boost productivity, maybe even surprise us once in a while by coming up with proofs that the paper writer couldn't. This is further of value if we predict a sharp upward trajectory of the capability of ATPs in the future. If anything, this could be self-fulfilling, as the demonstration of potential for good ATPs combined by a large corpus of proofs and problems in formal logical format could drive an increase in research on ATPs.
Forgive me if I sound like a salesman, but how doable is this? What will be the main challenges faced in developing NLP-based AI to convert papers, and how tractable are these challenges given today's state of the field?
P.s. I understand that proofs generated by ATPs are often hard to understand intuitively and can end up proving results without clearly exposing the underlying proof method used. But it is still a benefit to be able to use the final results
