# Multilingual Mathematical Autoformalization

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

## Key facts

- Cited by 39 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 35 references that are in the map.
- First posted on arXiv 7 Nov 2023.

## Builds on (most cited first, 20 of 20)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Llama 2: Open Foundation and Fine-Tuned Chat Models](https://mlsanity.com/paper/2307.09288/) (2023)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [RoFormer: Enhanced Transformer with Rotary Position Embedding](https://mlsanity.com/paper/2104.09864/) (2021)
- [GLU Variants Improve Transformer](https://mlsanity.com/paper/2002.05202/) (2020)
- [Root Mean Square Layer Normalization](https://mlsanity.com/paper/1910.07467/) (2019)
- [Improving Neural Machine Translation Models with Monolingual Data](https://mlsanity.com/paper/1511.06709/) (2015)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Unsupervised Machine Translation Using Monolingual Corpora Only](https://mlsanity.com/paper/1711.00043/) (2017)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Professor Forcing: A New Algorithm for Training Recurrent Networks](https://mlsanity.com/paper/1610.09038/) (2016)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Unsupervised Neural Machine Translation](https://mlsanity.com/paper/1710.11041/) (2017)
- [Evaluating Language Models for Mathematics through Interactions](https://mlsanity.com/paper/2306.01694/) (2023)
- [The FLoRes Evaluation Datasets for Low-Resource Machine Translation: Nepali-English and Sinhala-English](https://mlsanity.com/paper/1902.01382/) (2019)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)

## Built on by (most cited first, 30 of 39)

- [Scaling up Test-Time Compute with Latent Reasoning: A Recurrent Depth Approach](https://mlsanity.com/paper/2502.05171/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving](https://mlsanity.com/paper/2412.20735/) (2024)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [Autoformalizing Euclidean Geometry](https://mlsanity.com/paper/2405.17216/) (2024)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs](https://mlsanity.com/paper/2502.00963/) (2025)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [Large Language Model Reasoning Failures](https://mlsanity.com/paper/2602.06176/) (2026)
- [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025)
- [Mathesis: Towards Formal Theorem Proving from Natural Languages](https://mlsanity.com/paper/2506.07047/) (2025)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [Putnam-AXIOM: A Functional and Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs](https://mlsanity.com/paper/2508.08292/) (2025)
- [LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction](https://mlsanity.com/paper/2502.17925/) (2025)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [GFLean: An Autoformalisation Framework for Lean via GF](https://mlsanity.com/paper/2404.01234/) (2024)
- [FormaRL: Enhancing Autoformalization with no Labeled Data](https://mlsanity.com/paper/2508.18914/) (2025)
- [Can Transformers Do Enumerative Geometry?](https://mlsanity.com/paper/2408.14915/) (2024)
- [DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems](https://mlsanity.com/paper/2510.10815/) (2025)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [Semantic Search over 9 Million Mathematical Theorems](https://mlsanity.com/paper/2602.05216/) (2026)

## Abstract (arXiv)

Autoformalization is the task of translating natural language materials into machine-verifiable formalisations. Progress in autoformalization research is hindered by the lack of a sizeable dataset consisting of informal-formal pairs expressing the same essence. Existing methods tend to circumvent this challenge by manually curating small corpora or using few-shot learning with large language models. But these methods suffer from data scarcity and formal language acquisition difficulty. In this work, we create textttMMA, a large, flexible, multilingual, and multi-domain dataset of informal-formal pairs, by using a language model to translate in the reverse direction, that is, from formal mathematical statements into corresponding informal ones. Experiments show that language models fine-tuned on textttMMA produce 16-18% of statements acceptable with minimal corrections on the textttminiF2F and textttProofNet benchmarks, up from 0% with the base model. We demonstrate that fine-tuning on multilingual formal data results in more capable autoformalization models even when deployed on monolingual tasks.