There is a wide gap between the language of mathematics and its formalized versions. To bridge it, we may ask the following gigantic question: "Can we build a program that understands the language of mathematics used by mathematicians and can we mechanically verify its correctness?" This problem can naturally be divided in two subproblems, both very hard:
The system MathNat (Mathematics in controlled Natural language) aims at being the first step towards solving this problem, focusing mainly on the first question. It tries to automatically formalize the language of mathematics. The ultimate objective is to investigate how to check mechanically the validity of a mathematical text on a machine. This involves, among other things, translating an informal mathematical text into a formal text that can be understood by a proof assistant, theorem prover, or some similar system, to be verified or validated mechanically. The system MathNat provides a controlled language having a look and feel of textbook mathematics. It also support miscellaneous linguistic features to make it natural and expressive. A number of transformations are further applied on it to completely formalize it. See more details here (link: http://www.lama.univsavoie.fr/~humayoun/phd/mathnat.html)
Selected Publication:
