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


1 Answer 1


I can see several challenges, and the list below is not exhaustive:

i. The main problem is how to model a problem of translating a language test into a formal language. It will probably be something like the automatic translators, but with some guarantees that the proof semantics will be preserved. If you are more interested in this path, I recommend researching what PAC, Information Theory, Computational Proof theory, Complexity theory can contribute to this modeling.

ii. Another problem is how to get the data reliable. You commented that as people used it they would generate this data. But the problem is not just collecting the data. How much you will trust the data and how you will measure the model's performance in translation.

iii. Another problem is more humane, how do you get mathematicians to use such a system? And how to make the model self-explainable.

I believe that this is one of the most difficult problems in machine learning. I once saw this video a while ago and I don't know if it can help anything. I also recommend the stack exchange of theoretical computer science, there you will probably have a more complete answer.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .