English

Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description

Artificial Intelligence 2014-05-15 v1 Digital Libraries

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.

Keywords

Cite

@article{arxiv.1405.3451,
  title  = {Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description},
  author = {Cezary Kaliszyk and Josef Urban and Jiri Vyskocil and Herman Geuvers},
  journal= {arXiv preprint arXiv:1405.3451},
  year   = {2014}
}
R2 v1 2026-06-22T04:13:51.026Z