Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description
This addresses the challenge of formalizing mathematical proofs for researchers and automated theorem proving systems, but it appears incremental as it builds on existing translation and reasoning techniques.
The project aims to develop statistical machine translation methods for converting informal mathematics to formal mathematics, using annotated corpora and integrating learning-assisted automated reasoning as a semantic component.
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.