Can we build a program that understands informal mathematical text and can we mechanically verify it's correctness? MathNat project aims at being a first step towards answering this question. We develop a controlled language for mathematics (CLM), which is a precisely defined subset of English with restricted grammar and dictionary. Like textbook mathematics, CLM supports some complex linguistic features to make it natural and expressive. A number of transformations are further applied on it to completely formalise it. In this presentation, I'll give an overview of this work and report the current state and future directions. Web: http://www.lama.univ-savoie.fr/ humayoun/phd/mathnat.html