In order to express mathematics formally, it is necessary to specify it in a language that allows both checking of the scripts and creation of the content. In this paper we survey various languages that have been created for this purpose, including logical languages of proof assistants and other formal systems, semi-formal intermediate languages created with the purpose of managing and exchanging mathematical knowledge, as well as language frameworks which allow expressing the syntax and semantics of other languages and provide functionality like disambiguation.