Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar

Understand

In this paper we share several experiments trying to automatically translate informal mathematics into formal mathematics.

• In our context informal mathematics refers to human-written mathematical sentences in the LaTeX format; and formal mathematics refers to statements in the Mizar language.
• We conducted our experiments against three established neural network-based machine translation models that are known to deliver competitive results on translating between natural languages.
• To train these models we also prepared four informal-to-formal datasets.