Automatic Formalization of Mathematical Texts in System MathNat

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 sub-problems, both very hard:

  1. Parsing mathematical texts (mainly proofs) and translating those parse trees to a formal language after resolving linguistic issues.
  2. Validation of this formal version of mathematics.

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:

Contact Person:

Dr. Muhammad Humayoun, Assistant Professor, COMSATS Institute of Technology, Lahore, Pakistan.

Foreign Advisers:

Dr. Christophe Raffalli, Associate Professor, Department of Mathematics, University of Savoie, France. Homepage

Dr. Aarne Ranta, Professor of Computer Science, Department of Computer Science and Engineering, University of Gothenburg and Chalmers University of Technology. Homepage


Selected Publication:

  • M. Humayoun and C. Raffalli (2010), "MathNat - Mathematical Text in a Controlled Natural Language", Journal on Research in Computing Science, pp: 293-307, Vol: 46, Issue: Special issue: Natural Language Processing and its, Standard: ISSN: 1870-4069. (acceptance rate: 27%)
  • M. Humayoun and C. Raffalli (2010) "MathAbs: A Representational Language for Mathematics", Proceedings of the 8th International Conference on Frontiers of Information Technology, pp: 37-43, Issue: ACM 978-1-4503-0342-2/10/12, Standard: 978-1-4503-0342-2, Impact Factor: (acceptance rate: 29.25%)