### Developing Corpus-based Translation Methods between Informal and Formal Mathematics

Cezary Kaliszyk, Josef Urban, Jiří Vyskočil, and Herman GeuversProceedings of the 7th Conference on Intelligent Computer Mathematics (CICM 2014), Logical Methods in Computer Science 8543, pp. 435 – 439, 2014.

### Abstract

The goal of this project is to (i) accumulate annotated informal/formal mathematical corpora suitable for training semi-automated translation between informal and formal mathematics by statistical machine-translation methods, (ii) to develop such methods oriented at the formalization task, and in particular (iii) to combine such methods with learning-assisted automated reasoning that will serve as a strong semantic component. We describe these ideas, the initial set of corpora, and some initial experiments done over them.

### BibTeX

@inproceedings{CKJUJVHG-CICM14, author = "Cezary Kaliszyk and Josef Urban and Ji\c{r}\'i Vysko\c{c}il and Herman Geuvers", title = "Developing Corpus-based Translation Methods between Informal and Formal Mathematics", booktitle = "Proceedings of the 7th Conference on Intelligent Computer Mathematics", editor = "Stephen Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban", series = "Lecture Notes in Computer Science", volume = 8543, pages = "435--439", publisher = "Springer-Verlag", year = 2014, doi = "10.1007/978-3-319-08434-3_34" }