# Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs

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

## Key facts

- Cited by 27 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 32 references that are in the map.
- First posted on arXiv 5 Jan 2023.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Self-Attention with Relative Position Representations](https://mlsanity.com/paper/1803.02155/) (2018)
- [Universal Transformers](https://mlsanity.com/paper/1807.03819/) (2018)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Incorporating Copying Mechanism in Sequence-to-Sequence Learning](https://mlsanity.com/paper/1603.06393/) (2016)
- [The Devil is in the Detail: Simple Tricks Improve Systematic Generalization of Transformers](https://mlsanity.com/paper/2108.12284/) (2021)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)
- [Symbolic Brittleness in Sequence Models: on Systematic Generalization in Symbolic Mathematics](https://mlsanity.com/paper/2109.13986/) (2021)

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

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](https://mlsanity.com/paper/2405.01379/) (2024)
- [FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving](https://mlsanity.com/paper/2310.18021/) (2023)
- [Autoformalizing Euclidean Geometry](https://mlsanity.com/paper/2405.17216/) (2024)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [Adapting Large Language Models for Education: Foundational Capabilities, Potentials, and Challenges](https://mlsanity.com/paper/2401.08664/) (2023)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [FormaRL: Enhancing Autoformalization with no Labeled Data](https://mlsanity.com/paper/2508.18914/) (2025)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [LeanTutor: Towards a Verified AI Mathematical Proof Tutor](https://mlsanity.com/paper/2506.08321/) (2025)
- [Thinking Machines: Mathematical Reasoning in the Age of LLMs](https://mlsanity.com/paper/2508.00459/) (2025)
- [Do LLMs Really Struggle at NL-FOL Translation? Revealing their Strengths via a Novel Benchmarking Strategy](https://mlsanity.com/paper/2511.11816/) (2025)
- [Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine](https://mlsanity.com/paper/2506.02565/) (2025)
- [KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment](https://mlsanity.com/paper/2507.08665/) (2025)
- [Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees](https://mlsanity.com/paper/2604.19000/) (2026)
- [Safety without alignment](https://mlsanity.com/paper/2303.00752/) (2023)
- [Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification](https://mlsanity.com/paper/2511.00202/) (2025)
- [Towards Autoformalization of LLM-generated Outputs for Requirement Verification](https://mlsanity.com/paper/2511.11829/) (2025)
- [LeanTutor: Towards a Verified AI Mathematical Proof Tutor](https://mlsanity.com/paper/2601.17473/) (2026)

## Abstract (arXiv)

The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. In this paper, we introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover. The same architecture is also trained to translate simple imperative code decorated with Hoare triples into formally verifiable proofs of correctness in Coq. Experiments on a limited domain of artificial and human-written proofs show that the models generalize well to intermediate lengths not seen during training and variations in natural language.