A very different class of examples are to be found at the [Naproche project][1]: **About Naproche**: The Naproche project (Natural language Proof Checking) studies the semi-formal language of mathematics from a linguistic, philosophical and mathematical perspective. A central goal of Naproche is to develop a controlled natural language (CNL) for mathematical texts and adapted proof checking software which checks texts written in the CNL for syntactical and mathematical correctness. [1]: http://naproche.net/