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

arXiv: https://arxiv.org/abs/1405.3451 · HTML: https://mlsanity.com/paper/1405.3451/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 May 2014.

## Built on by (most cited first, 7 of 7)

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [Disambiguating Symbolic Expressions in Informal Documents](https://mlsanity.com/paper/2101.11716/) (2021)
- [Munkres' General Topology Autoformalized in Isabelle/HOL](https://mlsanity.com/paper/2604.07455/) (2026)
- [Translating SUMO-K to Higher-Order Set Theory](https://mlsanity.com/paper/2305.07903/) (2023)

## Abstract (arXiv)

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.